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

TL;DR

This paper introduces Goedel-Code-Prover, a hierarchical proof search framework for automated code verification in Lean 4, achieving significant success rates and efficiency improvements over existing methods.

Contribution

It presents a novel hierarchical proof search approach with a unified policy trained via reinforcement learning, improving automation and success rates in code verification.

Findings

Achieves 62.0% prove success rate on benchmarks, 2.6× better than baselines.

Model success improves monotonically with search iterations and sampling budget.

Outperforms larger neural provers in efficiency and success rate.

Abstract

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. Crucially, this score serves as both the training reward and the inference-time ranking criterion, ensuring strict alignment between optimization and deployment. We train Goedel-Code-Prover-8B, a single unified policy for both decomposition and completion, via supervised initialization followed by hybrid reinforcement learning, where a continuous decomposition reward drives 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$\times$ improvement over the strongest baseline, surpassing neural provers up to 84$\times$ larger. We further observe consistent inference-time scaling: success rates improve monotonically with search iterations and sampling budget, with our trained model achieving greater efficiency than frontier off-the-shelf models of comparable scale.