«فيرو» يضع وكلاء البرمجة أمام اختبار المستودع الكامل لا الدالة المنفردة

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

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

المقياس لا يكتفي بالحل

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

يتكون المقياس من 43 حالة متعددة الوحدات، مأخوذة من مستودعات واقعية تشمل Python وDafny وVerus وCoq. وتمتد الحالات بين بروتوكولات التشفير والأنظمة الموزعة. كل حالة هي مستودع Lean 4 متعدد الوحدات، وفيه واجهات برمجة محددة مسبقاً، ومواصفات رسمية انتقاها الباحثون، وتنفيذات مرجعية. ويتيح ذلك نمطي تقييم: برهاناً فقط، أو شيفرة وبرهاناً معاً.

حتى المرجع يحتاج إلى تدقيق

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

النتيجة ترسم حد القدرة الحالية

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

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