مُقدّمة كيمينا-بروفير: نحو نماذج استدلال رياضي كبيرة باستخدام التعلّم بالتعزيز

نُقدِّم نسخة تجريبية من Kimina-Prover، وهو نموذج لغوي كبير يُعدّ رائدًا في نمط استكشاف مبني على الاستدلال، مُطبّق على إثبات النظريات الرسمية، كما يُظهر هذا الإصدار التجريبي. وقد تم تدريب Kimina-Prover باستخدام نظام تعلم تعزيزي على نطاق واسع مستندًا إلى نموذج Qwen2.5-72B، ويُظهر أداءً قويًا في إنشاء البراهين باستخدام لغة Lean 4، من خلال استخدام نمط استدلال منظم نسميه \textit{نمط الاستدلال الرمزي}. يمكّن هذا النهج النموذج من تقليد استراتيجيات حل المشكلات البشرية في بيئة Lean، من خلال توليد خطوات البرهان بشكل تكراري وتحسينها تدريجيًا. ويُحقّق Kimina-Prover أداءً جديدًا على مستوى الحالة الراهنة في اختبار miniF2F، حيث بلغت النسبة 80.7% عند استخدام 8192 محاولة (pass@8192). وبالإضافة إلى تحسين الأداء في الاختبارات، تُسهم دراستنا في عدة رؤى مهمة: (1) يُظهر Kimina-Prover كفاءة عالية في استخدام العينات، حيث يُحقّق نتائج متميزة حتى مع عدد قليل جدًا من المحاولات (pass@1)، كما يُ-scalable بشكل فعّال مع زيادة الموارد الحاسوبية، وذلك بفضل نمطه الفريد في الاستدلال وتدريبه باستخدام التعلم التعزيزي؛ (2) نُثبت وجود تحسن واضح في الأداء مع زيادة حجم النموذج، وهي ظاهرة لم تُلاحظ سابقًا في النماذج العصبية الخاصة بإثبات النظريات في الرياضيات الرسمية؛ (3) يُظهر الأسلوب الاستدلالي المُتعلّم، الذي يختلف عن الخوارزميات التقليدية للبحث، إمكانات كبيرة في تقليل الفجوة بين التحقق الرمزي والحدس الرياضي غير الرسمي. ونُطلق نسخًا مُختصرة من Kimina-Prover مفتوحة المصدر، بحجم 1.5 مليار و7 مليارات معلمة.