Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
This addresses the problem of reducing effort and expertise needed for formal verification in software development, offering a practical tool with incremental improvements over existing methods.
The paper tackles the challenge of automating formal verification in proof assistants like Coq by introducing Cobblestone, a divide-and-conquer approach that uses LLMs to generate and iteratively refine proofs. The result shows that Cobblestone outperforms state-of-the-art non-LLM tools, proves many theorems other LLM-based tools cannot, achieves up to 58% theorem proof success with external input, and operates at low cost ($1.25 per run) and time (14.7 minutes on average).
Formal verification using proof assistants, such as Coq, is an effective way of improving software quality, but requires significant effort and expertise. Machine learning can automatically synthesize proofs, but such tools are able to prove only a fraction of desired software properties. We introduce Cobblestone, a divide-and-conquer approach for proof synthesis. Cobblestone uses a large language model (LLM) to generate potential proofs, uses those proofs to break the problem into simpler parts, automatically identifies which of those parts were successfully proven, and iterates on the remaining parts to build a correct proof that is guaranteed to be sound, despite the reliance on unsound LLMs. We evaluate Cobblestone on four benchmarks of open-source Coq projects, controlling for training data leakage. Fully automatically, Cobblestone outperforms state-of-the-art non-LLM tools, and proves many theorems that other LLM-based tools cannot, and on many benchmarks, outperforms them. Each Cobblestone run costs only $1.25 and takes 14.7 minutes, on average. Cobblestone can also be used with external input, from a user or another tool, providing a proof structure or relevant lemmas. Evaluated with such an oracle, Cobblestone proves up to 58% of theorems. Overall, our research shows that tools can make use of partial progress and external input to more effectively automate formal verification.