ملخص تقني: CAM-Bench

بيان المشكلة

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

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

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

تعاني معايير الاختبار الحالية من صعوبة في تقييم ما إذا كانت النماذج قادرة على تتبع هذه الافتراضات المحلية، وتفكيك البراهين بناءً على سياقات الكتب الدراسية، وتطبيق النتائج الأولية التي قد لا تكون متاحة بعد كـ "تمهيدات" (lemmas) قياسية في المكتبات الرسمية مثل Mathlib4. هناك حاجة إلى معيار اختبار يستهدف مسائل الرياضيات التطبيقية حيث يكون "السياق المحلي" بنفس أهمية نص النظرية نفسها.

المنهجية

يقدم المؤلفون CAM-Bench، وهو معيار اختبار لإثبات النظريات باستخدام لغة Lean 4، يتكون من 1,000 هدف للإثبات مستمد من 778 تمريناً من الكتب الدراسية في مجالات الأمثلة (optimization)، والجبر الخطي العددي، والتحليل العددي. يعتمد بناء هذا المعيار على خط إنتاج جديد لاستعادة التبعية والصياغة الرسمية مصمم لتحويل التمارين المعتمدة على السياق إلى أهداف قائمة بذاتها وقابلة للتحقق آلياً.

1. خط إنتاج استعادة التبعية والإثراء

لمعالجة الطبيعة غير المستقلة للتمارين في الكتب الدراسية، طور المؤلفون إجراءً لتوسيع التبعية التكراري (الخوارزمية 1):

• التوسيع التكراري: بدءاً من تمرين خام، يستخرج النظام المراجع (النظريات، المعادلات، الخوارزميات) ويسترجع مراجعها وتعريفاتها بشكل تكراري حتى عمق محدد.
• الطبيعية من الأسفل إلى الأعلى (Bottom-Up Naturalization): تتم معالجة شجرة التبعية من الأسفل إلى الأعلى، حيث يقوم "طابع طبيعي" (naturalizer) مدعوم بنموذج لغة كبيرة بدمج التمثيلات المثرية، وحل المراجع المحلية، وتوحيد الرموز، وتنعيم الانتقالات لضمان دمج التعريفات من المستوى الأدنى قبل أن تستخدمها التبعيات من المستوى الأعلى.
• استعادة الشروط الضمنية: يقوم النظام بجعل الافتراضات المطلوبة صريحة (مثل قيود النطاق، الإيجابية، التحدب) فقط عندما يكون ذلك مدعوماً بالمسألة الأصلية أو السياق المسترجع. هذا الإثراء مرتبط بالمصدر؛ فهو لا يخمن التبعيات المفقودة بل يستبعدها إذا تعذر استرجاعها.
• المراجعة متعددة الجولات: تخضع البيانات المثرية لحلقة تحقق للتأكد من عدم وجود افتراضات مفقودة، أو انحراف في المهمة، أو عدم ملاءمة للغة Lean. وتقتصر الإصلاحات على معالجة العيوب المحلية دون تغيير الهدف الرياضي أو اختراع تبعيات غير مدعومة.

2. الصياغة الرسمية المدفوعة بالنمذجة المجزأة

بمجرد تحديد هدف غير رسمي، يقوم النظام بتحويله إلى كود Lean 4 باستخدام استراتيجية البناء الجزئي ذي السياق المجمد:

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

3. بناء المعيار والتحقق من الصحة

تتضمن مجموعة البيانات النهائية التمرين الخام، والسياق المسترجع، والنظرية غير الرسمية الموحدة، وهدف Lean النهائي. يحدث التحقق على مستويين:

• على مستوى المصدر: يضمن أن الهدف غير الرسمي أمين للتمارين الموجودة في الكتاب الدراسي ومستقل بذاته.
• على مستوى Lean: يضمن أن الإعلان الرسمي يحافظ على الهدف غير الرسمي الذي تمت مراجعته. وقد تبين أن 92.5% فقط من الإعلانات المرشحة كانت قابلة للاستخدام بعد التحقق الدلالي، مما يسلط الض الضوء على صعوبة الصياغة الآلية الدقيقة.

