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

关于AI的论文阅读。与Rob一起。让您了解最新的研究成果。此阅读由火星竞赛提供。在红色星球上获得赞誉。可在Android和iOS上使用。DeepSeek Prover V1.5。利用证明助手反馈进行强化学习和蒙特卡洛树搜索。

2024年作者:

辛瓦振、任子子、宋俊晓、肖继红、赵万义、王浩成、卢博、张李伟、卢湛、杜楚曦、高文俊、朱齐浩、杨迪建、戈子本、吴子峰、罗富丽、阮崇。

我们介绍了DeepSeqProver v1.5,这是一个为Lean 4中的定理证明而设计的开源语言模型,它通过优化训练和推理过程来增强DeepSeqProver v1。该模型在DeepSeqMathBase上进行预训练,专门用于形式化数学语言,并使用从DeepSeqProver v1派生的增强型形式化定理证明数据集进行监督微调。

通过来自证明助手反馈的强化学习进一步改进。除了DeepSeqProver v1的单次完整证明生成方法外,我们还提出了RmaxTS,这是一种蒙特卡洛树搜索的变体,它采用了一种内在奖励驱动的探索策略来生成不同的证明路径。

DeepSeq Prover v1.5 表明比 DeepSeq Prover v1 有显著改进,在高中水平的 Mini F2F 基准测试集上取得了新的最先进的结果(63.5%),以及在本科水平的 ProofNet 基准测试集上取得了新的最先进的结果(25.3%)。核心贡献者 1. 简介 1.1. 贡献

我们提出了一个开发基于语言模型的形式化数学证明器的综合框架,该框架集成了几个关键组件:大规模数学预训练、形式化数学语料库构建和增强、来自证明助手反馈的在线强化学习以及用于长期规划和定理证明的树搜索方法。

预训练模型、监督微调模型和强化学习模型以及蒙特卡洛树搜索算法的代码可公开用于进一步研究和应用。预训练。我们通过在高质量的数学和代码数据上进一步预训练来增强我们的基础模型在形式化定理证明和数学推理方面的能力,重点关注 Lean、Isabel 和 Metamath 等形式化语言。

监督微调。我们通过实现两种数据增强技术来改进 Lean4Code 补全数据集。首先,我们使用 DeepSeq coder V2-236B(Zhu 等人,2024)在 Lean4Code 旁边注释自然语言思维链注释,将形式化定理证明与自然语言推理对齐。

其次,我们在 Lean-4 证明代码中插入中间策略状态信息,使我们的模型能够有效地利用编译器反馈。然后使用结果数据集来微调预训练模型。强化学习 我们采用 GRPO 算法(Xiao 等人,2024)对监督微调模型进行来自证明助手反馈的强化学习 (RLPAF)。

来自 Lean Prover 的验证结果作为奖励监督,增强了模型与验证系统形式规范的一致性。蒙特卡洛树搜索 我们通过引入一种新的抽象和相应的搜索算法来推进形式化定理证明中的树搜索方法。我们的截断恢复机制充当状态-动作抽象,将树搜索过程无缝集成到整个证明生成框架中。

我们提出了 RMAX-TS,这是一种创新的蒙特卡洛树搜索算法,它利用 RMAX(Brafman 和 Tenenholz,2002)策略来解决稀疏奖励证明搜索问题中的探索挑战。通过分配内在奖励,该算法鼓励证明代理生成不同的规划路径,从而促进对证明空间的广泛探索。

1.2 评估和指标摘要 Mini F2F 在单次完整证明生成设置中,DeepSeq Prover V1.5 在 Mini F2F 的测试集上实现了 60.2% 的通过率,比 DeepSeq Prover V1 的 50.0% 提高了绝对 10.2 个百分点。结合树搜索技术进一步将通过率提高到新的最先进水平 63.5%。

ProofNet。DeepSeat Prover v1.5 在 ProofNet 的单次完整证明生成设置中也表现出强大的性能,验证集的通过率为 21.6%,测试集的通过率为 23.7%。树搜索技术的集成进一步增强了这些结果,在验证集上实现了 25.4% 的新的最先进通过率,在测试集上实现了 25.3% 的新的最先进通过率。2. 模型训练。2.1.

预训练。为了增强我们的语言模型生成形式化证明和通过数学语言进行推理的能力,我们进一步预训练了我们的基础模型(Xiao 等人)。此改进包括在包含代码和自然语言数学内容的高质量数据集上进行训练。我们特别关注在证明辅助中广泛使用的形式化语言,例如 Lean、Isabelle 和 Metamath。我们将此改进的模型指定为 DeepSeqProver v1.5 base。

