DeepSeek تطلق DeepSeek-Prover-V2 مع بحث إثبات متكرر ومعيار ProverBench الجديد

أعلنت شركة DeepSeek AI عن إطلاق نموذج DeepSeek-Prover-V2، وهو نموذج لغوي كبير مفتوح المصدر للإثبات النظري الشكلي في بيئة Lean 4. يستخدم النموذج خط أنابيب إثبات متكرر يعتمد على DeepSeek-V3 لتوليد بيانات تهيئة عالية الجودة عن طريق تحليل النظريات المعقدة إلى أهداف فرعية وصياغتها شكلياً. ثم يقوم نموذج ذو 7 مليارات معلمة بإثبات هذه الأهداف الفرعية، ويتم إقران الإثباتات الكاملة مع سلسلة التفكير (chain-of-thought) لنموذج DeepSeek-V3 بغرض التدريب. يعمل التعلم المعزز بالتغذية الراجعة الثنائية على تحسين النموذج بشكل إضافي. يحقق نموذج النسخة ذات 671 مليار معلمة نسبة نجاح 88.9% في اختبار MiniF2F-test، ويحل 49 مسألة من أصل 658 مسألة في مجموعة PutnamBench. كما قدمت DeepSeek مجموعة بيانات ProverBench، والتي تضم 325 مسألة من مسابقات AIME والكتب المدرسية لتقييم التفكير الرياضي. يتوفر النموذج بحجمين: 7 مليارات معلمة و671 مليار معلمة.