Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification

1. Problem Statement

The paper addresses the challenge of automated formal code verification using Large Language Models (LLMs). While LLMs excel at code generation, they lack guarantees of correctness. Formal verification (using tools like Lean 4) requires constructing machine-checkable proofs, a task that current automation struggles with due to three specific gaps between mathematical theorem proving and code verification:

• Ungrounded Decomposition: Unlike mathematics, where LLMs learn proof strategies from vast text corpora (textbooks, papers), there is no comparable corpus for program correctness reasoning. Consequently, LLMs often propose subgoals that are semantically invalid or no simpler than the original goal.
• Concept Proliferation: In math, proofs rely on shared libraries (e.g., Mathlib). In code verification, every new program introduces unique functions, control flows, and data structures, requiring the discovery of properties from scratch without pre-existing lemmas.
• Tactic Distribution Shift: Code verification requires discrete, recursive reasoning (e.g., list induction, bit-vector logic) and specialized tactics (e.g., grind, native_decide), whereas mathematical proofs rely heavily on algebraic tactics. Models trained on math often fail to invoke the correct tools for code.

The core difficulty is a compound search problem: a single incorrect decomposition can render the entire proof intractable, and the search space is fragile.

2. Methodology: Hierarchical Proof Search Framework

The authors propose a framework that decomposes complex verification goals into structurally simpler sub-lemmas before attempting tactic-level proving. The system is built around a unified policy ($\pi$) that handles both decomposition (planning) and completion (proving).

A. The Decomposition Score ($S$)

A central innovation is a principled decomposition score that serves as both the training reward and the inference-time ranking criterion. This score $S$ combines two axes:

1. Constructive Justification (Validity):
   • Proof Reconstruction: The proposed lemmas must logically entail the parent theorem. The LLM must generate a proof term $\pi_{parent}$ that verifies $(L_1 \land \dots \land L_k) \implies G$.
   • Quickcheck Filter: Automated counterexample search (via quickcheck) is applied to each lemma. If a counterexample is found, the decomposition is discarded. This ensures subgoals are empirically consistent.
2. Decomposition Effectiveness (Simplicity):
   • Measured by the Operator Footprint ($d(\cdot)$), which counts the total number of logical and domain-specific operators in the Abstract Syntax Tree (AST) of a goal.
   • The score calculates the reduction ratio: $r = \max(1 - \frac{\bar{d}(L)}{d(G)}, 0)$, where $\bar{d}$ is a smoothed maximum of the subgoal footprints (using LogSumExp to be sensitive to partial progress).

The final score is $S = v \cdot r$, where $v$ is the binary validity gate.

B. Training Pipeline: Hybrid Reinforcement Learning

The authors train Goedel-Code-Prover-8B (based on a Qwen-3-8B backbone) using a two-stage process to resolve the "reward mismatch" between dense decomposition signals and sparse binary proof signals:

1. Supervised Fine-Tuning (SFT): The model is initialized using 281K decomposition pairs and 151K completion pairs generated by frontier models (GPT-5.2, Gemini-3-Flash).
2. Hybrid Reinforcement Learning (RL):
   • Decomposition: Optimized via Group Relative Policy Optimization (GRPO) using the continuous decomposition score $S$ as the reward. This drives exploration and curriculum expansion.
   • Completion: Stabilized via Supervised Replay. The model attempts to prove lemmas; if it fails, a frontier model provides a solution. The model is then trained on these high-quality trajectories to prevent the completion capability from stagnating due to sparse binary rewards.

C. Inference Pipeline

Inference operates in two sequential stages:

1. Recursive Lemma Decomposition: The policy iteratively selects the goal with the highest operator footprint, decomposes it, and verifies the result via proof reconstruction and quickcheck. This continues until a budget is exhausted or all goals are leaf lemmas.
2. Iterative Lemma Completion: The policy attempts to prove the remaining leaf lemmas using iterative tactic generation, refining based on Lean compiler feedback.

3. Key Contributions

1. Hierarchical Framework: A novel approach for Lean 4 code verification that separates goal decomposition from tactic generation, addressing the specific challenges of code verification (concept proliferation, tactic shift).
2. Principled Decomposition Score: A unified metric combining logical validity (proof reconstruction + quickcheck) and structural simplicity (operator footprint reduction), used consistently for both training rewards and inference search.
3. Hybrid RL Pipeline: A training strategy that jointly optimizes decomposition (via continuous rewards) and completion (via supervised replay), enabling a single unified policy to handle both tasks effectively.
4. State-of-the-Art Performance: Demonstrating that a purpose-trained 8B model can outperform significantly larger models (up to 84x larger) and frontier reasoning models.

4. Experimental Results

The framework was evaluated on three benchmarks comprising 427 tasks: Verina (189 tasks), Clever (161 tasks), and AlgoVeri (77 tasks).

• Overall Success Rate: The Goedel-Code-Prover-8B achieved a 62.0% overall prove success rate.
  • Verina: 68.8%
  • Clever: 54.0%
  • AlgoVeri: 62.3%
• Comparison:
  • 2.6x improvement over the strongest baseline (BFS-Prover-V2-32B, which scored ~23.8%).
  • Surpassed frontier models like GPT-5.3-Codex and DeepSeek-Prover-V2-671B (671B parameters), despite being 84x smaller.
• Inference-Time Scaling: Success rates improved monotonically with increased search iterations and parallel sampling budgets ($pass@k$), indicating the model has not yet saturated its scaling potential.
• Proof Complexity: Verified proofs averaged 8–17 decomposed lemmas and over 130 lines of code, with the most complex proofs exceeding 680 lines.
• Ablation Studies:
  • Removing hierarchical decomposition dropped success rates to ~26%.
  • Joint training of decomposition and completion yielded synergistic gains, outperforming configurations where only one component was trained.
  • The decomposition score showed a strong correlation with success (AUROC = 0.903), validating its use as a search guide.

5. Significance

This work bridges the gap between "code that appears to work" and "code that is provably correct." It demonstrates that hierarchical decomposition is the critical missing link for applying LLMs to code verification, a domain where direct tactic generation fails. By introducing a domain-specific scoring mechanism and a hybrid training pipeline, the authors show that smaller, specialized models can outperform massive, general-purpose provers in complex verification tasks. This approach offers a scalable path toward automating safety-critical software verification, moving beyond the limitations of testing and SMT-based auto-active verifiers.