تقدم الورقة Diversify2Verify، وهو خط أنابيب متعدد المراحل يعتمد على LLM لـ Why3 يولد تنفيذات متنوعة للمصفوفات/القوائم بشكل تكراري وأمرى لتعزيز إمكانية التحقق التلقائي. يستنتج النهج عقودًا محددة للتمثيل ويستخدم إصلاح التعليقات التوضيحية الموجهة من قبل المدقق ذو الحدود للتعامل مع فشل التحقق.
- قام المؤلفون ببناء مجموعة معايير تتكون من 73 مهمة على الأعداد الصحيحة والمصفوفات والقوائم، مما أنتج 292 متغيرًا للتنفيذ.
- تحقق Diversify2Verify مبدئيًا في 96 عنصرًا، وارتفع العدد إلى 154 بعد مرحلتين من الإصلاح.
- تحسن التحقق على مستوى العناصر من 32.9% إلى 52.7%.
- على مستوى المهام، تم التحقق من متغير واحد على الأقل لـ 49 من أصل 73 مهمة، محققًا معدل نجاح بنسبة 67.1%.
تُظهر هذه النتائج أن تنوع التنفيذات يساعد في العثور على عناصر مواتية للتحقق بين البرامج المكافئة للمهام.