APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries
تقدم هذه الورقة APE-Bench، وهو أول إطار عمل ومعيار منهجي لتقييم هندسة الإثبات الآلية في مكتبات الرياضيات الرسمية من خلال استخراج مهام واقعية على نطاق المستودعات وتوفير هيكل موحد للتحقق من كل من التصحيح النحوي والصحة الدلالية عبر مختلف تنفيذات الوكلاء.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك تحاول تعليم روبوت كيف يكون أمين مكتبة بارعاً لمكتبة ضخمة وحية من البراهين الرياضية. هذه المكتبة، المسماة Mathlib، تحتوي على ملايين الصفحات. وهي ليست مجرد كتاب ثابت؛ بل يتم إعادة كتابتها وتوسيعها وإصلاحها باستمرار من قبل خبراء بشريين.
لفترة طويلة، اختبر الباحثون الروبوتات على قدرتها على حل ألغاز رياضية فردية ومعزولة (مثل "أثبت أن 2+2=4"). ولكن في العالم الحقيقي، لا يقتصر العمل الرياضي على حل لغز واحد فحسب؛ بل يتعلق بـ هندسة البراهين. وهذا يعني التنقل في كامل المكتبة، والعثور على الأدوات المناسبة، وإصلاح الصفحات المعطلة، والتأكد من أن إضافاتك الجديدة تتناسب تماماً مع ملايين الصفحات الموجودة بالفعل دون أن تكسر أي شيء آخر.
يقدم هذا البحث طريقة جديدة لاختبار الروبوتات على هذه المهارات الواقعية. إليك التفاصيل باستخدام تشبيهات بسيطة:
1. المشكلة: "اللغز المنفرد" مقابل "المكتبة الحية"
- الطريقة القديمة (miniF2F): تخيل اختبار طباخ عبر إعطائه بطاقة وصفة واحدة وسؤاله عن طهي طبق واحد. إذا كان الطبق مذاقه جيداً، فقد نجح. لكن هذا لا يخبرك ما إذا كان بإمكله إدارة مطبخ كامل، أو طلب المكونات، أو إصلاح فرن معطل.
- الواقع: العمل الرياضي الحقيقي يشبه إدارة ذلك المطعم. عليك التنسيق مع طهاة آخرين، واستخدام أدوات محددة، والتأكد من أن طبقك الجديد لن يفسد قائمة الطعام بأكملها.
- الفجوة: كانت الاختبارات الحالية تتحقق فقط مما إذا كان بإمكان الروبوت طهي ذلك الطبق المنفرد. لم تكن تتحقق مما إذا كان بإمكان الروبوت التعامل مع فوضى المطبخ الحقيقي.
2. الحل: APE-Bench (اختبار "المكتبة الحية")
ابتكر المؤلفون APE-Bench، وهو ميدان اختبار جديد يحاكي صيانة المكتبة في الحياة الواقعية.
- كيف يعمل: بدلاً من إعطاء الروبوت لغزاً وهمياً، يبحث النظام في التاريخ الحقيقي لمكتبة Mathlib. يجد لحظة قام فيها خبير بشري بإجراء تغيير ("commit")، ثم يخفي ذلك التغييد، ويسأل الروبوت: "إليك المكتبة قبل التغيير. إليك ملاحظة توضح ما أراد الإنسان فعله. هل يمكنك إجراء هذا التغيير؟"
- اللمسة المميزة: لا يتم تقييم الروبوت فقط بناءً على ما إذا كان الكود "يعمل" (بناء الجملة/syntax). بل يتم تقييمه بناءً على شيئين:
- الترجمة (Compilation): هل تمت ترجمة الكود بالفعل دون أخطاء؟ (هل احترق الطبق؟)
- التحقق الدلالي (Semantic Check): هل قام الروبوت بالفعل بما طُلب منه؟ (هل أصلح المشكلة الصحيحة، أم أنه قام فقط بتغيير أسطر عشوائية؟)
3. البنية التحتية: APE-Harness (الـ "مطبخ العالمي")
لتشغيل هذه الاختبارات بشكل عادل، بنوا نظاماً يسمى APE-Harness. فكر في هذا كـ محاكي مطبخ عالمي.
- "العقد": يأتي كل اختبار مع عقد صارم. يقول: "أنت في نسخة محددة من المكتبة. يمكنك فقط لمس هذه الملفات. يجب أن تثبت أنك أنجزت المهمة".
- "السقالات" (Scaffolds): تم تصميم النظام بحيث يمكنك توصيل روبوتات مختلفة (مثل Claude Code، أو Codex، أو APE-Agent الخاص بهم) في نفس المطبخ. ولأن قواعد المطبخ (العقد) هي نفسها للجميع، يمكنك المقارنة بعدل بين من هو الطباخ الأفضل حقاً، بدلاً من مجرد رؤية من حالفه الحظ في فهم التعليمات.
- خدعة "السفر عبر الزمن": تحتوي المكتبة على 67 نسخة مختلفة (مثل 67 طبعة مختلفة من كتاب). تخزين جميعها سيتطلب مساحة هائلة. بنى المؤلفون نظام "إزالة التكرار" ذكياً. إذا كانت صفحة ما متطابقة في النسخة 1 والنسخة 67، فإن النظام يخزنها مرة واحدة فقط ويشير إليها فقط. وفر هذا 85% من مساحة التخزين و98% من الأموال اللازمة لمعالجة البيانات.
4. النتائج: من اجتاز الاختبار؟
اختبروا ثلاثة من أفضل نماذج الذكاء الاصطناي (GPT-5.2، وGemini 3 Pro، وGemini 3 Flash) على هذا الاختبار الجديد والأكثر صعوبة.
- الصعوبة: كان الاختبار الجديد أصعب بكثير من اختبارات "اللغز المنفرد" القديمة.
- في الاختبارات القديمة، حصلت الروبوتات على 80-90% من الإجابات الصحيحة.
- في اختبار "صيانة المكتبة" الجديد، حصل أفضل روبوت على 47% فقط.
- الفائز: كان Gemini 3 Flash هو الأكثر كفاءة. لقد حل أكبر عدد من المشكلات مقابل أقل تكلفة. حاولت النماذج الأخرى بذل جهد أكبر (عدد دورات محادثة أكثر) لكنها نفدت من "ميزانيتها" قبل الانتهاء.
- الدرس المستفاد: الروبوتات بارعة في حل المسائل الرياضية المنعزلة، لكنها لا تزال تعاني مع المهمة المعقدة والفوضوية لإدارة قاعدة بيانات برمجية ضخمة ومتطورة.
5. لماذا يهم هذا؟
يزعم البحث أن هذه هي المرة الأولى التي نمتلك فيها طريقة منهجية ومؤتمتة لاختبار ما إذا كان بإمكان الذكاء الاصطناعي القيام بـ "هندسة البرمجيات من أجل البراهń".
- إنه ينقل الأهداف من "هل يمكن للذكاء الاصطناعي حل مسألة رياضية؟" إلى "هل يمكن للذكاء الاصطناعي العمل كرياضي محترف في بيئة فريق؟"
- إنه يوفر ساحة لعب عادلة حيث يمكن مقارنة أنظمة الذكاء الاصطنا المختلفة باستخدام نفس القواعد والأدوات تماماً.
باخت-القول: بنى المؤلفون محاكاة واقعية لمكتبة رياضية ضخمة وفوضوية ومجموعة من القواعد لاختبار ما إذا كان بإمكان الذكاء الاصطناعي إصلاحها. ووجدوا أنه بينما يتحسن الذكاء الاصطناعي، إلا أنه لا يزال أمامه طريق طويل قبل أن يتمكن من إدارة المشاريع الرياضية المعقدة والواقعية بمفرده بشكل موثوق.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.