يقدّم باحثون EasyProver، وهو نظام يستخدم وكلاء الذكاء الاصطناعي لإثبات العبارات أو دحضها بلغة Lean، المخصصة لكتابة براهين يمكن التحقق منها آليًا. كما يقدّمون Aegis، وهو معيار يحوّل مسائل البرمجة التنافسية إلى مهام للتحقق مرتبطة بتطبيقات مكتوبة بلغة Rust.
في تقييم الباحثين، أثبت EasyProver صحة 1,054 من أصل 2,000 عبارة اختيرت من Aegis، ضمن حد زمني يبلغ 30 دقيقة لكل عبارة. وتورد الورقة البحثية أيضًا نتائج مرتفعة على معايير راسخة لإثبات النظريات، يقول الباحثون إنها تقترب من الحد الأقصى الممكن.
لماذا يهم
بالنسبة إلى فرق البرمجيات التي تدرس تطبيق عمليات تحقق رسمية على شيفرات Rust، يوفّر Aegis مهامًا تتضمن تفاصيل مثل تحويلات الأعداد الصحيحة وسلوك الإخفاق. لكن ما إذا كان EasyProver قادرًا على التحقق من شيفراتها بكفاءة لا يزال غير معروف.
