我们介绍了DeepSeek-Prover-V1.5，这是一种为精益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%）的测试集上取得了最新的最先进的结果
大型语言模型的最新进展对人工智能中的数学推理和定理证明产生了重大影响。尽管在自然语言领域取得了显著进展，但语言模型在形式定理证明方面仍面临重大挑战，例如使用Lean（Moura和Ullrich，2021）和Isabelle（Paulson，1994），这需要满足验证系统形式规范的严格推导。即使是像GPT-4（OpenAI，2023）这样的高级模型也难以处理复杂的形式证明，这突显了所涉及的编码和数学的复杂性。一个形式化的定理证明模型不仅必须掌握像Lean定理证明器这样的形式化系统的语法和语义，还必须将抽象的数学推理与精确的形式表示对齐。形式定理证明中的语言模型通常采用两种策略：校对步骤生成（Polu和Sutskever，2020；Jiang等人，2022；Lample等人，2022年；Yang等人，2023；Wu等人，2024）和整体证明生成（Jiang等人。证明步骤生成预测每个后续策略，并使用形式验证器对其进行验证，以获得有关当前策略状态的更新信息，通常利用树搜索技术构建有效的证明。相比之下，整个证明生成在计算上是高效的，它基于定理语句生成整个证明代码，需要较少的通信预算来协调证明者模型和形式定理验证器之间。虽然DeepSeek-Prover-V1（Xin等人，2024）在精益4中通过完整的证明生成取得了最先进的成果，但这种范式带来了独特的挑战。它需要在不获取中间战术状态的情况下进行长时间序列预测，而未来的战术取决于这些隐藏的结果。在精益的策略模式中，证明是通过一系列转换证明状态的策略来构建的。这种顺序性引入了复合错误的风险（Ross等人，2011），其中一次误解可能会导致与有效证明路径的重大偏差。更具体地说，在生成长证明时，自回归模型可能对中间策略状态有错误的信念。为了在保持整个证明生成的简单性和计算效率的同时，在证明步骤生成中无缝集成中间策略状态，我们在DeepSeek-Prover-V1.5中开发了一种统一的方法。该方法通过截断和恢复机制结合了证明步骤和整个证明生成技术的优点。该过程从标准的完整证明生成开始，语言模型在定理语句前缀之后完成证明代码。然后，精益证明者验证此代码。如果证明正确且完整，则程序终止。如果检测到错误，则在第一条错误消息处截断代码，并丢弃任何后续代码。然后，成功生成的证明代码被用作生成下一个证明段的提示。为了提高模型新完成的准确性，我们在提示末尾添加了精益4证明器的最新状态作为注释。值得注意的是，我们的方法并不局限于从上次成功应用的策略中恢复。我们将截断和恢复机制集成到蒙特卡洛树搜索中（MCTS；Coulom，2006），其中截断点由树搜索策略调度。此外，我们提出了一种新的MCTS无奖励探索算法，以解决证明搜索的奖励稀疏问题。我们赋予树搜索代理内在动机，即好奇心（Schmidhuber，2010），以广泛探索策略状态空间。这些算法模块扩展了我们整个证明生成模型的功能，使其成为交互式定理证明的灵活工具，可以有效地利用证明辅助反馈并生成各种解决方案候选。
2.3. 来自证明辅助反馈的强化学习强化学习（RL）已被证明在增强监督微调语言模型的数学推理能力方面是有效的（Shao等人，2024）。为了进一步推进DeepSeek-Prover-V1.5-SFT，我们引入了强化学习阶段，从而形成了DeepSeek-Prover-V1.5-RL模型。该阶段利用RL根据精益4证明者的验证反馈来提高性能。此RL过程的具体细节如下。
提示。在强化学习阶段，我们使用监督微调数据集中的定理语句子集作为训练提示。我们选择了DeepSeek Prover-V1.5-SFT在多次尝试后生成正确证明的成功率适中的定理。这确保了模型有改进的空间，同时仍然能够收到积极的反馈。经过过滤后，我们保留了大约4.5k个唯一定理语句。每个定理都以CoT和非CoT引导提示作为前缀，以增强模型在这两种模式下的证明生成能力。
奖励。当通过RL训练LLM时，训练好的奖励模型通常会提供反馈信号。相比之下，形式定理证明得益于证明助手对生成的证明的严格验证，提供了显著的优势。具体来说，如果验证正确，则每个生成的证明将获得1的奖励，否则将获得0的奖励。虽然这个二进制奖励信号是准确的，但它也是稀疏的，特别是对于对监督微调模型具有挑战性的定理。为了减轻这种稀疏性，我们选择了具有挑战性但可实现的训练提示，如上所述。
强化学习算法。我们采用组相对策略优化（GRPO；Shao等人，2024）作为我们的RL算法，与PPO（Schulman等人，2017）相比，该算法表现出了更优的有效性和效率，主要是因为它消除了训练额外批评模型的必要性。具体来说，GRPO对每个定理提示的一组候选证明进行采样，并根据组内输出的相对回报来优化模型。我们的快速选择策略旨在在候选人中包括正确和不正确的证明，与GRPO的群体相对性很好地保持一致，从而加强培训过程。
培训设置。我们基于SFT模型进行RL训练，该模型既是施加Kullback-Leibler（KL）散度惩罚的初始模型，也是参考模型。我们使用5e-6的恒定学习率，KL惩罚系数设置为0.02。对于每个定理，我们对一组32个候选证明进行采样，最大长度设置为2048。训练批大小配置为512。
