DeepSeek团队近日发布了一款名为DeepSeek-Prover-V1.5的开源数学大模型，该模型在高中和大学级别的定理证明任务上取得了新的SOTA（State of The Art）成果。
DeepSeek-Prover-V1.5是一个基于语言模型的定理证明器，旨在解决形式化数学中的定理证明问题。它通过优化训练和推理过程，在DeepSeek-Prover-V1的基础上进行了改进。该模型在DeepSeekMath-Base上进行了预训练，并使用增强的形式化定理证明数据集进行了监督微调。此外，它还通过强化学习从证明助手反馈（RLPAF）中进行了进一步的优化。
DeepSeek-Prover-V1.5引入了一种名为RMaxTS的Monte-Carlo树搜索变体，该变体采用内在奖励驱动的探索策略来生成多样化的证明路径。与DeepSeek-Prover-V1相比，DeepSeek-Prover-V1.5在高中级别的miniF2F基准测试集上取得了63.5%的通过率，在大学级别的ProofNet基准测试集上取得了25.3%的通过率，显著提高了性能。
DeepSeek-Prover-V1.5的成功得益于其综合的框架，该框架结合了大规模的数学预训练、形式化数学语料库的构建和增强、基于证明助手反馈的在线强化学习以及用于定理证明的树搜索方法。该模型的预训练版本、监督微调版本和强化学习版本，以及Monte-Carlo树搜索算法的代码，都已公开发布，供进一步研究和应用。
然而，DeepSeek-Prover-V1.5也存在一些局限性。首先，尽管它在高中和大学级别的定理证明任务上取得了显著的成果，但在更复杂的数学问题上，如研究生级别的定理证明，其性能可能受到限制。其次，DeepSeek-Prover-V1.5的训练和推理过程可能需要大量的计算资源和时间，这可能限制了它的实际应用。
