DeepSeek

引言 近期大语言模型的进展显著影响了人工智能中的数学推理和定理证明。尽管在自然语言领域取得了显著进步，但语言模型在形式化定理证明方面仍然面临巨大挑战，例如使用 Lean 和 Isabelle，这需要满足验证系统形式化规范的严格推导。即使是像 GPT-4 这样的先进模型，在处理复杂的形式化证明时也显得力不从心，这突显了所涉及的编码和数学的复杂性。一个形式化定理证明模型不仅必须掌握像 Lean 定理证明器这样的形式化系统的语法和语义，还必须将抽象的数学推理与精确的形式化表示对齐。 形式化定理证明中的语言模型通常采用两种策略：证明步骤生成和完整证明生成。证明步骤生成预测每个后续策略（tactic）并使用形式化验证器对其进行验证，以获取有关当前策略状态的更新信息，通常利用树搜索技术来构建有效证明。相比之下，完整证明生成计算效率高，它根据定理陈述生成整个证明代码，协调证明器模型和形式化定理验证器之间的通信预算较少。虽然 DeepSeek-Prover-V1 在 Lean 4 中通过完整证明生成取得了最先进的结果，但这种范式也带来了其独特的挑战。它需要在无法访问中间策略状态的情况下进行长序列预测，并且未来的策略依赖于这些隐藏的结果。在 Lean 的策略模式中，证明是通过一系列转换证明状态的策略来构建的。这种顺序性引入了复合错误的风险，即单个误解可能导致严重偏离有效的证明路径。更具体地说，自回归模型在生成长证明时可能对中间策略状态有错误的认知。 为了在证明步骤生成中无缝集成中间策略状态，同时保持完整证明生成的简单性和计算效率，我们在 DeepSeek-Prover-V1.5 中开发了一种统一的方法。该方法通过截断-恢复机制结合了证明步骤生成和完整证明生成技术的优点。该过程始于标准的完整证明生成，其中语言模型在定理陈述前缀之后完成证明代码。然后 Lean 证明器验证此代码。如果证明正确且完整，则过程终止。如果检测到错误，则代码在第一个错误消息处被截断，并丢弃任何后续代码。成功生成的证明代码随后被用作生成下一个证明片段的提示词。为了提高模型新补全的准确性，我们将来自 Lean 4 证明器的最新状态作为注释附加在提示词的末尾。值得注意的是，我们的方法不限于从最后成功应用的策略恢复。我们将截断-恢复机制集成到蒙特卡洛树搜索 [MCTS] 中，其中截断点由树搜索策略安排。此外，我们提出了一种新颖的用于 MCTS 的无奖励探索算法，以解决证明搜索的奖励稀疏性问题。我们赋予树搜索智能体内在动机，即好奇心（a.k.a. curiosity），以广泛探索策略状态空间。这些算法模块扩展了我们完整证明生成模型的功能，使其成为交互式定理证明的灵活工具，可以有效利用证明助手反馈并生成多样化的解决方案候选。 贡献 我们提出了一个用于开发基于语言模型的形式化数学证明器的综合框架，该框架集成了几个关键组成部分：大规模数学预训练、形式化数学语料库的构建与增强、利用证明助手反馈的在线强化学习，以及用于定理证明中长期规划的树搜索方法。预训练模型、监督微调模型、强化学习模型，以及蒙特卡洛树搜索算法的代码，均已公开，可供进一步研究和应用。 预训练：我们通过在高质量的数学和代码数据上进行进一步预训练，重点关注 Lean、Isabelle 和 Metamath 等形式化语言，以增强我们基础模型在形式化定理证明和数学推理方面的能力。 监督微调：我们通过实施两种数据增强技术来改进 Lean 4 代码补全数据集。首先，我们使用 DeepSeek-Coder V2 236B 为 Lean 4 代码标注自然语言思维链注释，从而将形式化定理证明与自然语言推理对齐。其次，我们在 Lean 4 证明代码中插入中间策略状态信息，使我们的模型能够有效利用编译器反馈。然后，使用生成的数据集对预训练模型进行微调。 强化学习：我们采用 GRPO 算法，利用证明助手反馈（RLPAF）对监督微调模型进行强化学习。Lean 证明器提供的验证结果作为奖励监督信号，增强了模型与验证系统形式化规范的对齐。 蒙特卡洛树搜索：我们通过引入一种新颖的抽象及其对应的搜索算法，推进了形式化定理证明中的树搜索方法。我们提出的截断并恢复机制作为一种状态-动作抽象，将树搜索过程无缝集成到完整证明生成框架中。我们推出了 RMaxTS，这是一种创新的蒙特卡洛树搜索算法，它利用 RMax 策略来解决稀疏奖励证明搜索问题中的探索难题。通过分配内在奖励，该算法鼓励证明器智能体生成多样化的规划路径，从而促进对证明空间的广泛探索。 评估和指标总结 miniF2F：在单次完整证明生成设置下，DeepSeek-Prover-V1.5 在 miniF2F 测试集上实现了 60.2% 的通过率，相较于 DeepSeek-Prover-V1 的 50.0%，绝对提升了 10.2 个百分点，这是一个显著的进步。结合树搜索技术后，通过率进一步提升至新的最先进水平 63.5%。 ProofNet：DeepSeek-Prover-V1.5 在 ProofNet 的单次完整证明生成设置下同样表现出强大的性能，其验证集通过率为 21.6%，测试集通过率为 23.7%。集成树搜索技术进一步提升了这些结果，在验证集上达到了 25.4% 的新最先进通过率，在测试集上达到了 25.3% 的新最先进通过率。 预训练 为了增强我们语言模型在生成形式化证明和通过数学语言进行推理方面的熟练度，我们进一步对我们的基础模型进行了预训练。这一改进涉及在包含代码和自然语言数学内容的高质量数据集上进行训练。我们特别关注了在证明助手中广泛使用的形式化语言，例如 Lean、Isabelle 和 Metamath。我们将这个改进后的模型命名为 DeepSeek-Prover-V1.5-Base。 ...

