Goedel-Code-Prover：面向开放状态的最新代码验证的分层证明搜索
Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification
AI总结：
本文提出Goedel-Code-Prover框架，通过分层证明搜索提升Lean4中代码验证的自动化水平，实现62%的成功率，优于现有基线方法。
摘要：
大型语言模型（LLMs）可以生成合理代码，但其正确性保证有限。形式验证需要构建机器可检查的证明，这一任务仍超出当前自动化能力。我们提出了一种分层证明搜索框架，用于Lean4中的自动化代码验证，将复杂验证目标分解为结构更简单的子目标后再尝试战术层面的证明。核心是结合构造性证明与结构性有效性原则的分解评分，该评分同时作为训练奖励和推理时间排名标准，确保优化与部署的一致性。我们通过监督初始化后接混合强化学习训练了Goedel-Code-Prover-8B，一个统一的分解与完成策略。在三个基于Lean的代码验证基准测试中，包含427个任务，我们的8B参数模型实现了62.0%的证明成功率，比最强基线提高了2.6倍，超越神经证明器84倍。我们还观察到一致的推理时间扩展：成功率随搜索迭代次数和采样预算单调增加，训练模型在同等规模下更高效。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
