في عالم إثبات النظريات الآلي، يبدو أن التحديات تزداد تعقيدًا. فمعظم معايير اختبار البرهنة الآلية (Automated Theorem Proving) تعتمد على ما نسميه 'الوضع السهل'، حيث يتم تضمين الإجابة النهائية ضمن البيان الرسمي، مما يسهل المهمة نسبيًا مقارنةً بما يواجهه الإنسان من تحديات.

لكن ماذا لو أردنا اختبار الأنظمة في ظروف أكثر صرامة ودقة؟ هنا يأتي دور 'الوضع الصعب' الذي يتطلب من الأنظمة اكتشاف الإجابة بشكل مستقل قبل صياغة البرهان الرسمي. لتحقيق هذا الهدف، قدم الباحثون إسهامين رئيسيين.

أولاً، تم إصدار نسختين محدّثتين تحملان اسم MiniF2F-Hard وFIMO-Hard، وهما نسخ معاد تصنيفها من معايير اختبار البرهنة الآلية الشهيرة. ثانيًا، تم تقديم إطار Discover And Prove (DAP)، الذي يستخدم نماذج اللغة الكبيرة (Large Language Models) في عمليات التفكير اللغوي الطبيعي مع تأمل ذاتي صريح لاكتشاف الإجابات، ثم إعادة صياغة البيانات الصعبة إلى بيانات سهلة لاستخدامها مع البرهانات الآلية الحالية.

لقد أحدث DAP ثورة في المجال؛ فعلى CombiBench زاد من عدد المشكلات المحلولة من 7 (وكانت النتيجة السابقة 16) إلى 10، بينما على PutnamBench أصبح أول نظام يثبت رسميًا 36 نظرية في الوضع الصعب. الأهم من ذلك، كشف DAP أن النماذج اللغوية الحديثة تتجاوز نسبة دقة الإجابات 80% في نفس المشكلات التي تدير البرهان الآلي فيها تحت 10%، مما يُظهر فجوة كبيرة في الأداء تُناسبها المعايير الصعبة بشكل فريد.

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