DeepSeek-Prover-V1.5 是什么：DeepSeek 的 Lean 4 定理证明模型

它是什么

DeepSeek-Prover-V1.5 是深度求索在 2024 年 8 月 15 日开源的数学定理证明模型，专门用 Lean 4 这种形式化语言写数学证明。形式化证明和平时写在纸上的证明不同，每一步都要严格到计算机能逐行检查，证明对不对由 Lean 的证明检查器说了算，不存在“看起来对”。这让定理证明成了检验 AI 推理能力的一块试金石：要么证出来、通过检查，要么失败，没有模糊空间。

怎么训出来的

它在 DeepSeekMath-Base 的基础上，针对形式化数学语言做了专门训练。第一步是监督微调，使用的是在 DeepSeek-Prover-V1 基础上增强过的形式化定理证明数据集。第二步是强化学习，奖励信号来自证明助手的反馈（RLPAF）：模型写出的证明交给 Lean 检查，通过就给奖励，不通过就不给。因为对错完全由检查器判定，这种奖励非常干净，不会出现奖励模型被钻空子的问题。

RMaxTS：会探索的树搜索

上一代 Prover-V1 是一次性生成完整证明，一次不对就重来。V1.5 提出了 RMaxTS，一种蒙特卡洛树搜索的变体：把证明过程看成一棵树，每一步有多种走法，模型可以边走边看 Lean 的反馈，在有希望的分支上继续深入。RMaxTS 用内在奖励来驱动探索，鼓励模型尝试新的证明路径，而不是在相似的思路里打转，从而生成更多样的证明尝试，提高找到正确证明的概率。

成绩怎么样

官方报告称，DeepSeek-Prover-V1.5 相比 V1 有显著提升，在高中数学竞赛级别的 miniF2F 测试集上，以及本科数学水平的 ProofNet 测试集上，都取得了当时开源模型的新高成绩，其中 miniF2F 测试集达到 63.5% 的通过率。

适合谁

研究 AI 数学推理、形式化验证的研究者，以及用 Lean 做数学形式化的社区，是它最直接的用户；它的“检查器反馈强化学习加树搜索”思路，后来在更多推理模型里都能看到影子。普通用户很难直接用上，需要先熟悉 Lean。AI 主线的看法是：定理证明是少数“对错有铁证”的领域，DeepSeek 在这里积累的强化学习经验，为它后来的推理模型打下了基础。