基于 Lean 的过程验证强化学习用于定理证明

# 基于过程验证的强化学习在定理证明中的应用（Lean平台） 来源：https://arxiv.org/html/2606.20068 ###### 摘要 尽管基于可验证奖励的强化学习（RLVR）通常依赖于单一的二元验证信号，但在形式化推理中，符号化证明助手提供了丰富、细粒度的结构化反馈。这种结构化过程与非结构化奖励之间的差距，凸显了密集且可靠的反馈的重要性。在本工作中，我们证明Lean证明助手本身可以作为符号化过程预言机，在训练过程中同时提供结果级别和细粒度的策略级别验证反馈。证明尝试被解析为策略序列，Lean的详细展开过程会标记出局部正确的步骤以及最早出错的步骤，从而提供基于类型理论的密集、源自验证器的信用信号。我们将这些结构化奖励融入GRPO风格的强化学习目标中，采用首次错误传播和首次令牌信用方法，平衡结果级别和过程级别的优势。在STP-Lean和DeepSeek-Prover-V1.5上的实验表明，在大多数设置中，策略级监督优于仅基于结果的基线，在MiniF2F和ProofNet等基准测试上取得了改进。除了实验上的提升，我们的研究还揭示了一个更广阔的视角：符号化证明助手不仅在评估时充当验证器，还可以在训练时充当过程级别的奖励预言机。这为结合语言模型的可扩展性与符号化验证的可靠性进行形式化推理的强化学习框架开辟了一条道路。 ## 1 引言 自动定理证明（ATP）是人工智能的长期目标之一（Newellet al.,1957 (https://arxiv.org/html/2606.20068#bib.bib1)）。与自然语言（NL）推理（通常包含模糊或含混的符号）相比，基于形式逻辑和类型理论的形式化定理证明提供了技术性和精确的语言来证明数学定理（Church,1940 (https://arxiv.org/html/2606.20068#bib.bib3)；Fitting,1996 (https://arxiv.org/html/2606.20068#bib.bib2)）。目前，交互式定理证明器（ITP），如Lean（de Mouraet al.,2015 (https://arxiv.org/html/2606.20068#bib.bib4)；Moura and Ullrich,2021 (https://arxiv.org/html/2606.20068#bib.bib7)）、Isabelle（Nipkowet al.,2002 (https://arxiv.org/html/2606.20068#bib.bib5)）和Coq（Barraset al.,1997 (https://arxiv.org/html/2606.20068#bib.bib6)），是验证数学证明的可靠且强大的工具。Lean证明是一系列策略组成的序列，自动化部分处理常规的算术/逻辑和验证——因此ITP在完全自动化和人类指导之间提供了一个中间地带。相比之下，LLM通过预训练和后训练从大型语料库中建模下一个令牌的概率，学习词汇相关性而非基于规则的符号操作（Brownet al.,2020 (https://arxiv.org/html/2606.20068#bib.bib8)）。通过进一步的指令微调和基于人类反馈的强化学习（RLHF）等技术，LLM已经发展到处理包括问答、摘要、对话在内的广泛任务（Ouyanget al.,2022 (https://arxiv.org/html/2606.20068#bib.bib9)；Baiet al.,2022 (https://arxiv.org/html/2606.20068#bib.bib10)）。特别地，针对推理任务的强化学习（RL）方法旨在通过鼓励生成长的思维链来增强模型的推理能力（DeepSeek-AIet al.,2025 (https://arxiv.org/html/2606.20068#bib.bib13)；OpenAIet al.,2024 (https://arxiv.org/html/2606.20068#bib.bib11)）。与其他通常根据最终答案来验证或奖励LLM响应的推理任务（Cobbeet al.,2021 (https://arxiv.org/html/2606.20068#bib.bib12)）相比，当LLM用形式语言做出响应时，定理证明器可以验证整个证明的正确性。在这种背景下，考虑到ITP的人机协作特性，越来越多的工作尝试使用LLM进行形式化定理证明（AlphaProof and AlphaGeometry teams,2024 (https://arxiv.org/html/2606.20068#bib.bib16)；Trinhet al.,2024 (https://arxiv.org/html/2606.20068#bib.bib15)）。LLM充当证明者代理，而定理证明器充当验证器，在推理时用于搜索和验证策略及前提，或者用来用已验证的样本扩充形式化推理数据集（Lampleet al.,2022 (https://arxiv.org/html/2606.20068#bib.bib18)；Wanget al.,2023 (https://arxiv.org/html/2606.20068#bib.bib19)；Yinget al.,2024a (https://arxiv.org/html/2606.20068#bib.bib17)；Zhuet al.,2025 (https://arxiv.org/html/2606.20068#bib.bib57)）。此外，最近的一些研究将Lean定理证明器提供的二元反馈纳入了其在线RL框架（Xinet al.,2024b (https://arxiv.org/html/2606.20068#bib.bib20)）。Lean中基于策略的证明结构包含与推理任务相关的信息，例如策略的位置或证明错误/失败的性质。这种结构化信息不仅捕捉了证明的结果，还捕捉了底层的推理过程。然而，尽管具有潜力，只有少数工作探索了将这种细粒度监督纳入LLM的训练中（Jiet al.,2025 (https://arxiv.org/html/2606.20068#bib.bib52)）。与此同时，最近的推理RL方法越来越强调使用基于过程的奖励模型（PRM）来指导模型行为。虽然这些模型表现出了有希望的性能，但关于PRM如何构建、推理步骤或步骤奖励应如何定义、它们应该依赖什么样的训练信号或数据集，仍然缺乏清晰度（Yuanet al.,2024 (https://arxiv.org/html/2606.20068#bib.bib22)；Luoet al.,2024 (https://arxiv.org/html/2606.20068#bib.bib24)；Cuiet al.,2025 (https://arxiv.org/html/2606.20068#bib.bib23)）。与依赖PRM或长自然语言COT（Linet al.,2025a (https://arxiv.org/html/2606.20068#bib.bib29)；b (https://arxiv.org/html/2606.20068#bib.bib33)）的最新方法不同，我们在RL训练期间直接利用Lean证明助手作为**符号化过程预言机**，不需要任何自然语言指导。对于每个生成的证明，Lean提供（i）全局结果信号和（ii）通过信息树和错误日志提供的细粒度策略级反馈。虽然Lean可以提供细粒度的策略级信号，但在RL训练中有效地利用它们并非易事。Lean输出符号化、树结构的语言反馈，例如证明状态和错误位置，而LLM在自回归令牌序列上操作，并从RL中的标量奖励中学习。这种表示上的不匹配带来了信用分配挑战：必须将符号化验证器反馈转换为结构化的令牌级训练信号。为了弥合这一差距，我们引入了一个结构化信用分配框架，用于将符号化验证器信号集成到在线RL目标中，该框架需要三个组件：（i）整合细粒度信号的形式化表示，（ii）将Lean的符号化反馈简化为每个策略分数的原则性规则，以及（iii）从每个策略分数到令牌级优势的映射。我们使用策略级MDP、基于Lean语义的首次错误传播规则以及首次令牌信用分配策略来实例化这个流程。我们将生成的每个策略信号集成到结合了结果级和过程级优势的组相对策略优化（GRPO）风格目标中。这使得我们可以实现精确的、基于类型理论的信用分配，且基于验证器反馈，无需辅助PRM。实验上，我们发现将符号化验证器反馈纳入RL目标在MiniF2F和ProofNet上持续提升了性能，证明了细粒度验证器信号对于推理任务中可靠信用分配的价值。我们的主要贡献如下： - •**形式化Lean的符号化反馈。** 我们形式化了Lean的符号化、策略级反馈，并将其简化为标量训练信号，从而实现细粒度的、令牌级信用分配。 - •**符号化验证器指导的RL。** 我们将从Lean导出的结果级和策略级奖励整合到一个RL框架中，提供了密集且可验证的信用分配。 - •**基准上的稳定改进。** 在MiniF2F和ProofNet上，我们的方法始终优于仅基于结果的RL和普通基线，无需自然语言符号或外部PRM即可获得更稳定和更稳健的提升。 见图1图1：通过Lean结合结果级和策略级奖励的整体框架：证明YY被解析为策略T1,...,T5T_1,\dots,T_5，Lean提供结果反馈g(Y)g(Y)和步骤级错误（例如，在T3T_3处失败会使后续策略无效）。然后，奖励分配给每个策略的第一个令牌。 ## 2 相关工作 #### 自动定理证明 自动定理证明通常包括两个阶段。第一个是自动形式化，即将自然语言数学陈述转换为形式化陈述。LLM已被用于此任务（Wuet al.,2022 (https://arxiv.org/html/2606.20068#bib.bib25)），生成了诸如MiniF2F、ProofNet、Deepseek-Prover和LeanWorkbook等数据集（Zhenget al.,2022 (https://arxiv.org/html/2606.20068#bib.bib30)；Azerbayevet al.,2023 (https://arxiv.org/html/2606.20068#bib.bib31)；Xinet al.,2024a (https://arxiv.org/html/2606.20068#bib.bib14)；Yinget al.,2024a (https://arxiv.org/html/2606.20068#bib.bib17)）。第二个阶段是证明生成，可以通过树搜索逐步进行（Polu and Sutskever,2020 (https://arxiv.org/html/2606.20068#bib.bib26)；Azerbayevet al.,2024 (https://arxiv.org/html/2606.20068#bib.bib28)；Wuet al.,2024 (https://arxiv.org/html/2606.20068#bib.bib27)；Xinet al.,2024b (https://arxiv.org/html/2606.20068#bib.bib20)）或一次性生成整个证明（Xinet al.,2024a (https://arxiv.org/html/2606.20068#bib.bib14)；Linet al.,2025b (https://arxiv.org/html/2606.20068#bib.bib33)）。现有的方法如Lean-STaR和RMaxTS仅在推理时使用Lean作为步骤检查器（Linet al.,2025a (https://arxiv.org/html/2606.20068#bib.bib29)；Xinet al.,2024b (https://arxiv.org/html/2606.20068#bib.bib20)），而最近的工作在训练期间将Lean用作整个证明的验证器（Wanget al.,2025a (https://arxiv.org/html/2606.20068#bib.bib44)；Zhanget al.,2025 (https://arxiv.org/html/2606.20068#bib.bib45)；Renet al.,2025 (https://arxiv.org/html/2606.20068#bib.bib46)）。在本文中，我们超越了步骤检查或整个证明验证，通过在在线RL训练中使用Lean的细粒度、策略级反馈作为基于过程的奖励。 #### 语言模型中的强化学习 除了PPO（Schulmanet al.,2017 (https://arxiv.org/html/2606.20068#bib.bib38)）和GRPO（Shaoet al.,2024 (https://arxiv.org/html/2606.20068#bib.bib37)）等算法进步外，奖励塑造和信用分配仍然是RL中的核心挑战。基于结果的奖励（Cobbeet al.,2021 (https://arxiv.org/html/2606.20068#bib.bib12)）虽然广泛用于RLHF，但存在稀疏性问题（Chanet al.,2024 (https://arxiv.org/html/2606.20068#bib.bib40)；Zhenget al.,2023 (https://arxiv.org/html/2606.20068#bib.bib41)）。基于过程的奖励模型（PRM）通过分配步骤级奖励来解决这个问题（Lightmanet al.,2023 (https://arxiv.org/html/2606.20068#bib.bib39)；Setluret al.,2024 (https://arxiv.org/html/2606.20068#bib.bib42)；Kazemnejadet al.,2024 (https://arxiv.org/html/2606.20068#bib.bib21)；Yuanet al.,2024 (https://arxiv.org/html/2606.20068#bib.bib22)；Cuiet al.,2025 (https://arxiv.org/html/2606.20068#bib.bib23)）。奖励可以隐含地定义（Cuiet al.,2025 (https://arxiv.org/html/2606.20068#bib.bib23)），也可以通过正确性注释（Lightmanet al.,2023 (https://arxiv.org/html/2606.20068#bib.bib39)）或蒙特卡洛展开成功率（Wanget al.,2024 (https://arxiv.org/html/2606.20068#bib.bib48)）来显式定义，但现有方法需要大型的步骤级正确性注释数据集。这激发了我们利用Lean证明器本身作为过程预言机的方法，无需人工标签或采样即可自动验证每一步。更多讨论见附录A (https://arxiv.org/html/2606.20068#A1)。 ## 3 预备知识 ### 3.1 Lean4 在Lean定理证明中，要建立的陈述表示为一个初始目标，并通过一系列策略逐步简化为子目标。每个策略通过将其与库中的引理或定理进行统一来解析和详细展开，生成新的子目标并验证其有效性。详细展开阶段产生结构化的信息树，记录证明状态和错误消息。最后，内核确保展开后的证明在类型理论上是一致的，并且构成原始定理的有效证明。形式上，让xx表示提供给LLM的定理陈述，让YY表示响应，即用Lean语言表达的证明。记Y\mathcal{Y}为Lean证明的集合，T\mathcal{T}为策略的集合。对于Y∈YY\in\mathcal{Y}，我们将证明YY视为从抽象语法树（AST）解析并根据其起始位置排序的策略序列(T1,T2,...,TN(Y))(T_1,T_2,\dots,T_{N(Y)})，其中N(Y)N(Y)是YY中策略的数量，这与LLM的自回归生成过程一致。每个策略TiT_i对应YY中的令牌yty_t。Lean将策略表示为AST节点；每个节点编码策略的语法结构和绑定上下文，并可能携带元数据，如错误消息、证明状态和索引，用户（或训练框架）可以通过这些元数据与Lean交互。如果一个策略没有出现在错误日志中，那么它已经被成功详细展开并通过了Lean内部的基于规则的验证，这保证了该步骤在依赖类型理论下是局部正确的。因此，任何未被标记为错误的策略都构成一个已验证的推理步骤——即使它没有帮助完成证明，因为某些子目标仍然存在或后续策略失败。换句话说，Lean确保策略级别的正确性，而证明级别的完备性则取决于整个序列是否解决了所有目标。利用这种解析和验证反馈，我们定义解析函数f:Y→T∗f:\mathcal{Y}\to\mathcal{T}^*为对TacSet(Y)\mathsf{TacSet}(Y)排序得到的序列：f(Y)=(T1,...,TN(Y))f(Y)=(T_1,\dots,T_{N(Y)})。我们还定义全局评分函数g:Y→[0,1]g:\mathcal{Y}\to[0,1]，其中如果YY通过Lean验证器则g(Y)=1g(Y)=1，否则为0；以及每个策略的评分函数φ:{(Y,T)∣Y∈Y,T∈TacSet(Y)}⟶{1,d1,d2}\varphi:\{(Y,T)\mid Y\in\mathcal{Y},\,T\in\mathrm{TacSet}(Y)\}\ \longrightarrow\ \{1,d_1,d_2\}。具体地， φ(Y,T)={1,ifg(Y)=1,d1,else ifg(Y)=0andThas no errors in Lean,d2,else ifg(Y)=0andTcontains errors.\varphi(Y,T)=\begin{cases}1,&\text{if }g(Y)=1,\\ d_1,&\text{else if }g(Y)=0\text{ and }T\text{ has no errors in Lean},\\ d_2,&\text{else if }g(Y)=0\text{ and }T\text{ contains errors.}\end{cases}结合这些组件，我们通过f,g,φf,g,\varphi来表示Lean的角色，即Lean:Y→{0,1}×(T×{1,d1,d2})∗\displaystyle\mathrm{Lean}: \mathcal{Y}\to\{0,1\}\times(\mathcal{T}\times\{1,d_1,d_2\})^*，Lean(Y)\displaystyle\mathrm{Lean}(Y)=(g(Y),[(T1,φ(Y,T1)),...,(TN(Y),φ(Y,TN(Y)))])=(g(Y),[(T_1,\varphi(Y,T_1)),...,(T_{N(Y)},\varphi(Y,T_{N(Y)}))])，其中f(Y)=(T1,...,TN(Y))f(Y)=(T_1,\dots,T_{N(Y)})。