摘要 我们引入了 DeepSeek-Prover-V2，这是一个开源的大语言模型，专为 Lean 4 中的形式化定理证明而设计，其初始化数据通过由 DeepSeek-V3 驱动的递归定理证明流程收集。冷启动训练过程始于通过提示 DeepSeek-V3 将复杂问题分解为一系列子目标。已解决子目标的证明被整合成思维链，结合 DeepSeek-V3 的逐步推理，为强化学习提供初始冷启动。这个过程使我们能够将非形式化和形式化数学推理整合到一个统一的模型中。由此产生的模型 DeepSeek-Prover-V2-671B 在神经定理证明方面取得了最先进的性能，在 MiniF2F-test 上达到了 88.9% 的通过率，并解决了 PutnamBench 中 658 个问题中的 49 个。除了标准基准测试，我们引入了 ProverBench，这是一个包含 325 个形式化问题的集合，以丰富我们的评估，其中包括从近期 AIME 竞赛（24-25 年）中选取的 15 个问题。对这 15 个 AIME 问题的进一步评估显示，该模型成功解决了其中的 6 个。相比之下，DeepSeek-V3 使用多数投票解决了这些问题中的 8 个，这突出表明大语言模型中形式化和非形式化数学推理之间的差距正在大幅缩小。 1. 引言 大语言模型 (LLMs) 推理能力的出现彻底改变了人工智能的众多领域，特别是在数学问题解决领域 (DeepSeek-AI, 2025)。这些进展很大程度上得益于推理阶段的扩展范式，最显著的是通过自然语言思维链推理 (Jaech et al., 2024)。LLMs 不再仅仅依靠一次前向传播来得出答案，而是可以反思中间推理步骤，从而提高准确性和可解释性。尽管自然语言推理在解决竞赛级数学问题方面取得了成功，但其应用于形式化定理证明仍然面临根本性挑战。LLMs 以一种固有的非形式化方式进行自然语言推理，依赖于启发式方法、近似和数据驱动的猜测模式，这些往往缺乏形式化验证系统所需的严格结构。相比之下，Lean (Moura and Ullrich, 2021)、Isabelle (Paulson, 1994) 和 Coq (Barras et al., 1999) 等证明助手在严格的逻辑基础上运行，其中每个证明步骤都必须明确构建并形式化验证。这些系统不允许任何歧义、隐含假设或细节遗漏。弥合非形式化、高层次推理与形式化验证系统的句法严谨性之间的差距，仍然是神经定理证明领域一个长期存在的挑战 (Yang et al., 2024)。为了利用非形式化数学推理的优势来支持形式化定理证明，一种经典方法是根据自然语言证明草图的指导，对形式化证明进行分层分解。Jiang 等人 (2023) 提出了一个名为 Draft, Sketch, and Prove (DSP) 的框架，该框架利用大语言模型生成自然语言的证明草图，然后将其翻译成形式化证明步骤。这种非形式化到形式化的定理证明范式与分层强化学习中的子目标概念非常相似 (Barto and Mahadevan, 2003; Nachum et al., 2018; Eppe et al., 2022)，其中复杂的任务被分解为更简单的子任务的层次结构，这些子任务可以独立解决，以逐步实现总体目标。在形式化定理证明中，子目标通常是一个中间命题或引理，有助于证明更大的定理 (Zhao et al., 2023, 2024)。这种分层分解与人类解决问题的策略一致，并支持模块化、可重用性和更高效的证明搜索 (Wang et al., 2024b; Zheng et al., 2024)。最近的研究通过采用多层层次结构进行结构化证明生成 (Wang et al., 2024a)，以及利用强化学习技术优化复杂定理分解为可管理子目标 (Dong et al., 2024)，进一步扩展了这一范式。 ...

