ملخص تقني: FormalRewardBench

بيان المشكلة

تعتمد التطورات الأخيرة في مبرهنات النظريات العصبية بشكل كبير على التعلم المعزز بالمكافآت القابلة للتحقق (RLVR). في هذا النموذج، توفر مساعدات الإثبات (مثل Lean 4) إشارات صحة ثنائية (نجاح/فشل) بناءً على التحقق من النوع (type checking). وبينما تعد هذه الإشارات قابلة للتوسع ومحصنة ضد "اختراق المكافأة" (reward hacking)، إلا أنها تعاني من مشكلة التخصيص المتناثر للائتمان (sparse credit assignment): حيث لا تتلقى النماذج أي إشارة تعلم للتقدم الجزئي في المسائل الصعبة، إذ تحصل البراهين التي تفشل في الخطوة النهائية على نفس المكافأة الصفرية التي يحصل عليها النهج الخاطئ تماماً.

وللتخفيف من حدة ذلك، اقترح الباحثون نماذج مكافأة متعلمة قادرة على تقييم جودة البرهان بما يتجاوز التحقق الثنائي. ومع ذلك، فإن مقارنة نماذج المكافأة هذه أمر صعب حالياً لأنها تتطلب عادةً تجارب استئصال (ablations) مكلفة باستخدام التعلم المعزز (RL). علاوة على ذلك، تركز المعايير المرجعية الحالية لنماذج المكافأة (مثل RewardBench وProcessBench) على الاستدلال اللغوي الطبي way غير الرسمي ولا تعالج الدقة النحوية، وصحة النوع، والسلامة المنطقية المطلوبة لإثبات النظريات الصورية. لا يوجد حالياً معيار مرجعي لتقييم نماذج المكافأة مباشرة على البراهين الصورية دون الحاجة إلى عمليات تدريب.

المنهجية

يقدم المؤلفون FormalRewardBench، وهو أول معيار مرجعي مصمم لتقييم نماذج المكافأة لإثبات النظريات الصورية في Lean 4. يتكون المعيار من 250 زوج تفضيل، حيث يحتوي كل زوج على برهان صحيح تم التحقق منه رسمياً ونسخة أخرى غير صحيحة.

بناء مجموعة البيانات

مستمدة مجموعة البيانات من MiniF2F، وهي مجموعة تضم 488 مسألة رياضية بمستوى الأولمبياد تمت صياغتها رسمياً في Lean 4. يستخدم المؤلفون خط إنتاج محكوم لحقن الأخطاء لتوليد براهين غير صحيحة تستوفي ثلاثة معايير:

1. الصلاحية النحوية: يجب أن يُفسر البرهان غير الصحيح ككود Lean صالح برمجياً.
2. المعقولية الدلالية: يجب ألا تكون الأخطاء تافهة (مثل متغيرات غير معرفة)، بل يجب أن تعكس أنماط فشل واقعية.
3. أنماط الخطأ الواقعية: يجب أن تحاكي الأخطاء حالات الفشل الفعلية لنماذج اللغات الكبيرة (LLMs).

استراتيجيات حقن الخطأ

تُستخدم خمس استراتيجيات منسقة من قبل خبراء لتوليد النسخ غير الصحيحة، والتي تم تنفيذها عبر أوامر (prompts) لنموذج (Claude Opus 4.5):

1. التباينات الدنيا في نقطة واحدة: تعديلات دقيقة على البراهين الصحيحة (مثل تبديل الفرضيات، تغيير اسم متغير واحد أو اسم Lemma) مما يسبب فشلاً دلالياً مع الحفاظ على الصلاحية النحوية.
2. التبرير باللغة الطبيعية: تعزيز البراهين غير الصحيحة بتعليقات لغوية طبيعية مضللة تبرر الاستدلال المعيب، وذلك لاختبار "تحيز الإسهاب" (verbosity bias).
3. حقن كود بايثون: استبدال خطوات برهان Lean الرسمية بكود بايثون قابل للتنفيذ قد يحل المسألة حسابياً ولكنه يفشل في تلبية متطلبات البرهان الرسمي (لاختبار الالتزام بالمهمة).
4. أخطاء النماذج القسرية: توليد براهين تحتوي على أخطاء رسمية شائعة تم تحديدها في مخرجات النماذج السابقة، مثل التطبيق الخاطئ للـ tactic، أو اختيار فرضية خاطئة، أو تعيين Lemma غير صحيح.
5. البراهين غير الصحيحة المسهبة: توليد براهين طويلة بشكل غير ضروري ذات هياكل معقدة و Lemmas وسيطة تعمل على تمويه العيوب المنطقية الأساسية.

بروتوكول التقييم

يقيم المعيار النماذج في إعدادين:

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

النتائج الرئيسية

قيم المؤلفون أربع فئات من النماذج: نماذج اللغات الرائدة (Frontier LLMs)، نماذج اللغات القاضية (Judge LLMs)، نماذج اللغات عامة الأغراض، والنماذج المتخصصة في إثبات النظريات.

1. التسلسل الهرمي للأداء: حققت نماذج اللغات الرائدة (مثل Claude Opus 4.5) أعلى أداء (59.8% دقة زوجية). وتفوقت نماذج اللغات القاضية (المدربة على بيانات التفضيل) بشكل كبير على مبرهنات النظريات المتخصصة بين النماذج مفتوحة الأوزان (52.8% مقابل 12.8% لبعض النماذج المتخصصة).
2. الفجوة بين التوليد والتقييم: سجلت نماذج إثبات النظريات المتخصصة (مثل DeepSeek-Prover-V2-7B و Gödel-Prover-V2-8B) أسوأ أداء (تراوح بين 0.0% و 24.4%). ورغم تحقيقها أفضل مقاييس pass@k في MiniF2F، إلا أن هذه النماذج تواجه صعوبة في تقييم البراهين. ويعزو المؤلفون ذلك إلى نقص التدريب على اكتشاف الأخطاء؛ فهذه النماذج مُحسّنة لتوليد براهين صحيحة عبر SFT و RLVR ولكنها لم تتعلم كيفية تحديد أو نقد الأخطاء.
3. تدرج صعوبة الخطأ:
   • الأسهل: حقن كود بايثون (S3)، حيث يعتمد الكشف على تحديد اللغة بدلاً من فهم البرهان.
   • الأصعب: البراهين غير الصحيحة المسهبة (S5) والأخطاء القسرية (S4). حققت حتى أفضل النماذج حوالي 60% في S5 وحوالي 50% في S4.
   • محدودية النماذج القاضية: أظهرت النماذج القاضية نمطاً ثنائي المنوال: أداء يقترب من المثالية في حقن بايثون ولكنه ينهار إلى ما يقرب من الصفر في البراهين المسهبة، مما يشير إلى أن تدريب التفضيل الخاص بها يطور تمييزاً سطحياً بدلاً من الاستدلال الرسمي العميق.
4. تحيز الموضع: لوحظ تحيز كبير في الموضع عبر جميع الفئات، لا سيما في المبرهنات المتخصصة (على سبيل المثال، فضل DeepSeek-Prover-V2-7B البرهان الأول بنسبة 94.9% بغض النظر عن الصحة).

الأهمية والادعاءات

يدعي البحث ثلاث مساهمات رئيسية:

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

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

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