FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
تقدم الورقة البحثية FormalProofBench، وهو معيار خاص لتقييم قدرة نماذج الذكاء الاصطناعي على توليد براهين رياضية ذات مستوى دراسات عليا ومحققة رسميًا بلغة Lean 4، كاشفةً أن أفضل النماذج أداءً حقق دقة تبلغ 33.5% فقط، مع تقديم تحليل شامل لاستخدام الأدوات، وأنماط الفشل، والكفاءة.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك معلم تقدم اختبار رياضيات لفصل من الروبوتات الذكية جداً، ولكنها مغرورة أحياناً.
في الماضي، كان يتم اختبار هذه الروبوتات (نماذج الذكاء الاصطناعي) في مسائل رياضية حيث يتعين عليها فقط كتابة الحل بلغة إنجليزية عادية. كان الأمر يشبه مطالبتها بكتابة مقال حول كيفية حل لغز ما. كان بإمكانها أن تبدو مقنعة للغاية، باستخدام كلمات كبيرة وجمل تبدو منطقية. ولكن، تماماً مثل طالب حفظ "روح" أو "نمط" البرهان دون القيام بالرياضيات فعلياً، كان بإمكانها إخفاء أخطاء صغيرة قاتلة في مقالاتها. قد يغفل المعلم البشري عن خطأ صغير، وقد يحصل الروبوت على درجة ناجحة رغم أن الإجابة خاطئة.
الاختبار الجديد: "FormalProofBench"
أنشأ مؤلفو هذه الورقة البحثية اختباراً جديداً أكثر صرامة يسمى FormalProofBench. بدلاً من كتابة مقال، يتعين على الروبوتات الآن كتابة كود بلغة صارمة جداً ولا تغفر الأخطاء تسمى Lean 4.
فكر في Lean 4 كأنه حكم روبوت شديد الصرامة لا ينام أبداً ولا يرتكب أخطاء:
- إذا احتوى برهان الروبوت على فجوة منطقية واحدة، أو خطوة ناقصة، أو تعريف خاطئ، فسيصرخ الحكم فوراً: "فشل!" (FAIL!) ويوقف اللعبة.
- لا يوجد "ربما"، ولا "يبدو جيداً"، ولا "أعتقد أن هذا صحيح". الأمر ثنائي: نجاح أو فشل.
الإعداد: لغز الـ 40 دورة
هذا الاختبار ليس مجرد سؤال يُطرح لمرة واحدة. إنه أشبه بمستوى في لعبة فيديو حيث يحصل الروبوت على 40 دورة لحل مسألة رياضية بمستوى الدراسات العليا.
- الأدوات: لدى الروبوت صندوق أدوات. يمكنه البحث عن قواعد في مكتبة رقمية ضخمة (Mathlib)، وتشغيل أكواد اختبار صغيرة ليرى ما إذا كانت الخطوة تعمل، ثم يقدم إجابته النهائية في النهاية.
- الهدف: يجب على الروبوت أخذ مسألة رياضية معقدة (مثل إثبات نظرية حول الاحتمالات أو الجبر) وترجمتها إلى كود "Lean" يقبله الحكم.
النتائج: الروبوتات تتحسن، لكنها لا تزال تتعثر
اختبر الباحثون أذكى نماذج الذكاء الاصطناي في العالم (مثل Claude و GPT-5 و Gemini) على 200 من هذه المسائل الصعبة. وإليكم ما وجدوه:
- نماذج "التفكير" هي الفائزة: تمكن أفضل روبوت، وهو Claude Opus 4.5، من حل حوالي 33.5% من المسائل. قد يبدو هذا الرقم منخفضاً، ولكن تذكروا: هذه مسائل رياضيات بمستوى الدراسات العليا، حتى طلاب الدكتوراه البشر يعانون معها.
- الانخفاض الحاد: بعد النموذج الأول، انخفضت الدرجات بشكل حاد. النماذج التالية الأفضل حلت حوالي 18% أو أقل.
- السر الخفي (استخدام الأدوات): اكتشفت الورقة نمطاً رائعاً. الروبوتات التي حققت أفضل النتائج لم تكن فقط "تفكر" بعمق؛ بل كانت تكرر المحاولة (Iterating).
- الاستراتيجية السيئة: بعض الروبوتات استمرت في طلب المساعدة من المكتبة (البحث) مراراً وتكراراً، فتعثرت في حلقة مفرغة، مثل شخص يبحث عن مفتاح في كل درج دون أن يجرب فتح الباب أبداً.
- الاستراتيجية الجيدة: استخدمت الروبوتات الفائزة أداة "تشغيل الكود" (Run Code) باستمرار. جربت خطوة، ورأت أنها فشلت، فأصلحتها، ثم جربت مرة أخرى، ورأت أنها فشلت مجدداً. لقد تعاملت مع البرهان كأنه جلسة تصحيح أخطاء (Debugging session). كلما زاد عدد مرات "تشغيل الكود" والحصول على ردود فعل، زادت قدرتهم على النجاح.
لماذا يهم هذا الأمر؟
فكر في هذا كجسر بين الحدس البشري واليقين الآلي.
- حالياً، يتفوق الذكاء الاصطناعي في "الظهور بمظهر ذكي" (مرحلة المقال).
- يوضح هذا الاختبار أن الذكاء الاصطناعي بدأ يتعلم كيف يكون دقيقاً ومنضبطاً.
إذا تمكن الذك- الاصطناعي في النهاية من اجتياز هذا الاختبار بدرجات عالية، فهذا يعني أننا لن نملك فقط روبوتات "تتحدث" عن الرياضيات؛ بل سنملك روبوتات يمكنها إثبات حقائق رياضية جديدة دون ارتكاب أخطاء. يمكن أن يساعد هذا علماء الرياضيات البشر في التحقق من أعمالهم، واكتشاف نظريات جديدة، وضمان أن أسس العلم راسخة تماماً.
باخت-ة القول:
تقول الورقة البحثية: "لقد صنعنا حكماً آلياً صارماً للرياضيات. روبوتات الذكاء الاصطناعي الأفضل بدأت تجتاز الاختبار، لكنها لا تزال ترتكب أخطاء. الروبوتات التي تنجح هي تلك التي لا تخشى التجربة، والفشل، والإصلاح، ثم المحاولة مرة أخرى، بدلاً من مجرد التخمين".
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.