摘要 强化学习（RL）已被广泛应用于大规模大语言模型（LLMs）的后训练阶段。最近，通过强化学习激励大语言模型推理能力的实践表明，适当的学习方法可以实现有效的推理时可扩展性。强化学习的一个关键挑战是在可验证问题或人为规则之外的各种领域中为大语言模型获取准确的奖励信号。在这项工作中，我们研究了如何通过增加推理计算来改进通用查询的奖励建模（RM），即**，并进一步研究如何通过适当的学习方法提高性能-计算扩展的有效性。 对于奖励建模方法，我们采用pointwise generative reward modeling（GRM），以便为不同输入类型提供灵活性，并具备推理时扩展的潜力。对于学习方法，我们提出了Self-Principled Critique Tuning（SPCT），通过在线强化学习在 GRM 中培养可扩展的奖励生成行为，以自适应地生成原则并准确地进行批判，从而产生了DeepSeek-GRM模型。此外，为了实现有效的推理时扩展，我们使用并行采样来扩展计算使用量，并引入了一个元奖励模型来指导投票过程以获得更好的扩展性能。实验表明，SPCT 显著提高了 GRM 的质量和可扩展性，在各种奖励建模基准测试中优于现有方法和模型，且没有严重的偏见，并且与训练时扩展相比可以实现更好的性能。DeepSeek-GRM 在某些任务中仍然面临挑战，我们相信这可以通过未来在通用奖励系统方面的努力来解决。这些模型将被发布并开源。 引言 我们能否设计一种旨在为通用奖励模型实现有效推理时间扩展的学习方法？ 在这项工作中，我们研究了不同的[奖励模型方法]，发现逐点生成式奖励建模（GRM）可以在纯语言表示内统一对单个、成对和多个响应的评分，从而克服了挑战(1)。我们探索发现，某些原则可以在适当的标准内指导生成式奖励模型的奖励生成过程，进而提高奖励质量，这启发了我们：奖励模型的推理时间可扩展性或许可以通过扩展高质量原则和准确批判的生成来实现。 基于这一初步认识，我们提出了一种新颖的[学习方法]，自我原则化批判调优（SPCT），旨在培养生成式奖励模型中有效的推理时间可扩展行为。通过利用基于规则的在线强化学习，SPCT使生成式奖励模型能够学习根据输入查询和响应自适应地设定原则和批判，从而在通用领域产生更好的结果奖励（挑战(2)）。随后，我们开发了DeepSeek-GRM-27B，该模型基于Gemma-2-27B，并使用SPCT进行了后训练。对于[推理时间扩展]，我们通过多次采样来扩展计算资源的使用。通过并行采样，DeepSeek-GRM可以生成不同的原则集合以及相应的批判，然后通过投票决定最终奖励。通过更大规模的采样，DeepSeek-GRM能够基于多样性更高的原则进行更准确的判断，并输出粒度更精细的奖励，这解决了挑战(3)&(4)。此外，除了通过投票方式，我们还训练了一个元奖励模型以获得更好的扩展性能。实验证明，SPCT显著提高了生成式奖励模型的质量和可扩展性，在多个综合性奖励模型基准测试中表现优于现有方法和模型，且没有表现出严重的领域偏差。我们还将DeepSeek-GRM-27B的推理时间扩展性能与参数量高达671B的更大模型进行了比较，发现相较于通过增大模型规模进行训练时间扩展，我们的方法能实现更优的性能。尽管当前方法在效率和特定任务方面仍面临挑战，但我们相信，通过SPCT及后续的努力，具有增强可扩展性和效率的生成式奖励模型可以作为通用奖励系统的多功能接口，推动大语言模型后训练和推理领域的前沿发展。 总的来说，我们的主要贡献如下： 我们提出了一种名为 自洽原则批判调整(SPCT) 的新颖方法，旨在提升通用奖励模型有效的推理时可扩展性，并由此产生了 DeepSeek-GRM 模型。此外，我们还引入了一个元奖励模型（meta RM），以在投票机制之外有效提升 DeepSeek-GRM 的推理时扩展性能。 我们通过实验证明，相较于现有方法及若干强大的公开模型，SPCT 显著提升了通用奖励模型（GRM）的质量和推理时可扩展性。 我们亦将 SPCT 训练方案应用于更大规模的大语言模型（LLM），并发现就训练时间而言，推理时扩展的表现可能优于模型规模扩展。 不同奖励模型（RM）方法的比较 如图2所示，奖励模型（RM）方法主要由奖励生成范式和评分模式决定，这从本质上影响了 RM 的推理时可扩展性和输入灵活性。对于奖励生成范式，我们区分三种主要方法：标量、半标量和生成式。标量方法为给定的查询和响应分配标量值，而半标量方法既生成文本判断（称为“评语”），也生成标量奖励值。生成式方法仅生成作为文本奖励的评语，奖励值可从中提取。对于评分模式，我们区分两种主要方法：逐点式和配对式。逐点式方法为每个响应分配一个独立的分数，而配对式方法则从所有候选响应中选择单个最佳响应。为了扩展推理时的计算使用，我们关注基于采样的方法，这些方法为相同的查询和响应生成多组奖励，然后聚合得到最终奖励。因此，RM 的推理时可扩展性取决于是否能通过多次采样获得不同的奖励，而标量 RM 在大多数情况下会因此失效，因为其奖励生成是不变的；输入灵活性则定义为 RM 是否支持对单个、成对以及多个响应进行评分，其中配对式 RM 几乎无法对单个响应评分，并且通常需要额外技术来处理多个响应。逐点式生成式奖励模型（GRM）的公式为： 其中 $x$ 是查询，$y_i$ 是第 $i$ 个响应，$r_{\theta}$ 是由 $\theta$ 参数化的奖励函数，$\mathcal{R}$ 是奖励，$\boldsymbol{C}$ 是评价，$S_i$ 是 $y_i$ 的个体分数，而 $f_{\mathrm{extract}}(\cdot)$ 从生成结果中提取奖励。通常，奖励是离散的，并且在这项工作中，我们默认分配 $S_i \in \mathbb{N}, 1 \leq S_i \leq 10$。 ...