2.2 监督微调 在本节中,我们将探讨 DeepSeqProver v1.5 监督微调中涉及的方法和过程。具体来说,我们通过添加详细的解释性注释来增强 DeepSeqProver v1 的证明数据集。此增强旨在提高自然语言描述和 lean-for 代码之间的一致性,从而促进更好的形式化数学推理。

此外,我们还结合了中间策略状态。训练设置。我们基于预训练模型进行监督微调,并训练 90 亿个标记,使用 2048 的批量大小和 1E4 的恒定学习率。训练过程从 100 个预热步骤开始,以稳定学习动态。训练示例随机连接以形成序列,最大上下文长度为 4096 个标记。

2.3 来自证明助手反馈的强化学习 强化学习已被证明可以有效地增强监督微调语言模型的数学推理能力。为了进一步推进 DeepSeqProver v1.5-SFT,我们加入了强化学习阶段,从而产生了模型 DeepSeqProver v1.5-RL。

此阶段利用 RL 根据来自 Lean4 证明器的验证反馈来增强性能。此 RL 过程的细节如下所示。提示 在强化学习阶段,我们使用监督微调数据集中的定理语句子集作为训练提示。我们选择 DeepSeqProver v1.5 SFT 在多次尝试后能够生成正确证明的定理。

这确保了模型有改进的空间,同时仍然能够获得积极的反馈。过滤后,我们保留了大约 4.5K 个独特的定理语句。每个定理都以 COD 和非 COD 指导提示为前缀,以增强模型在两种模式下的证明生成能力。奖励 当通过 RL 训练 LLM 时,训练好的奖励模型通常会提供反馈信号。

相反,形式化定理证明受益于证明助手对生成的证明的严格验证,这具有显著优势。具体来说,如果生成的证明被验证为正确,则获得 1 的奖励,否则获得 0 的奖励。虽然此二元奖励信号是准确的,但它也是稀疏的,特别是对于监督微调模型难以处理的定理而言。

为了减轻这种稀疏性,我们选择对监督微调模型具有挑战性但可实现的训练提示,如上所述。强化学习算法。我们采用组相对策略优化 (GRPO)(Xiao 等人,2024)作为我们的 RL 算法,该算法已被证明比 PPO(Schulman 等人,2017)具有更高的有效性和效率,主要是因为它消除了训练额外评论家模型的必要性。

具体来说,GRPO 为每个定理提示采样一组候选证明,并根据组内输出的相对奖励来优化模型。我们的提示选择策略旨在使候选者中可能同时包含正确和不正确的证明,这与 GRPO 的组相对性质非常吻合,从而增强了训练过程。

训练设置。我们基于 SFT 模型进行 RL 训练,该模型既作为初始模型,也作为施加 Kolbach-Leibler 散度惩罚的参考模型。我们使用 5E6 的恒定学习率,KL 惩罚系数设置为 0.02。对于每个定理,我们采样一组 32 个候选证明,最大长度设置为 2048。训练批量大小配置为 512。2.4. 评估。

基准。我们在以下基准上评估定理证明性能,以比较每个训练阶段后的模型能力。Mini F2F。Jung 等人,2022。侧重于高中水平练习和竞赛(如 AMC、AMI 和 EMO)的形式化问题解决能力,重点是代数和数论。

该基准包括 244 个验证问题和 244 个测试问题,最初为 Lean 3,并根据 Young,2023 提供的版本手动转换为 Lean 4.9.0。ProofNet,Azarbayev 等人,2023,评估本科水平数学的形式化定理证明能力。

它包含来自广泛使用的本科教科书的 185 个验证问题和 186 个测试问题,涵盖实分析和复分析、线性代数、抽象代数和拓扑学。这些问题最初为 Lean 3,并手动转换为 Lean 4.9.0。提示配置 对于 DeepSeqProver v1.5 base 的每次证明尝试,我们独立地从验证集中采样三个证明演示来构建少样本提示。

对于 Mini F2F 基准,我们使用来自 YONG 2023 的人工编写的证明,而对于 ProofNet 基准,我们使用 DeepSeqProver v1.5 RL 生成的正确证明作为少样本演示。对于 DeepSeqProver v1.5 SFT 和 DeepSeqProver v1.5 RL,我们采用两种类型的指导提示,一种鼓励思维链 (caught) 在每个证明步骤之前进行推理,另一种则不鼓励 (non-caught)。

