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

1. Problem Statement

Formal verification using proof assistants like Coq is highly effective for ensuring software correctness but is prohibitively expensive due to the need for significant human expertise and manual effort to write mathematical proofs.

• Limitations of Existing Tools:
  • SMT-based Hammers (e.g., CoqHammer): Can automatically prove simple goals but fail on complex theorems requiring induction or high-level planning.
  • Tactic-by-Tactic Search (e.g., Proverbot9001): Uses neural networks to predict the next step. While they leverage intermediate states, they struggle with the vast search space and often lack a high-level proof plan.
  • Whole-Proof Generation (e.g., PALM): Uses Large Language Models (LLMs) to generate an entire proof at once. While they possess high-level reasoning, they often fail because they cannot access intermediate proof states to correct errors, and they rely heavily on the LLM's ability to construct a viable plan in a single shot.
• The Gap: There is a need for a system that combines the high-level planning capabilities of LLMs with the ability to leverage intermediate states and local search, without requiring expensive fine-tuning of the model.

2. Methodology: The Cobblestone Approach

Cobblestone introduces a divide-and-conquer strategy that bridges the gap between whole-proof generation and tactic-by-tactic search. It operates as a recursive, iterative loop that decomposes complex proofs into smaller, solvable sub-proofs.

Core Workflow

1. Initial Attempt: Cobblestone first attempts to prove the goal using CoqHammer (an SMT-based tool).
2. LLM Sampling: If the hammer fails, it prompts an LLM (e.g., GPT-4) to generate whole proof candidates.
   • It uses Chain-of-Thought (CoT) prompting and varies the context (with/without relevant lemmas) to generate diverse candidates.
3. Fail-Safe Execution & Fault Localization:
   • Instead of stopping at the first error (as Coq normally does), Cobblestone uses a novel Fail-Safe Mode.
   • It recursively parses the proof structure (prefixes and subproofs defined by bullets -, --, etc.).
   • It executes the proof, replacing failing tactics with admit (a placeholder) to allow the execution to continue.
   • Result: It identifies exactly which subproofs (subgoals) are correct and which are broken, annotating them as "correct" or "in progress."
4. Recursive Decomposition:
   • Cobblestone retains the correct subproofs.
   • It recursively invokes itself on the failed subgoals (the "in progress" parts).
   • In the recursive call, it attempts to prove the specific subgoal, again trying CoqHammer first, then sampling the LLM.
5. Assembly: Once all subgoals are proven, Cobblestone assembles the valid parts from the original attempt and the recursive solutions into a single, sound proof.

Key Technical Innovations

• Fail-Safe Mode: A mechanism to execute LLM-generated proofs that contain errors. It isolates errors to the deepest level of the proof tree, preserving valid work that occurs after an error in the original script.
• No Fine-Tuning Required: Unlike tools like POETRY or Rango, Cobblestone does not require fine-tuning the LLM. It works with off-the-shelf instruction-tuned models by simply adjusting API calls.
• External Oracle Integration: The system includes "API access points" to accept external input, such as a human-provided proof structure or a list of relevant lemmas, which can be used to guide the decomposition.

3. Key Contributions

1. Cobblestone Tool: A novel, fully automated proof synthesis system that uses a divide-and-conquer approach to leverage partial successes from failing proofs.
2. Fail-Safe Mode: A new execution method for theorem provers that localizes errors within a proof script, allowing the system to salvage correct subproofs even when the overall proof fails.
3. Comprehensive Evaluation: A rigorous evaluation on four benchmarks (CoqGym, coq-wigderson, coq-bb5, PnVRocqLib), including datasets created after GPT-4's training cutoff to prevent data leakage.
4. Cost-Effectiveness Analysis: Demonstration that the approach is economically viable, with an average cost of $1.25 and 14.7 minutes per theorem.

4. Experimental Results

The authors evaluated Cobblestone against state-of-the-art non-LLM tools (CoqHammer, Proverbot9001, Tactician) and LLM-based tools (PALM, Rango, and custom baselines).

• Performance vs. Non-LLM Tools:
  • On CoqGym100, Cobblestone proved 48% of theorems, significantly outperforming CoqHammer (30%) and Proverbot9001 (17%).
  • It proved 46 theorems that all non-LLM tools combined could not.
• Performance vs. LLM Tools:
  • Cobblestone outperformed PALM (a whole-proof generator) on three of the four benchmarks, even when PALM was run 15 times to match Cobblestone's token usage.
  • It proved 8–9% more theorems than PALM on specific datasets.
  • Complementarity: Cobblestone and PALM proved largely disjoint sets of theorems. When combined, they proved significantly more than either alone.
• Ablation Studies:
  • CoqHammer Contribution: Removing CoqHammer reduced Cobblestone's success rate by nearly half (e.g., from 48% to 25% on CoqGym100), proving the synergy between neural and symbolic methods.
  • Search Strategy: The recursive divide-and-conquer approach was superior to a simple "tactic-by-tactic" search or a single-shot whole-proof attempt.
  • Temperature: Using a sampling temperature of 1.0 (diversity) improved performance over temperature 0.
• External Input: When provided with "perfect" external information (relevant lemmas or proof decomposition), Cobblestone's success rate increased to 58% on CoqGym100.

5. Significance and Conclusion

Cobblestone represents a paradigm shift in automated formal verification by treating proof synthesis as a recursive decomposition problem rather than a single-shot generation or a linear search.

• Efficiency: It maximizes the utility of LLMs by allowing them to focus on high-level planning while using the theorem prover to verify and isolate errors locally.
• Scalability: By not requiring fine-tuning, it can easily adapt to new LLMs as they are released.
• Human-in-the-Loop: The architecture naturally supports semi-automated workflows where human engineers can provide high-level hints (lemmas or structure) to guide the AI, bridging the gap between fully automated and fully manual verification.
• Economic Viability: At ~$1.25 per theorem, it offers a practical path toward scaling formal verification for larger software systems.

The paper concludes that tools can effectively leverage partial progress and external input to automate formal verification more robustly than previous methods, making high-assurance software more accessible.