SubgoalXL: التعلم القائم على الأهداف الفرعية للخبراء في إثبات النظريات

المبرهنة الرسمية، وهي مجال يجمع بين الرياضيات وعلوم الحاسوب، شهدت اهتمامًا متجددًا بفضل التقدم في نماذج اللغات الكبيرة (LLMs). يقدم هذا البحث نظام SubgoalXL، وهو منهج جديد يجمع بين البراهين القائمة على الأهداف الفرعية والتعلم الخبير لتعزيز قدرات نماذج اللغات الكبيرة في المبرهنة الرسمية داخل بيئة Isabelle. يعالج SubgoalXL تحديين حاسمين: نقص البيانات المتخصصة في الرياضيات والمبرهنة، والحاجة إلى تحسين قدرات الاستدلال متعدد الخطوات في نماذج اللغات الكبيرة. من خلال تحسين كفاءة البيانات واستخدام الإشراف على مستوى الأهداف الفرعية، يتمكن SubgoalXL من استخراج معلومات أكثر غنىً من البراهين التي تم إنشاؤها بواسطة البشر بشكل محدود. يدمج الإطار استراتيجيات البرهان الموجهة للأهداف الفرعية بنظام التعلم الخبير، مما يؤدي إلى تكرار تحسين مولدات العبارات الرسمية والبراهين والأهداف الفرعية. باستغلال مزايا بيئة Isabelle في البراهين القائمة على الأهداف الفرعية، حقق SubgoalXL أداءً رائدًا جديدًا بنسبة 56.1٪ في Isabelle على مجموعة بيانات miniF2F القياسية، مما يمثل تحسنًا مطلقًا بنسبة 4.9٪. وبشكل لافت للنظر، نجح SubgoalXL في حل 41 مشكلة من AMC12 و9 مشاكل من AIME و3 مشاكل من IMO من مجموعة بيانات miniF2F. هذه النتائج تؤكد فعالية تعظيم الاستفادة من البيانات المحدودة واستخدام التوجيه المستهدف للاستدلال المعقد في المبرهنة الرسمية، مما يساهم في التقدم المستمر لقدرات الاستدلال الصناعي. يمكن الحصول على التنفيذ من الرابط \url{https://github.com/zhaoxlpku/SubgoalXL}.