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

Computer Science > Software Engineering arXiv:2603.19329 (cs) [Submitted on 18 Mar 2026] Title:Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification Authors:Zenan Li, Ziran Yang, Deyuan (Mike)He, Haoyu Zhao, Andrew Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, Zhendong Su, Chi Jin View a PDF of the paper titled Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification, by Zenan Li and 9 other authors View PDF HTML (experimental) 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 ex...