DeepSeek تكشف عن Prover-V2: ثورة نماذج LLM في الإثبات الرياضي الرسمي
قدمت DeepSeek نموذج DeepSeek-Prover-V2، وهو نموذج لغة كبير مفتوح المصدر (LLM) يتم تصميمه بدقة للمجال المعقد لإثبات المبرهنات الرسمية داخل إطار Lean 4. يستفيد هذا النموذج الجديد من خط أنابيب إثبات المبرهنات المتكرر، مستغلًا قوة نموذج DeepSeek-V3 الأساسي المتطور من DeepSeek. Lean 4، أحدث تكرار لبرنامج Lean لإثبات المبرهنات، هو مساعد إثبات تفاعلي تم تطويره بواسطة Microsoft Research. تمكن لغة البرمجة الوظيفية المتطورة ونظام إثبات المبرهنات التفاعلي هذا علماء الرياضيات وعلماء الكمبيوتر من بناء براهين رسمية مع تحقق آلي لا مثيل له.
يمثل المشروع خطوة هائلة نحو سد الفجوة بين الاستدلال الرياضي الرسمي وغير الرسمي. من خلال الاستفادة من القدرات الكامنة في نماذج LLM للأغراض العامة، يسعى إلى معالجة المجال عالي التنظيم لإثبات المبرهنات الرسمي بشكل فعال. يفترض فريق بحث DeepSeek أن نهجهم المبتكر يعكس العمليات المعرفية التي يستخدمها علماء الرياضيات البشريون عند إنشاء البراهين، وتشريح النظريات المعقدة بدقة إلى مكونات أكثر قابلية للإدارة والفهم.
توسيع إطار التقييم: تقديم ProverBench
في خطوة مهمة لتعزيز دقة أبحاثهم، قام فريق DeepSeek بتوسيع إطار التقييم الخاص بهم بشكل كبير من خلال تقديم ProverBench، وهي مجموعة معايير جديدة تمامًا مصممة بدقة خصيصًا للتقييم الشامل لقدرات إثبات المبرهنات الرسمية. تعمل هذه المجموعة الشاملة كمورد قيم لتقييم أداء نماذج LLM في سياق الرياضيات الرسمية.
"بالإضافة إلى المعايير التقليدية، نقدم بفخر ProverBench، وهي مجموعة منسقة بدقة تضم 325 مشكلة مُضفية، لإثراء عملية التقييم لدينا. تتضمن هذه المجموعة 15 مشكلة تم اختيارها بعناية من مسابقة الرياضيات الأمريكية الدعوية (AIME) الأخيرة، وتحديدًا من السنوات 24-25،" أوضح الباحثون.
إن إدراج مسائل AIME في مجموعة بيانات ProverBench أمر جدير بالذكر بشكل خاص، حيث إنه يقدم مجموعة من المسائل الرياضية الصعبة والمثبتة والتي يتم الاعتراف بها على نطاق واسع داخل المجتمع الرياضي. يوفر هذا أساسًا موحدًا وصارمًا لتقييم أداء DeepSeek-Prover-V2 ومقارنته بالأساليب الأخرى.
نتائج أولية واعدة: معالجة مشكلات AIME
كشفت النتائج الأولية الناتجة عن الاختبارات الصارمة على مشكلات AIME الصعبة هذه عن أداء واعد بشكل استثنائي من نموذج إثبات المبرهنات المتخصص المصمم بدقة. يفيد فريق DeepSeek بفخر أن DeepSeek-Prover-V2 أظهر براعته من خلال حل 6 من أصل 15 مشكلة AIME تم تقديمها بنجاح. بالمقارنة، تمكن نموذج DeepSeek-V3 للأغراض العامة، عند استخدام تقنيات التصويت بالأغلبية، من حل 8 مشكلات بنجاح.
تسلط هذه النتائج الضوء على إمكانات كل من نماذج LLM المتخصصة والعامة في معالجة المشكلات الرياضية المعقدة. في حين أن النموذج للأغراض العامة أظهر معدل نجاح أعلى قليلاً في هذا المعيار المحدد، فقد أظهر نموذج إثبات المبرهنات المتخصص كفاءته في الاستدلال الرياضي الرسمي.
محاكاة بناء البراهين البشرية: نهج سلسلة التفكير
"بالنظر إلى التحديات الموثقة جيدًا التي غالبًا ما تواجهها النماذج للأغراض العامة عند محاولة إنتاج براهين Lean كاملة، فقد أمرنا DeepSeek-V3 بشكل استراتيجي بإنشاء رسم تخطيطي لإثبات عالي المستوى فقط، مع حذف التفاصيل المعقدة عمدًا. تتوج سلسلة التفكير الناتجة في نظرية Lean تتكون من سلسلة من العبارات، يتم اختتام كل منها بدقة بعلامة نائب آسف، مما يشير بفعالية إلى هدف فرعي يحتاج إلى حل. يحاكي هذا النهج المبتكر بأناقة الأسلوب البشري لبناء الإثبات، حيث يتم تقليل النظرية المعقدة تدريجيًا إلى سلسلة من الافتراضات الأكثر قابلية للإدارة، "أوضح فريق DeepSeek.
يتوافق هذاالنهج المبتكر لإنشاء الرسوم التخطيطية للإثبات عالية المستوى مع الطريقة التي غالبًا ما يتعامل بها علماء الرياضيات مع البراهين المعقدة. من خلال التركيز على الهيكل العام والخطوات الرئيسية، يمكن للنموذج توجيه التحسين اللاحق وإكمال الإثبات بشكل فعال.
إستراتيجية منهجية: معالجة كل مكون من مكونات الإثبات بشكل فردي
ثم يستخدم النظام بدقة استراتيجية منهجية ومنظمة لمعالجة كل مكون من مكونات الإثبات على حدة. يضمن هذا النهج المنهجي مراعاة كل جانب من جوانب الإثبات بعناية ومعالجته بطريقة منطقية ومتماسكة. ينشئ النظام نهجًا منظمًا للغاية لإثبات المبرهنات، بالاعتماد على النتائج التي تم التوصل إليها مسبقًا لضمان أساس متين لكل خطوة لاحقة.
"بالاستفادة من الأهداف الفرعية التي تم إنشاؤها بواسطة DeepSeek-V3، نتبنى إستراتيجية حل متكررة لحل كل خطوة إثبات وسيطة بشكل منهجي. نستخرج تعبيرات الهدف الفرعي من عبارات التوفر لاستبدالها بالأهداف الأصلية في المشكلات المحددة ثم ندرج الأهداف الفرعية السابقة كفرضيات. يتيح هذا الإنشاء حل الأهداف الفرعية اللاحقة باستخدام النتائج الوسيطة للخطوات السابقة، وبالتالي تعزيز هيكل تبعية أكثر توطينًا وتسهيل تطوير افتراضات أبسط،" أوضح الباحثون بالتفصيل.
تعد إستراتيجية الحل المتكررة جانبًا رئيسيًا في قدرة النظام على التعامل مع البراهين المعقدة. من خلال تقسيم المشكلة إلى أهداف فرعية أصغر وأكثر قابلية للإدارة، يمكن للنظام تطبيق إمكاناته المنطقية بشكل فعال على كل مكون على حدة.
تحسين الموارد الحسابية: نموذج متخصص بـ 7 مليارات معلمة
لتحسين الموارد الحسابية بشكل فعال وضمان معالجة فعالة، يستخدم النظام بشكل استراتيجي نموذجًا أصغر ومتخصصًا للغاية بـ 7 مليارات معلمة لمعالجة الافتراضات المحللة. يعتبر هذا النهج أمرًا بالغ الأهمية لإدارة المتطلبات الحسابية المرتبطة بعمليات البحث الموسعة عن الإثبات بشكل فعال، مما يضمن قدرة النظام على العمل بكفاءة دون أن تطغى عليه تعقيد مساحة البحث. يتوج هذا النهج في النهاية بإثبات كامل مشتق تلقائيًا عند حل جميع الخطوات المحللة بنجاح.
"يعمل الإطار الخوارزمي على مرحلتين متميزتين، مستفيدًا من نموذجين متكاملين: DeepSeek-V3 لتحليل الافتراضات ونموذج مثبت 7B لإكمال تفاصيل الإثبات الرسمية المقابلة،" وصف الباحثون.
يسمح هذا النهج المكون من مرحلتين للنظام بالاستفادة من نقاط القوة لكل من النموذج العام الكبير والنموذج المتخصص الأصغر. يتم استخدام النموذج الكبير لإنشاء رسومات تخطيطية للإثبات عالية المستوى، بينما يتم استخدام النموذج الأصغر لملء التفاصيل وإكمال الإثبات الرسمي.
تجميع بيانات الاستدلال الرسمي: مسار طبيعي
تؤسس هذه الهندسة المصممة بدقة مسارًا طبيعيًا وبديهيًا لتجميع بيانات الاستدلال الرسمي بشكل فعال، ودمج الاستدلال الرياضي عالي المستوى بسلاسة مع المتطلبات الصارمة والدقيقة للتحقق الرسمي. هذا التكامل ضروري لضمان موثوقية وجدارة نتائج النظام بالثقة.
"نحن نقوم برعاية مجموعة فرعية من المشكلات الصعبة التي لم يتم حلها بواسطة النموذج المثبت 7B بطريقة شاملة، ولكن تم حل جميع الأهداف الفرعية المحللة بنجاح. من خلال تجميع براهين جميع الأهداف الفرعية، نقوم ببناء إثبات رسمي كامل للمشكلة الأصلية،" أوضح الباحثون.
يسمح هذا النهج للنظام بالتعلم من أخطائه وتحسين قدرته على حل المشكلات المعقدة. من خلال تحديد الأهداف الفرعية المحددة التي تسبب صعوبات، يمكن للنظام تركيز جهوده على تحسين أدائه في تلك المجالات.
المخاوف والتحديات: تفاصيل التنفيذ قيد التدقيق
على الرغم من الإنجازات التقنية التي لا يمكن إنكارها التي أظهرها DeepSeek-Prover-V2، فقد أثار بعض الخبراء في هذا المجال مخاوف ذات صلة بشأن بعض تفاصيل التنفيذ. أشار إليوت جليزر، وهو عالم رياضيات رائد يحظى باحترام كبير في Epoch AI، إلى المشكلات المحتملة التي تستدعي مزيدًا من التحقيق.
بعض المخاوف بشأن ورقة DeepSeek-Prover-V2. أمثلة يحتمل أن تكون غير مُضفية، وتشير المناقشة حول Lean zulip إلى أن براهين PutnamBench هي هراء وتستخدم آسفًا ضمنيًا (ربما مخفيًا في تكتيك التطبيق؟) لم يتم الإبلاغ عنه في حلقة القراءة والتقييم والطباعة الخاصة بهم.
تسلط هذه المخاوف الضوء بوضوح على التحديات المستمرة المتأصلة في مجال التحقق الرسمي، حيث يمكن حتى لأصغر تفاصيل التنفيذ التي تبدو غير مهمة أن تمارس تأثيرًا كبيرًا بشكل غير متناسب على الصلاحية والموثوقية الإجمالية للنتائج. تتطلب عملية التحقق الرسمي اهتمامًا ثابتًا بالتفاصيل والتزامًا دقيقًا بالمعايير المعمول بها.
إن احتمال وجود أمثلة غير مُضفية واحتمال وجود تكتيكات "آسف" مخفية في براهين PutnamBench يثيران أسئلة مهمة حول دقة واكتمال عملية التحقق. تؤكد هذه المخاوف على الحاجة إلى التدقيق المستمر والتحقق المستقل من النتائج.
التوفر والموارد: إضفاء الطابع الديمقراطي على الوصول إلى إثبات المبرهنات الرسمي
جعلت DeepSeek برنامج Prover-V2 الخاص بها متاحًا بحجمين مختلفين للنماذج، لتلبية مجموعة متنوعة من الموارد الحسابية والأهداف البحثية. الإصدار الأول هو نموذج بـ 7 مليارات معلمة مبني على Prover-V1.5-Base السابق، ويتميز بطول سياق ممتد يصل إلى 32 ألف رمز. الإصدار الثاني هو نموذج أكبر بكثير بـ 671 مليار معلمة تم تدريبه على DeepSeek-V3-Base. كلا النموذجين متاحان الآن بسهولة على HuggingFace، وهي منصة رائدة لمشاركة نماذج التعلم الآلي والتعاون فيها.
بالإضافة إلى النماذج نفسها، جعلت DeepSeek أيضًا مجموعة بيانات ProverBench الكاملة، التي تحتوي على 325 مشكلة مُضفية بدقة لأغراض التقييم، متاحة على HuggingFace. توفر مجموعة البيانات الشاملة هذه للباحثين والمطورين موردًا قيمًا لتقييم أداء نماذجهم ومقارنتها بـ DeepSeek-Prover-V2.
من خلال إتاحة هذه الموارد مجانًا، تعمل DeepSeek على إضفاء الطابع الديمقراطي على الوصول إلى تكنولوجيا إثبات المبرهنات الرسمية وتعزيز التعاون داخل المجتمع البحثي. من المرجح أن يؤدي هذا النهج مفتوح المصدر إلى تسريع التقدم في هذا المجال ويؤدي إلى اكتشافات جديدة في الاستدلال الآلي والتحقق.
يمكّن هذا الإصدار الباحثين والمطورين بالموارد اللازمة للتعمق في قدرات وقيود هذه التكنولوجيا. من خلال توفير وصول مفتوح إلى النماذج ومجموعة بيانات ProverBench، تشجع DeepSeek على مزيد من الاستكشاف وجهود التعاون لمعالجة المخاوف التي أثارها الخبراء في هذا المجال. يحمل هذا النهج التعاوني المفتاح لكشف تعقيدات إثبات المبرهنات الرسمية وتدعيم موثوقية هذه التطورات الرائدة.