Makalah ini memperkenalkan Diversify2Verify, sebuah pipa berbasis LLM bertahap untuk Why3 yang menghasilkan implementasi array/list rekursif dan imperatif yang beragam untuk meningkatkan kemampuan verifikasi otomatis. Pendekatan ini menyimpulkan kontrak spesifik representasi dan menggunakan perbaikan anotasi terarah verifier berbatas untuk menangani kegagalan verifikasi.
- Para penulis membangun benchmark dari 73 tugas atas bilangan bulat, array, dan list, menghasilkan 292 varian implementasi.
- Diversify2Verify awalnya memverifikasi 96 artefak, meningkat menjadi 154 setelah dua tahap perbaikan.
- Verifikasi tingkat artefak meningkat dari 32,9% menjadi 52,7%.
- Pada tingkat tugas, setidaknya satu varian terverifikasi untuk 49 dari 73 tugas, mencapai tingkat keberhasilan 67,1%.
Hasil-hasil ini menunjukkan bahwa keberagaman implementasi membantu menemukan artefak yang ramah verifikasi di antara program-program setara tugas.