This paper proposes Cobblestone, a novel proof synthesis tool that leverages a large-scale language model (LLM) to improve the efficiency of formal verification using proof assistants like Coq. Cobblestone generates potential proofs using the LLM, which are then used to divide the problem into smaller parts. It automatically identifies successfully proven parts and iterates over the remaining parts to ultimately produce a correct proof. Despite the uncertainty of the LLM, Cobblestone guarantees the correctness of the generated proofs. Experimental results show that Cobblestone outperforms existing state-of-the-art tools, proving many theorems that other LLM-based tools fail to prove. Its efficiency is demonstrated by an average execution cost of $1.25 and a runtime of 14.7 minutes. Furthermore, it can utilize external input from users or other tools to leverage the proof structure or related lemmas, proving up to 58% of theorems. This study demonstrates the potential of leveraging partial progress and external input to improve the efficiency of formal verification automation.
