براهين Lean لأكواد الذكاء الاصطناعي تنهار بعد إعادة الهيكلة في 13-27% من الحالات

متى يصمد البرهان الرسمي أمام إعادة الهيكلة؟

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

اقترح مؤلفو الدراسة منهجية أسموها RefactorProof لقياس ذلك. أخذوا 185 مسألة من معيار VERINA المعروف (الذي يفحص الكود والبراهين بلغة Lean معاً) وطبّقوا على كل مسألة خمسة أنواع من إعادة الكتابة الآلية التلقائية بالكامل: استخراج جزء من المنطق إلى دالة مستقلة، تبديل عاملي عمليات تبديلية، عكس الشروط، وغير ذلك. وبالنسبة لكل إعادة كتابة، جرى إثبات بشكل منفصل - عبر Lean - أن سلوك البرنامج لم يتغير. وفي النهاية، تم الحصول على 458 نسخة مُثبتة من الكود. بعد ذلك، طُبّق على كل نسخة البرهان الأصلي (المطابق حرفياً) وتمت ملاحظة ما إذا كان Lean لا يزال يعتبره صحيحاً.

ما الذي ثبت أنه هش، وما الذي صمد؟

البراهين المرجعية التي كتبها مؤلفو VERINA بأيديهم لـ46 مسألة، صمدت أمام إعادة الهيكلة بخسائر طفيفة تقريباً - بنسبة انكسار لا تتجاوز 4.3%. لكن هذا لا يعني أن البراهين المكتوبة يدوياً أكثر موثوقية بطبيعتها: فهذه الـ46 مسألة هي الأبسط في المعيار القياسي، بمتوسط طول للكود يبلغ سطراً واحداً، ولا تتجاوز نسبة المسائل التكرارية فيها 6.5%.

أما البراهين التي أنشأتها نماذج متخصصة في البرهنة - وهي DeepSeek-Prover-V2-7B ونسختان من Goedel-Prover-V2 (8B و32B) - فقد انكسرت بشكل أكبر بكثير: بلغت نسبة الفشل 13.3% إلى 26.8%. لكن عند مقارنة النماذج بالمرجع على مجموعة متجانسة من المسائل، تنعكس الصورة: تصمد براهين النماذج أمام إعادة الهيكلة أكثر من البراهين المرجعية - بفارق 15.6 نقطة مئوية لـDeepSeek-7B، و18.8 نقطة لـGoedel-32B، و20.3 نقطة لـGoedel-8B. والفرق ذو دلالة إحصائية في الحالات الثلاث.

لماذا تنهار بعض البراهين وتصمد أخرى؟

توصل الباحثون إلى آلية محددة للصمود. فالبراهين المرجعية تبدأ عادةً بأمر `unfold`، الذي يفكك تعريف الدالة مباشرة داخل النص. أما براهين النماذج، فهي أكثر ميلاً إلى تسمية استدعاء الدالة ومتنها صريحاً كمتساويين عبر تكتيك `rfl` (ما يُسمى "الجسر التعريفي")، ثم إثبات باقي البرهان آلياً.

وعندما يُنقل الكود إلى دالة مستقلة (استخراج المنطق)، يعمل هذا "الجسر" بشكل أكثر موثوقية بكثير: على مستوى المسائل، تصمد البراهين التي تستخدم الجسر في 6 من أصل 6 حالات، في حين لا تصمد الاستراتيجيات الأخرى إلا في 6 من أصل 31 حالة. لكن لهذه التقنية جانب معكوس: فإذا غيّرت إعادة الكتابة متن الدالة نفسه بشكل جوهري (لا مجرد موضعه)، يتوقف الجسر المرتبط بنص المتن المحدد عن العمل من الناحية النوعية - فهذه البراهين لا تصمد إلا في 0 من أصل 3 حالات، مقابل 17 من أصل 19 حالة للبراهين الأعم، غير المرتبطة بصياغة محددة.

الانكسار ليس كارثة

الاستنتاج العملي الأهم هو أن فشل برهان في المرور بعد إعادة الهيكلة لا يعني بالضرورة إعادة صياغة مكلفة. فحص الباحثون ذلك مباشرة: أخذوا البراهين المنكسرة وحاولوا إصلاحها بتعديل بسيط ودقيق واحد - إعادة تسمية معرّف واحد. ومن بين 54 حالة انكسار مناسبة في البراهين المرجعية، تم إصلاح 51 منها بهذه الطريقة؛ ومن بين 85 حالة انكسار في براهين النماذج، تم إصلاح 58 منها.

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