DeepSeek-Prover-V2: إحداث ثورة في التفكير الرياضي الرسمي من خلال التعلم المعزز
2025-04-30
DeepSeek-Prover-V2 هو نموذج لغة كبير مفتوح المصدر مصمم لإثبات النظريات الرسمية في Lean 4. يستخدم خط أنابيب إثبات نظريات متكرر مدعوم بواسطة DeepSeek-V3 والتعلم المعزز لدمج كل من التفكير الرياضي غير الرسمي والرسمي. يبدأ النموذج بتحليل المشكلات المعقدة إلى أهداف فرعية باستخدام DeepSeek-V3، وتركيب أدلة هذه الأهداف الفرعية لإنشاء بيانات أولية للتعلم المعزز. يحقق DeepSeek-Prover-V2-671B أداءً متطورًا، حيث يصل إلى معدل نجاح 88.9٪ في اختبار MiniF2F وحل 49 مشكلة من PutnamBench. كما تم تقديم مجموعة بيانات مرجعية جديدة، وهي ProverBench، والتي تحتوي على 325 مشكلة رسمية من مسابقات المدارس الثانوية والكتب المدرسية.
الذكاء الاصطناعي
إثبات النظريات