附录 A 中提供了详细示例指标。我们使用通过 K 准确性指标评估定理证明性能,该指标衡量模型在 K 次尝试内生成正确证明的成功率。每个模型都部署在一个单一的 A100-40G GPU 上,利用 VLLM 框架(Kwan 等人,2023)进行样本生成。

采样参数设置为温度为 1,顶部 p 值为 0.95,最大标记限制为 2048。然后使用 Lean-4 定理证明器验证生成的证明。对于此验证,我们导入 MATHLIB4、MATHLIB Community,2020 和 ESOP、LIMPURG 和 FRUM,2023,以访问预定义的前提和策略。验证过程的时限为 300 秒。

跨训练阶段的比较。图 3 显示了 Mini F2F 和 ProofNet 数据集上每个训练阶段的比较分析。我们的基础模型 DeepSeqProver v1.5 Base 达到了显著的通过率,使用三样本提示解决了 Mini F2F 基准测试集上近三分之一的问题。

监督微调阶段(产生 DeepSeqProver v1.5-SFT)的性能明显优于基础模型,通过 1.28 准确率在 MiniF2F 上增加了大约三分之二,在 ProofNet 上增加了一倍。随后的强化学习阶段进一步增强了模型的性能,提高了通过 K 的准确率。

所有 K 值的准确性。与自然语言数学中的发现(例如 DeepSeat Math 中报道的发现,Xiao 等人,2024)相反,在自然语言数学中,强化学习主要提高了前 K 个正确答案的比例,我们观察到形式化定理证明中基本能力的真正增强。这种改进不仅在样本预算较小的情况下很明显,而且随着样本预算的增加仍然保持稳定。

这一结论得到了后面具有更大样本预算的蒙特卡洛树搜索实验的进一步支持,如第 4.2 节所述。COD 和非 COD 之间的比较 我们比较了 DeepSeqProver V1.5 SFT 和 DeepSeqProver V1.5 RL 的非 COD 和 COD 生成模式的性能。图 3 中的结果表明,COD 模式在大多数设置中始终优于非 COD 模式。

具体来说,DeepSeq Prover v1.5 RL 利用这些增强的定理证明模式,在两个基准测试中都取得了优异的性能,MiniF2F 的平均准确率为 51.6%,ProofNet 的平均准确率为 18.2%。COD 模式中自然语言推理的集成显着增强了形式化证明写作的规划和执行。

有关使用和不使用自然语言思维链的证明策略的详细比较,请参阅附录 A3 中提供的示例。面向探索的蒙特卡洛树搜索 3.1. 策略级树抽象。为了在整个证明生成设置中实现树搜索方法,我们引入了一种证明树抽象来定义定制的状态和动作空间,并利用截断和恢复机制。

大致遵循 Yao 等人,2023 的范例,我们首先将不完整的证明分解成一系列对应于单个证明步骤的树节点,然后利用存储在这些树节点中的部分内容来继续证明生成过程。图 4 说明了从整个证明生成中构建证明搜索树的过程。

截断。将证明分解成树节点。我们在策略级别构建证明搜索树,其中每条树边代表策略状态的单个转换步骤。最初,我们将模型生成的整个证明提交给 lean 证明器以将其解析为策略。然后,我们在最早的验证错误处截断证明,确保所有后续策略代码都可以成功应用于将证明推进到所需的定理。

策略代码被分割成几个代码片段,每个片段包含一个有效的策略代码及其相关的思维链注释,对应于表示策略状态转换的单个树边。通过这种抽象,每个策略代码都被转换成一系列树节点,形成从根到特定节点的路径。

恢复。从树节点生成证明。在 Lean 4 中,不同的策略可以导致相同的策略状态,这意味着我们证明树中的每个节点都可以对应于实现相同结果的各种策略代码。为了处理这个问题,我们在每个节点存储这些等效策略代码的集合。当树搜索代理扩展节点时,它会随机选择一个策略作为语言模型的提示。

此提示包括以选择的策略结尾的不完整证明代码以及来自 lean 证明器的策略状态信息作为注释块。微调模型(参见第 2.2 节)已接受过训练以识别和使用此格式,使用增强了策略状态注释的不完整代码来指导后续的证明生成。

3.2 通过蒙特卡洛树搜索进行交互式定理证明 我们的证明搜索树是使用标准蒙特卡洛树搜索范例开发的。Coulomb,2006。Brown 等人,2012。它迭代地应用四个步骤:选择、扩展、模拟和反向传播。我们将模拟步骤集成到扩展中,因为我们的整个证明生成模型本质上是从扩展节点进行展开。

