MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries
تقدم الورقة البحثية MathlibPR، وهو معيار مستمد من سجلات طلبات السحب الحقيقية لـ Lean/Mathlib4، لتقييم قدرة النماذج اللغوية الكبيرة والوكلاء على التمييز بين المساهمات الجاهزة للدمج وتلك غير المدمجة، مما يكشف عن معاناتهم الحالية ويسلط الضوء على إمكانات المعيار في تطوير مساعدي المراجعة ونماذج المكافأة.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل مكتبة ضخمة وحية للرياضيات تسمى Mathlib. إنها ليست مجرد كتاب؛ بل هي موقع بناء مشترك وعملاق، حيث يقوم علماء الرياضيات وعلماء الحاسوب ببناء أساس مثالي وخالٍ من الأخطاء لجميع فروع الرياضيات. وللحفاظ على سلامة هذه المكتبة وفائدتها، يجب أن يجتاز كل جزء جديد من الكود (ما يسمى بـ "طلب السحب" أو Pull Request أو PR) اختبارين:
- اختبار "هل يعمل؟": هل يعمل الكود فعلياً دون أن يتوقف عن العمل؟ (يقوم الحاسوب بالتحقق من ذلك).
- اختبار "هل هو مواطن صالح؟": هل يتناسب الكود مع بقية المكتبة؟ هل كُتب بالأسلوب الصحيح؟ هل هو واضح بما يكفي ليستخدمه الآخرون؟ (يقوم البشر بالتحقق من ذلك).
لفترة طويلة، كان الذكاء الاصطناعي (AI) بارعاً في اجتياز الاختبار الأول. يمكنه كتابة كود يعمل بشكل مثالي. لكن الاختبار الثاني — المراجعة البشرية — أصبح يمثل عقبة (عنق زجاجة). هناك الكثير من الطلبات المقدمة، وهناك عدد غير كافٍ من المراجعين البشر للتحقق مما إذا كان الكود جاهزاً حقاً ليتم دمجه في المكتبة.
هذه الورقة البحثية تطرح سؤالاً بسيطاً: هل يمكن للذكاء الاصطناعي أن يتعلم كيف يكون هو المراجع؟ هل يمكن للذكاء الاصطناعي أن ينظر إلى قطعة من الكود تعمل بالفعل، ويقرر ما إذا كانت "جاهزة للدمج" أم أنها تحتاج إلى مزيد من العمل؟
ولمعرفة ذلك، أنشأ المؤلفون اختباراً جديداً يسمى MATHLIBPR.
التجربة: "اختبار تذوق أعمى" للكود
فكر في MATHLIBPR كاختبار تذوق أعمى لوصفة جديدة.
- الإعداد: أخذ الباحثون تاريخاً حقيقياً من مكتبة Mathlib. لقد جمعوا آلاف من عمليات تقديم الكود التي اجتازت بالفعل اختبار "هل يعمل؟" (أي أنها تم تجميعها بنجاح).
- التحدي: قدموا هذه المقاطع البرمجية لمختلف نماذج الذكاء الاصطناعي (مثل DeepSeek وQwen وغيرها) وسألوها: "هل هذا جاهز للنشر في المكتبة، أم يجب إعادته لإجراء تعديلات؟"
- الخدعة: لم يكن الذكاء الاصطناعي يعرف النتيجة النهائية. لم يكن بإمكانه سؤال المراجعين البشر: "هل أعجبكم هذا؟". كان عليه أن يحكم بناءً على الكود نفسه فقط، تماماً كما سيفعل المراجع البشري.
لقد اختبروا الذكاء الاصطناعي في ثلاث جولات، مع إعطائه المزيد والمزيد من الأدلة:
- الجولة الأولى: مجرد التغييرات في الكود وبعض أدلة الأسلوب (Style Guides).
- الجولة الثانية: الكود بالإضافة إلى قائمة بالأخطاء الآلية لتدقيق الكود (مثل المدقق الإملائي للكود).
- الجولة الثالثة: الكود، والأخطاء، بالإضافة إلى وصف المؤلف لما كان يحاول القيام به.
النتائج: تعثر الذكاء الاصطناعي
كانت النتائج مفاجئة ومخيبة للآمال قليلاً لمجتمع الذكاء الاصطناعي.
- لم يستطع الذكاء الاصطناعي تمييز الفرق. حتى مع وجود كل تلك الأدلة الإضافية، واجهت نماذج الذكاء الاصطناعي صعوبة في التمييز بين الكود الذي قُبل في النهاية والكود الذي رُفض أو أُعيد لإجراء إصلاحات.
- "انحياز الموافقة": كانت معظم نماذج الذكاء الاصطناعي متفائلة للغاية. فقد مالوا إلى قول: "نعم، هذا رائع!" حتى عندما كان الكود فوضوياً أو لا يتناسب مع أسلوب المكتبة. نادراً ما قالوا: "لا، هذا يحتاج إلى عمل".
- خيار "لا أعرف": بعض النماذج، عندما واجهت قراراً صعباً، كانت تكتفي بالقول: "لست متأكداً". ورغم أن هذا الصدق متاح، إلا أنه لا يساعد المكتبة على المضي قدماً.
- السياق الإضافي لم يساعد كثيراً: لم يؤدِ إعطاء الذكاء الاصطناعي مزيداً من المعلومات (مثل نية المؤلف أو تقارير الأخطاء الآلية) إلى تحسين قدرته بشكل ملحوح على اتخاذ القرار الصحيح.
كان أحد الاكتشافات المثيرة للاهتمام هو أنه حتى عندما نظر الذكاء الاصطناعي إلى نفس المشروع في وقتين مختلفين (مرة عندما كان فوضوياً، ومرة عندما تم إصلاحه وقبوله)، فإنه غالباً لم يستطع معرفة أي النسختين كانت "الأفضل". كان الأمر أشبه بطالب يؤدي اختباراً في موضوع درس موضوعه، لكنه فشل في ملاحظة الفرق بين المسودة الأولية والمقال النهائي.
لماذا هذا مهم؟
تخلص الورقة البحثية إلى أنه بينما يتفوق الذكاء الاصطناعي في كتابة الكود الذي يعمل، فإنه حالياً سيء جداً في مراجعة الكود لمعرفة ما إذا كان ينتمي إلى مكتبة عالية الجودة.
المؤلفون لا يقولون إن الذكاء الاصطناعي يجب أن يحل محل المراجعين البشر. بدلاً من ذلك، هم يرون في هذا المعيار (MATHLIBPR) نقطة انطلاق. إنه أداة لتدريب أنظمة الذكاء الاصطناستقبل المستقبل لتكون "مساعد مراجع" أفضل. الهدف هو بناء ذكاء اصطناعي يمكنه مساعدة البشر من خلال رصد مشكلات الأسلوب الواضحة أو نقص التوثيق، ليعمل كخط دفاع أول بحيث يركز المراجعون البشر على الأجزاء الأكثر صعوبة وإبداعاً في الوظيفة.
باختة القول: الذكاء الاصطناعي بناءٌ بارع، لكنه في الوقت الحالي مفتش سيء. توفر هذه الورقة أول اختبار حقيقي لقياس مدى سوئه بالضبط، حتى نتمكن من تعليمه كيف يصبح أفضل.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.