التجميع في Lean يبالغ في تقدير دقة الصياغة الشكلية: فجوة تصل إلى 29.5 نقطة مئوية

يقبل Lean أي تصريح (declaration) ما دام سليمًا من حيث الأنواع، أما ما يعنيه هذا التصريح من حيث المعنى فلا يتحقق منه المُجمِّع. قاس مؤلفو دراسة «Beyond Compilation» مدى مبالغة مقياس «تم التجميع بنجاح» في تقدير جودة الصياغة الشكلية التلقائية (autoformalization)، أي ترجمة العبارات الرياضية من اللغة الطبيعية إلى Lean. وأبرز رقم في الدراسة أن الوكيل المزوّد بأدوات ينجح تجميع 87.2% من 227 عبارة جامعية، بينما لا يمرّ عبر المعيار الدلالي سوى 57.7%. والفارق البالغ 29.5 نقطة مئوية يمثل شيفرة Lean تبدو سليمة تمامًا، لكنها تصوغ شيئًا مختلفًا عمّا طُلب.

كيف يعمل الفحص

لا يتوافر لمعظم المهام ترجمة مرجعية إلى Lean، ولذلك لا يمكن المقارنة بإجابة «ذهبية». يعتمد المؤلفون معيارًا مركّبًا: تُقبل العبارة إذا جُمِّعت في Lean، وإذا اعتبرها نموذجا LLM من عائلتين مختلفتين، بصورة مستقلة، ترجمة صحيحة للصياغة الأصلية.

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

النتائج الرئيسية للأنظمة الثمانية:

• الفجوة بين نسبة العبارات المجمَّعة ونسبة العبارات المقبولة تتراوح بين 1.3 و29.5 نقطة مئوية؛
• الوكيل المزوّد بأدوات: 87.2% تجميع مقابل 57.7% عبارات مقبولة؛
• راجع البشر جميع حالات رفض الوكيل: وتبيّن أن 23.8 نقطة مئوية من أصل 29.5 هي أخطاء ترجمة حقيقية؛
• في ستة من أصل سبعة أنظمة تعمل بمحاولة واحدة (one-shot)، تمثّل أخطاء الترجمة الحقيقية 78–100% من الفجوة، وفق مراجعة من مرحلتين أجراها Claude Opus 5.5 مع Lean وGPT-6.1 Sol، وجرت مطابقتها مع التقييم البشري.

حين يخطئ الحَكَم

أكثر النتائج مفاجأة تتعلق بالنماذج الأحدث. كان GPT-5.2 أحد الحَكَمَين، وطلب المؤلفون منه تقييم ترجمات نموذجين أحدث منه، هما GPT-6 Astra وClaude Opus 5.5. قبل الحَكَم 83% من العبارات لدى كل منهما، في حين أن نتيجة GPT-5.2 نفسه بمحاولة واحدة (one-shot) هي 21%.

ثم حلّلت المراجعة ذات المرحلتين حالات الرفض لدى هذين النموذجين. ومن بين 54 عبارة مرفوضة، تبيّن أن 4 فقط هي أخطاء ترجمة حقيقية، أي 7%. أما بقية حالات الرفض فهي أخطاء من الحَكَم. وهذا ينسجم مع منطق بسيط: كلما قلّت أخطاء النظام، قلّت الأخطاء الحقيقية بين حالات رفضه، وبرز أكثر «ضجيج» الحَكَم نفسه. فالحَكَم الذي لا يتطور مع النماذج التي يقيّمها يصبح عنق زجاجة في المعيار.

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

ماذا أظهر استبعاد الأدوات (ablation)

شغّل المؤلفون الوكيل ضمن تجربة استبعاد (ablation) بتصميم 2^3، أي تفعيل ثلاث أدوات وتعطيلها في جميع التركيبات الثماني. ويأتي الجزء الأكبر من تحسّن التجميع من التغذية الراجعة من Lean: يرى الوكيل الأخطاء ويصحّح الشيفرة. لكن ما يقارب نصف هذا التحسن لا يجتاز المعيار الدلالي. فالوكيل يتعلم كيف يحقق التجميع، لا كيف يحافظ على دقة المعنى. والأثر المعتاد: لإزالة الخطأ يسقط شرط من العبارة، أو يُضعَف المُكمِّم (quantifier)، أو تُستبدل البنية.

ما الذي ينبغي تغييره في الممارسة

إذا كنت تبني خط معالجة (pipeline) للصياغة الشكلية التلقائية أو تدرّب نموذجًا على إشارة من Lean، فإن اعتماد التجميع مكافأةً وحيدة يعطي تقديرًا متحيزًا ويدفع نحو صياغات متدهورة. ولا بد من طبقة دلالية واحدة على الأقل: حَكَمان من عائلات مختلفة، ومراجعة بشرية انتقائية لحالات الرفض.

عند العمل مع نماذج جديدة، يجدر التحقق مما إذا كان الحَكَم متأخرًا عن النظام الذي يقيّمه. وإذا تبيّن أن معظم حالات الرفض أخطاء حَكَم لا أخطاء ترجمة، فقد حان وقت مراجعة المقياس. الشيفرة والبيانات منشورتان على GitHub (grenadeComing/beyond-compilation)، ولذلك يمكن إعادة إنتاج المنهج على عبارات خاصة بك.