DeepSeek-Prover-V1.5: استغلال ملاحظات مساعد الإثبات لتعلم التدعيم والبحث الشجري مونت كارلو

نقدم نموذج اللغة المفتوح المصدر DeepSeek-Prover-V1.5، المصمم لإثبات النظريات في Lean 4، والذي يعزز DeepSeek-Prover-V1 من خلال تحسين عمليات التدريب والاستدلال. تم تدريب النموذج مسبقًا على DeepSeekMath-Base مع التركيز على اللغات الرياضية الرسمية، ثم خضع لضبط مراقب باستخدام مجموعة بيانات متقدمة لإثبات النظريات الرسمية مشتقة من DeepSeek-Prover-V1. يتم تحقيق المزيد من التحسينات من خلال التعلم التعزيزي من ردود فعل مساعد الإثبات (RLPAF). بالإضافة إلى أسلوب إنشاء البرهان بالمرور الواحد الذي يتبعه DeepSeek-Prover-V1، نقترح RMaxTS، وهو نوع من البحث الشجري مونتي كارلو يستخدم استراتيجية استكشاف مدفوعة بالمكافآت الذاتية لتوليد مسارات برهان متنوعة. يظهر DeepSeek-Prover-V1.5 تحسينات كبيرة على DeepSeek-Prover-V1، حيث حقق نتائج جديدة رائدة في مجالها على مجموعة الاختبار للمعيار miniF2F للمرحلة الثانوية (63.5%) ومعيار ProofNet للمرحلة الجامعية (25.3%).