وكيل للتعلم في السياق لإثبات النظريات الرسمية

نقدّم وكيلًا للتعلم في السياق (in-context learning) مخصصًا لإثبات النظريات الرسمية في بيئات مثل Lean وCoq. تُعد النماذج الحالية الأفضل في هذا المجال مُدرّبة بشكل مُخصص على بيانات إثبات مُحدّدة للبيئة. على العكس، يعتمد نهجنا، المُسمّى COPRA، على طلب تكراري من نموذج لغوي كبير عالي القدرة وعام (GPT-4) لاقتراح تطبيقات التكتيك (tactic applications) ضمن عملية بحث تراجعية (backtracking) قائمة على الحالة (stateful). تُنفّذ التكتيكات المقترحة في بيئة الإثبات الأساسية. ويُستخدم التغذية المرتدة الناتجة عن التنفيذ لبناء مُدخل السؤال التالي للنموذج، جنبًا إلى جنب مع معلومات مختارة من سجل البحث ونظريات استُخلِصت من قاعدة بيانات خارجية. تم تقييم تنفيذنا لـ COPRA على معيار miniF2F الخاص بـ Lean، وعلى مجموعة من المهام الخاصة بـ Coq من مشروع CompCert. على هذه المعايير، يتفوّق COPRA بشكل كبير على الاستدعاءات القليلة (few-shot) لنموذج GPT-4. كما يُقارن بشكل مُرضٍ مع النهج القائم على التدريب المُخصص (finetuning)، حيث يتفوّق على ReProver، وهو نموذج مُدرّب مُخصص حديث ورائد في مجال Lean، من حيث مقياس النجاح (pass@1). يُتاح كودنا وبياناتنا على الرابط: https://github.com/trishullab/copra.