ملخص تقني: Verus-SpecGym

بيان المشكلة

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

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

المنهجية

1. المعيار المرجعي: VERUS-SPECBENCH

قدم المؤلفون VERUS-SPECBENCH، وهو معيار مرجعي يتكون من 581 مهمة لكتابة المواصفات مستمدة من مشكلات برمجة من Codeforces. تم اختيار هذه المشكلات لاستهداف Verus، وهو إطار عمل للتحقق من الصحة لغة Rust.

• هيكل المهمة: توفر كل مهمة للوكيل وصفاً للمشكلة بلغة طبيعية، وهيكلاً رسمياً لـ Verus (يحدد أنواع المدخلات/المخرجات ودوال pre_spec و post_spec فارغة)، وحالات اختبار عينة، وتوثيقاً.
• مصادر البيانات: يعتمد المعيار على مصدرين متميزين لحالات الاختبار:
  • اختبارات Codeforces الرسمية: تُستخدم أساساً للتحقق من الاكتمال (المدخلات الصالحة والمخرجات الصحيحة).
  • "اختراقات" (Hacks) Codeforces: مدخلات عدائية كتبها متنافسون بشريون لكسر الحلول غير الصحيحة التي اجتازت الاختبارات الرسمية. هذه الاختراقات حاسمة للتحقق من السلامة (soundness) (تحديد المدخلات غير الصالحة أو المخرجات غير الصحيحة التي قد يقبلها النماذج عن طريق الخطأ).

2. البيئة: VERUS-SPECGYM

يتم التقييم في VERUS-SPECGYM، وهي بيئة وكيلة حيث تتفاعل النماذج مع Verus، وواجهة سطر أوامر bash، ونظام ملفات.

• التحسين التكراري: يقرأ الوكلاء المشكلة، ويكتبون المواصفات، ويقومون بتحسينها بشكل تكراري بناءً على التغذية الراجعة من أمر تقييم مخصص (verus_gym_specgen_check).
• المواصفات القابلة للتنفيذ: الابتكار التقني الرئيسي هو توسيع آلية exec_spec في Verus. عادة ما تكون مواصفات Verus عبارة عن محمولات منطقية (logical predicates) لمثبت النظريات ولا يمكن تشغيلها على مدخلات ملموسة. قام المؤلفون بتوسيع exec_spec (وتحديداً تقديم exec_spec_unverified!) لترجمة المواصفات المولدة إلى كود Rust قابل للتنفيذ. وهذا يسمح للنظام بتشغيل المواصفة مقابل حالات اختبار ملموسة لتحديد القبول أو الرفض بشكل حتمي.

3. إطار التقييم

يقسم الإطار "الدقة" (faithfulness) إلى أربعة مجالات من حالات الاختبار:

1. اكتمال ما قبل الشرط (Pre-completeness): يجب قبول المدخلات الصالحة بواسطة pre_spec.
2. سلامة ما قبل الشرط (Pre-soundness): يجب رفض المدخلات غير الصالحة بواسطة pre_spec.
3. اكتمال ما بعد الشرط (Post-completeness): يجب قبول أزواج (المدخل، المخرج) الصحيحة بواسطة post_spec.
4. سلامة ما بعد الشرط (Post-soundness): يجب رفض أزواج (المدخل، المخرج) غير الصحيحة بواسطة post_spec.

يستخدم المقيم استراتيجية حل ثنائية المستويات:

• التحقق الرمزي (Symbolic Check): يحاول إثبات سلوك المواصفة باستخدام مثبت SMT الخاص بـ Verus.
• الاحتياط التنفيذي (Executable Fallback): إذا كان الإثبات الرمزي غير حاسم، يتم تجميع المواصفة إلى كود Rust قابل للتنفيذ وتشغيلها على حالة الاختبار الملموسة. يضمن هذا حتى المواصفات المعقدة إمكانية تقييمها بشكل حتمي.

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

