MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement

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

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

أدرك الباحثون وراء MathForm أنه لكي تجعل الروبوت يتحدث لغة الرياضيات الرسمية بشكل مثالي، لا يمكنك مجرد تركه يكتب مسودة ويأمل في الأفضل. لقد بنوا خط تجميع من ثلاث خطوات لإصلاح سير عمل الروبوت. أولاً، قبل أن يكتب الروبوت سطراً واحداً من الشفرة، يقوم وكيل "باحث" (Researcher) بمسح مكتبة Mathlib الضخمة للعثور على التعريفات والقواعد الدقيقة التي يحتاجها الروبوت لهذا المشكل المحدد. إنه يشبه إعطاء الطاهي صفحة كتاب الطبخ الخاصة بـ "قطعة اللحم" قبل أن يمسك بالسكين. ثانياً، يكتب الروبوت شفرته، ثم يقوم "مفتش" (Inspector) بفحصها. إذا كانت الشفرة تحتوي على خطأ في الصيغة (مثل فاصلة مفقودة)، يشير المفتش إلى ذلك. وإذا كانت الشفرة تعمل ولكنها تعني شيئاً خاطئاً (مثل قول "جميع الأعداد" بينما كان المقص p المقصود هو "الأعداد الموجبة فقط")، يشرح المفتش الخطأ الدلالي. ثالثاً، بدلاً من الاستسلام، يستخدم الروبوت هذه التغذية الراجعة لإعادة كتابة شفرته. يستمر في الدوران عبر دورة "اكتب-افحص-أصلح" هذه حتى تصبح الشفرة مثالية.

باستخدام هذه الحلقة الذكية، أنشأ الفريق مجموعة بيانات ضخمة جديدة تسمى FormalVerse، تحتوي على حوالي 367,000 مثال رياضي تم التحقق منها. ثم قاموا بتدريب نموذج جديد، MathForm-8B، على هذه البيانات. كانت النتائج مفاجئة: هذا النموذج الصغير نسبياً (8 مليارات معلمة) أصبح أفضل في ترميز الرياضيات من النماذج الأكبر بكثير (32 مليار معلمة) التي اعتمدت على أساليب "التخمين والأمل" القديمة. في ستة اختبارات رياضية صعبة مختلفة، اجتاز MathForm-8B "فحص الاتساق" الصارم (أي أن الشفرة تعني بالفعل ما قاله المشكل البشري) بنسبة 72.4% من الوقت، متفوقاً على أفضل النماذج السابقة. وحتى في أكثر مسائل الجبر تجريداً وصعوبة، تفوق بشكل ملحوظ على منافسيه الأكبر حجماً. تشير الورقة البحثية إلى أنه من خلال منح النموذج الأدوات المناسبة للبحث عن المعلومات وفرصة التعلم من أخطائه، فأنت لا تحتاج إلى عقل عملاق لتكون عبقري رياضيات؛ بل تحتاج فقط إلى سير عمل ذكي.