كيف تمكن مختبر صيني من كسر عنق الزجاجة في البرهان الرياضي المعزز بالذكاء الاصطناعي

البراهين الرياضية الشكلية، النوع الذي يتم التدقيق فيه بواسطة الآلات وليس البشر، هي المعيار الذهبي للدقة. لكن ترجمة البراهين غير الشكلية التي يكتبها علماء الرياضيات باللغة الطبيعية إلى لغات شكلية مثل Lean لا تزال تمثل تحديًا مستعصيًا وطويل الأمد. فريق من جامعة نانجينغ وشركة Polixir Technologies يقول الآن إنه نجح في كسر عنق الزجاجة الرئيسي في هذا المسار.

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

تحليل عنق الزجاجة

لتحديد أين يتم إنفاق موارد وقت الاختبار بشكل أفضل، أجرى الباحثون تجربة تدخل مضبوطة. تحت تتبع أخطاء Lean متطابق وميزانية تصحيح ثابتة، سمحوا لواحد فقط من الوكلاء الثلاثة بمراجعة مخرجاته مع تجميد الاثنين الآخرين. حقق تدخل المفكك باستمرار أعلى دقة في البرهان الكامل: 51.1% بعد خمس جولات على عينة مكونة من 184 من ProofFlowBench، مقارنة بـ 45.1% للمنسق و 33.7% للمثبت.

"المفكك يحدد صعوبة كل التزام لاحق"، يكتب المؤلفون. التفكيك الذي ينتج وحدات برهان ذرية مكتفية بذاتها مع تبعيات واضحة يقلل من التنسيق والإثبات إلى مهام محلية يمكن للوكلاء اللاحقين التعامل معها. الوحدات سيئة النطاق تترك المنفذ بأهداف غامضة أو غير مكتملة.

كيف يعمل ToMap

بدلاً من توزيع موارد وقت الاختبار عبر جميع الوكلاء الثلاثة، يركزها ToMap على المفكك. يحافظ على مجموعة من التفكيكات المحتملة باللغة الطبيعية، ويقيم كل منها وفقًا لمقياس ثلاثي الأبعاد (الوفاء الدلالي، وقابلية الإثبات، وملاءمة Lean)، ويستخدم حدود Pareto الناتجة لتوجيه التطور التكراري لاستدعاءات التفكيك، وهي تقنية مستوحاة من خوارزمية GEPA لتحسين استدعاءات الانعكاس.

بوابة الالتزام تحجز دورة التنسيق-المثبت-Lean والتحقق الباهظة الثمن للمرشحين الذين يستوفون حدًا أدنى في جميع الأبعاد الثلاثة للمقياس. "ردود فعل المقياس رخيصة وكثيفة، وتوجه الجزء الأكبر من البحث، بينما يوفر التحقق من Lean إشارات حقيقة موثوقة ولكنها باهظة الثمن محجوزة للمرشحين الواعدين"، يشرح المؤلفون.

النتائج والمقارنات

على ProofFlowBench، حقق ToMap المدعوم من Gemini3-Pro درجة صحة تركيبية ودقة دلالية مشتركة بلغت 40.22%، بتحسن قدره 19.0 نقطة مئوية عن أفضل طريقة سابقة، Codex End2End (21.20%). على miniF2F، مجموعة بيانات مسائل المنافسة على مستوى المدارس الثانوية، وصل ToMap إلى 55.74%، بتحسن 8.2%. كما تفوق النظام على الأساليب القائمة على التدريب مثل ProofBridge، الذي يتطلب نموذج استرجاع ومترجم مضبوط، مع الحفاظ على تكاليف الاستدلال فقط أقل.

تكشف دراسات الإزالة عن مقايضة واضحة بين الوقت والأداء: تظهر معظم المكاسب خلال 3-5 تكرارات تطورية، وبعدها تتضاءل العوائد. وهذا يعطي إرشادًا عمليًا لاختيار ميزانية التكرار تحت قيود زمنية أو تكلفة.

"الطرق التي تولد برهانًا واحدًا متكاملًا بلغة Lean يمكن أن تحقق درجة عالية نسبيًا من الصحة التركيبية، لكنها تكافح لترجمة الخطوات الفردية للبراهين باللغة الطبيعية بأمانة"، يلاحظ المؤلفون. "التنسيق الشكلي خطوة بخطوة يحافظ بشكل أفضل على الوفاء الدلالي من خلال مواءمة العملية الشكلية بشكل صريح مع خطوات البرهان الوسيطة."

القيود والعمل المستقبلي

التقييم يقتصر على براهين على مستوى المعايير، وليس رياضيات طويلة على مستوى البحث. يفترض النظام أيضًا أن براهين الإدخال صحيحة، والتعامل مع البراهين غير الشكلية الخاطئة أو غير المكتملة لا يزال مشكلة مفتوحة. توسيع الإطار لاكتشاف وإصلاح التفكير المعيب تم وضع علامة عليه كعمل مستقبلي.

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