تفكيك الألغاز: التعلم القائم على العروض ذات الأهداف الفرعية لإثبات النظريات الرسمية

تمثّل النماذج اللغوية الكبيرة (LLMs) مسارًا مثيرًا للاستكشاف في مجال إثبات النظريات الرسمية. ومع ذلك، ما يزال الاستخدام الكامل لهذه النماذج، وخاصة فيما يتعلق بتنسيق وتنظيم الأمثلة التوضيحية، مجالًا غير مُستكشَف بالكامل. من أجل تحسين كفاءة النماذج اللغوية الكبيرة، نقدّم إطارًا تعلّميًا قائمة على الأهداف الجزئية، يتكوّن من عنصرين رئيسيين: أولاً، مسترشدين بمناهج تعلّم الأهداف الجزئية من مجالات التعلّم التكاملي والروبوتات، نقترح بناء أهداف جزئية متميزة لكل مثال توضيحي، وتحسين هذه الأهداف وفقًا للنظريات ذات الصلة بتعلّم الأهداف الجزئية. ثانيًا، نستفيد من التطورات الحديثة في نماذج الانتشار (diffusion models) للتنبؤ بأفضل تنظيم ممكن، مع معالجة مشكلتين معقّدتَين ما زالا يعاني منهما مجال تنظيم الأمثلة التوضيحية: اختيار المجموعات الجزئية وتحديد الترتيب. من خلال دمج منهجيات تعلّم الأهداف الجزئية، نجحنا في رفع دقة الإثبات السائدة من 38.9٪ إلى 44.3٪ على معيار miniF2F. علاوة على ذلك، يمكن لاستخدام نماذج الانتشار في تنظيم الأمثلة التوضيحية أن يؤدي إلى تحسين إضافي في الدقة إلى 45.5٪، أو تحقيق تحسين بقيمة 5 أضعاف في كفاءة العينة مقارنة بالطريقة القياسية المتبعة منذ فترة طويلة. يُمكن الاطلاع على الكود الخاص بنا عبر الرابط: \url{https://github.com/HKUNLP/subgoal-theorem-prover}.