We introduce DeepSeek-Prover-V1.5, an open-source language model designed for theorem proving in Lean 4, which enhances DeepSeek-Prover-V1 by optimizing both training and inference processes. Pre-trained on DeepSeekMath-Base with specialization in formal mathematical languages, the model undergoes supervised fine-tuning using an enhanced formal theorem proving dataset derived from DeepSeek-Prover-V1. Further refinement is achieved through reinforcement learning from proof assistant feedback (RLPAF). Beyond the single-pass whole-proof generation approach of DeepSeek-Prover-V1, we propose RMaxTS, a variant of Monte-Carlo tree search that employs an intrinsic-reward-driven exploration strategy to generate diverse proof paths. DeepSeek-Prover-V1.5 demonstrates significant improvements over DeepSeek-Prover-V1, achieving new state-of-the-art results on the test set of the high school level miniF2F benchmark ($63.5\%$) and the undergraduate level ProofNet benchmark ($25.3\%$).
核心贡献 · Key contributions
提出 RMaxTS，一种基于内在奖励驱动的蒙特卡洛树搜索变体，用于稀疏奖励的证明搜索。 Proposes RMaxTS, a Monte-Carlo tree search variant with intrinsic-reward-driven exploration for sparse-reward proof search.
引入截断-恢复机制，通过树搜索将整体证明生成与证明步骤生成相结合。 Introduces a truncate-and-resume mechanism that integrates whole-proof generation with proof-step generation via tree search.
使用 7B 参数模型在 miniF2F（63.5%）和 ProofNet（25.3%）基准上取得最先进结果。 Achieves state-of-the-art results on miniF2F (63.5%) and ProofNet (25.3%) benchmarks using a 7B parameter model.
采用基于证明助手反馈的强化学习（RLPAF）结合 GRPO 算法，增强整体证明生成能力。 Employs reinforcement learning from proof assistant feedback (RLPAF) with GRPO to enhance whole-proof generation.
通过自然语言思维链注释和中间策略状态增强监督微调数据。 Augments supervised fine-tuning data with natural language chain-of-thought comments and intermediate tactic states.
开源模型和蒙特卡洛树搜索代码，以促进进一步研究。 Provides open-source model and code for Monte-Carlo tree search to facilitate further research.
局限 · Limitations
评估仅限于 Lean 4 证明助手；未验证对其他证明助手的泛化能力。 Evaluation limited to Lean 4 theorem prover; generalization to other proof assistants not verified.
在 miniF2F 和 ProofNet 上的性能可能无法反映真实世界的复杂定理证明场景。 Performance on miniF2F and ProofNet may not reflect real-world complex theorem proving scenarios.
RMaxTS 依赖内在奖励，可能无法扩展到极大的搜索空间。 RMaxTS relies on intrinsic rewards which may not scale to extremely large search spaces.
模型规模（7B 参数）可能限制推理深度，与更大的前沿模型相比存在差距。 Model size (7B parameters) may limit reasoning depth compared to larger frontier models.
证明搜索的利用方面（如评论模型）未解决；需要未来工作。 Exploitation aspect of proof search (e.g., critic model) not addressed; future work needed.
论文章节 · Sections（共 18）
摘要Abstract
1 引言1 Introduction
1.1 贡献1.1 Contributions
1.2 评估与指标概述1.2 Summary of Evaluations and Metrics
2.1 预训练2.1 Pre-training
2.2 监督微调2.2 Supervised Fine-tuning
2.3 基于证明助手反馈的强化学习2.3 Reinforcement Learning from Proof Assistant Feedback
2.4 评估2.4 Evaluation
3.1 策略级树抽象3.1 Tactic-level Tree Abstraction
3.2 基于蒙特卡洛树搜索的交互式定理证明3.2 Interactive Theorem Proving via Monte-Carlo Tree Search
3.3 蒙特卡洛树搜索的内在奖励3.3 Intrinsic Rewards for Monte-Carlo Tree Search
3.4 蒙特卡洛树搜索的并行化3.4 Parallelization of Monte-Carlo Tree Search
3.5 与现有方法的比较3.5 Comparison with Existing Methods
4 实验结果4 Experimental Results
4.1 主要结果4.1 Main Results
4.2 重新审视训练策略在大规模采样中的有效性4.2 Re-Examining the Effectiveness of Training Strategies on Large-scale Sampling
4.3 RMaxTS 的消融研究4.3 Ablation Studies on RMaxTS
5 结论、局限与未来工作5 Conclusion, Limitation, and Future Work