摘要

我们介绍了DeepSeek-Prover-V1.5，这是一款为Lean 4定理证明设计的开源语言模型，通过优化训练和推理过程，对DeepSeek-Prover-V1进行了增强。该模型在DeepSeekMath-Base上预训练，并专注于形式数学语言，随后使用从DeepSeek-Prover-V1派生的增强型形式定理证明数据集进行监督微调。此外，通过从证明助手反馈中进行强化学习（RLPAF），进一步提升了模型的性能。除了DeepSeek-Prover-V1采用的一次性全证明生成方法外，我们还提出了一种名为RMaxTS的蒙特卡洛树搜索变体，该方法采用内在奖励驱动的探索策略来生成多样化的证明路径。DeepSeek-Prover-V1.5在高中水平的miniF2F基准测试集（63.5%）和大学本科水平的ProofNet基准测试集（25.3%）上展示了显著的改进，取得了新的最先进成果。