Source-linked AI summary
Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification
Zenan Li, Ziran Yang, Deyuan He, Haoyu Zhao, Andrew Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, Zhendong Su, Chi Jin
TL;DR
LLMs can generate plausible code without certifying correctness, motivating automated synthesis of machine-checkable proofs for formal specifications. The paper proposes hierarchical proof search in Lean 4 with a shared decomposition score and unified policy for decomposition and completion. Across three benchmarks, the 8B-parameter model achieves 62.0% prove success and improves with larger search budgets, while the reported evaluation has important compute and experimental-scope limitations.
Problem
LLM-generated code can appear correct while testing cannot certify the absence of subtle errors or specification mismatches, leaving machine-checkable proof synthesis insufficiently automated.
Method
The framework recursively decomposes Lean verification goals into simpler lemmas, ranks decompositions with a score combining constructive justification and structural simplicity, and iteratively proves leaves with a unified policy.
Results
62.0% overall prove success was achieved across 427 tasks, representing a 2.6× improvement over the strongest baseline under the reported inference settings.
Takeaways & Limitations
Hierarchical search shows consistent inference-time scaling, with success improving monotonically as search iterations and sampling budget increase.
Takeaways & Limitations
The evaluation is not compute-matched to parallel single-pass baselines, and one RL run prevents across-seed variance and significance estimates.
Abstract
from arXiv · showhide
Large language models (LLMs) can generate plausible code but offer limited guarantees of correctness. Formally verifying that implementations satisfy specifications requires constructing machine-checkable proofs, a task that remains beyond current automation. We propose a hierarchical proof search framework for automated code verification in Lean~4 that decomposes complex verification goals into structurally simpler subgoals before attempting tactic-level proving. Central to our approach is a principled decomposition score that combines constructive justification with structural effectiveness. The same score serves as both the training reward and the inference-time ranking criterion, aligning optimization and deployment. We train Goedel Code Prover, a single unified policy for both decomposition and completion, through supervised initialization followed by hybrid reinforcement learning, where a continuous decomposition reward supports planning exploration while supervised replay stabilizes proof generation. On three Lean-based code verification benchmarks comprising 427 tasks, our 8B-parameter model achieves a 62.0% prove success rate, a 2.6 improvement over the strongest baseline under the reported inference settings. We further observe consistent inference-time scaling: success rates improve monotonically with search iterations and sampling budget, while whole-proof baselines plateau within the evaluated budgets.
1 Introduction
The paper frames code verification as a gap between plausible LLM-generated code and machine-checked correctness, then proposes hierarchical proof search that decomposes goals before tactic proving. A unified 8B policy uses a shared decomposition score for training and inference, achieving strong results across three Lean 4 benchmarks.
- Motivation: Formal verification addresses the limits of testing by constructing machine-checked proofs that implementations satisfy formal specifications.Testing cannot certify the absence of subtle logical errors, boundary-case violations, or specification mismatches.
- Motivation: Code-verification proofs remain labor-intensive because they require reasoning about program-specific operations, invariants, and auxiliary assertions.The paper identifies filtering, membership, and inductive reasoning as examples of proof work not suggested directly by specifications.
- Challenges: Code verification faces ungrounded decomposition and compound domain shift, including proliferating program concepts and program-specific tactic distributions.These mismatches make mathematical decompose-and-prove methods difficult to transfer directly to program verification.
- Approach: The proposed framework recursively decomposes verification goals into lemmas and then proves the resulting subgoals iteratively.A single unified policy performs both lemma decomposition and lemma completion.
- Approach: The decomposition score combines constructive justification with structural simplicity and serves as both the training reward and inference-time ranking criterion.Structural ranking uses operator-footprint reduction, while hybrid reinforcement learning refines decomposition and supervised replay stabilizes completion.
- Results: 62.0% overall prove success was achieved across 427 tasks, with success rates of 68.8%, 54.0%, and 62.3% on Verina, Clever, and AlgoVeri.The 8B-parameter model achieved a 2.6× improvement over the strongest baseline under the reported inference settings, with success improving as search iterations and sampling budget increased.
- Results: The framework is presented as outperforming reported frontier-model and neural-prover baselines under their respective inference settings.The contribution summary also emphasizes the unified policy, shared score, and hybrid training pipeline.
2 Lean-based Code Verification
Lean-based code verification treats a program, precondition, and postcondition as a formal verification task whose goal is a machine-checkable proof term. The paper focuses on synthesizing that proof through interactive tactic generation while assuming the specification is already formalized.
- Task formulation: The verification input consists of a Lean program C, precondition P, and postcondition Q expressed as Lean predicates.The objective is to establish a Hoare-style relationship between inputs satisfying P and outputs satisfying Q.
- Task formulation: The proof objective is to construct a machine-checkable proof term τ that Lean’s kernel accepts as a valid derivation of the verification goal.This formalizes correctness as a kernel-checked derivation rather than an informal claim about program behavior.
- Scope and assumptions: The paper assumes that the program and its associated predicates are already formalized in Lean, leaving translation from informal specifications out of scope.Proof synthesis may still require quantifier elimination, induction, invariant generation, and auxiliary assertions.
- Proof interaction: LLM-driven synthesis proceeds through interactive tactic generation, where Lean checks each command, updates the proof state, and produces new subgoals.The loop continues until all goals are discharged or the attempt is abandoned.
- Verification platform: Lean 4 is used because explicit goal states and fine-grained compiler diagnostics support iterative LLM-driven proof search.The paper also highlights Lean’s small trusted kernel and rich library ecosystem as workflow advantages.
3 Hierarchical Verification Framework
The framework scores and searches lemma decompositions before tactic-level proof generation, combining constructive validity checks with structural simplicity. A unified policy is trained and deployed across sequential decomposition and completion stages.
- 3.1 Score for Lemma Decomposition: The decomposition score combines proof reconstruction, quickcheck validation, and structural reduction to rank candidate lemma decompositions.Constructive justification ensures proposed lemmas entail the parent theorem, while quickcheck rejects lemmas with counterexamples and structural metrics reward simpler subgoals.
- 3.1 Score for Lemma Decomposition: Operator footprint measures structural difficulty by counting logical and program operators in a Lean abstract syntax tree.In the running example, the original goal has d(G) = 18, while two sub-lemmas have footprints 7 and 8.
- 3.1 Score for Lemma Decomposition: The final score S multiplies structural reduction by validity and is used identically as the training reward and inference-time ranking criterion.Diagnostic plots may instead show an unnormalized residual-difficulty quantity, where lower values indicate simpler decompositions.
- 3.2 Unified Policy Learning and Inference: The same autoregressive policy is initialized with supervised decomposition and completion trajectories, then refined through hybrid reinforcement learning.The method uses a continuous structural score for decomposition exploration and supervised replay to stabilize completion under sparse proof-acceptance signals.
- 3.2.2 Inference Pipeline: Inference first decomposes goals until its budget is exhausted, then repeatedly generates and compiler-checks proofs for remaining leaf lemmas.Failed completion attempts receive Lean diagnostics for iterative revision, while invalid decompositions are discarded after proof reconstruction or quickcheck failure.
4 Experiments
Experiments evaluate the framework on three Lean 4 code-verification benchmarks using soundness-controlled metrics, component ablations, failure analyses, and inference-time scaling studies. The framework achieves strong cross-benchmark performance, while hierarchical search, trained components, and additional search budget contribute to results.
- Evaluation setup: The evaluation covers Verina, Clever, and AlgoVeri, with 427 tasks and comparisons against frontier reasoning models and neural provers.The model is trained from a Qwen-3-8B backbone with supervised fine-tuning and hybrid reinforcement learning; evaluation tasks are decontaminated from training data.
- Evaluation setup: Only complete Lean-verified proofs count as successful, while unsound bypasses such as Lean.ofReduceBool and Lean.trustCompiler are rejected.The reported metric is the fraction of problems solved within the inference budget.
- Proof complexity: Verified problems average 8–17 auxiliary lemmas and 130–167 proof-code lines, with maximum proof lengths of 680, 559, and 534 lines across the benchmarks.These statistics indicate that the evaluation includes substantially structured proofs rather than only short proof scripts.
- Inference-time scaling: Prove success rises with completion iterations and pass@k, while baseline pass@k curves plateau rapidly within the evaluated budgets.The persistent pass@1-to-pass@32 gap indicates remaining benefit from parallel search, whereas brute-force sampling without hierarchical decomposition shows diminishing returns.
- Failure analysis: Quickcheck rejects 31.8%–46.4% of runs, while proof reconstruction rejects 44.9%–59.4% of decomposition iterations.These rates use different denominators and represent complementary decomposition failure modes.
- Inference-time scaling: Lower unnormalized decomposition scores predict higher prove rates on Verina, achieving AUROC 0.903.The score’s raw form represents residual difficulty, while the normalized score is used for higher-is-better ranking during training and inference.
5 Related work
Prior theorem-proving advances do not transfer directly to Lean 4 code verification because code verification faces concept proliferation and tactic distribution shift.
- Mathematical theorem-proving advances do not transfer directly to code verification because programs introduce many domain-specific concepts and require different tactics.Code verification involves fresh computational structures and specialized automation over discrete and recursive domains.
6 Conclusion
The paper presents hierarchical proof search for Lean 4 code verification, using one decomposition score for both training and inference. Across three benchmarks, the 8B model achieves strong performance, while the authors identify important evaluation, accounting, and scope limitations.
- Conclusion: 62.0% overall prove success rate is achieved across three benchmarks, representing a 2.6× improvement over the strongest baseline under the reported inference settings.The evaluation is not compute-matched to parallel single-pass baselines.
- Limitations: The evaluation lacks across-seed variance, comparable token and cost accounting, and per-task cross-system AlgoVeri outcomes.The authors also note scope boundaries involving pre-formalized programs, syntactic operator counting, and single-procedure reasoning.
- Related work: The work relates its approach to hierarchical proof search, continuous decomposition scoring, and hybrid reinforcement learning for Lean 4 code verification.The related-work discussion contrasts this setting with mathematical theorem proving and symbolic program synthesis.
C Verification Paradigms and Why Lean
Lean provides a small trusted kernel and transparent interactive proof states for LLM-driven verification, while code verification remains difficult because decomposition, concepts, and tactics differ from mathematical proving.
- Verification paradigms: SMT-based verifiers such as Dafny and Verus discharge verification conditions through external automated solvers.This mediates much of the reasoning through solver components.
- Why Lean: Lean uses a small trusted kernel as its verification authority and exposes explicit goals, hypotheses, and diagnostics during proof construction.This supports iterative tactic execution and debugging by an LLM agent.
- Cross-system comparison: 62.3% success is reported on AlgoVeri, compared with published Gemini-3-Flash rates of 40.3% for Dafny, 24.7% for Verus, and 7.8% for Lean on aligned-contract tasks.The comparison uses 77 aligned-contract tasks.
- Challenges: Code verification is harder than mathematical theorem proving because it combines ungrounded decomposition, concept proliferation, and tactic distribution shift.These challenges make the search space especially sensitive to slight decomposition errors.
E Complete Proof for the Running Example
The running example is proved through a complete machine-checked Lean proof that decomposes the specification into auxiliary lemmas about filtering, counts, uniqueness, and recursive scanning.
- Proof structure: The complete FindSingleNumber proof contains six auxiliary lemmas and more than 130 lines of proof code.The lemmas cover list filtering, element counting, uniqueness, and the recursive scanner.
- Implementation: The implementation recursively scans remaining elements and returns the first element whose filtered occurrence list has length one.The helper functions define filtering and the recursive search used by the verified implementation.
- Auxiliary lemmas: The proof establishes that filtering an element is equivalent to counting its occurrences, then derives existence and uniqueness of the element counted once.These intermediate results support the characterization of the algorithm’s returned value.
- Auxiliary lemmas: The recursive-scanner lemma shows that the selected element has filtered-list length one, while subsequent lemmas characterize the result and exclude other unique elements.The final theorem combines these results with the precondition and postcondition.
- Training procedure: The hybrid training algorithm jointly optimizes decomposition with GRPO and completion with supervised replay while collecting newly decomposed lemmas online.Its reward multiplies constructive verification by a decomposition-quality term.
G Implementation Details
The implementation combines custom Lean tactics, curated training trajectories, supervised fine-tuning, hybrid reinforcement learning, and hierarchical inference. Prompt templates separate decomposition from completion, while off-the-shelf instantiation tests the framework beyond its training setup.
- Scoring and verification: Custom operatorcount and quickcheck tactics verify structural complexity and search for counterexamples during decomposition scoring.operatorcount counts logical and program operators; quickcheck evaluates universally quantified lemmas by randomized native execution.
- Inference: Hierarchical inference repeatedly decomposes the largest-footprint open goal, verifies candidate lemmas, and updates the open-goal set under a 32-goal limit.The decomposition stage runs for up to 128 iterations, with failed reconstruction or quickcheck candidates discarded.
- Data and training: Training data combines 5K automatically formalized and filtered programming problems with constructively justified decomposition and kernel-accepted completion trajectories.Exact-match filtering removes evaluation overlaps, while trajectory filtering retains positive structural-reduction decompositions and accepted proofs.
- Data and training: Supervised fine-tuning on decomposition and completion trajectories is followed by GRPO reinforcement learning with supervised replay to stabilize proof completion.The implementation uses three supervised epochs and 100 reinforcement-learning steps across 16 GPUs.
- Prompting and deployment: Decomposition prompts produce reasoning traces, helper lemmas, and a main proof, whereas completion prompts request SEARCH/REPLACE edits to proof bodies.Inference uses up to 128 completion iterations per lemma and a two-phase strategy for tactic proving and compilation-error repair.
- Off-the-shelf instantiation: GPT-OSS-120B improves from 20.1% whole-proof generation to 44.9% with hierarchical search when used for both stages.This supports a structural benefit from decomposition beyond the frontier models used for data collection, without constituting a frontier-free training run.
H.2 Training–Evaluation Decontamination Audits
The decontamination audits test both exact contiguous overlap and embedding similarity between evaluation and retained training implementations. They find no substantial shared problem content across the benchmarks, with only two low-level nearest-neighbor flags.
- Audit design: The audit compares each benchmark implementation against all 4,277 retained training implementations after stripping boilerplate.This supplements title-and-description exact matching with an ExactSubstr-style contiguous-substring check.
- Substring audit: At 50 characters, Clever and AlgoVeri matches are generic Lean fragments; no benchmark task matches at 100 or 200 characters.The reported matches therefore do not indicate shared substantive problem content at the longer thresholds.
- Embedding audit: Embedding screening flags 2/427 tasks, or 0.47%, both from Verina, as nearest training neighbors above cosine similarity 0.95.The flagged tasks are verina advanced 42/maxProfit and verina advanced 18/isArmstrong.
H.3 Decomposition Score Beyond the Evaluation Benchmarks
Beyond the evaluation benchmarks, the decomposition score is informative mainly for Hoare-style program-correctness statements, while its operator-footprint reduction is not a general-purpose measure of mathematical decomposition. Additional inference compute improves the framework, whereas whole-proof baselines plateau.
- Score scope: Nine of 14 Hoare-style cases have positive reduction ratios, while abstract type-safety, structural, categorical, and pure-mathematics cases have zero.This behavior matches the score’s intended focus on isolating simpler program sub-properties from operator-heavy postconditions.
- Score scope: Operator-footprint reduction is therefore informative primarily for Hoare-style program-correctness statements, not general mathematical decomposition quality.The evidence delineates the metric’s intended setting rather than establishing broad applicability across theorem types.
- Inference scaling: The residual operator-footprint ratio decreases steadily with additional iterations, indicating increasingly effective goal simplification under larger search budgets.Lower residual ratios correspond to more aggressive simplification and higher reduction ratios.
- Inference scaling: Whole-proof baseline curves plateau before k=1024 on all three benchmarks, while the hierarchical framework continues improving with additional compute.The comparison contrasts structured search with independently sampled whole-proof attempts.
H.8 Decomposition Score Correlation on Training Data
On training data, lower unnormalized decomposition scores remain associated with higher prove rates, extending the score–provability relationship beyond Verina. The score also decreases across all three benchmarks after training, with lower values corresponding to simpler decompositions and higher normalized scores.
- Training-data correlation: Lower raw decomposition scores are associated with higher prove rates on the training distribution.This in-distribution association is consistent with the relationship observed on Verina but does not establish out-of-distribution generalization.
- Training-data correlation: The unnormalized decomposition score predicts downstream provability on Verina with AUROC = 0.903.The training-data analysis tests whether this association is unique to the evaluation set.
- Score distributions: Mean raw scores fall from 282 to 185 on Verina, 437 to 329 on Clever, and 271 to 196 on AlgoVeri.Lower raw scores correspond to structurally simpler decompositions and higher normalized S.
- Score distributions: Before and after training, the score distributions are compared across benchmarks, with lower values designated as better.The figures present unnormalized decomposition-score distributions before and after training.