Cet article propose Cobblestone, un nouvel outil de synthèse de preuves qui exploite un modèle de langage à grande échelle (LLM) pour améliorer l'efficacité de la vérification formelle à l'aide d'assistants de preuve comme Coq. Cobblestone génère des preuves potentielles à l'aide du LLM, qui servent ensuite à diviser le problème en parties plus petites. Il identifie automatiquement les parties prouvées avec succès et itère sur les parties restantes pour produire une preuve correcte. Malgré l'incertitude du LLM, Cobblestone garantit l'exactitude des preuves générées. Les résultats expérimentaux montrent que Cobblestone surpasse les outils de pointe existants, prouvant de nombreux théorèmes que d'autres outils basés sur le LLM ne parviennent pas à prouver. Son efficacité est démontrée par un coût d'exécution moyen de 1,25 $ et un temps d'exécution de 14,7 minutes. De plus, il peut utiliser des données externes provenant d'utilisateurs ou d'autres outils pour exploiter la structure de preuve ou les lemmes associés, prouvant jusqu'à 58 % des théorèmes. Cette étude démontre le potentiel de l'exploitation des progrès partiels et des données externes pour améliorer l'efficacité de l'automatisation de la vérification formelle.
