В статье представлен Diversify2Verify, поэтапный конвейер на основе LLM для Why3, который генерирует разнообразные рекурсивные и императивные реализации массивов/списков для улучшения автоматизируемости верификации. Подход выводит контракты, специфичные для представления, и использует ограниченную верификатором-направляемую коррекцию аннотаций для обработки неудач верификации.
- Авторы создали бенчмарк из 73 задач по целым числам, массивам и спискам, что дало 292 варианта реализации.
- Diversify2Verify изначально верифицировал 96 артефактов, после двух проходов коррекции это число увеличилось до 154.
- Уровень верификации на уровне артефакта вырос с 32,9% до 52,7%.
- На уровне задач по крайней мере один вариант был верифицирован для 49 из 73 задач, что обеспечило успешность на уровне 67,1%.
Эти результаты демонстрируют, что разнообразие реализаций помогает находить артефакты, удобные для верификации, среди программ, эквивалентных по задаче.