算法工作流程的详细设计如下:选择步骤(又名树策略)从根节点开始向下遍历,以识别一个有希望扩展的节点。此算法步骤的目标是在探索和利用之间进行权衡。树节点 S 处的树策略是通过选择最大化来自有效操作集的值的动作来计算的,

TREPOLICY = arg max C HildRen S union /Q UCB S A 1 其中 Q 表示从选择历史派生的动作值的基于样本的估计,充当从先前试验中检索高价值候选者的利用组件。

UCB-S-A 表示通过上限置信界 (UCB-H-2002) 计算的探索奖励,随着状态-动作对 (S-A) 的重复执行而减小。更具体地说,QUCB-S-A 代表 Q-S-A 的乐观估计,并且可以作为具有高概率的上限。我们将节点值和 UCB 奖励的详细设置的讨论推迟到第 3.3 节。

扩展。下一步是调用证明生成模型来扩展选择阶段提名的节点。恢复存储在指定用于扩展的节点上的不完整证明代码,我们执行整个证明生成以提出一系列后续策略,并将生成的证明提交给 LeanProver 进行验证。这种证明完成的尝试相当于在标准 MCTS 框架内进行单次展开模拟。

当验证结果表明证明已完成时,搜索过程已准备好终止,因为它找到了所需定理的新证明。否则,我们将解析验证反馈并将生成的证明截断到最早验证错误的断言。其余策略将转换为要合并到搜索树中的节点路径。

重要的是要注意,因为我们使用整个证明生成设置,其中输出是包含一系列策略的整个证明,而不仅仅是下一个策略,所以我们的扩展过程可能会在每次迭代中将树节点路径插入到搜索树中。这与为竞争性游戏设计的传统 MCTS 不同,后者通常每次迭代只扩展一层子节点。Silver 等人,2016-2018。Schrittweiser 等人,2020。

反向传播,每次树搜索迭代的最后阶段是更新从根到扩展节点的选择轨迹上的值统计信息,即更新等式 1 中所述的树策略相关的值。令 tau 等于根 S1S1S2S2S3。

S tau 减 1 等于 ST。圆除法斜杠表示 TTH 迭代的选择轨迹,以 ST 作为扩展节点结束。我们通过考虑最新的轨迹奖励 R tau 来更新 tau 中所有 SA 元素的 QUCB SA,详细信息参考等式。

7. 奖励的外部来源来自编译器反馈,具体来说,对于完成的证明分配奖励 R_Extrinsic = 1,对于未解决的证明分配奖励 R_Extrinsic = 0。在第 3.3 节中,我们将介绍一种内在奖励机制来增强奖励分配,从而增强代理对探索的激励。

3.3. 蒙特卡洛树搜索的内在奖励 在形式化定理证明的搜索问题中,外部奖励极其稀疏,即,只有在证明完全解决时,搜索代理才能获得非零奖励。更具体地说,证明搜索过程形成一个树结构,只有少数叶子节点提供非零奖励,这与统计强化学习文献中著名的硬探索案例相匹配,Krishnamurti 等人,2016。

为了促进稀疏奖励顺序决策中的探索,一个经典的范例是构建内在奖励(Schmidhuber,2010),鼓励代理不仅优化外部奖励,而且还获取有关交互环境的一般信息(Bellemere 等人,2016,Huthuf 等人,2016,Podik 等人,2017,Berda 等人,2019)。

在本节中,我们将介绍我们应用于树搜索的内在奖励驱动的探索算法 R-Max,即 R-Max TS,以在证明搜索问题中结合无奖励探索。应用于 MCTS 的 R-Max。我们采用 R-Max(Brafman 和 Tenenholz,2002),这是一种经典的探索机制,为蒙特卡洛树搜索构建内在奖励。R-Max 的核心思想是探索状态空间的广泛覆盖范围。

代理在到达未见状态时会奖励自己最大数量的奖励。在证明搜索的上下文中,在证明完成之前不会提供外部奖励,我们的算法过程类似于 0Rmax(Jin 等人,2020),其中代理的探索完全由内在奖励驱动,即设置 R,tau,等于 R 内在,tau。

树扩展步骤的内在奖励取决于是否将新节点添加到搜索树中。r_intrinsic = i,至少有一个新节点添加到搜索树中。3. 其中 tau 表示需要为反向传播分配奖励的最新选择轨迹。这种探索策略优先扩展证明模型生成导致各种策略状态的策略的节点。

由于多个 lean 代码可以导致中间状态的相同转换,因此这种启发式方法可以潜在地减少冗余生成并提高样本效率。用于非平稳奖励的 UCB。蒙特卡洛树搜索的 UCB 探索奖励的常见设置是使用 UCB 1(Hour at All,2002)。

