ليرا: تهيئة التصحيح المزدوج في إثبات النظرية الآلي

تمثّل النماذج اللغوية الكبيرة (LLMs) مسارًا مثيرًا للاهتمام للبحث في مجال إثبات النظريات الرسمية. ومع ذلك، لا يزال الجزء الأكبر من إمكاناتها الكاملة، وخاصة فيما يتعلق بتقليل الظواهر الوهمية (hallucinations) وتحسين الأداء من خلال رسائل الأخطاء الناتجة عن أدوات الإثبات، مجالًا لم يُستكشف بشكل كافٍ حتى الآن. لتعزيز فعالية النماذج اللغوية الكبيرة في هذا المجال، نقدّم "ليرا" (Lyra)، وهي إطار عمل جديد يعتمد على آلية تصحيح مزدوجة: التصحيح بالأداة (Tool Correction - TC) والتصحيح التخميني (Conjecture Correction - CC). لتنفيذ التصحيح بالأداة في مرحلة ما بعد معالجة الأدلة الرسمية، نستفيد من المعرفة السابقة من خلال استخدام أدوات إثبات محددة مسبقًا (مثل Sledgehammer) لتوجيه استبدال الأدوات الخاطئة. يساهم التصحيح بالأداة بشكل كبير في تقليل الظواهر الوهمية، مما يُحسّن الدقة العامة للدليل. بالإضافة إلى ذلك، نقدّم آلية التصحيح التخميني، وهي آلية تغذية راجعة للأخطاء مصممة للتفاعل مع أداة الإثبات لتحسين التخمينات المتعلقة بالدليل الرسمي باستخدام رسائل الأخطاء الناتجة عن الأداة. مقارنةً بالإطار السابق للتحسين، فإن التصحيح التخميني المُقترح يُحسّن النتائج باستخدام تعليمات (instructions) دون الحاجة إلى جمع مجموعة مزدوجة من البيانات (الإخراج، الخطأ، والتحسين). وقد حقق أسلوبنا أداءً متقدمًا (SOTA) على كلا المجموعتين: التحقق من صحة miniF2F (من 48.0% إلى 55.3%) والاختبار (من 45.5% إلى 51.2%). كما قمنا بعرض حلّ ثلاث مشكلات من أولمبياد الرياضيات الدولية (IMO) باستخدام ليرا. نعتقد أن التصحيح بالأداة (الذي يُطبّق في مرحلة ما بعد المعالجة لتقليل الظواهر الوهمية) والتصحيح التخميني (الذي يُعدّل الأهداف الفرعية من خلال التفاعل مع البيئة) يمكن أن يقدّما مسارًا واعدًا للبحث المستقبلي في هذا المجال.