Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning

إليك ملخص تقني مفصل لورقة البحث بعنوان "تحسين الصياغة التلقائية لـ Lean4 عبر الضبط الدقيق لاتساق الدورات" للباحث أرسين شيبزوكوف.

1. بيان المشكلة

الصياغة التلقائية (Autoformalization) هي مهمة ترجمة العبارات الرياضية من اللغة الطبيعية (NL) إلى لغات الإثبات الرسمية مثل Lean4. وبينما أظهرت النماذج اللغوية الكبيرة (LLMs) قدرات واعدة في الاستنتاج، إلا أنها غالباً ما تولد أكواد Lean4 صحيحة تركيبياً (تنجح في التجميع/Compilation) ولكنها غير صحيحة دلالياً، حيث تفشل في التقاط المعنى الرياضي المقصود.

التحدي الجوهري الذي تعالجه هذه الدراسة هو تحسين الأمانة الدلالية (Semantic Fidelity) للترجمة من اللغة الطبيعية إلى Lean4 دون الاعتماد على أدوات خارجية مكلفة (مثل مترجم Lean4 كامل أو مدقق رمزي) أثناء حلقة التدريب. يبحث المؤلف فيما إذا كان اتساق الدورة (Cycle Consistency) — أي القدرة على الترجمة من لغة طبيعية $\to$ Lean4 $\to$ لغة طبيعية واستعادة المعنى الأصلي — يمكن أن يعمل كإشارة تدريب فعالة لتعزيز أداء النموذج.

2. المنهجية

2.1 بنية النموذج والإعداد

• النموذج الأساسي: Qwen3.5-2B (نموذج لغوي بـ 2 مليار معلمة).
• استراتيجية الضبط الدقيق: يتم تطبيق التكيف منخفض الرتبة (LoRA) حصرياً على طبقات الشبكة الأمامية (FFN) ($r=16, \alpha=32$)، مما ينتج عنه حوالي 9.4 مليون معلمة قابلة للتدريب.
• نظام النموذج المزدوج:
  1. $f_\theta$ (nl2lean): النموذج القابل للتدريب الذي يحول اللغة الطبيعية إلى Lean4.
  2. $g_\phi$ (lean2nl): نموذج ترجمة عكسية يحول Lean4 إلى لغة طبيعية. يتم تدريب هذا النموذج عبر الضبط الدقيق الخاضع للإشراف (SFT) ثم يتم تجميده خلال مرحلة التعلم التعزيزي (RL).

2.2 مسار التدريب

يتم التدريب على مرحلتين متميزتين:

المرحلة الأولى: الضبط الدقيق الخاضع للإشراف (SFT)

• البيانات: مجموعة بيانات FineLeanCorpus (FLC)، وهي تتكون من 509 ألف زوج من (لغة طبيعية/Lean4). تم تطهير البيانات من PutnamBench (معيار اختبار محجوز يتكون من 660 مسألة تنافسية) باستخدام تشابه TF-IDF.
• الأنواع المختبرة:
  1. SFT المنهجي (Curriculum SFT): التدريب بالتتابع على بيانات مرتبة حسب الصعوبة (من 1 إلى 10).
  2. SFT بدون منهجية (No-Curriculum SFT): التدريب على نفس مجموعة البيانات المبعثرة.
• الهدف: إنشاء خط أساس قوي واختبار ما إذا كان ترتيب الصعوبة يساعد في التعلم.

المرحلة الثانية: التعلم التعزيزي (RL) عبر خوارزمية GRPO

• الخوارزمية: تحسين السياسة النسبي للمجموعات (Group Relative Policy Optimization - GRPO). تتجنب هذه الخوارزمية الحاجة إلى نموذج ناقد (Critic) منفصل من خلال تطبيع المكافآت ضمن مجموعات من الإكمالات التي تم أخذ عينات منها.
• إشارة المكافأة (اتساق الدورة):
  لكل عبارة Lean4 مولدة $\hat{l}$ من النص المحفز $s$، تُعرف المكافأة $r$ كالتالي:
  $$r(\hat{l}, s) = \cos(e(s), e(g_\phi(\hat{l})))$$
  حيث $e(\cdot)$ هو تضمين الجملة (Sentence Embedding) من نموذج all-MiniLM-L6-v2. يقيس هذا التشابه الجيبي (Cosine Similarity) بين عبارة اللغة الطبيعية الأصلية واللغة الطبيعية المعاد ترجمتها.
• الهدف: تعظيم مكافأة اتساق الدورة مع الحفاظ على عقوبة KL للبقاء قريباً من سياسة المرجع الخاصة بـ SFT.

3. المساهمات الرئيسية

1. اتساق الدورة كإشارة تدريب: تثبت الورقة أن استخدام اتساق الدورة القائم على التضمين كمكافأة في GRPO يحسن بشكل كبير الجودة الدلالية للصياغة التلقائية، متفوقاً على SFT القياسي.
2. اختبار المنهجية (Ablation of Curriculum Learning): تدرس الدراسة بدقة ما إذا كان التدريب على بيانات مرتبة حسب الصعوبة (1 $\to$ 10) يوفر فوائد مقارنة بالتدريب المبعثر. تظهر النتائج عدم وجود فائدة ملموسة لنموذج بحجم 2B، مما يشير إلى أن ترتيب المنهج لا يعوض القدرة المحدودة للنموذج في هذه المهمة المحددة.
3. مسار RL فعال من حيث المعلمات: يقدم العمل مساراً فعالاً من حيث المعلمات (LoRA + GRPO) يحسن الأداء على وحدة معالجة رسومات واحدة دون الحاجة إلى زمن انتقال (Latency) لمترجم Lean4 حي أثناء التدريب.
4. تقييم شامل: تم تقييم النماذج على كل من مجموعات البيانات داخل التوزيع (FLC held-out) وخارج التوزيع (PutnamBench)، مما يوفر تقييماً قوياً للتعميم.