其中 gamma 等于 tau 元素 tau 表示包含作为中间选择步骤的树策略轨迹 tau 的列表。为了便于讨论,我们组织列表 gamma 等于 tau,以便新收集的轨迹具有较大的下标索引。在这项工作中,我们建议使用 UCB 方法的替代变体。

请注意,等式 3 中导出的内在奖励是非平稳奖励信号,其期望值随着探索的进展而衰减。这是因为随着搜索树通过复杂的探索而扩展,发现具有未见策略状态的新节点肯定变得更加困难。

为了解决非平稳性,我们考虑折扣上限置信界 (DUCB)(Garavir 和 Mollins,2011),它使用折扣因子 gamma 元素 0, 1 来平滑地丢弃那些过时的反馈记录,其中新接收的反馈将在值估计中分配更大的权重。

在实践中,我们说 gamma 等于 0.99。请注意,DUCB 中的折扣因子 gamma 的作用与其在无限范围 MDP 的值迭代中的作用不同。折扣应用于树搜索迭代,而不是应用于单个轨迹内的动作步骤范围。

3.4 蒙特卡洛树搜索的并行化 为了提高蒙特卡洛树搜索的效率,我们实现了 Chaslott 等人描述的几种已建立的并行化技术。我们在每个节点部署 256 个 MCTS 运行器,每个 GPU 一个语言模型,证明生成的批量大小为 512。

lean 证明器是通过 REPL 调用的,并在具有数千个 CPU 内核的集群上执行,其中每个证明验证任务都由一个单独的进程处理,在沙箱中创建和终止。语言模型的证明生成和 lean 证明器的验证都是异步处理的。此设置允许 MCTS 运行器执行并发树搜索操作,从而显着加快该过程。

树并行化 我们使用 32 个线程工作器来管理每个搜索树,以并行化树迭代步骤。这种方法有效地调度和平衡了证明生成和 lean 验证的任务。每个线程工作器通过选择要扩展的候选节点、调用语言模型生成证明、使用 lean 证明器验证生成的证明以及执行反向传播来迭代地执行树搜索循环。

虚拟损失。为了鼓励并发线程工作器之间进行多样化的节点选择,我们为正在进行的迭代分配虚拟奖励 r 等于零。这涉及暂时激发零奖励的反向传播并将其在完成时更新为真实奖励。这种策略促进了对不同节点进行扩展的探索,从而提高了整体搜索效率。

3.5. 与现有方法的比较。在形式化数学证明搜索中使用语言模型的方法通常分为两种主要策略。多遍证明步骤生成。这种策略将证明过程分解成多个策略生成和验证的片段,通常遵循树搜索模式。它涉及一次生成和验证一个策略,对下一个策略重复此过程,直到没有证明目标为止。

值得注意的例子包括 GPTF(Polu 和 Sutskever)、Polu 等人的 Thor、Jong 等人的 Reprover、Yong 等人的 Hypertree 证明搜索、Lample 等人的内部 LM2 步骤证明器、Woo 等人。单遍完整证明生成 这种方法尝试一次生成和验证整个证明

如果证明不正确,则模型在下次尝试中生成新的证明。此类别中的方法包括 DSP(Zhang 等人)、SubGolProver(Zhao 等人)、LegoProver(Wang 等人)、Lyra(Zheng 等人)和 MiniCTX(Hu 等人)。我们的证明树搜索方法独特地桥接了这两种策略,提供了一种新颖的混合方法。

它从整个证明生成开始,类似于单遍方法,但通过实现复杂的截断和恢复机制来扩展此方法。此过程涉及将生成的证明截断到其成功的初始段,将此段解析成单个策略,并从此点恢复树搜索。此迭代过程有效地实现了蒙特卡洛树搜索,将单遍完整证明生成与多遍证明步骤生成无缝集成。

因此,我们可以训练一个具有几乎相同目标的单一模型来同时支持这两种策略。我们的实验结果表明,这种统一方法在这两种设置中都取得了优异的性能。通过结合现有方法的优势并引入创新技术,我们的方法为形式化数学证明搜索提供了一种更通用和有效的解决方案,这可能为该领域的未来发展铺平道路。4. 实验结果

在本节中,我们将使用两个不同的基准评估 DeepSeqProver v1.5 的定理证明能力:MiniF2F,它包含高中水平的练习和竞赛问题;ProofNet,它涉及本科水平的定理。我们将介绍完整证明生成和蒙特卡洛树搜索方法的结果,使用与第 2.4 节相同的训练模型和推理配置,以确保一致性。4.1

