ملخص تقني: من الاستدلال إلى الكود: تحسين GRPO للغات غير الممثلة كفاية

بيان المشكلة

لا يزال توليد كود دقيق وقابل للتنفيذ في لغات البرمجة غير الممثلة كفاية (مثل Prolog و Lisp) يشكل تحديًا كبيرًا للنماذج اللغوية الكبيرة (LLMs). وبينما تتفوق النماذج في اللغات ذات الموارد العالية مثل Python، فإنها تفشل باستمرار في البرمجة المنطقية بسبب ندرة بيانات التدريب العامة. تؤدي ندرة البيانات هذه إلى أنماط فشل محددة: هلوسة مقدمات (predicates) غير موجودة، فرض تدفق تحكم إمرِي (imperative) على النماذج التصريحية (declarative)، وسوء التعامل مع التوحيد (unification) والتراجع (backtracking). إن الضبط الدقيق الخاضع للإشراف القياسي (SFT) غير كافٍ لأنه يعتمد على أمثلة بشرية نادرة ولا يعمل مباشرة على تحسين صحة التنفيذ.

المنهجية

يقترح البحث إطار عمل للتعلم المعزز بالجوائز القابلة للتحقق (RLVR) يستخدم التغذية الراجعة القائمة على التنفيذ لتدريب نماذج لغوية كبيرة صغيرة الحجم (عائلة Qwen2.5-Coder، من 0.5 مليار إلى 7 مليارات معلمة) دون الاعتماد على مجموعات بيانات واسعة منسقة بشريًا.

الإطار الأساسي

• الخوارزمية: يستخدم المؤلفون خوارزمية تحسين السياسة النسبي للمجموعات (GRPO)، وهي خوارزمية تدرج السياسة التي تلغي الحاجة إلى شبكة دالة قيمة منفصلة (على عكس PPO). تقوم GRPO بتقدير الميزة (advantage) للمخرجات بالنسبة لمجموعة من مخرجات الأقران التي تم أخذ عينات منها من نفس المطالبة، مما يقلل من العبء الحسابي.
• حلقة التدريب: يدمج النظام مفسر Prolog (عبر PySwip) مباشرة في حلقة التدريب. يقوم النموذج اللغوي بتوليد الكود استجابةً لمطالبات اللغة الطبيعية (تحديدًا من مجموعة بيانات GSM8K)، ويقوم المفسر بتنفيذ الكود لتوفير إشارة صحة حقيقية.
• نظام الجوائز: تجمع دالة مكافأة متعددة الأهداف أربع إشارات:
  1. جوائز التنسيق: عقوبات ومكافآت للالتزام بقالب XML صارم (<reasoning>, <code>, <query>)، لضمان إمكانية استخراج الكود. يتم تطبيق عقوبة محددة إذا تم إدراج الاستعلام بشكل خاطئ داخل كتلة الكود.
  2. جوائز الصحة: بناءً على نتائج التنفيذ:
     • +1.0: تطابق تام مع الحقيقة الأرضية.
     • -1.0: خطأ منطقي (يتم تنفيذه ولكن بنتيجة خاطئة).
     • -0.5: خطأ في بناء الجملة (يفشل في التجميع/التنفيذ).
     • -0.1: انتهاء المهلة أو عدم وجود مخرجات.

التدخلات التقنية الرئيسية

حدد المؤلفون نمط فشل يسمى "تقلص الاستدلال" (reasoning contraction)، حيث تسبب التدريب القياسي باستخدام GRPO مع عقوبة تباعد كولباك - ليبلر (KL divergence) في انهيار نموذج 7B إلى أنماط مخرجات قصيرة ومحفوظة، مما أدى إلى تدهور الدقة بمرور الوقت. ولمعالجة ذلك، قدموا تعديلين حاسمين:

1. إزالة تباعد KL: سمح إلغاء عقوبة KL للسياسة بالابتعاد أكثر عن الخط المرجعي الخاضع للإشراف، مما مكن النموذج من استيعاب نموذج البرمجة المنطقية المتميز.
2. مكافأة مدركة للطول: تمت إضافة آلية مكافأة محددة لتشجيع سلاسل الاستدلال ضمن نطاق عدد توكنات مستهدف، مما يمنع النموذج من قطع عملية الاستدلال الخاصة به.

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

1. حالة سائدة جديدة لـ Prolog: أثبتوا أن RLVR بالتغذية الراجعة القائمة على التنفيذ يمكن أن تعوض النقص الشديد في البيانات، مما أرسى معيارًا جديدًا لتوليد كود Prolog على GSM8K باستخدام نموذج بـ 7 مليارات معلمة.
2. التحليل التجريبي لأنظمة GRPO: حددوا "تقلص الاستدلال" كنمط فشل محدد لـ KL-regularized RL في البرمجة المنطقية، وشخصوا الظروف التي يكون فيها تخفيف هذا القيد مفيدًا.
3. التعميم لما وراء الحساب: أظهروا أن التحسينات تنتقل إلى 20 مهمة متنوعة في Prolog (Rosetta Code) وإلى معيار GSM-Symbolic، حيث تضاعفت دقة Zero-shot أكثر من مرتين.
4. صلاحية عبر اللغات: تحققوا من النهج على لغة Lisp، مما أثبت أن RL المدفوع بالمفسر فعال عبر عائلات مختلفة من اللغات غير الممثلة كفاية.

النتائج

أُجريت التجارب على مجموعة بيانات GSM8K، مع تقييمات على Rosetta Code و GSM-Symbolic (متغيرات P1 و P2).

• أداء GSM8K:
  • حقق نموذج Qwen2.5-Coder-7B المحسن (Zero-shot، بدون KL، مع قيد الطول) pass@4 بنسبة 0.882.
  • في إعدادات One-shot، وصلت نفس الإعدادات إلى 0.893، متفوقة على PROPER (Mistral-7B, 0.72)، و Llama 3.3 70B (0.839)، و Qwen2.5-Coder-32B (0.873).
  • بدون إزالة KL، عانى نموذج 7B من انحراف الأداء، حيث انخفض من خط أساس قدره 0.814 إلى 0.672.
• GSM-Symbolic:
  • في مجموعة بيانات P2 الصعبة (التي تتطلب معالجة رمزية أعمق)، ارتفع pass@4 لنموذج 7B من خط أساس قدره 0.298 إلى 0.673.
• أداء Lisp:
  • حسن هذا النهج pass@4 لـ Lisp من 0.572 إلى 0.873. ومع ذلك، كان لإزالة قيد KL مكاسب متواضعة في Lisp مقارنة بـ Prolog، مما يشير إلى أن التدريب "غير المقيد" هو الأكثر أهمية للغات المتخصصة للغاية ومنخفضة الموارد.
• Rosetta Code:
  • ضاعف نموذج 7B خط أساس Zero-shot الخاص به تقريبًا، ليصل إلى pass@4 قدره 0.46.

الأهمية والادعاءات

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

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