تعلم إثبات النظريات من خلال التفاعل مع مساعدي الإثبات

يثبت البشر النظريات بالاعتماد على التفكير الرفيع والبصائر المحددة للمشكلة. تقدم مساعدو البرهان (Proof assistants) نظامًا رسميًا يشبه التفكير الرياضي للبشر، حيث يتم تمثيل النظريات في المنطق من الدرجة العليا والبراهين كاستراتيجيات رفيعة المستوى. ومع ذلك، يجب على الخبراء البشريين بناء البراهين يدويًا عن طريق إدخال الاستراتيجيات إلى مساعد البرهان. في هذا البحث، ندرس مشكلة استخدام التعلم الآلي لتمكين التفاعل مع مساعدي البرهان بشكل آلي. قمنا ببناء "CoqGym"، وهو مجموعة بيانات وبيئة تعلم على نطاق واسع تحتوي على 71 ألف برهان مكتوب من قبل البشر من 123 مشروعًا تم تطويرها باستخدام مساعد البرهان Coq. طورنا "ASTactic"، وهو نموذج يستند إلى التعلم العميق ويولد استراتيجيات كبرامج في شكل أشجار الصيغ المجردة (Abstract Syntax Trees - ASTs). تظهر التجارب أن "ASTactic" الذي تم تدريبه على "CoqGym" يمكنه إنتاج استراتيجيات فعالة ويمكن استخدامه لإثبات نظريات جديدة لم يكن بالإمكان إثباتها سابقًا بواسطة الطرق الآلية. الكود متاح على الرابط: https://github.com/princeton-vl/CoqGym.