http://joschu.net/blog/kl-approx.html $$ K L[q, p]=\sum_x q(x) \log \frac{q(x)}{p(x)}=E_{x \sim q}\left[\log \frac{q(x)}{p(x)}\right] $$ 它解释了一个我在各种代码中使用过的技巧，我将 $K L[q, p]$ 近似为 $\frac{1}{2} (\log p(x) - \log q(x))^2$ 的样本平均值，对于来自 $q$ 的样本 $x$，而不是更标准的 $\log \frac{q(x)}{p(x)}$。 这篇文章将解释为什么这个表达式是 KL 的一个好的（虽然有偏差的）估计器，以及如何在保持其低方差的同时使其无偏差。 我们计算 $KL$ 的选项取决于我们对 $p$ 和 $q$ 有什么样的访问权限。 在这里，我们将假设我们可以计算任何 $x$ 的概率（或概率密度）$p(x)$ 和 $q(x)$，但我们无法解析地计算 $x$ 上的总和。 为什么我们不能解析地计算它呢？ 精确计算它需要太多的计算或内存。 没有闭合形式的表达式。 我们可以通过仅存储对数概率（log-prob）来简化代码，而无需存储整个分布。如果KL散度仅用作诊断工具，这会是一个合理的选择，就像在强化学习中经常出现的情况一样。 估计总和或积分的最常见策略是使用蒙特卡洛估计。给定样本 $x_1, x_2, \dots \sim q$，我们如何构建一个好的估计？ 一个好的估计量是无偏的（它具有正确的均值）并且具有低方差。我们知道一个无偏估计量（在来自 $q$ 的样本下）是 $\log \frac{q(x)}{p(x)}$。然而，它具有高方差，因为它对于一半的样本是负的，而KL散度始终是正的。让我们将这个朴素估计量称为 $k_1 = \log \frac{q(x)}{p(x)} = - \log r$，其中我们定义了比率 $r=\log \frac{p(x)}{q(x)}$，它将在后续计算中频繁出现。 ...

