في عالم الذكاء الاصطناعي، يظهر اتجاه جديد يحمل معه وعدًا كبيرًا لتوليد كود موثق بشكل رسمي من مواصفات دقيقة. وهذا ما يطلق عليه مصطلح 'Vericoding'. بينما تُظهِر النماذج الحديثة للإبداع في الذكاء الاصطناعي (AI) وعودًا واعدة في هذا المجال، إلا أن هنالك حاجة ملحة لمنهجية موحدة تمكننا من تقييم هذه النماذج عبر أنظمة مختلفة.

يأتي هنا دور معيار AlgoVeri، الذي تم تصميمه لتقديم تقييم شامل لتوليد الكود الموثوق في 77 خوارزمية كلاسيكية باستخدام لغات مثل دافني (Dafny) وفيروس (Verus) ولين (Lean). يتميز AlgoVeri بأنه يفرض عقوداً وظيفية متطابقة، مما يكشف عن الفجوات الحرجة في القدرات الموجودة في أنظمة التحقق.

تشير النتائج إلى أن النماذج الرائدة قد حققت نجاحاً ملحوظاً في دافني، حيث وصلت نسبة النجاح إلى 40.3% مع نموذج Gemini-3 Flash، وذلك بفضل القدرة على استخدام التجريدات عالية المستوى والأتمتة . ومع ذلك، فإن الأداء ينهار تحت قيود الذاكرة لنظام فيروس، حيث بلغت نسبة النجاح 24.7%، ونسبة 7.8% فقط مع الحاجة إلى إنشاء برهان صريح في لين.

علاوة على ذلك، يكشف التحليل الذي قمنا به عن انحراف حاد في ديناميات حساب وقت الاختبار: حيث يستفيد نموذج Gemini-3 بشكل فعّال من الإصلاحات التكرارية لتحسين الأداء، على النقيض من نموذج GPT-OSS الذي يصل إلى نقطة التشبع مبكراً. كما تُظهر دراستنا أيضًا أن تصميم اللغة له تأثير كبير على مسار تحسين النماذج، حيث يسمح دافني للنماذج بالتركيز على الدقة المنطقية، بينما تُبقي فيروس ولين النماذج محاصرة في حواجز نحوية وسمية مستمرة.

يمكنكم الاطلاع على كافة البيانات وكود التقييم في [رابط GitHub].