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

📄 arXiv: 2408.08152v1 📥 PDF

作者: Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, Chong Ruan

分类: cs.CL, cs.AI, cs.LG, cs.LO

发布日期: 2024-08-15

💡 一句话要点

DeepSeek-Prover-V1.5：利用证明助手反馈进行强化学习和蒙特卡洛树搜索，提升定理证明能力。

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)

关键词: 定理证明 强化学习 蒙特卡洛树搜索 形式化验证 语言模型 Lean 4 RMaxTS

📋 核心要点

  1. 现有定理证明模型在探索多样化证明路径方面存在不足，限制了其解决复杂问题的能力。
  2. 论文提出RMaxTS，一种基于内在奖励驱动的蒙特卡洛树搜索变体，旨在生成更多样化的证明路径。
  3. DeepSeek-Prover-V1.5在miniF2F和ProofNet基准测试上取得了显著提升，验证了所提出方法的有效性。

📝 摘要（中文）

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%）上取得了新的state-of-the-art结果，显著优于DeepSeek-Prover-V1。

🔬 方法详解

问题定义：论文旨在提升形式化定理证明的自动化水平，特别是在Lean 4证明助手中的应用。现有方法，如DeepSeek-Prover-V1，主要采用单次全证明生成策略，缺乏对不同证明路径的有效探索，难以应对复杂定理的证明。

核心思路：论文的核心思路是结合强化学习和蒙特卡洛树搜索，利用证明助手的反馈信号作为奖励，引导模型探索更有希望的证明路径。通过内在奖励机制鼓励模型发现新的证明策略，从而提高证明成功率。

技术框架：DeepSeek-Prover-V1.5的技术框架主要包含三个阶段：预训练、监督微调和强化学习。首先，在DeepSeekMath-Base上进行预训练，使模型具备基本的数学知识和形式化语言理解能力。然后，使用增强的定理证明数据集进行监督微调，提高模型生成有效证明的能力。最后，通过RLPAF和RMaxTS算法进行强化学习，进一步优化模型的探索策略。

关键创新：论文的关键创新在于RMaxTS算法，它是蒙特卡洛树搜索的一种变体，采用内在奖励驱动的探索策略。与传统的蒙特卡洛树搜索不同，RMaxTS不仅考虑外部奖励（证明助手的反馈），还引入了内在奖励，鼓励模型探索未知的证明路径，从而生成更多样化的证明。

关键设计：RMaxTS算法的关键设计包括内在奖励函数的设计和探索-利用平衡策略。内在奖励函数旨在衡量证明路径的新颖性和潜在价值。探索-利用平衡策略则需要在探索新的证明路径和利用已知的有效策略之间进行权衡。具体的参数设置和损失函数细节在论文中进行了详细描述，但具体数值未知。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

DeepSeek-Prover-V1.5在miniF2F基准测试的高中级别测试集上取得了63.5%的准确率，在ProofNet基准测试的本科级别测试集上取得了25.3%的准确率。相较于DeepSeek-Prover-V1，性能得到了显著提升，表明RMaxTS算法和RLPAF的有效性。

🎯 应用场景

该研究成果可应用于自动化定理证明、形式化验证、软件工程等领域。通过提高定理证明的自动化水平，可以减少人工干预，加速数学研究和软件开发过程。未来，该技术有望应用于更复杂的数学问题和更大规模的软件系统。

📄 摘要（原文）

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\%$).