Process-Verified Reinforcement Learning for Theorem Proving via Lean
作者: Minsu Kim, Se-Young Yun
分类: cs.AI
发布日期: 2026-06-18
💡 一句话要点
提出基于Lean的过程验证强化学习以提升定理证明效率
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)
关键词: 强化学习 定理证明 符号验证 Lean证明助手 过程级奖励 深度学习 自动推理
📋 核心要点
- 现有的强化学习方法通常依赖单一的二元验证信号，缺乏细粒度的反馈，限制了其在定理证明中的应用。
- 本文提出利用Lean证明助手作为符号过程Oracle，提供结果级和策略级的验证反馈，从而改善训练过程中的奖励信号。
- 实验结果显示，策略级监督在MiniF2F和ProofNet等基准测试中表现优于仅依赖结果的基线，验证了方法的有效性。
📝 摘要（中文）
本文探讨了在强化学习中利用可验证奖励的局限性，提出了利用Lean证明助手作为符号过程Oracle的方法。通过解析证明尝试为策略序列，Lean提供了密集且可靠的反馈信号，结合GRPO风格的强化学习目标，实验结果表明，策略级监督在多个基准测试中优于仅依赖结果的基线方法。这项研究不仅展示了符号证明助手在训练中的潜力，还为结合语言模型的可扩展性与符号验证的可靠性开辟了新路径。
🔬 方法详解
问题定义：本文旨在解决现有强化学习方法在定理证明中缺乏细粒度、可靠的反馈信号的问题，导致训练效果不佳。
核心思路：通过将Lean证明助手作为符号过程Oracle，提供密集且基于验证的反馈信号，结合GRPO风格的强化学习目标，平衡结果和过程级的优势。
技术框架：整体架构包括将证明尝试解析为策略序列，Lean的推导过程标记局部有效步骤和最早失败步骤，形成密集的奖励信号。主要模块包括反馈生成、奖励信号整合和强化学习训练。
关键创新：最重要的创新在于将符号证明助手不仅作为评估时的验证器，还作为训练过程中的奖励Oracle，打破了传统方法的局限。
关键设计：在损失函数设计上，采用了首次错误传播和首次令牌奖励的方法，确保奖励信号的有效性和可靠性，同时优化了网络结构以适应策略级监督。
🖼️ 关键图片
📊 实验亮点
实验结果表明，策略级监督在大多数设置中优于仅依赖结果的基线方法，特别是在MiniF2F和ProofNet基准测试中，表现出显著的性能提升，验证了该方法的有效性和实用性。
🎯 应用场景
该研究的潜在应用领域包括自动定理证明、形式化验证和智能合约等。通过结合强化学习与符号验证，能够提升系统的可靠性和效率，推动智能系统在复杂推理任务中的应用。未来，该方法可能在教育、科研和工业界的形式化验证中发挥重要作用。
📄 摘要（原文）
While reinforcement learning from verifiable rewards (RLVR) typically has relied on a single binary verification signal, symbolic proof assistants in formal reasoning offer rich, fine-grained structured feedback. This gap between structured processes and unstructured rewards highlights the importance of feedback that is both dense and sound. In this work, we demonstrate that the Lean proof assistant itself can serve as a symbolic process oracle, supplying both outcome-level and fine-grained tactic-level verified feedback during training. Proof attempts are parsed into tactic sequences, and Lean's elaboration marks both locally sound steps and the earliest failing step, yielding dense, verifier-grounded credit signals rooted in type theory. We incorporate these structured rewards into a GRPO-style reinforcement learning objective with first-error propagation and first-token credit methods that balances outcome- and process-level advantages. Experiments with STP-Lean and DeepSeek-Prover-V1.5 show that tactic-level supervision outperforms outcome-only baselines in most settings, delivering improvements on benchmarks such as MiniF2F and ProofNet. Beyond empirical gains, our study highlights a broader perspective: symbolic proof assistants are not only verifiers at evaluation time, but can also act as process-level reward oracles during training. This opens a path toward reinforcement learning frameworks that combine the scalability of language models with the reliability of symbolic verification for formal reasoning.