摘要

我们提出 DeepSeek-Prover-V1.5，这是一个专为 Lean 4 环境下定理证明设计的开源语言模型，通过优化训练与推理过程，对 DeepSeek-Prover-V1 进行了全面升级。该模型基于 DeepSeekMath-Base 进行预训练，并在形式化数学语言方面具有专长，随后利用从 DeepSeek-Prover-V1 派生的增强型形式化定理证明数据集，通过监督微调进一步优化。在此基础上，我们采用基于证明助手反馈的强化学习（Reinforcement Learning from Proof Assistant Feedback, RLPAF）方法进行持续精调。与 DeepSeek-Prover-V1 仅采用单次全证明生成的策略不同，我们提出 RMaxTS——一种基于内在奖励驱动探索策略的蒙特卡洛树搜索（Monte-Carlo Tree Search）变体，能够生成多样化的证明路径。实验结果表明，DeepSeek-Prover-V1.5 在性能上显著超越 DeepSeek-Prover-V1，在高中水平的 miniF2F 基准测试集上达到 63.5% 的新最优成绩，同时在本科水平的 ProofNet 基准测试集上也取得 25.3% 的新高分，刷新了当前最先进水平。