في الآونة الأخيرة، شهدنا تقدمًا ملحوظًا في نماذج البرهنة الآلية التي تستخدم التعلم التعزيزي مع مكافآت قابلة للتحقق (Reinforcement Learning with Verifiable Rewards - RLVR)، حيث تقدم أدوات البرهنة إشارات ثنائية تعبر عن صحة البرهان. لقد كانت هذه المكافآت القابلة للتحقق ميسورة وقابلة للتوسع، لكنها تعاني من نقص في توزيع المكافآت، مما يعني أن النماذج لا تتلقى إشارات تعلم من المشاكل المعقدة التي لا يُكافأ فيها التقدم الجزئي. هذا يفتح بابًا لفهم نماذج مكافآت جديدة يمكنها تقييم جودة البرهان بما يتجاوز التحصين الثنائي.

لكن كيف يمكننا المقارنة بين نماذج المكافآت المختلفة؟ عادةً، يتطلب الأمر تدريبات مكلفة قد تتجاوز حدود الموارد المتاحة. لمواجهة هذه التحديات، تم تقديم معيار FormalRewardBench، وهو الأول من نوعه لتقييم نماذج المكافآت في البرهان الرسمي باستخدام Lean 4. يتكون المعيار من 250 زوجًا من تفضيلات حيث يتم ربط البرهنة الصحيحة بنماذج خاطئة تم إنشاؤها من خلال خمس استراتيجيات دقيقة لحقن الأخطاء.

تضمن الدراسة تقييم نماذج لغوية متقدمة مثل Claude Opus 4.5 ونموذج CompassJudger-1-14B، بالإضافة إلى نماذج البرهان المتخصصة مثل DeepSeek-Prover-V2-7B. نتائج هذه التجارب أظهرت أن النماذج اللغوية المتقدمة حققت الأداء الأعلى بنسبة 59.8%، بينما لم تتجاوز نماذج البرهان التقليدية 24.4%، مما يشير إلى عدم انتقال مهارات البرهان إلى تقييم البرهانات.

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

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