Appearance
DeepSeek-Prover-V1.5：用证明助理反馈训练数学推理模型
—— DeepSeek 研究团队技术报告
内容摘要
教大模型做数学推理一直是个难题。传统方法要么靠人工标注推理步骤（成本高、规模小），要么用答案对错作为奖励信号（反馈粗糙，难以定位错误）。DeepSeek-Prover-V1.5提出了第三条路：利用形式化证明助理的反馈。
证明助理（如Lean、Coq、Isabelle）是数学家用来验证定理证明的工具。这些工具能对每一步推理给出明确的反馈：这一步逻辑正确吗？类型匹配吗？是否遵守了公理系统？这种反馈比简单的"答案对错"要精细得多，而且完全自动化，不需要人工标注。
DeepSeek-Prover-V1.5的核心思路是：让模型生成形式化证明代码（而不是自然语言推理），然后把证明助理的反馈作为强化学习的奖励信号。如果证明通过了，说明推理正确，给正奖励；如果在某一步失败了，模型就知道这一步有问题，可以尝试其他路径。
为了提升搜索效率，团队还引入了蒙特卡罗树搜索（MCTS）：不是盲目生成证明，而是通过树搜索探索多条可能的证明路径，优先扩展那些看起来更有希望的分支。实验表明，在MiniF2F和ProofNet这两个数学定理证明基准上，Prover-V1.5的成功率显著超越了传统的基于人类反馈的强化学习方法。
核心发现
形式化反馈比答案对错更有价值 传统强化学习只能告诉模型"最终答案对还是错"，但无法指出具体哪一步推理出了问题。证明助理的反馈是逐步的、可定位的：如果证明在第5步失败了，模型就知道问题出在那里，可以针对性地调整策略。这种细粒度反馈能让模型更快地学会正确的推理模式。
MCTS能有效探索证明空间 数学定理的证明空间非常大：每一步都有无数种可能的引理、策略、变换。如果随机搜索，几乎不可能找到正确证明。蒙特卡罗树搜索通过"探索-利用"平衡机制，优先扩展那些部分成功的路径，同时也会适度尝试新路径，避免陷入局部最优。实验表明MCTS能让证明成功率提升30%以上。
RL让模型学会自我纠错 在训练过程中，模型会尝试各种证明路径，其中大部分都会失败。但通过强化学习，模型能从失败中学习：哪些策略容易导致类型不匹配？哪些引理组合更可能成功？经过足够的训练，模型甚至能学会在证明过程中检查中间结果，发现潜在问题后主动调整方向。
跨任务迁移能力 虽然Prover-V1.5是在Lean形式化系统上训练的,但团队发现模型学到的推理策略可以迁移到其他需要严谨推理的任务：比如代码验证、逻辑推理、甚至复杂的数学应用题。这说明形式化训练能让模型学到更本质的推理能力，而不只是记住特定领域的知识。
章节要点速览
第一章 引言 数学定理证明需要极其严谨的逻辑推理，传统语言模型难以胜任。形式化证明助理能提供高质量、可解释的反馈，但如何将这种反馈有效整合到LLM训练中是个挑战。
第二章 相关工作 回顾了数学推理、定理证明、强化学习等领域的相关研究。传统方法包括基于模板的证明生成、基于神经网络的策略学习、以及基于搜索的证明发现等，但这些方法都存在泛化能力弱或效率低的问题。
第三章 方法 详细介绍了三个核心组件：
- 证明助理反馈机制：如何将Lean的编译错误转化为强化学习奖励
- RL形式化：状态空间（部分证明）、动作空间（可能的下一步）、奖励设计（通过给高分，失败给负分，部分成功给中等分）
- MCTS集成：如何通过树搜索高效探索证明空间，包括节点选择策略、扩展策略、反向传播机制
第四章 实验设置 基准测试包括MiniF2F（244个精选的数学竞赛题）和ProofNet（更大规模的定理库）。对比方法包括传统RLHF、监督学习、以及基于检索的证明生成。评测指标是证明成功率（能否在限定步数内完成证明）。
第五章 结果与分析 Prover-V1.5在MiniF2F上的成功率达到了50.8%，比传统RLHF方法高出15个百分点。在ProofNet上，模型能证明其中68%的定理。消融实验显示：去掉MCTS，成功率下降20%；去掉形式化反馈改用答案对错，成功率下降25%。这证明了两个组件都至关重要。
第六章 讨论与局限 模型在某些类型的定理上表现仍然不佳，比如需要复杂归纳或构造性证明的问题。另外，形式化证明语言（Lean）本身有学习成本，限制了方法的通用性。未来方向包括支持更多证明助理、提升搜索效率、以及迁移到更广泛的推理任务。
第七章 结论 DeepSeek-Prover-V1.5证明了形式化反馈和强化学习的组合能显著提升模型在严谨推理任务上的能力。这种方法不依赖大规模人工标注，具有很好的可扩展性，为训练更可靠的推理模型提供了新思路。
Prover-V1.5的核心创新在于： 通过将形式化验证工具的反馈引入强化学习，让模型能在没有人工标注的情况下，自己学会严谨的数学推理和定理证明。