今天，我们很高兴地介绍 Unsloth 中的推理功能！DeepSeek 的 R1 研究揭示了一个“顿悟时刻”，在这个时刻，R1-Zero 通过使用群体相对策略优化（GRPO）自主学习分配更多的思考时间，而无需人类反馈。 我们增强了整个 GRPO 过程，使其使用的 VRAM 比 Hugging Face + FA2 少 80%。这使您能够仅使用 7GB 的 VRAM 和 Qwen2.5（1.5B）重现 R1-Zero 的“顿悟时刻”。 尝试我们的免费 GRPO notebook：Colab 上的 Llama 3.1（8B） 有关其他模型（如 Phi-4）的 GRPO 笔记本，请访问我们的文档 💡 主要细节 使用 15GB VRAM，Unsloth 允许您将任何模型（最多 15B 参数）转换为推理模型，例如 Llama 3.1（8B）、Phi-4（14B）、Mistral（7B）或 Qwen2.5（7B） 最低要求：仅需 7GB VRAM 即可在本地训练您自己的推理模型。 Tiny-Zero 的出色团队展示了您可以使用 Qwen2.5（1.5B）实现自己的“顿悟时刻——但这需要 2xA100 GPU（160GB VRAM）。现在，使用 Unsloth，您只需一台 7GB VRAM 的 GPU 就可以实现同样的“顿悟时刻”。 之前，GRPO 仅支持完全微调，但我们已使其与 QLoRA 和 LoRA 一起工作。 请注意，这并不是微调 DeepSeek 的 R1 蒸馏模型或使用 R1 的蒸馏数据进行微调，Unsloth 已经支持。这是将标准模型转换为完整的推理模型，使用 GRPO。 ...

DeepSeek-R1-Zero最鼓舞人心的结果之一是通过纯强化学习（RL）出现的“顿悟时刻”。在顿悟时刻，模型学习到自我反思等新兴技能，这有助于它进行上下文搜索以解决复杂的推理问题。 在R1-Zero发布后的几天内，几个项目独立地在较小的规模（例如，1B到7B）上“再现”了R1-Zero类训练，并且都观察到了顿悟时刻，这通常伴随着响应长度的增加。我们遵循他们的设置来仔细审查R1-Zero类训练过程，并在本博客中分享以下发现： 💡 a) R1-Zero类训练中可能没有顿悟时刻。 相反，我们发现顿悟时刻（例如自我反思模式）出现在第0个周期，即基础模型。 b) 我们发现基础模型的响应中存在表面自我反思（SSR），在这种情况下，自我反思不一定导致正确的最终答案。 c) 我们通过RL对R1-Zero类训练进行了更深入的观察，发现响应长度增加的现象并不是由于自我反思的出现，而是RL优化良好设计的基于规则的奖励函数的结果。 1. 顿悟时刻出现在第0个周期 1.1 实验设置 基础模型。我们调查了由不同组织开发的广泛的基础模型系列，包括Qwen-2.5, Qwen-2.5-Math, DeepSeek-Math, Rho-Math, 和 Llama-3.x。 提示模板。我们直接使用在R1-Zero和SimpleRL-Zero中应用的模板来提示基础模型： 模板1（与R1-Zero相同） A conversation between User and Assistant. The user asks a question, and the Assistant solves it. The assistant first thinks about the reasoning process in the mind and then provides the user with the answer. The reasoning process and answer are enclosed within <think> </think> and <answer> </answer> tags, respectively, i.e., <think> reasoning process here </think> <answer> answer here </answer>. User: {Question} Assistant: ...

看到一个cuda层面实现kernel的库Liger Kernel，速度极快。 ==直接一行调用GRPO loss：== grpo_loss = LigerFusedLinearGRPOLoss() 以下为Liger Kernel库简介： Liger Kernel 是一个专门为大语言模型（LLM）训练设计的 Triton 内核集合。它可以有效提高多 GPU 训练的吞吐量 20%，并减少 60% 的内存使用。我们已经实现了与 Hugging Face 兼容的 RMSNorm、RoPE、SwiGLU、CrossEntropy、FusedLinearCrossEntropy 等功能，未来还会增加更多。该内核开箱即用，支持 Flash Attention、PyTorch FSDP 和 Microsoft DeepSpeed。 我们还添加了优化的训练后内核，为对齐和蒸馏任务节省高达 80% 的内存。我们支持 DPO、CPO、ORPO、SimPO、JSD 等多种损失函数。 只需一行代码，Liger Kernel 就可以提高 20% 以上的吞吐量，并减少 60% 的内存使用，从而实现更长的上下文长度、更大的批量大小和更大的词汇表。 注意： 基准测试条件：LLaMA 3-8B，批量大小 = 8，数据类型 = bf16，优化器 = AdamW，梯度检查点 = True，分布式策略 = FSDP1，使用 8 个 A100 GPU。 Hugging Face 模型在 4K 上下文长度时开始出现内存不足（Out of Memory, OOM），而 Hugging Face + Liger Kernel 可以扩展到 16K。 ...