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

• URL: http://arxiv.org/abs/2603.19329v1
• Date: Wed, 18 Mar 2026 18:42:04 GMT
• Title: Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification
• Abstract summary: Large language models (LLMs) can generate plausible code but offer limited guarantees of correctness.<n>We propose a hierarchical proof search framework for automated code verification in Lean4.<n>We train Goedel-Code-Prover-8B, a single unified policy for both decomposition and completion.
• Score: 34.98335927187393
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• LLM-as-a-Verifier: A General-Purpose Verification Framework [74.40111651545979]
  We introduce LLM-as-a-Verifier, a general-purpose verification framework.<n>It provides fine-grained feedback for agentic tasks without requiring additional training.<n>It achieves state-of-the-art performance on several benchmarks.
  arXiv  Detail & Related papers  (2026-07-06T17:59:35Z)
• Automating Formal Verification with Reinforcement Learning and Recursive Inference [0.0]
  We train open-source models in Dafny with verifiable rewards (RLVR) and verifier-guided inference-time search.<n>With a fixed base model, the full scaffold with proof reviser improves pass rate on an initial VeriCoding pilot set from 46.2% under direct repair to 69.2%.<n>We also introduce Dalek-Bench, a repository-scale Lean benchmark derived from the Rust $texttcurve25519-dalek$ verification project.
  arXiv  Detail & Related papers  (2026-05-29T06:59:28Z)
• Automating Formal Verification with Agent-Guided Tree Search [0.0]
  Formal verification offers a path to provably correct software, but writing verified code remains expensive enough that the technique is rarely used in production.<n>Recent benchmarks measure their ability to translate specifications into code and machine-checked iteration of correctness.<n>This thesis evaluates the state of such LLM-driven verified-code generation in Lean and develops search-based methods for improving performance.
  arXiv  Detail & Related papers  (2026-05-26T14:50:47Z)
• TIER: Trajectory-Invariant Execution Rewards for Multi-Step Tool Composition [62.56752617853322]
  Outcome-based rewards provide only sparse feedback, while trajectory-supervised rewards depend on annotated reference solutions.<n>We propose TIER: Trajectory-Invariant Execution Rewards, a reward framework that derives supervision directly from function schemas and runtime execution.
  arXiv  Detail & Related papers  (2026-05-16T03:47:26Z)
• Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving [8.420305724549603]
  Automated theorem proving with large language models in Lean 4 is commonly approached through either step-level tactic prediction with tree search or whole-proof generation.<n>These two paradigms represent opposite granularities for constructing supervised training data.<n>We propose segment-level supervision, a training data construction strategy that extracts locally coherent proof segments for training policy models.
  arXiv  Detail & Related papers  (2026-05-12T10:18:28Z)
• WybeCoder: Verified Imperative Code Generation [22.401681809856896]
  WybeCoder is an agentic code verification framework.<n>It enables prove-as-you-generate development where code, invariants, and proofs co-evolve.
  arXiv  Detail & Related papers  (2026-03-31T00:06:44Z)
• Verifiable Reasoning for LLM-based Generative Recommendation [106.7765000777685]
  Reasoning in Large Language Models (LLMs) has recently shown strong potential in enhancing generative recommendation.<n>We propose a novel textbftextitreason-verify-recommend paradigm, which interleaves reasoning with verification to provide reliable feedback.<n>Experiments on four real-world datasets demonstrate that VRec substantially enhances recommendation effectiveness and scalability without compromising efficiency.
  arXiv  Detail & Related papers  (2026-03-08T16:55:45Z)
• Distill and Align Decomposition for Enhanced Claim Verification [51.93960785128124]
  Complex claim verification requires decomposing sentences into verifiable subclaims.<n>We propose a reinforcement learning approach that optimises decomposition quality and verifier alignment.<n>Our framework enables smaller language models to achieve state-of-the-art claim verification.
  arXiv  Detail & Related papers  (2026-02-25T12:32:04Z)
• CVeDRL: An Efficient Code Verifier via Difficulty-aware Reinforcement Learning [57.24524263804788]
  Code verifiers play a critical role in post-verification for LLM-based code generation.<n>Existing supervised fine-tuning methods suffer from data scarcity, high failure rates, and poor inference efficiency.<n>We show that naive RL with only functionality rewards fails to generate effective unit tests for difficult branches and samples.
  arXiv  Detail & Related papers  (2026-01-30T10:33:29Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction [32.14733357890831]
  We propose AssertCoder, a novel unified framework that automatically generates high-quality SVAs.<n>AssertCoder employs a modality-sensitive preprocessing to parse heterogeneous specification formats.<n>The framework incorporates a mutation-based evaluation approach to assess assertion quality.
  arXiv  Detail & Related papers  (2025-07-14T14:43:14Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  We propose ProofAug, a procedure that equips LLMs with automation methods at various granularities.<n>Our method is validated on the miniF2F benchmark using the open-source deep-math-7b-base model and the Isabelle proof assistant.<n>We also implement a Lean 4 version of ProofAug that can improve the pass@1 performance of Kimina-Prover-seek-Distill-1.5B from 44.3% to 50.4%.
  arXiv  Detail & Related papers  (2025-01-30T12:37:06Z)
• Reasoning Through Execution: Unifying Process and Outcome Rewards for Code Generation [27.484259938667776]
  Large Language Models excel at code generation yet struggle with complex programming tasks that demand reasoning.<n>We introduce Outcome Refining Process Supervision, which unifies process and outcome supervision by leveraging executable verification.<n>Experiments across 5 models and 3 benchmarks show consistent gains, with 26.9% higher correctness and 42.2% improved code efficiency.
  arXiv  Detail & Related papers  (2024-12-19T17:59:42Z)
• Self-Evaluation Guided Beam Search for Reasoning [61.523627290397556]
  We introduce a stepwise self-evaluation mechanism to guide and calibrate the reasoning process of Large Language Model (LLM) We propose a decoding algorithm integrating the self-evaluation guidance via beam search. Our approach surpasses the corresponding Codex-backboned baselines in few-shot accuracy by $6.34%$, $9.56%$, and $5.46%$ on the GSM8K, AQuA, and StrategyQA.
  arXiv  Detail & Related papers  (2023-05-01T02:37:59Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.