1. VERUS-SPECGYM & VERUS-SPECBENCH: أول بيئة وكيلة ومعيار مرجعي مصمم خصيصاً لتقييم الأتمتة التلقائية للمواصفات باستخدام مواصفات قابلة للتنفيذ وحالات اختبار عدائية مستمدة من "الاختراقات" (hacks).
2. مقيم المواصفات القابلة للتنفيذ: توسيع مبتكر لآلية exec_spec في Verus يتيح الاختبار الحتمي لدقة المواصفات دون الحاجة إلى مواصفات مرجعية كتبها خبراء أو الاعتماد فقط على أحكام النماذج اللغوية الكبيرة.
3. مجموعة التقييم العدائية: بناء مجموعة تقييم شاملة باستخدام اختراقات بشرية من Codeforces، مما يثبت أن هذه المدخلات العدائية تكشف عن فشل المواصفات الذي تغفله الاختبارات الرسمية.
4. التحليل التجريبي لأنماط الفشل: تحليل مفصل يظهر أن النماذج الرائدة القادرة على توليد كود صحيح غالباً ما تفشل في كتابة مواصفات دقيقة، حيث تتجمع الإخفاقات في إغفال افتراضات المدخلات، وقبول مخرجات غير صحيحة، ورفض مخرجات صالحة.

النتائج

قيم المؤلفون ستة نماذج لغوية رائدة ومفتوحة المصدر (بما في ذلك gemini-3.1pro و gpt5.3-codex و opus4.6 وعدة نماذج مفتوحة المصدر) تحت ميزانية ثابتة للحوسبة والوقت.

• فجوة الأداء: النموذج الأقوى، gemini-3.1pro، حل 77.8% من المهام. حلت النماذج الرائدة الأخرى ما بين 51.1% و 57.8%، بينما حققت النماذج مفتوحة المصدر نسبة 21.5%–25.5% فقط.
• الكود مقابل المواصفات: في مجموعة فرعية من المشكلات التي استطاع فيها gpt5.3-codex توليد كود قابل للتنفيذ وصحيح (بنسبة نجاح 81.8%)، فشل في كثير من الحالات في كتابة مواصفة دقيقة لنفس المشكلة. يشير هذا إلى أن الأتمتة التلقائية للمواصفات هي عقبة متميزة ومنفصلة عن توليد الكود.
• أهمية اختبارات السلامة: إن التقييم بناءً على اختبارات الاكتمال فقط يبالغ في تقدير الأداء بشكل كبير. أدى إضافة اختبارات السلامة (المستمدة من الاختراقات) إلى انخفاض قيمة Pass@1 لنموذج gpt5.3-codex من 77.8% إلى 58% ولنموذج gemini-3.1pro من 82% إلى 78%.
• محدودية استخدام النماذج اللغوية كحكم (LLM-as-a-Judge): عند استخدام نموذج لغوي كحكم لتقييم المواصفات، فاته 26% من الإخفاقات التي اكتشفها المقيم التنفيذي. يشير هذا إلى أن الاختبار التنفيذي يوفر إشارة أكثر موثوقية للخطأ الدقيق المتأصل في هذه المهمة.
• أنماط الفشل: كشف التحليل النوعي عن ثلاثة أنماط متكررة للفشل:
  1. إغفال افتراضات المدخلات: نقص في الوعود الهيكلية العالمية (مثل افتراض وجود حل في حين لا يوجد).
  2. قبول مخرجات غير صحيحة: الفشل في فرض قيود الأمثلية أو الصحة (مثل قبول أزواج غير أولية فيما بينها).
  3. رفض مخرجات صالحة: كتابة مواصفات معقدة أو مقيدة للغاية ترفض الإجابات الصحيحة.

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

تدعي الورقة أن الأتمتة التلقائية للمواصفات باتت في متناول الوكلاء الرائدين ولكنها لا تزال هشة، حتى في المشكلات التي يمكنهم فيها بنجاح توليد كود صحيح. يوضح العمل أن:

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

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