أعلنت شركة DeepSeek عن إصدار DeepSeek-Prover-V2، نموذج لغة كبير مفتوح المصدر متخصص في إثبات النظريات الرياضية الشكلية داخل بيئة Lean 4. يعتمد الإصدار الجديد على نهج متطور يجمع بين البحث التكراري عن الإثباتات واستخدام DeepSeek-V3 لتوليد بيانات تدريب عالية الجودة بشكل ذاتي.
تعتمد الطريقة على إجراء تدريب فريد يبدأ بمطالبة نموذج DeepSeek-V3 بتحليل النظريات الرياضية المعقدة إلى مجموعة من المسائل الأصغر والأيسر تناولاً. في الوقت ذاته، يقوم النموذج بصياغة خطوات الإثبات في Lean 4 لإنشاء سلسلة منظمة من المسائل الجزئية. ثم يستخدم فريق البحث نموذجاً أصغر بـ 7 مليارات معامل للبحث عن الإثباتات لكل مسألة جزئية، وبعد إثبات جميع الخطوات يتم دمج الإثبات الشكلي الكامل مع استدلال السلسلة النقاشية لنموذج DeepSeek-V3.
حقق النموذج الأساسي DeepSeek-Prover-V2–671B بحجم 671 مليار معامل نتائج متقدمة في هذا المجال. وصل النموذج إلى نسبة نجاح 88.9 بالمئة على مجموعة اختبار MiniF2F، وحل 49 مسألة من أصل 658 مسألة من مجموعة PutnamBench. يتوفر النموذج في حجمين: نسخة بـ 7 مليارات معامل بطول سياق ممتد يصل إلى 32 ألف رمز، ونسخة أكبر بـ 671 مليار معامل.
أطلقت الشركة أيضاً معيار ProverBench الجديد الذي يضم 325 مسألة رياضية. يشمل المعيار 15 مسألة صيغت من بطولات AIME الأخيرة للعامين 24 و25، بالإضافة إلى 310 مسائل أخرى مستوحاة من كتب دراسية وموارد تعليمية تغطي مستويات صعوبة متنوعة.
التعليقات (0)
لا توجد تعليقات بعد. كن أول المعلّقين.