RefactorProof: براهين LLM تنهار بعد إعادة هيكلة الكود

عادةً ما تتحقق معايير توليد الكود القابل للتحقق من البرهان على تنفيذ واحد ثابت. أراد مؤلفو RefactorProof معرفة ما يحدث إذا أُعيدت كتابة التنفيذ مع الحفاظ على السلوك. من بين 185 مهمة في VERINA تُترجم بنجاح في بيئتهم المثبّتة، بنوا 458 نسخة معتمدة من Lean. ولم تتغير المواصفة ولا البرهان المطلوب التحقق منه ولو بايتًا واحدًا. والنتيجة: في إعادة الهيكلة البنيوية تفشل البراهين في اجتياز التحقق بأعداد كبيرة. فنسبة البراهين الناجية (task-normalized structural PSR) تبلغ 4,3% للبراهين المرجعية من VERINA، و13,3–26,8% لمدقّقات LLM المتخصصة.

كيف يعمل اختبار الهشاشة

الفكرة بسيطة وقاسية. فالبرهان الصوري مرتبط بنص برنامج محدد: الأسماء وترتيب التعريفات وبنية التعبيرات. وإذا استخرج المطوّر دالة، أو غيّر شكل الحساب، أو أعاد تسمية متغير، فلا يتغير شيء من الناحية المنطقية، لكن البرهان في Lean قد يتوقف عن البناء. وفي التطوير الفعلي تجري إعادة الهيكلة باستمرار، ولذلك فإن السؤال عمّا إذا كان البرهان سيصمد أمام التعديل سؤال عملي.

يوفّر VERINA براهين مرجعية لـ46 مهمة فقط، وكلها من القسم الأساسي. لذلك يبني المؤلفون المقارنات الرئيسية بين النموذج والمرجع على 21–25 مهمة قصيرة غير تكرارية، اختاروها بحيث يقف جميع المشاركين على أرضية واحدة. إنها عينة ضيقة، ويجب قراءة نطاق الاستنتاجات في ضوء ذلك.

الآلات هشّة، لكن البشر أكثر هشاشة

المفاجأة أن براهين النماذج جاءت أكثر صمودًا من البراهين المرجعية. ففي المهام القابلة للمقارنة، تتفوق النماذج في نسبة البراهين غير المعدّلة التي نجت بوجه عام على المواد المرجعية من VERINA. ولا تشمل فترات الثقة 95% الصفر لأيٍّ من النماذج الثلاثة.

• DeepSeek-Prover-V2-7B: +15,6 نقطة مقارنةً بالمرجع
• Goedel-Prover-V2-32B: +18,8 نقطة
• Goedel-Prover-V2-8B: +20,3 نقطة

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

العطل لا يعني أن الإصلاح مكلف

يتعلق التحفظ الرئيسي في الورقة بكلفة العطل. فالتعديلات المحددة مسبقًا لمعرّف واحد تصلح 51 من أصل 54 حالة فشل بنيوي مؤهلة في البراهين المرجعية، و58 من أصل 85 حالة فشل مؤهلة في براهين النماذج. أي أن معظم «الهشاشة» يزول بتعديل رخيص، وفي البراهين المرجعية يُصلَح تقريبًا كل شيء. أما في النماذج فالصورة أسوأ: نحو 68% مقابل 94%.

لذلك يقيس RefactorProof استقرار البرهان غير المعدّل عند إعادة الهيكلة تحديدًا. وهو لا يقيّم كلفة صيانة البرهان بعد انكساره، ويؤكد المؤلفون ذلك صراحةً.

المعطيات الرئيسية للدراسة

• المعيار: RefactorProof، مشتق من VERINA
• المهام الأصلية: 185 (تُترجم في بيئة Lean المثبّتة)
• النسخ المعتمدة: 458
• البراهين المرجعية في VERINA: 46 مهمة، القسم الأساسي فقط
• العينة القابلة للمقارنة: 21–25 مهمة قصيرة غير تكرارية
• Structural PSR للبراهين المرجعية: 4,3%
• Structural PSR للمدقّقات المتخصصة: 13,3–26,8%
• النماذج المختبَرة: DeepSeek-Prover-V2-7B وGoedel-Prover-V2-32B وGoedel-Prover-V2-8B
• الإصلاح بتعديل معرّف واحد: 51/54 في البراهين المرجعية، 58/85 في النماذج
• المنصة: NeurIPS 2026 Workshop on AI for Verifiable Coding؛ التصنيفات cs.AI وcs.LO وcs.SE

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

تتلقى الفرق التي تبني خطوط عمل من نوع «LLM يكتب الكود والبرهان، وLean يتحقق» إشارة واضحة: التحقق على تنفيذ ثابت واحد يبالغ في تقدير الموثوقية. أضيفوا إلى CI نسخًا معاد هيكلتها من البرنامج، وشغّلوا البرهان عليها. وإذا فشل البرهان، فجرّبوا أولًا الإصلاحات التلقائية الرخيصة للمعرّفات، فبحسب بيانات الورقة تعالج هذه الإصلاحات نسبة كبيرة من الحالات. وعند تقييم نماذج prover، لا تكتفوا بنسبة المهام المحلولة، بل انظروا أيضًا إلى بقاء البراهين عند تغيير الكود. وبالنسبة لمؤلفي المعايير، الاستنتاج مباشر كذلك: ينبغي قياس الاستقرار وكلفة الإصلاح معًا. والمقياس الثاني غير موجود بعد في RefactorProof.