Cobblestone est une nouvelle méthode de synthèse de preuves pour l'assistant de preuve Coq. Elle utilise une stratégie de division et de conquête s'appuyant sur un modèle de langage à grande échelle (LLM). Elle utilise les preuves partielles générées par le LLM pour décomposer le problème en sous-problèmes plus petits et identifie automatiquement les sous-problèmes prouvés avec succès. Elle effectue ensuite la preuve itérative sur les sous-problèmes restants pour finalement construire une preuve globale correcte et solide. Les expériences menées sur le projet open source Coq montrent qu'elle surpasse les outils existants, basés ou non sur le LLM, avec un coût moyen de 1,25 $ et une durée d'exécution de 14,7 minutes. Elle peut également accepter des structures de preuves partielles ou des lemmes associés provenant d'utilisateurs ou d'autres outils, prouvant jusqu'à 58 % des théorèmes.