4. النتائج التجريبية

4.1 مقاييس الأداء

المقياس الأساسي هو متوسط اتساق الدورة ($\bar{C}$). يُستخدم فقدان الإنتروبيا المتقاطعة (Cross-entropy loss) كمقياس ثانوي لضمان عدم تدهور قدرات النموذج الأساسية في نمذجة اللغة.

• RL مقابل SFT: حقق نموذج RL تحسناً قدره 0.156 في متوسط اتساق الدورة على مجموعة FLC المحجوزة و 0.139 على PutnamBench مقارنة بخط أساس SFT.
• الدلالة الإحصائية: التحسينات عالية الأهمية ($p < 10^{-56}$).
• التكلفة: يأتي التحسن مع زيادة طفيفة جداً في فقدان الإنتروبيا المتقاطعة (فقط +0.011 نات)، مما يشير إلى أن النموذج يحتفظ بقدرته على نمذجة اللغة.
• نتيجة المنهجية: نماذج SFT Curriculum و SFT No-Curriculum لا يمكن التمييز بينهما إحصائياً، مما يؤكد أن ترتيب الصعوبة لا يقدم ميزة في هذا الحجم.

4.2 تحليل النتائج

• تدرج الصعوبة: يظهر تحسن RL بشكل أوضح في المسائل السهلة (الصعوبة 1) ويتناقص رتيباً مع زيادة الصعوبة. ويُعزى ذلك إلى إشارة المكافأة "الأكثر ضجيجاً" في المسائل الصعبة، حيث يكافح المترجم العكسي المجمد لتفسير مخرجات Lean4 المعقدة.
• أداء المجالات: يتفوق RL على SFT في جميع المجالات الرياضية. تظهر المجالات المنفصلة والجبرية (نظر الأعداد، الجبر) أعلى المكاسب، بينما تظهر المجالات المستمرة (التفاضل والتكامل، التحليل) درجات مطلقة أقل بسبب تعقيد تعريفات $\epsilon$-$\delta$ وهياكل Lean4 المطولة.
• انزياح التوزيع: في FLC، يخلق RL "ذيلاً ذا درجات عالية" (العديد من الدرجات > 0.8)، مما يشير إلى أنه قد يستغل الانتظامات الهيكلية في بيانات التدريب. أما في PutnamBench (الأكثر تنوعاً)، فإن التحسن هو إزاحة موحدة، مما يشير إلى تعميم أكثر حقيقية.

5. الأهمية والقيود

الأهمية:

• المحاذاة الدلالية: تثبت هذه الدراسة أن الاتساق الدلالي (عبر ترجمة الدورة) هو هدف قابل للتطبيق وقوي لتدريب نماذج الصياغة، مما يقلل من الاعتماد على حلقات التغذية الراجعة الهشة للمترجم (Compiler) أثناء التدريب.
• القابلية للتوسع مقابل RL: بينما يحسن توسيع النموذج إلى 9 مليار معلمة الأداء، إلا أن نموذج 2B المدرب بـ RL (GRPO) يتفوق على نموذج 9B المدرب فقط بـ SFT في البيانات داخل التوزيع، مما يسلط الضة على كفاءة إشارات RL.
• العملية: النهج فعال حاسوبياً، حيث يتطلب فقط تضمينات الجمل بدلاً من مترجم Lean4 كامل أثناء حساب مكافأة RL.

القيود:

• اختراق المكافأة (Reward Hacking): يحتوي مقياس اتساق الدورة على نقاط عمياء. يمكن للمترجم العكسي أحياناً أن "يردد" العبارة الأصلية حرفياً إذا كانت صياغة Lean4 مشابهة هيكلياً للغة الطبيعية، مما يعطي مكافأة مثالية حتى لو كانت الصياغة الرسمية فارغة رياضياً.
• المقياس البديل: اتساق الدورة هو مقياس بديل للصحة الدلالية. يمكن للنموذج إنتاج عبارات متسقة تركيبياً ولكنها خاطئة رياضياً ومع ذلك تسجل درجات عالية.
• تحيز المترجم العكسي: استخدام مترجم عكسي واحد مجمد لكل من المكافأة والتقييم يدخل تحيزاً منهجياً؛ حيث تؤثر أخطاء المترجم العكسي على جميع النماذج بالتساوي.

الخاتمة

تثبت الورقة أن الضبط الدقيق لاتساق الدورة عبر GRPO هو استراتيجية فعالة للغاية لتحسين الصياغة التلقائية لـ Lean4. فهي تتفوق بشكل كبير على SFT القياسي والتعلم المنهجي، خاصة في البيانات داخل التوزيع، مع الحفاظ على الكفاءة الحسابية. تشير النتائج إلى أنه بالنسبة للنماذج الصغيرة والمتوسطة، فإن التحسين من أجل دقة الرحلة الشاملة (Round-trip fidelity) يعد إشارة تدريب أكثر فعالية من ترتيب المنهج القائم على الصعوبة. يجب أن يركز العمل المستقبلي على دمج التغذية الراجعة الصعبة من المترجم (Compiler) للتخفيف من اختراق المكافأة ومزيد من التحقق على معايير متنوعة وخارج التوزيع.