لقد أظهرت نماذج اللغات الضخمة (Large Language Models) إمكانيات كبيرة في ميدان إثبات النظريات الرسمية، إلا أن الأداء في ذروته يتطلب عادةً موارد حاسوبية ضخمة خلال وقت الاختبار بسبب استخدام عمليات شاملة أو نوافذ سياق ممتدة. في هذا العمل، نلقي الضوء على مشكلة التوسع في هذا المجال من خلال الاستغلال الأمثل للبنية المعلوماتية التي يوفرها التحقق الرسمي، والتي تتمثل في ملاحظة أن المترجمات (Compilers) تقوم بربط نطاق واسع من محاولات الإثبات المتنوعة بمجموعة مضغوطة من أنماط الفشل المنظمة.

نقدم إطار عمل للعمليات التعلمية، يعمل على استغلال هذه الضغوط للحصول على تعلم فعال واستكشاف للإثباتات. يتضمن ذلك استخدام بحث الشجرة (Tree Search) لتصحيح الأخطاء محليًا استنادًا إلى تغذية راجعة صريحة من المدقق (Verifier)، مما يتجاوز التكاليف المرتبطة بجمع تاريخ طويل من محاولات الإثبات. أظهرت التقييمات الشاملة أن طريقتنا تعزز باستمرار من قدرات الاستدلال للنماذج الأساسية عبر نطاقات مختلفة.

ما يميز طريقتنا هو تحقيق أداء رائد في اختبارات PutnamBench بين النماذج ذات المعلمات التي تصل إلى 8 مليارات و 32 مليار معلمة، وذلك ضمن ميزانيات زمنية اختبارية قابلة للمقارنة. لذا، نقدم نموذجاً قابلاً للتوسع للاستدلال المدعوم من المدققين للأجيال القادمة.