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

لملء هذا الفجوة، تم تقديم MA-ProofBench، وهو بمثابة أول معيار رسمي مخصص للبرهنة الرياضية في التحليل الرياضي. يتضمن هذا المعيار 200 نظرية مُشكلة تغطي 6 مواضيع رئيسية و27 فئة فرعية، بما في ذلك نظرية القياس والتكامل، التحليل العقدي، والتحليل الوظيفي. تم تقسيم المشكلات إلى مستويين من الصعوبة: مستوى البكالوريوس (المستوى الأول، 100 مشكلة) ومستوى مؤهل الدكتوراه (المستوى الثاني، 100 مشكلة) وذلك لتقييم مدى أداء نماذج اللغة الكبيرة في البرهنة الرياضية على درجات عمق مختلفة.

كل مشكلة تم إنشاؤها من خلال شراكة بين الإنسان ومساعدات نماذج اللغة، تلاها مراجعة مستقلة من خبراء، لضمان بقاء البيانات الرسمية وفية للرياضيات الأصيلة. عند تقييم مجموعة من نماذج التفكير العامة وأدوات البرهنة الرسمية باستخدام MA-ProofBench، للأسف، كانت النتائج مخيبة للآمال. حتى أفضل نموذج، GPT-5.5، سجل فقط 16% في المستوى الأول و5% في المستوى الثاني، بينما معظم النماذج الأخرى جاءت قريبة من 0% في المستوى الثاني.

تشير التحليلات الإضافية إلى أن الأخطاء الشائعة تشمل خيال Mathlib والبراهين غير المكتملة، بينما تكشف تقييمات النسخة اللغوية الطبيعية من المعيار عن فجوة واضحة بين التفكير غير الرسمي والرسمى.

يمثل MA-ProofBench مرجعاً موثوقاً لتتبع التقدم في التفكير الرياضي الرسمي في المجالات المتقدمة، ويعد دليلاً هاماً للباحثين والمطورين في هذا المجال.