O artigo apresenta o Diversify2Verify, um pipeline em etapas baseado em LLM para Why3 que gera implementações diversas de arrays/listas recursivas e imperativas para aprimorar a verificabilidade automatizada. A abordagem infere contratos específicos da representação e emprega reparo de anotações guiado por verificador limitado para lidar com falhas de verificação.
- Os autores construíram um benchmark com 73 tarefas sobre inteiros, arrays e listas, resultando em 292 variantes de implementação.
- O Diversify2Verify verificou inicialmente 96 artefatos, aumentando para 154 após duas passadas de reparo.
- A verificação em nível de artefato melhorou de 32,9% para 52,7%.
- No nível de tarefa, pelo menos uma variante foi verificada para 49 das 73 tarefas, alcançando uma taxa de sucesso de 67,1%.
Esses resultados demonstram que a diversidade de implementações ajuda a encontrar artefatos favoráveis à verificação entre programas equivalentes por tarefa.