في عالم الرياضيات، تتميز المسائل التنافسية بتنوعها، حيث توجد نوعان رئيسيان: إثبات النظريات (Theorem Proving) وبناء الإجابات (Answer Construction). شهدنا مؤخراً تقدماً كبيراً في تقنيات الإثبات الرسمي بفضل التطورات الأخيرة في نماذج اللغات الضخمة (Large Language Models)، بينما ظل موضوع بناء الإجابات أقل دراسة حتى الآن.

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

إضافة إلى ذلك، لا يضمن فقط فحص الإثباتات في Lean أن الجواب المُنشأ هو إجابة معيارية: فالشهادات الدائرية أو غير المفهومة يمكن أن تلغي الكميات الوجودية، مما يؤدي إلى عدم اعترافها كإجابات محتملة. للتغلب على هذه الفجوة، تم تقديم إطار العمل extit{Enumerate-Conjecture-Prove} (ECP)، وهو نظام عصبي-رمزي في Lean يتيح بناء الإجابات مع تحقيق إثباتات رسمية.

يعتمد ECP على نماذج اللغات الضخمة لمساعدتها في تعداد الأدلة وبناء إجابات مرشحة، كما يستعين بنماذج الإثبات لانتاج إثباتات موثوقة. في اختبارات على مجموعة PutnamBench ومجموعة MathArena المؤتمتة، تمكن ECP من حل 17 من أصل 346 و18 من أصل 75 حالة بقبول، مما يتفوق على معايير نماذج اللغات في ميزانيات الاستدلال المتجانسة.

لمزيد من التفاصيل، يمكنكم زيارة رابط الكود المقدم على GitHub: [https://github.com/sunjia72/ecp-lpar].