في عالم البرمجة المتطور، تقدم نماذج اللغات الضخمة (Large Language Models) وعوداً مثيرة في تحسين عمليات تطوير البرمجيات، إلا أن التحدي الكبير الذي يواجهها هو ضمان دقة الكود الذي تنتجه. غالباً ما يتم الإخفاق في هذا الصدد بسبب الأكواد المعيبة أو المولدة نتيجة لـ "هلوسة" النموذج.

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

في دراستنا الجديدة، نقدم مجموعة بيانات تحت اسم "NaturalLanguage2VerifiedCode (NL2VC)"، والتي تحتوي على 60 مشكلة خوارزمية معقدة. ونجري تقييمًا لـ 11 مجموعة مشكلة مختارة عشوائياً عبر سبعة نماذج طويلة الوزن باستخدام استراتيجيات ترويج متنوعة: ترويج بدون سياق، وترويج مع توقيع يقدم دعائم هيكلية، وترويج ذاتي الشفاء يستفيد من التغذية الراجعة التكرارية من مُحقق Dafny.

علاوة على ذلك، لمواجهة مشكلة التحقق الفارغ، حيث يُحقق النموذج متطلبات المُحقق بمواصفات تافهة، قمنا بدمج منصة uDebug لضمان التحقق الوظيفي. تُظهر نتائجنا أن الترويج بدون سياق يؤدي إلى فشل شبه شامل، بينما تسهم التوقيعات الهيكلية والشفاء الذاتي التكراري في تغيير دراماتيكي في الأداء. على وجه الخصوص، حقق نموذج Gemma 4-31B معدل نجاح في التحقق يبلغ 90.91%، بينما ارتفع نموذج GPT-OSS 120B من 0% إلى 81.82% بفضل التغذية الراجعة المبنية على التوقيع.

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