L'article présente Diversify2Verify, un pipeline par étapes basé sur LLM pour Why3 qui génère des implémentations récursives et impératives diverses de tableaux/listes afin d'améliorer la vérifiabilité automatique. L'approche infère des contrats spécifiques à la représentation et utilise une réparation d'annotation guidée par le vérificateur avec bornes pour gérer les échecs de vérification.
- Les auteurs ont construit un benchmark de 73 tâches sur les entiers, les tableaux et les listes, produisant 292 variantes d'implémentation.
- Diversify2Verify a initialement vérifié 96 artefacts, passant à 154 après deux passes de réparation.
- La vérification au niveau des artefacts est passée de 32,9 % à 52,7 %.
- Au niveau des tâches, au moins une variante a été vérifiée pour 49 des 73 tâches, atteignant un taux de succès de 67,1 %.
Ces résultats démontrent que la diversité des implémentations aide à trouver des artefacts favorables à la vérification parmi les programmes équivalents en termes de tâche.