المساهمات الرئيسية

1. مجموعة بيانات CAM-Bench: معيار منسق يحتوي على 1,000 هدف لإثباتات Lean تغطي مجالات الأمثلة (optimization)، والجبر الخطي العددي، والتحليل العددي. توفر المجموعة آثاراً قابلة للتتبع من التمارين الخام إلى أهداف Lean التي يمكن التحقق منها آلياً، مما يسد الفجوة في تقييم الرياضيات التطبيقية.
2. خط إنتاج استعادة التبعية: طريقة مبتكرة لبناء أهداف Lean دقيقة من تمارين تعتمد على السياق. وهي تجمع بين التوسيع التكراري للتبعية، والإثراء المرتبط بالمصدر، والإصلاح المقيد للتعامل مع التعريفات المحلية والافتراضات التي لا تعد من دروس Mathlib4 القياسية.
3. التقييم الشامل وتحليل الأخطاء: تقيم الورقة نماذج اللغات الكبيرة الرائدة ووكلاء الصياغة الرسمية على CAM-Bench. وتحدد أنماط الفشل المحددة:
   • الارتباط بالمكتبة/واجهة برمجة التطبيقات (API Grounding): تفشل النماذج في ربط البراهن بالبنية التحتية المتاحة لـ Mathlib، حيث تقوم بتأليف واجهات برمجة تطبيقات (hallucinating) أو تفقد نتائج الربط.
   • التمثيل الرسمي: أخطاء في انضباط الأنواع، وعدم تطابق الأبعاد/المؤشرات، وفشل التحويل (coercion).
   • تفكيك البرهان: عدم القدرة على تفكيك البراهين طويلة الأمد إلى تمهيدات مساعدة أو الحفاظ على السيطرة على الحجج المعقدة المتعلقة بالأمثلة أو الحسابات العددية.

النتائج

الأداء المرجعي

• النماذج غير الوكيلية (Non-Agentic Models): حتى أقوى النماذج غير الوكيلية (مثل Deepseek-v4-pro، وClaude-sonnet-4-6) حققت دقة منخفضة في Lean المتحقق منها، حيث وصلت أفضلها إلى 19.67% (Pass@32).
• الفجوة بين الرسمي وغير الرسمي: هناك تباين كبير بين الصحة غير الرسمية (دقة Pass@1 غير رسمية ~70–84%) والصحة الرسمية في Lean (أقل من 20%). تلتقط النماذج الحجج عالية المستوى لكنها تفشل في تلبية قواعد Syntax الصارمة لـ Lean، وانضباط الأنواع، وقيود المكتبة.
• التحسن الوكي (Agentic Improvement): حققت أنظمة البحث عن البراهين الوكيلية (مثل GPT-5.4 مع الإصلاح التكراري واستخدام الأدوات) تحسناً ملحوظاً، حيث وصلت إلى 44.00% من الدقة المتحقق منها في Lean. ومع ذلك، جاء ذلك بتكلفة عالية من الرموز (Tokens) (~1.96 مليون رمز مقابل ~0.26–0.70 مليون للنماذج المرجعية).

تقييم الوكلاء الخارجيين

تم تقييم نظامين وكيلين خارجيين، M2F و Aristotle، على 200 حالة عينة مع ميزانية زمنية قدرها 8 ساعات:

• M2F: حل 143/200 حالة (71.5%).
• Aristotle: حل 125/200 حالة (62.5%).
  على الرغم من هذه التحسينات، لا يزال المعيار غير مشبع. وقد عُزي العديد من الإخفاقات إلى نقص البنية التحتية الرياضية، وسلاسل التمهيدات المساعدة الطويلة، والاستدلال الخاص بالأمثلة (optimization).

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

تدعي الورقة أن CAM-Bench يعمل كمكمل حاسم لمعايير الاختبار الرسمية الحالية من خلال استهداف مسائل الرياضيات التطبيقية التي تعتمد على مفاهيم الكتب الدراسية والنتائج الأولية. وتكمن أهميته في:

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

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