🤖 AI

Process-Verified Reinforcement Learning for Theorem Proving via Lean

本文介绍了一种强化学习框架，该框架利用 Lean 证明助手作为符号过程预言机（symbolic process oracle），以提供密集、细粒度且可靠的策略级（tactic-level）反馈，与传统的仅基于结果的奖励方法相比，显著提升了在 MiniF2F 和 ProofNet 等基准测试上的定理证明性能。

原作者： Minsu Kim, Se-Young Yun

发布于 2026-06-19

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Minsu Kim, Se-Young Yun

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在教一个机器人解决复杂的数学谜题。在过去，我们教这些机器人（即大语言模型）的方式，就像是在玩一场由一位非常严格的裁判监督的“靠近或远离（Hot or Cold）”游戏。

旧的方法：“通过或失败”教练
以前，机器人会写出数学题的完整解法。裁判（一个叫做 Lean 的计算机程序）会查看最终答案，然后只说一句话：“你答对了！”或者“你答错了。”

如果机器人答错了，它完全不知道原因。是第一步就出错了？还是中间用错了公式？或者只是时间不够了？这就像一个学生在没看到评分纸的情况下得到了一个“不及格”，机器人只能猜测哪里出了错，然后重试，这种方式既慢又低效。

新的方法：“循序渐进”教练
这篇论文介绍了一种更聪明的训练机器人的方式。与其仅仅等待最终答案，不如让 Lean 裁判循序渐进地观察机器人的思考过程。

把数学证明想象成用积木搭塔：

旧的方法： 你搭好整个塔，如果最后塌了，教练只会说：“坏塔。”你必须猜测是哪块积木导致了坍塌。
新的方法（本论文）： 教练看着你放置每一块积木。
- 如果你放对了一块，教练会给你一个微小的“做得好！”（正向信号）。
- 如果你放错了一块，教练会立即说：“停！这块不对。”
- 至关重要的一点是： 教练会解释，因为那块积木错了，所以你放在它上面的每一块积木现在都是无效的，即使它们看起来本身没错。这被称为**“首错传播（First-Error Propagation）”**。它教会机器人，一个错误会毁掉整个基础。

论文是如何运作的
研究人员使用了一种叫做**强化学习（Reinforcement Learning）**的方法。以下是他们“秘方”的拆解：

神谕（The Oracle）： 他们不仅将 Lean 证明助手作为最终的评判者，还将其作为过程神谕（Process Oracle）。这意味着它扮演着一个完美理解逻辑规则的超级老师，能够实时发现错误。
反馈循环： 当机器人尝试解决问题时，Lean 会将解法分解为一系列“策略（Tactics）”（即小的逻辑步骤）。
- 如果整个证明成功，机器人会获得一个大的奖励。
- 如果证明失败，Lean 会告诉机器人究竟是哪一步失败了。机器人由此学习到，失败之前的步骤是正确的，但失败的那一步以及之后的所有步骤都是错误的。
信用分配系统（The Credit System）： 论文发现，一个步骤中最关键的部分是该步骤的第一个词（或 Token）。它就像是一个“命令词”（例如：“加”、“乘”、“假设”）。研究人员决定将奖励或惩罚专门针对这个第一个词进行分配。这有助于机器人学习如何为这项工作选择正确的“命令”，而不是仅仅死记硬背整个句子。

结果
当他们在著名的数学基准测试（MiniF2F 和 ProofNet）上测试这种新方法时：

机器人学习得更快，犯错更少。
与仅使用“通过/失败”反馈训练的机器人相比，它们变得更加稳定和可靠。
它们的表现优于那些试图使用其他不太精确的方法来猜测哪些步骤是好的机器人。

大局观
核心结论是，形式化证明助手（如 Lean）不应仅仅被用来在最后检查答案。它们可以在训练过程中充当教练。通过提供关于机器人“如何思考”而非仅仅是“得出什么结论”的密集、具体的反馈，我们可以构建出更聪明、更可靠的 AI 来解决困难的逻辑问题。

他们没有做的事情
这篇论文非常明确地说明了其成就。它并未声称解决了所有的数学问题，也没有声称这种方法适用于写故事或与人聊天。它严格限于教 AI 使用 Lean 语言来证明数学定理。他们还指出，他们没有将自己的方法与其他“学习型”教练进行比较，因为对于这种特定类型的数学，目前还不存在需要大量人类编写示例的教练。

技术摘要：基于 Lean 的过程验证强化学习用于定理证明

问题陈述

自动定理证明（ATP）旨在为数学定理生成形式化证明。虽然大语言模型（LLM）在推理任务方面取得了进展，但它们在强化学习（RL）过程中通常依赖于自然语言（NL）或二元结果奖励（正确/错误）。这造成了一个差距：

稀疏反馈： 标准的 RL 方法通常仅使用最终的二元信号（证明通过/失败），这导致了稀疏的信用分配（credit assignment），难以引导模型完成长链推理。
非结构化 vs. 结构化： 与提供每一步推理细粒度类型论验证的符号证明助手（如 Lean、Coq、Isabelle）不同，LLM 是基于 Token 序列和标量奖励进行训练的。
过程奖励模型（PRMs）： 虽然最近的工作使用 PRM 提供步骤级奖励，但这些方法通常需要大规模标注数据集，或依赖于基于自然语言思维链（CoT）的监督，缺乏符号验证的严谨性。

核心解决的问题是：如何利用符号证明助手（Lean）提供的丰富、结构化的反馈来训练 LLM，而不依赖于外部可能存在噪声的 PRM 或人工标注。

