DeepSeek 发布定理证明模型 DeepSeek-Prover-V2

发生了什么

深度求索发布了开源的形式化定理证明模型 DeepSeek-Prover-V2，用于 Lean 4。论文于 2025 年 4 月 30 日发布在 arXiv 上，维基百科将发布日期记为 2025 年 5 月 1 日。^[1][3]

定理证明是指说明一个数学命题可以从已接受的公理和已证结论推出。在 Lean 4 中，证明本身就用这门语言书写，因此正确性可以由程序机械检查。这类基准由竞赛风格的题目组成，同一套题目上的结果便于比较不同模型。

关键细节

冷启动训练数据来自由 DeepSeek-V3 驱动的递归证明流程，该流程把问题拆成子目标。^[1]

子目标的证明结果与 DeepSeek-V3 逐步推理的内容被整合为思维链数据，使一个模型同时包含非形式化推理和形式化推理。^[1]

模型在 MiniF2F-test 基准上达到 88.9% 的通过率，并解出了 PutnamBench 658 道题中的 49 道。^[1]

论文提出了 ProverBench，包含 325 道形式化题目，其中 15 道来自 AIME 2024 和 2025 竞赛。^[1]

影响

由计算机检查的证明不依赖对作者的信任，因此形式化定理证明被视为获得可检验数学结论的途径。论文中，形式化证明与自然语言解题在同一批 AIME 题目上的对比，是它就这一问题给出的最直接的证据。