Cobblestone es un novedoso método de síntesis de pruebas para el asistente de pruebas Coq, que emplea una estrategia de "divide y vencerás" aprovechando un modelo de lenguaje a gran escala (LLM). Utiliza las pruebas parciales generadas por el LLM para descomponer el problema en subproblemas más pequeños e identifica automáticamente los subproblemas que se han demostrado correctamente. A continuación, ejecuta iterativamente la prueba en los subproblemas restantes para construir una prueba general correcta y sólida. Los experimentos en el proyecto Coq de código abierto demuestran que supera a las herramientas existentes, tanto basadas en LLM como no basadas en LLM, con un coste medio de 1,25 $ y una duración de 14,7 minutos. También acepta estructuras de prueba parciales o lemas relacionados de usuarios u otras herramientas, demostrando hasta el 58 % de los teoremas.
