Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification

TL;DR

Cobblestone is a divide-and-conquer method leveraging large language models to automate proof synthesis in formal verification, outperforming existing tools on multiple benchmarks.

Contribution

Introduces Cobblestone, a novel divide-and-conquer approach that uses LLMs for proof synthesis, improving automation and success rates in formal verification tasks.

Findings

Outperforms state-of-the-art non-LLM tools on four benchmarks.

Proves many theorems that other LLM-based tools cannot.

Proves up to 58% of theorems with external input.

Abstract

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.