DeepSeek-Prover

背景：AI数学家的诞生

你有没有想过——如果让AI来做数学证明题，会是怎样的体验？不是简单地算答案，而是像数学家一样，用严格的逻辑一步步证明每一步推理？这正是DeepSeek-Prover-V1.5试图攻克的核心问题：让大语言模型真正学会形式化数学定理证明。

这个项目来自国内AI团队DeepSeek（深度求索），他们曾在2024年开源了DeepSeekMath系列模型，在数学推理领域引起不小反响。DeepSeek-Prover-V1.5是他们定理证明方向的最新成果，刷新了高中级数学定理证明的准确率纪录。

什么是形式化定理证明？

与传统给答案的AI不同，形式化定理证明要求模型产出的证明必须能被计算机严格验证。这就像装修房子：普通AI能给你一个看起来差不多的方案，而形式化证明必须精确到每一颗螺丝钉的位置，任何一步跳步都会导致验证失败。

项目使用的证明语言是Lean 4——一种现代化的形式化数学语言，由微软研究院的Leonardo de Moura开发。Lean 4不仅是证明工具，还是一门完整的编程语言，能表达极其复杂的数学结构，从群论到拓扑学无所不包。

核心创新：从SFT到RLPAF+RMaxTS

DeepSeek-Prover-V1.5的核心创新有两层：

第一层：RLPAF（强化学习证明反馈）

传统做法是SFT（监督微调）——给模型看大量题目-证明对，让它模仿。DeepSeek-Prover-V1.5在SFT基础上引入了RLPAF，让模型在证明过程中接收来自Lean 4证明助手本身的反馈信号。

Lean 4验证器会告诉模型：哪一步走不通、哪个战术（tactic）选择错误。通过这种即时纠错机制，模型学会的不仅是模仿正确答案，更是理解证明失败的原因，从而探索更广阔的证明空间。

第二层：RMaxTS（内在奖励驱动的蒙特卡洛树搜索）

这是更激动人心的部分。在单一生成模式（DeepSeek-Prover-V1）的基础上，V1.5引入了RMaxTS——一种蒙特卡洛树搜索（MCTS）的变体。

RMaxTS的核心思想是：面对同一个定理，模型不再只生成一条证明路径，而是并行探索多条证明树，利用内在奖励（intrinsic reward）引导搜索方向。如果某条分支快速失败，模型会转向其他分支，避免在死路上浪费计算资源。

这一机制使得V1.5在高中难度的miniF2F基准上达到了63.5%的准确率（DeepSeek-Prover-V1为50%），在本科难度的ProofNet上达到25.3%（InternLM2-StepProver为18.1%）。

技术架构：三层模块化设计

项目代码组织清晰，分为三大模块：

• 算法层（prover/algorithms/）：搜索策略实现，包括RMaxTS（rmax_tree_search.py）、基础采样（sampling.py）
• Lean后端（prover/lean/）：Lean 4验证器（verifier.py）、AST解析（ast_parser.py）、证明对象管理
• 分布式Worker（prover/workers/）：数据加载、生成器、调度器、搜索进程管理

推理引擎选用vLLM 0.4.1（基于PagedAttention的高效推理框架），配合Transformers 4.40.1做tokenization和模型加载。核心推理通过prover/lean/verifier.py与本地Lean 4 REPL通信，由elan工具管理的Lake构建系统驱动。

硬件需求：这不是随便跑跑的项目

项目明确要求80GB+ VRAM（BF16精度）的GPU。A100/H100是推荐配置，RTX 3090/4090（24GB）可通过int4量化勉强运行，但速度会很慢。此外，还需要准备200GB+磁盘空间，其中Mathlib4数学库本身就需要约50GB。

争议与局限

必须指出的是，25.3%的ProofNet本科级准确率说明当前模型在更高难度的数学证明上仍有相当长的路要走。形式化定理证明的正确性要求极高，任何一步跳步都会导致整个证明失败，这比开放域问答要困难得多。

此外，项目采用双重许可证：代码用MIT，模型权重用单独的模型协议（LICENSE-MODEL），商用需要注意合规。

行业意义

DeepSeek-Prover-V1.5代表了AI for Math的一个重要方向——从近似答案走向可验证推理。随着形式化数学库（如Mathlib4）的不断壮大，结合RL和MCTS的搜索策略，这条路线的潜力远未触顶。如果模型能在本科数学上达到60%+，将对数学教育、软件验证、编译器优化等领域产生深远影响。