主要结果。我们对 DeepSeqProver v1.5 与之前的最先进语言模型进行了比较分析,突出了其性能和进步。通用模型。GPT 3.5 和 GPT 4(OpenAI,2023)是 OpenAI 开发的先进生成式 AI 模型,以其在各种任务(包括代码生成)中的有效性而闻名。

尽管这些模型并非专门为定理证明而设计,但其庞大的参数规模赋予了它们显著的能力。Kopra、Thacker等人2023年提出的基于上下文学习的代理,利用这些大型语言模型提出策略应用,促进了这些模型在形式化定理证明中的评估。此外,我们还研究了Lema,Azarbayev等人2024年提出的系列

在广泛的通用数学语料库上训练的语言模型,通常用作形式化定理证明的基础模型。形式化数学的专用模型:GPTF、POLU和Sutskever,2020。POLU等人,代表了将Transformer应用于定理证明任务的证明步骤生成的初步尝试,利用最佳优先搜索模块构建完整的证明。

后续进展包括Reprover,Yong等人,2023年,LLM-STEP,Wellick & Saha,2023年,以及LeanStar,Lin等人,2024年。超树证明搜索,Lample等人,2022年,探索了在使用Lean的形式化定理证明中使用蒙特卡洛树搜索。

同时进行的工作,Intern LM2 Math,Ying等人,和Intern LM2 Stebb Prover,Wu等人也展现了优异的性能。指标 我们使用Pass at K准确率指标比较DeepSeq Prover V1.5与最先进模型的性能,该指标评估模型在K次尝试内生成正确证明的能力。

我们根据以下规则显示样本预算K,以使不同生成方案的计算预算保持一致。对于单次通过采样方法,我们将样本预算K定义为生成的证明总数,对于与树搜索方法进行比较的方便性,较大的K值被分解。对于最佳优先搜索方法,遵循Azarbayev等人2024年的符号,我们提出

k = n*s*t,其中n表示最佳优先搜索尝试次数,s表示每次扩展生成的策略数量,t表示扩展迭代次数。对于树搜索方法,例如Rmax TS和HTPS,Lampel等人2022年,我们提出k = n*t,其中n表示树搜索尝试次数,t表示在树扩展中调用的模型生成次数。

Mini F2F结果 表1提供了各种定理证明方法在Mini F2F测试数据集上的比较分析。在单次通过完整证明生成设置中,DeepSeqProver v1.5 RL实现了最高的通过率60.2%,比DeepSeqProver v1的50.0%提高了10.2个百分点。

在样本预算限制为128次尝试的情况下,DeepSeqProver v1.5 RL证明了51.6%的问题,显著优于其他完整证明生成方法,并且与领先的树搜索方法相当。在树搜索方法类别中,DeepSeqProver v1.5 RL+Rmax TS以62.7%的通过率领先,创造了新的最先进水平,并与现有方法之间形成了显著差距。

值得注意的是,DeepSeat Prover v1.5 RL只需要3200次完整证明生成采样就能达到54.9%的通过率,超过了之前的最先进结果InternLM两步证明器,后者执行64×3200次树搜索才能在ProofNet上达到54.5%的结果。表2提供了各种定理证明方法在ProofNet数据集上的比较分析。

DeepSeq Prover v1.5 RL在单次通过完整证明生成设置中以及通过增强RMAX TS分别实现了22.6%和25.3%的整体ProofNet数据集通过率。这些结果超过了现有的最先进方法Reprover,13.8%,和Intern LM2 StepProver,18.1%。

当完整证明生成尝试次数限制为3200次时,DeepSeq Prover v1.5也证明了21.7%的定理,比之前的最先进的Intern LM2 step prover提高了3.6%。

方法 样本预算 Proof Net 验证集 测试集 全部 单次通过完整证明生成方法 DeepSeat Prover V1.5 Base 128 6.6% ± 0.9% 9.7% ± 0.7% 7.5% ± 0.7% 3,210.8% 15.6% 13.2%

DeepSeek Prover V1.5 SFT 128 19.9% ± 0.4% 15.9% ± 0.6% 17.9% ± 0.3% 3,220.7% ± 0.7% 21.0% ± 0.9% 20.9% ±

0.6% 4 × 6422.2% 23.7% 22.9%

Deep Seat Prover V1.5 RL 128 20.1% ± 0.5% 18.2% ± 0.5% 19.1% ± 0.4% 3,221.4% ± 0.3% 22.0% ± 0.5% 21.7%

± 0.4%,4 × 6421.6%,23.7%,22.6%。树搜索方法。Reprover,参考文献55,13.8% Intern LM2 step prover,参考文献52,1 × 32 × 118.1%。