方法论

本文提出了一种**过程验证强化学习（Process-Verified Reinforcement Learning）**框架，该框架将 Lean 的符号反馈直接集成到组相对策略优化（GRPO）目标函数中。该方法由三个主要部分组成：

1. 符号过程先知（Symbolic Process Oracle）

作者不仅将 Lean 视为最终的验证器，还将其作为训练期间的过程先知（process oracle）来使用。

解析： 生成的证明基于抽象语法树（AST）被解析为策略序列（ $T_1, \dots, T_N$ ）。
验证： Lean 的阐述（elaboration）过程提供两种类型的信号：
- 结果信号： 一个全局二元得分 $g(Y) \in \{0, 1\}$ ，指示整个证明是否有效。
- 过程信号： 为每个策略提供细粒度的反馈，识别局部有效的步骤以及第一个错误的具体位置。

2. 信用分配策略

为了弥合符号反馈与 Token 级 RL 之间的差距，作者引入了特定的分配规则：

首错传播（First-Error Propagation）： 如果策略 $T_j$ 失败，则所有后续策略（ $T_k$ ，其中 $k \ge j$ ）都被视为错误。这反映了证明的因果性质：无效的前缀会使整个后续推理链失效。
策略级评分 ( $\phi$ )：
- 如果证明通过（ $g(Y)=1$ ），则所有策略获得正分（1）。
- 如果证明失败（ $g(Y)=0$ $g (Y) = 0$ ）：
  - 位于第一个错误之前的策略获得部分得分（ $d_1$ ）。
  - 第一个出错的策略及其后续所有策略获得惩罚得分（ $d_2$ ）。
Token 级映射： 策略级的优势（advantage）仅分配给每个策略的第一个 Token（即关键字，例如 intro、apply）。这与确定证明策略的语义决策点相一致。

3. RL 目标函数（GRPO 集成）

该框架将结果优势和过程优势结合到一个单一的 GRPO 目标中：

结果优势 ( $A_{outcome}$ )： 基于相对于组平均值的全局通过/失败状态进行计算。
过程优势 ( $A_{process}$ )： 基于策略级得分进行计算，并通过组的平均结果奖励进行归一化，以平衡问题难度。
组合优势： 对于响应 $i$ 中属于策略 $j$ 的第一个 Token $t$ ：
$A_{i,t} = A_{outcome, i, t} + A_{process, i, j}$
对于非第一个 Token，仅应用结果优势。这种公式化方法避免了对价值模型或辅助 PRM 的需求，完全依赖于验证器的地面真值（ground truth）。

核心贡献

符号反馈的形式化： 作者将 Lean 的策略级反馈形式化为标量训练信号，实现了无需自然语言引导的细粒度 Token 级信用分配。
符号验证器引导的 RL： 他们将直接源自 Lean 的结果和策略级奖励集成到 RL 框架中，提供了密集且可验证的信用分配。
稳定的基准测试提升： 该方法在 MiniF2F 和 ProofNet 基准测试上表现出持续的改进，优于仅基于结果的 RL 以及传统的基线模型，且不需要外部 PRM 或自然语言表示。

实验结果

实验使用 STP-Lean 和 DeepSeek-Prover-V1.5（7B 模型）在 MiniF2F-Test 和 ProofNet-Test 基准测试上进行。

性能增益：
- STP-Lean： 所提方法使 MiniF2F pass@64 提升了 2.5%（从 56.7% 提升至 59.2%），ProofNet pass@32 提升了 1.4%。
- DeepSeek-Prover-V1.5： 在所有设置下均观察到持续但微小的改进。
对比基线：
- 该方法优于“仅结果”的 GRPO，后者表现出不稳定性，并在某些配置下未能提升 ProofNet 的表现。
- 它在采用单次生成（single-shot generation）方式且无需大规模推理时搜索预算的情况下，达到了与强树搜索基线（如 InternLM2.5-StepProver、DeepSeek-Prover-RL+RMaxTS）竞争力的水平。
消融实验：
- Token 分配： 将信用分配给策略的第一个 Token 相比于将信用分布在所有 Token 或最后一个 Token 上，能产生最稳定的结果。
- 首错传播： 移除此规则会导致性能显著下降，证实了将后续步骤视为无效步骤的必要性。
- 超时处理： 15 秒的验证超时提供了最佳平衡，既鼓励了简洁的证明，又不会丢弃有效的复杂证明。

重要性与主张

论文声称，符号证明助手不应仅被视为评估工具，而应被视为训练过程中的主动过程级奖励先知。通过利用形式化推理系统中固有的“丰富、细粒度的结构化反馈”，作者展示了一条结合 LLM 的可扩展性与符号验证的可靠性的 RL 路径。

研究强调了：

密集、可验证的信号： 使用证明器自身的错误日志和阐述树提供了一种健全且密集的奖励信号，其效果优于稀疏的二元结果或学习到的 PRM。
稳定性： 全局结果奖励与局部策略奖励的结合稳定了训练，防止了仅靠策略训练导致的过早收敛以及仅靠结果训练导致的稀疏性问题。
效率： 该方法在无需树搜索的计算开销或训练单独 PRM 的数据需求下，实现了最先进或具有竞争力的性能。

作者对其局限性保持谦逊，指出其方法依赖于固定的奖励分数（ $d_1, d_2$ ）而非学习到的优势估计器，且目前专注于非 CoT 的纯 Lean 证明，这为设计长篇自然语言推理的奖励留下了空间。