«فيرو»: معيار جديد يكشف محدودية وكلاء الذكاء الاصطناعي في بناء برمجيات مثبتة رياضياً عبر المستودعات المعقدة

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

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

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

شملت التجارب تقييم تكوينات متقدمة من وكلاء البرمجة الرائدين بعد تزويدهم بالوصول المباشر إلى حزمة أدوات لغة «لين». وأظهرت النتائج أن أقوى الوكلاء أداءً تمكن من حل 27 حالة فقط من أصل 43 حالة يتضمنها المعيار، في حين عجزت جميع النماذج عن إغلاق أو إثبات أي من المواصفات الرياضية في المستودعات الأكثر تعقيداً وصعوبة. تعكس هذه النتائج الفجوة الكبيرة بين قدرات الوكلاء الحالية ومتطلبات تطوير البرمجيات المؤكدة رياضياً في البيئات الواقعية متعددة الوحدات.

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