DeepSeat Prover V1.5 SFT + R-Max TS 1 × 3,222.2% ± 0.7% 21.6% ± 0.2% 21.9% ± 0.4% 4 × 6,423.8% 25.8% 24.8%

DeepSeq Prover v1.5 RL + R max TS 1 × 3,222.0% ± 0.3% 21.5% ± 0.8% 21.8% ± 0.4% 4 × 6,425.4% 25.3% 25.3% 表2. 与ProofNet数据集上最先进技术的比较。

请注意,ProofNet的验证集用于在监督微调中执行专家迭代。4.2. 重新审视大型样本训练策略的有效性。我们重新审视了N/A大型样本设置中几个训练模块的影响,重点关注单次通过完整证明生成和蒙特卡洛树搜索。结果表明,第2.4节中提出的观察结果和发现可以推广到具有大型样本大小的采样场景。

强化学习的总体增强 为支持在线强化学习从验证反馈中通常增强模型能力的说法,我们使用大型样本预算将最终模型与仅SFT版本进行比较。比较结果以表3中的两列显示。DeepSeqProver v1.5 RL在所有生成设置中始终优于SFT模型,无论是否应用思维链策略。

结果还表明,通过进行在线RL获得的改进与通过RMAX TS获得的改进是正交的,可以进一步结合以提高性能。通过集成COD提示和RMAX TS,DeepSeq Prover v1.5 RL在Mini F2F测试中实现了62.7%的通过率。

此性能比SFT模型提高了3.7%,突出了强化学习在增强证明完成模型整体有效性方面的关键作用。COT、非COT和混合策略 我们比较了两种生成模式,即非COT和COT,在MiniF2F测试数据集上的性能。表3所示的结果表明,随着样本预算的增加,COT相对于非COT模式的优势被放大。

这表明,结合自然语言思维链可以使定理证明的规划路径多样化,可能导致更广泛的推理策略和更具创新性的解决方案。

结果还表明,这两种模式在不同问题上具有互补的优势。模型在COT模式下的定理证明策略在数学思维上更加系统和主动,而在非COT模式下,模型可以有效地使用Lean高级策略来解决可以在Lean的自动化机制内解决的计算问题。

为了利用这些优势,我们考虑了一种混合策略,在表3中用非COT和COT表示,将一半的样本预算分配给COT模式,其余的分配给非COT模式。这两种引导提示的简单组合在进一步提升证明完成模型的性能方面显示出巨大的前景,在Mini F2F测试中实现了63.5%的通过率。在附录B中,我们展示了说明这两种生成模式不同优势的示例问题。

4.3. 关于R-Max TS的消融研究。内在奖励和折扣UCB。我们研究了R-Max TS的两个核心组件的有效性,即EQ中定义的内在奖励。3.和EQ中陈述的折扣上限置信界限。

7. 我们首先实现一个使用标准UCT算法的基线,Kochish和Zepesvari,2006年,没有内在奖励,其中探索完全由UCB奖励驱动。请注意,由于没有为该基线提供非零奖励,因此UCB公式的所有变体都变得等效,因为节点选择完全由访问计数决定。

图5中的实验结果表明,在没有内在奖励的情况下,没有R内在的UCT的性能退化为与非搜索方法相当的水平。此外,我们考虑使用标准UCB1的R max TS,参考EQ。对于,而不是折扣UCB,表示为R max TS,dUCB → UCB1,

结果表明,使用UCB1奖励的Rmax TS的性能也中等,与没有R内在的UCT相当。这是因为UCB1旨在通过详尽的探索来保证渐近性能,R等人,2002年,假设样本量足够大。

相反,折扣UCB可以加速非平稳内在奖励的值传播,防止R内在的指导被访问计数的指导所支配。这表明折扣UCB机制是对内在奖励驱动探索的关键补充。策略状态信息的指导 在扩展树节点时,我们将中间策略状态信息作为注释块连接到不完整的代码中,以指导证明完成。

通过提供的辅助信息,证明完成模型可以增强其对策略状态的内部表示,为长范围规划提供中间指导。为了证明这种优势,我们对直接从原始不完整代码进行代码完成而无需访问策略状态信息的Rmax TS进行了实验,表示为Rmax TS。在图5中没有策略状态。

结果表明,在没有策略状态信息的情况下,通过应用树搜索获得的性能变得中等,尤其是在处理需要大量样本的难题时。这突出表明,编译器信息的集成是树搜索算法的一个重要组成部分,增强了其整体有效性和样本效率。

