DeepSeek-Prover-V2: نموذج لغوي كبير مفتوح المصدر لإثبات النظريات الرياضية

يُعَدُّ الاستدلال الرياضي الرسمي مجالاً متخصصاً في الذكاء الاصطناعي يتطلب اتساقاً منطقياً دقيقاً. على عكس حل المشكلات غير الرسمية، التي تسمح بالحدس والخوارزميات غير المحددة بدقة، يعتمد إثبات النظريات الرسمي على أن تكون كل خطوة موصوفة بالكامل، ودقيقة، وقابلة للتحقق من خلال الأنظمة الحاسوبية. تلعب برامج مساعدة الإثبات، مثل Lean و Coq و Isabelle، دور الأطر البنيوية التي تُبنى ضمنها هذه الإثباتات الرسمية. يتطلب تشغيلها سلامة منطقية دون مجال للإغفال أو التقريبات أو الافتراضات غير المعلنة. هذا ما يجعل التحدي صعباً بشكل خاص لأنظمة الذكاء الاصطناعي، خاصة النماذج اللغوية الكبيرة، التي تُجيد إنتاج استجابات لغوية طبيعية متماسكة، لكنها تفتقر عادةً إلى الدقة اللازمة لإنتاج إثباتات رسمية قابلة للتحقق.

التحدي: جسر الهوة بين الاستدلال الرسمي وغير الرسمي

ومع ذلك، فإن الرغبة في الجمع بين هذه القوى، وهي طلاقة الذكاء الاصطناعي في الاستدلال غير الرسمي وهيكل التحقق الرسمي، أدت إلى ابتكارات جديدة على واجهة نماذج اللغة وأتمتة المنطق الرسمي. تبرز مشكلة رئيسية تتمثل في عدم قدرة نماذج اللغة الحالية على سد الفجوة المفاهيمية بين الاستدلال الرسمي وغير الرسمي. تتميز نماذج اللغة عادةً بقدرتها على توليد تفسيرات شبيهة بالتفسيرات البشرية وحل مسائل رياضية مكتوبة بلغة طبيعية. ومع ذلك، فإن هذا الاستدلال غير رسمي بطبيعته، وغالباً ما يفتقر إلى الدقة البنيوية المطلوبة لأنظمة المنطق الرسمي. بينما يمكن للبشر القفز بشكل حدسي من خطوة استنتاجية إلى أخرى، تتطلب برامج مساعدة الإثبات تسلسلاً كاملاً من الخطوات، خالياً من أي غموض. لذلك، يكمن التحدي في توجيه نماذج الذكاء الاصطناعي لإنتاج مخرجات رسمية متماسكة منطقياً من عملياتها الداخلية غير الرسمية والحدسية. تصبح هذه المشكلة أكثر تعقيداً عند التعامل مع نظريات متقدمة من مجالات مثل نظرية الأعداد أو الهندسة، حيث تكون الدقة أمراً بالغ الأهمية.

DeepSeek-Prover-V2: حلول مبتكرة

سعت الجهود الأخيرة إلى معالجة هذه المشكلة من خلال توجيه النماذج أولاً لتوليد مخططات إثبات بلغة طبيعية، ثم تُترجم يدوياً أو شبه آلياً إلى خطوات إثبات رسمية. تتضمن إحدى الاستراتيجيات المعروفة تقسيم نظرية معقدة إلى أهداف فرعية أصغر. يمثل كل هدف فرعي مبرهنة يمكن معالجتها بشكل مستقل، ثم دمجها لاحقاً لتشكيل إثبات كامل. طبقت أطر عمل مثل “المسودة، والرسم، والإثبات” هذه الفكرة، باستخدام نماذج اللغة لتوليد مخططات إثبات تُترجم بعد ذلك إلى لغة رسمية. تستخدم طريقة أخرى التعلم التعزيزي الهرمي، حيث تقسم المشكلات الرياضية المعقدة إلى طبقات أبسط.

قدم فريق من الباحثين من DeepSeek-AI نموذجاً جديداً، وهو DeepSeek-Prover-V2، مصمم لتوليد إثباتات رياضية رسمية من خلال الاستفادة من تقسيم الأهداف الفرعية والتعلم التعزيزي. يستخدم جوهر نهجهم DeepSeek-V3 لتقسيم نظرية معقدة إلى أهداف فرعية قابلة للإدارة، يتم ترجمة كل منها إلى عبارة “have” في Lean 4 مع موضع مؤقت يشير إلى أن الإثبات غير مكتمل. ثم يتم تمرير هذه الأهداف الفرعية إلى نموذج مُثبت بحجم 7 مليار معلمة، والذي يُكمل كل خطوة من خطوات الإثبات. بمجرد حل جميع الخطوات، يتم دمجها في إثبات Lean كامل، وإقرانها بالاستدلال بلغة طبيعية الأصلي الذي تم إنشاؤه بواسطة DeepSeek-V3. يشكل هذا مجموعة بيانات غنية لبدء التعلم التعزيزي.

أهم مميزات DeepSeek-Prover-V2:

• الاستفادة من البيانات الاصطناعية: يتم تدريب النموذج بالكامل من بيانات اصطناعية، دون استخدام خطوات إثبات مُعلّمة يدوياً.
• تقسيم الأهداف الفرعية: تقسيم المشكلة إلى أهداف فرعية أصغر، مما يسهل عملية الإثبات.
• التعلم التعزيزي: استخدام التعلم التعزيزي لتحسين دقة الإثبات.
• المنهج التعليمي: استخدام منهج تعليمي لزيادة تعقيد مهام التدريب تدريجياً.
• نوعان من تقسيم الأهداف الفرعية: استخدام نوعين من تقسيم الأهداف الفرعية، أحدهما يدمج الأهداف الفرعية السابقة كافتراضات، والآخر يعالجها بشكل مستقل.

النتائج والاختبارات

حقق النموذج معدل نجاح بلغ 88.9% في اختبار MiniF2F (Pass@8192)، وهو أعلى معدل تم الإبلاغ عنه بين نماذج الاستدلال الرسمي حتى الآن. كما حلّ 49 من أصل 658 مسألة من مجموعة بيانات PutnamBench، والتي تحتوي على تحديات رياضية متقدمة. كما عالج 6 من أصل 15 مسألة من مسابقات AIME (امتحان الرياضيات الأمريكي الدعائي) لعامي 2024 و 2025. تُبرز هذه المعايير قدرة النموذج على التعميم عبر مهام الاستدلال الرسمي المتعددة. حتى عند مقارنته بـ DeepSeek-V3، الذي يستخدم الاستدلال بلغة طبيعية، يُظهر النموذج الجديد أداءً تنافسياً، حيث يحل عدداً مماثلاً من مسائل AIME مع ضمان قابلية التحقق الرسمي.

خلاصة

يُمثل DeepSeek-Prover-V2 تقدماً مهماً في مجال إثبات النظريات الرياضية باستخدام الذكاء الاصطناعي. يُظهر النموذج قدرة عالية على حلّ مسائل رياضية معقدة، مع ضمان دقة الإثبات وقابلية التحقق منه. يُعدّ هذا النموذج مفتوح المصدر، مما يُسهّل على الباحثين والمهتمين تطويره وتحسينه.

(روابط المقال الأصلي، جيثب، تويتر، الخ… ستُضاف هنا)

المصدر: MarkTechPost