본 논문은 Coq와 같은 증명 보조기를 사용한 형식적 검증의 효율성을 높이기 위해, 대규모 언어 모델(LLM)을 활용한 분할 정복 방식의 새로운 증명 합성 도구인 Cobblestone을 제안합니다. Cobblestone은 LLM을 사용하여 잠재적인 증명을 생성하고, 이를 통해 문제를 더 작은 부분으로 나눕니다. 성공적으로 증명된 부분을 자동으로 식별하고, 나머지 부분에 대해 반복하여 최종적으로 정확한 증명을 생성합니다. LLM의 불확실성에도 불구하고, Cobblestone은 생성된 증명의 정확성을 보장합니다. 실험 결과, Cobblestone은 기존의 최첨단 도구들을 능가하는 성능을 보였으며, 특히 다른 LLM 기반 도구들이 증명하지 못한 많은 정리를 증명했습니다. 평균 실행 비용은 1.25달러, 실행 시간은 14.7분으로 효율적입니다. 또한, 사용자 또는 다른 도구로부터의 외부 입력을 받아 증명 구조 또는 관련 보조 정리를 활용할 수 있으며, 이 경우 최대 58%의 정리를 증명할 수 있음을 보였습니다. 이 연구는 부분적인 진행 상황과 외부 입력을 활용하여 형식적 검증 자동화의 효율성을 높일 수 있음을 보여줍니다.
