DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search

我们介绍了DeepSeek-Prover-V1.5，这是一个开源的语言模型，专门为Lean 4中的定理证明而设计，通过优化训练和推理过程来增强DeepSeek-Prover-V1。该模型在DeepSeekMath-Base上进行了预训练，专门针对正式数学语言进行了优化，然后使用从DeepSeek-Prover-V1衍生的增强形式定理证明数据集进行监督微调。通过证明助手反馈的强化学习（RLPAF），进一步对模型进行了优化。除了DeepSeek-Prover-V1的单遍完整证明生成方法，我们提出了RMaxTS，这是一种蒙特卡罗树搜索的变体，采用内在奖励驱动的探索策略来生成多样的证明路径。DeepSeek-Prover-V1.5比DeepSeek-Prover-V1有了显著的提升，在高中水平的miniF2F基准测试的测试集上实现了新的最先进结果（63.5%），并在本科水平的ProofNet基准测试中取得了25.3%的成绩。

DeepSeek-Prover-V1.5的问题是优化DeepSeek-Prover-V1的训练和推理过程，提高定理证明的准确率和效率。

DeepSeek-Prover-V1.5使用了预训练的语言模型和增强的正式定理证明数据集进行监督微调，同时通过强化学习从证明助手反馈中进行进一步的优化。此外，论文提出了一种基于蒙特卡罗树搜索的证明路径生成策略，可以生成多样化的证明路径。

DeepSeek-Prover-V1.5在高中和本科级别的基准测试中取得了新的最优结果，分别为63.5%和25.3%。此外，论文还开源了代码和数据集，并提供了一个值得深入研究的方向，即如何进一步提高证明路径生成的效率和准确率。

近期的相关研究包括：1）Transformer-based语言模型在自动定理证明中的应用；2）基于强化学习的证明搜索策略的研究；3）使用深度学习方法进行数学问题求解的研究。