5. 结论、局限性和未来工作 我们提出了DeepSeqProver v1.5,这是一个具有70亿参数的语言模型,它在Lean 4的形式化定理证明中优于所有开源模型。DeepSeqProver v1.5由DeepSeqProver v1.5 base初始化,后者使用形式化数学推理的专用语料库扩展了DeepSeqMathBase 7b的预训练。

监督微调是在一个全面的Lean-4代码完成数据集上进行的,该数据集包含来自各个数学领域的各种形式化定理。随后,我们使用GRPO通过在线强化学习来增强完整证明的生成。在开发DeepSeqProver v1.5模型后,我们引入了RMAX-TS,这是蒙特卡洛树搜索的一个变体,以通过大规模搜索和广泛的探索来提高问题解决能力。

这些组件形成了一个用于训练基于LLM的证明助理的综合管道,使DeepSeqProver v1.5能够比DeepSeqProver v1取得显著改进。DeepSeqProver v1.5的框架旨在为形式化定理证明建立一个类似AlphaZero的管道。专家迭代和合成数据的使用反映了强化学习的核心试错循环,编译器Oracle作为世界模型提供环境监督。

在RL范式中,集成的树搜索模块已被证明在提高各个领域的超人类性能方面非常有效:Silver等人,Fawzi等人,Lutz等人。在开发DeepSeq Prover v1.5时,我们专注于RL的探索方面,引入Rmax TS以使证明步骤的生成多样化。

然而,开发方面,特别是证明搜索问题,仍然未被探索。一个有前景的未来方向是训练一个评论家模型来评估不完整的证明并修剪搜索分支。这种部分证明评论家模型将隐式地执行时间信用分配,突然,1984年,将证明级别的反馈分解为逐步的值差异,Arjona-Medina等人,2019年。

开发用于评估长期规划路径并提供指导奖励的评论家模型是一个至关重要且具有挑战性的问题,Ng和Russell,2000年。Sorg等人,2010年。这值得进一步研究。最后,最近的工作已经超越了证明单个定理,转向在复杂的多定理Lean文件中处理现实世界的理论证明。Hu等人,2024年。这种转变是我们完整证明生成方法的自然延伸。

我们的观察结果表明,当前模型已经对文件级上下文有一定的理解。展望未来,我们将专注于增强这方面,以支持使用我们的语言模型进步来支持尖端的Lean数学形式化开发人员。参考文献 参考文献1. J. A. Arjona Medina、M. Gilhofer、M. Widrick、T. Untertheiner、J. Brandstetter和S. Hochreiter

Rutter。延迟奖励的回报分解。在第33届神经信息处理系统国际会议论文集中。第13566-13577页,2019年。参考文献2. P. Auer。使用置信界限进行开发探索权衡。机器学习研究杂志。3,11月,397-422,2002年。

参考文献3. P. Auer、N. Cessa Bianchi和P. Fischer。多臂老虎机问题的有限时间分析。机器学习,47. 235-256,2002年。参考文献4. Z. Azerbaev、B. Piotrowski、H. Sholkoff、E. W. Ayers、D. Radev和J. Avigod。

ProofNet。自动形式化和正式证明本科水平的数学。档案预印本档案。2302.12433,2023年。参考文献5. Z. Azarbayev、H. Sholkoff、K. Paster、M. Dos Santos、S. M. McAleer、A. Q. Zhang、J. Deng、S. Biderman和S. Wellick。

Lemma。一个用于数学的开放语言模型。在第12届国际学习表征会议上,2024年。参考文献6. M. G. Bellemare、S. Srinivasan、G. Ostrovsky、T. Scholl、D. Saxton和R. Munoz。统一基于计数的探索和内在动机。在第30届神经信息处理系统国际会议论文集中,第1479-1487页,2016年。

参考文献7. R. I. Brafman和M. Tenenholz。R. Max一种用于近似最优强化学习的通用多项式时间算法。机器学习研究杂志。3,10月,213-231,2002年。参考文献8. C. B. Brown、E. Powley、D. Whitehouse、S. M. Lucas、P. I. Cowling、P. Rolfshagen、S. Tavener、D. Perez、S. Samothrakis和S. Colton。

蒙特卡洛树搜索方法综述。IEEE计算智能与AI在游戏中的汇刊,4,1,1-43,2012年。参考文献9. Y. Berda、H. Edwards、Istaki和Oklemov。通过随机网络蒸馏进行探索。在第7届国际学习表征会议上,第1-17页,2019年。

感谢您收听本次朗读。如需全文及更多内容,请访问我们的主页。