在 DeepSeek 能够破圈而出的一众原因中，完全摒弃传统的监督微调（SFT）、转而采用大规模强化学习（RL）的创新之处是关键所在，这使得模型推理能力在质上取得显著突破，更证明了强化学习在提升大语言模型推理能力方面的巨大潜力。
近几年，学界和业界关于 RL 和 LLM 也涌现出了颇多具备开创性意义的研究成果。在 AI 智能体推理与决策研讨会（AIR 2025）上，来自伦敦大学学院、加州大学伯克利分校、普林斯顿大学、华盛顿大学、卡内基梅隆大学、Meta、华为等多位学术界和工业界的研究人员围绕强化学习、推理决策、AI 智能体展开讨论，回答了诸多问题，例如：
AI 系统如何模拟类人推理和决策过程？
最新的算法、框架和工具如何支持在不确定性下进行稳健的决策？
如何确保 AI 的决策过程是道德的、透明的且公正的?
……
从一系列前沿的推理决策研究中，可以看到 DeepSeek 的影子。2023 年，来自华盛顿大学的 Hanna Hajishirai 教授团队发布了一项关于大语言模型推理的开放训练方法的工作，研究强调，为了从预训练模型发展到最终模型，需要经历了三个阶段：指令微调、偏好微调以及具有可验证奖励的强化学习。而这一方法也是 DeepSeek 所采用的推理开放训练方法。
Meta GenAI 的田渊栋教授系统总结了当下应对大语言模型局限的解决方式，除了 Scaling Law 之外还有 Test-time Scaling（测试时扩展），即使用更大的模型加工具或思维链，使用不同的策略，最终可能会找到一个比单纯的大型模型更好的解决方案。田渊栋教授也分享了通过使用梯度上升（gradient ascent）对神经网络进行训练的方式，从而试图将符号结构与神经网络表示统一起来，但这一方法还处于非常初级的阶段，并不确定未来是否能成为主流。
俄亥俄州立大学的 Huan Sun 教授从隐式推理出发，探讨了数据集中的两种事实：原子事实与推断事实，并提出了一个与主流不相同的研究发现：泛化速度与绝对数据量并没有关系，而是与关键数据分布、特别是推断事实与原子事实的比例密切相关，且比例越高，泛化速度就越快。
同时，也有研究围绕 AI for Math 这一主流的推理能力应用领域。普林斯顿大学的金驰教授团队开发了Goedel-Prover 这一开源的大模型，通过将自然语言数学问题翻译成形式语言（如Lean 4），并生成形式化证明，从而解决形式化数学陈述和证明稀缺的问题，这一模型在自动定理证明方面达到了当前世界范围内的最佳性能水平。
更有实用性较强的 AI 智能体研究。卡内基梅隆大学的 Graham Neubig 教授团队提出了一个混合 Agents 方案，这种 Agents 能够交替执行浏览和 API 调用操作，并且在每一步中，它会选择与人类沟通、生成自然语言、执行Python代码（包括API调用）以及执行网页浏览操作。
AIR2025 由伦敦大学学院汪军、Meta GenAI 田渊栋等教授联合主办，致力于推动智能系统的发展，使其能够自主、适应性强且负责任地运行（会议详情及注册可访问官网：https://ai-agent-reasoning.com）。本次会议特别鸣谢来自加州大学伯克利分校的博士后研究员顾尚定。
这是一篇围绕 DeepSeek 的过去、当下与未来所展开的对人工智能的精彩讨论。AI 科技评论截取会议部分精彩内进行编译，以下为核心内容的演讲实录：
华盛顿大学的 Hanna Hajishirai 教授做了主题为“Open Training Recipes for Reasoning in Language Models”的演讲，探讨了语言模型推理的开放训练方法。
为了从预训练模型发展到最终模型，我们经历了三个阶段：指令微调、偏好微调以及具有可验证奖励的强化学习。这是我们 2023 年论文中引入的新内容。这基本上也是 DeepSeek 所采用的方法，后来我们发现 DeepSeek 也引入了同样的方法。
我们先来谈谈指令微调。指令微调中，人们也把它称为 SFT，即监督式微调。其核心思想是，你拿一个预训练的语言模型，然后向模型输入各种不同类型的任务指令，接着对模型进行微调，教会它如何遵循这些指令。
我们团队在这个方向上已经投入了很长时间。我们在 2022 年开始专注于语言模型的指令微调，当时主要关注的是自然语言处理（NLP）标签等语言测试。
2023 年，我们引入了一个自我指导框架（self-instruct framework），在这个框架下，我们教会模型合成生成越来越多的数据，以便我们能够获得更好的、更多的数据用于监督式微调。
这种范式在 2023 年得到了广泛的关注，我们看到在工业界和学术界都有很多工作基于自我指导框架展开，并设计了像 Alpaca、Vicuna 等模型。这些模型都大量使用了合成生成的指令数据进行训练。
下一步就是在监督式微调中进行偏好微调。这里有一个非常重要的步骤，就是数据整理。这和我刚才提到的合成数据生成是一样的，但同时也是一个很好的数据混合设置，因为当我们关注一组任务和我们试图优化的目标技能时，当我们增加一组任务的提示和完成内容时，我们可能会在其他组上失去准确性和改进。
比如，如果你在监督式微调中添加了大量数学提示和数学类型的数据，你可能会在知识回忆方面表现下降，因为你总是希望生成越来越长的思考链。所以，数据混合是构建一个好的微调模型中非常重要的一步。
刚才我们一直在讲数据，但现在我想聚焦于什么样的数据才真正有助于推理。这里所说的“推理”，举个例子，比如一个数学问题：一家商店正在进行衬衫促销，每件衬衫售价 25 美元，现在我们想买 7 件衬衫，总共要花多少钱？我们可以很容易地标注出答案是 125 美元，但仅仅用这种问题和金额答案作为监督式微调数据是不够的。
大家已经认识到，真正重要的是处理这种逐步推理的输出，它能一步步告诉我们发生了什么。这种数据可以成为监督式微调的优质来源。
这其实并不是一个新想法，它在自然语言处理（NLP）领域的语义解析、语义理解和推理方面已经被研究很久了。但现在它又在语言模型中重新受到关注，因为如今我们可以处理这种既包含语言又包含形式化表达的推理链。
在早期的研究中，我们只能依赖于形式化的推理图或推理思路。但现在面临的巨大挑战是：
这种逐步推理的标注虽然很好，能够帮助模型处理复杂的多步骤问题，也能揭示模型在预训练过程中所获得的推理过程，甚至因为有了这些标注，我们还能发现推理链中间可能出现的错误，比如答案是125，但推理过程中可能有错误，这有点类似于人类的思维过程。标注这种类型的推理提示非常困难。它成本高昂、耗时费力，而且不够多样化。
我们的方法是做混合数据策划，即：查看现有的资源，然后将其与合成数据生成相结合。事实上，我们采用了这篇非常有趣的论文中介绍的方法，用于合成地生成数据，但针对不同的用户角色。这为什么重要呢？因为它增加了生成提示的多样性。而且，它还使我们能够不断扩大这种思维链条以及这种很难收集的推理数据的规模。
论文链接：https://arxiv.org/abs/2406.20094
这是如何运作的呢？我们会给模型设定不同的用户角色，比如“这是一个化学动力学研究人员”，然后让模型以这个角色生成数据和数学问题。接下来，我们再给它设定一个不同的角色，让它生成一个逻辑推理问题，就可以得到这样的结果。
我们给模型提供了许多不同类型的用户角色。事实上，我们使用了25万种角色，包括计算机科学家、化学教授、五岁小孩等等。然后，我们让模型根据这些角色生成数学问题。通过这种方式，我们收集了 15 万道硬件数学题和 5 万道小学数学题。
我们还让模型生成编程问题，这主要是 Python 代码生成以及精确指令的遵循，贯穿于这些角色之中。在收集完这些提示后，我们使用了像 GPT-4o 或 Claude 这样的大模型来为我们生成思维链条数据。然后，它们生成了逐步的解决方案。
我们来看一下这是否有所帮助。我们已经在这些设置下进行了评估，查看了一个公开的数据集，例如在数学领域，有一些由社区驱动的公开开源数据集，这些数据集是由其他团队、朋友和学术界生成或策划的。然后，我们开始引入一些我们基于角色生成的合成数学问题。
这些曲线展示了在不同百分比下整合角色数据的情况，32 和 69 是我们不包含任何角色数据时在数学和 GSM8K 上的结果。而最后一列则显示了逐步增加角色生成数据的数量。
在数学领域，我们在 GSM8K 或高年级数学问题上取得了显著的提升。相比之下，我们在小学数学（GSM with K）上的提升较小，但仍然很有趣。
在生成合成数据时，一个重要的问题就是结果的质量。你可能会说：“好吧，你们生成了这些数学数据，然后让GPT-4为这些生成内容做标注，那么这些标注的质量高不高呢？”
为了提高数据的质量，我们做了以下工作：我们让 GPT-4 生成多个实例或者多条思维链条，然后进行了多数投票，并保留了那些大多数情况下答案正确的实例。
通过这种方式，我们删除了很多数据。我们基本上只保留了 60% 的数据。好消息是，即使只使用了 60% 的数据，我们在数学领域的准确率仍然相似，GSM8K 上甚至略有提升。
在整个通用方案中，我们不仅仅局限于数学，而是涉及许多不同类型的数据。
这是我们早期的混合方案，比如用于 Tulu 2 的。随着时间的推移，我们尝试了许多不同类型的混合方式，最终我们的混合方案给出了最佳的平均效果。正如你在中间看到的，例如，有些混合方案在安全性方面表现更好，而在其他方面表现稍差。但最终，我们希望在平均意义上达到一种平衡，于是我们最终选择了这种最终方案。
这是监督式微调阶段的结果。现在我们进入下一个阶段：偏好微调。
那么，偏好微调的作用是什么呢？它的想法是，我们将比较同一个提示的不同完成结果，并选择我们认为更强的那个。通常，这在风格和聊天评估中非常有用。比如它会告诉我们：“这个结果可能更符合人类的偏好。”但我们也发现，它甚至在推理测试中也有所提升。
我们将使用基于强化学习的方法来根据这种反馈、这种偏好数据进行优化。
在优化步骤中，我们将优化一个奖励，这个奖励是受到人类偏好的启发。同时，我们希望确保不会偏离原始语言模型太远。因此，我们加入了一个 KL 散度惩罚项。
我们如何进行优化？有哪些不同的算法可以用于优化这种形式化问题？通常，人们会使用 PPO（近端策略优化）。然后，去年还引入了一种更简单的算法，称为直接近端偏好优化（Direct Proximal Preference Optimization）。而我们的问题是：这两种算法中，哪一种更好？
在直接近端偏好优化（DPO）中，它就像是一种非常简单的基于学习的算法，与机器学习中的排序算法非常相似。而在近端策略优化（PPO）中，它是一种真正的强化学习方法，你有一个奖励模型，然后我们希望对策略模型进行优化。
在最近的研究中，我们决定从理论和实证的角度更深入地研究这个问题，以了解这些算法中哪一个更好。我们发现PPO（近端策略优化）始终优于DPO（直接近端偏好优化）。然而，PPO 的实现要复杂得多。它需要大量内存，因为我们希望同时将奖励模型和策略模型保留在内存中进行优化。而当我们处理更大的模型时，这会变得更加困难，吞吐量也会显著降低。
论文链接：https://arxiv.org/abs/2406.09279
这些是关键的发现。我们在比较这两种算法时注意到，有很多不同的变量在起作用。因此，我们开始分别对它们进行消融研究。比如说，这是我的初始监督微调结果，这些是我的平均性能，以及它们在一组任务——大量任务中的变化情况。
我们首先想研究数据的作用。我们最初加入了较弱的偏好数据，效果并不太强，所以只有一点点提升。当我们提高了偏好数据的质量时，我们看到了一个很大的跳跃。我们使用完全相同的数据，只是替换了算法，结果 PPO 带来了更好的提升。
当我们引入更大的奖励模型时，这是非常直观的——当我们有一个更大的奖励模型时，我们期望PPO能取得更好的结果，但实际的提升并没有达到我们的预期。我们原本以为，有了更大的奖励模型，我们应该会看到一个很大的跳跃，但结果却只是这么多。我们并没有看到太多提升，这让我们感到非常惊讶。
现在让我更具体地谈谈特定的推理测试，在一些数学推理测试上看到了几乎完全相同的趋势。但有趣的部分是，当我们将其与PPO结合时，我们实际上看到了一个更大的提升，尤其是在引入更大的奖励模型时。这非常有趣。当我们开始引入更具体的数学提示时，我们在这里看到了一个很大的跳跃。
因此，我们意识到，当我们专注于推理的提示时，情况就是这样。这也是我们在偏好微调阶段看到改进的方式。比如我们希望整合更多特定领域的数学问题。
我们把所有的发现汇总起来，然后设计了我们 2.3 模型中的偏好微调阶段：
首先，我们非常谨慎地选择提示词。我们使用了在监督微调阶段已经引入模型的一部分提示词。我们引入了新的提示，专注于像推理领域这样的特定领域，我们希望在这些领域看到更大的改进。同时，我们也引入了一些领域外的提示，并且发现这实际上也非常有帮助。
我们收集这些提示词，并从一个非常大的模型集合中查看偏好响应，比如从 70 亿参数的模型到像 GPT-4o 这样非常强大的模型。我们开始比较它们之间的偏好，看看哪一个更好，这样你的模型就会逐渐得到改进。我们还确保包含未请求的数据，确保将 Tulu 38B 和 70B 数据纳入其中，因为这是符合策略的。
然后，我们使用 GPT-4o、LLaMa 这样的模型作为评判，来为我们对这些四个维度（帮助性、指令遵循性、真实性、诚实性）的偏好进行排序。我们也尝试了不同的 LLM 作为评判，但结果差异不大。它们的结果几乎都差不多。
研究发现，我们在使用所有模型时看到了很大的提升。我们展示出，与之前的偏好数据混合集相比，我们看到了一个巨大的进步。同样，我们进行了大量的数据混合分析，研究应该从监督微调（SFT）中引入多少初始提示，以及应该引入多少新的提示。这经过了大量的实验，以确定最佳的混合比例。
我想在这里强调一点，对于 2.3 版本，我们决定在这个阶段再次使用 DPO（直接近端偏好优化），因为我们还想训练更大的模型，我们认为它的实验速度更快，而且很有帮助。因此，我们对 DPO 做了很多改进，比如我们让它进行了长度归一化等。我们进行了大量的超参数调整，最终发现，这真的效果很好，尤其是在这里使用 DPO。
但对于我们的 2.3 版本，我们实际上引入了一种新算法。我们将其称为“可验证奖励的强化学习”。当我们观察偏好微调时，我们实际上是在训练一个奖励模型，这是一个为模型的某种输出分配分数的神经网络。
我们的想法是，如果我们使用一个更简单的设置，仅仅使用一个验证机制，会怎么样呢？也就是说，如果我们生成的内容与标准答案等价，就返回 1，否则返回 0。所以它只是一个基于规则的、非常简单的奖励模型。
然后，我们训练这个非常简单、非常基础的强化学习框架，训练数据以提示的形式输入。如果生成的结果非常好，我们就优化并改进我们的策略。
它对于这类推理任务非常有用，因为我们在一开始就已经提到，为复杂的数学问题标注思维链条是非常困难的。然而，在很多情况下，最终答案就足够了。得出一个最终答案相对容易。或者我们处理的是一些生物学相关任务。对于所有这些任务，我们只需要两种标注：原始提示和最终答案。然后我们就可以进行验证。
我们甚至可以将其用于精确指令的遵循，如果给出一个非常复杂的指令，让模型生成一些内容。然后，我想了解满足的约束条件的百分比是多少，所以我们可以将这种验证扩展到不同的阶段。
这并不是一个全新的想法。但变化在于，现在的基础模型，或者是在监督微调阶段结束时的模型，已经得到了很大的改进。如今，我们能够生成相对较好的思维链条，并将其与真实情况相对比，从而判断它是否足够好，是否不好，等等。
这就是我们的最终方案。我们使用最终答案或可验证的约束来进行验证。我们并不是在训练中间的思维链条，而是让模型自己生成思维链条。我们采用了经典的强化学习实现，特别是这里我们使用了 PPO 算法，并且我们尝试了三个数据集。
结果是好的。以下展示是与这些数据集的基准对比，包括一些模型，比如DeepSeek V3、GPT-4o以及我们模型的不同版本，这些版本分别来自监督微调（SFT）、直接近端偏好优化（DPO）和可验证奖励的强化学习（RLV）。
这里有一个非常有趣的观察：当我们处理一个更大的模型，比如 405B 模型时，我们在强化学习驱动的推理（RLDR）阶段看到了更大的提升。所以，这条绿色的线显示了在自动验证强化（Auto VR）阶段的不同轮次中，我们的数学推理能力提升了多少，而粉色的线则显示了我们在处理 70B 参数模型时提升了多少。
这也与 DeepSeek V3 的发现非常一致，他们发现在处理更大模型时，强化学习带来的改进更为显著。这实际上是一个非常有趣的观察。这也引出了我们在本次讨论开始时提到的观点，即如果基础模型变得更好，那么我们对强化学习微调（RFM）的期望也会更高。
我们最近做了一个很小的改动，就是把 PPO 换成了 GRPO。我们借鉴了 DeepSeel 的想法，尝试将强化学习的实现从 PPO 迁移到 GRPO，并将其应用于一个更好的基础模型——QwenMath。我们在数学推理方面看到了显著的提升。
我们在一个非常大的任务集合上进行了评估，这些任务涵盖了推理、知识回忆、安全性等方面，且在所有这些方面都保持了良好的平衡，结果如下：
最后，我在这里提到的所有内容都与训练有关，即如何从基础模型发展到能够进行推理的真实且良好的模型。我们在最近的一篇论文中，还没有将其整合到 Tulu 配方中，但我们目前正在做这项工作，我们开始专注于数学类任务，即数学推理任务。
然后我们开始收集非常高质量的推理数据和更复杂的数学问题。我们最初收集了 6 万个样本，然后进行了大量的质量筛选，最终得到了 1000 个多样化的样本。然后我们生成了这种深度思考的推理链条，通过从 Gemini 思考模型中提炼出深度思考的标记。不久前，我们将其替换为DeepSeek R1推理模型。到目前为止，我们只进行了简单的监督微调（SFT），结果非常好。
然后我们采用了一种非常简单但令人惊讶的推理时扩展方法，得到了一个非常有趣的结果。我们允许模型在生成结果时有一定数量的标记预算，然后我们将这个标记预算从 512 调整到 2048，或者对于 GPQA 来说，调整到 496 等等。
如果模型没有用完它的标记预算，我们就添加一种延续标记，后让模型再思考一会儿。通过这种方式，我们发现模型现在能够生成更好、更深入的推理路径，这非常有趣。还有一个更有趣的事实：当我们没有添加任何标记，只是简单地让模型生成更多内容时，我们并没有看到这种效果。
俄亥俄州立大学的 Huan Sun 教授做了主题为“Understanding Reasoning in LLMs and Agents:From Grokking of lmplicit Reasoning to Test-Time Scaling with Verifiers”的演讲，探讨了从隐式推理的领悟到测试时通过验证器进行的扩展。
首先来谈谈什么是隐式推理。
论文链接：https://arxiv.org/abs/2405.15071
当模型已经掌握了原子效应，我们希望模型能够推理出多跳查询，比如“奥巴马妻子的生日”或者“比较年龄属性值后，预测谁更年轻”等问题。我们希望模型能够直接预测答案，而不是在模型内部进行语言化的思考，也不需要语言化地表达中间步骤。
CoT（思维链）现在非常流行。那么，为什么“隐性”的推理很重要呢？
首先，大规模训练或预训练的默认模式大多数情况下是不需要 CoT 的，所有数据都是可用的。实际上，为训练提供推理器可能会非常昂贵。而且，从根本上来说，我认为这决定了语言模型从数据中学习事实和规则结构的能力。如果一个模型能够在内部进行思考，那么它在压缩和整合信息方面可能会更强大。
我们对这样的结果感到好奇，想要了解其中的原因，于是我们开始了探索之旅，试图回答以下问题：
Transformer 是否能够学会隐式推理呢？又或者，是否存在一些根本性的限制，阻碍了模型获得这种能力？
哪些因素会影响这种能力的获取？是数据、技能、分布，还是模型架构？
这个数据集非常有趣。我们使用合成数据设置来控制研究，以便得出严谨的结论。
在我们的数据集中有两种事实：一种被称为原子事实（atomic facts），另一种被称为推断事实（infer factor）。
原子事实就像是知识图谱中的每个边，是单一关系，单一关系不能再进一步拆分，这就是原子事实。
而对于推断事实，你可以将它们视为由原子事实组合而成的多跳关系。在这里，我们专注于两种组合。例如，将“母亲”这一关系和“出生地”结合起来，模型应该能够回答这样的问题：当提到母亲的出生地是阿拉巴马州时，模型能够推断出答案。这就是我们所说的推断事实。
模型的目标是能够归纳并应用潜在的规则。为了使模型能够归纳出潜在规则，我们在训练过程中提供了一种混合的原子效应和推断事实。我们希望模型在训练中能够学会这些潜在规则，比如如何应用这些原子效应来推导出多跳事实。
例如，现在给定一个新的查询，比如关于哈勃望远镜的查询，我们希望模型在测试时能够应用这些归纳出的规则，并正确回答这个新的多跳查询。
但更有趣的是，我们有 ID 和 OOD 两种设置，基本上涵盖了分布内和分布外的所有情况。这意味着我们将所有的原子效应分成两组：一组用于 ID 设置，另一组用于 OOD 设置。
对于用于 ID 设置的原子效应，我们会将这个集合中的所有原子事实进行组合，并将推断出的事实划分为训练集和测试集。在这个测试设置中，我们称之为 ID 测试集。对于另一组原子效应，我们会对这个集合中的原子事实进行组合，而这些推断出的事实将被用作测试。
所以，你可以这样理解：如果一个多跳查询，比如（h，r1）、（h，r2）属于 ID 设置，这意味着它们涉及的原子事实已经在训练中与其他原子效应组合过。但如果这个多跳查询属于 OOD 设置，那么这些原子效应虽然在训练中出现过，但它们与其他任何因素的组合在训练中都没有出现过。
我们在训练集上训练这个模型，并测试其在 ID 的表现。现在，我们先来看一下这两个任务的学习曲线，可以观察到，模型能够达到完美的分布内泛化性能，但是，这需要在过拟合之后进行更长时间的训练。
对于这两个任务，正如你所看到的，过拟合大致发生在这里，这意味着模型在这一点上倾向于完美地拟合训练性能，但它需要经过更多步骤的优化，才能使分布内泛化性能赶上并达到完美的表现。这种延长的训练周期就是我们所说的“阻塞期”。
第二个发现是，我们来看一下蓝色曲线。可以观察到，在组合性任务中，Transformer 并没有实现完全的泛化。所以，分布内泛化性能从未提升，但相比之下，它最终赶上并达到了完美的表现。
我们还发现，泛化速度与绝对数据量并没有关系，而是与关键数据分布、特别是推断事实与原子事实的比例密切相关。也就是说，比例越高，泛化速度就越快。
这似乎与之前的研究结果相矛盾，他们认为存在一个临界数据量的概念，即所谓的“突破现象”。但我们认为实际上起决定作用的是推断事实与原子事实之间的比例。
然而，仍有一些更重要的问题有待进一步探讨。例如，泛化过程中发生了什么？为什么会出现泛化？为什么不同任务之间的泛化水平会有所不同？
这就需要我们进行更多的分析，以剖析在泛化过程中模型内部的工作机制。在这部分，我们使用了来自机制可解释性文献中的一些标准技术，称为 Logit lens。
我们可以利用 logit 镜头将模型的内部状态投影回输入空间。例如，你可以看到这里的标记 r1 是最大的成分之一，我们将其视为代表 r1 关系的隐藏状态。这是一个高层次的想法。因果归因（Causal Attribution）的目的是衡量一个隐藏状态与另一个状态之间的因果关系。在这里，我们关注的是 r1 在第四层的隐藏状态与目标预测之间的差异。
具体操作如下：在正常的运行过程中，我们输入一个常规的查询，然后生成最终的预测结果。这个过程是在模型已经过拟合之后进行的，因此模型总是能够预测出目标。关键在于，我们还会进行一种干扰实验，即用随机采样的 r1' 替换 r1，然后通过网络获取 r1' 的隐藏表示，并用它替换正常运行中 r1 的隐藏表示，观察这一变化如何影响最终的预测结果。我们会多次重复这个过程，通过采样许多不同的随机实体，观察最终预测结果的改变频率。
在那之后，你可以将整个神经网络视为一个从输入到输出传播信息的计算图。基于连接的强度，我们可以在那些连接非常弱的边上进行剪枝。在经过阻塞或者在阻塞的最后阶段，我们在模型检查点（checkpoint）上进行机制分析。我们发现了我们所说的“泛化电路”，用于这两个任务。让我带你看看这个，这对我们来说非常有趣。
对于组合任务，这个泛化电路是这样的：它看起来像一个顺序的或分阶段的电路。你可以看到，在前四层，模型试图检索第一个事实。然后在最后四层，模型试图检索第二个事实。在前四层，也就是底层，模型试图同时并行地检索这两个实体的属性级别，这就是为什么我们称其为并行的。然后在上层，模型试图进行比较操作，并得出结论，比如 a 是否大于或小于 b。
我们还通过 Logit lens 检查每个隐藏状态代表的输入 token。我们发现，这个隐藏表示实际上代表标记 B，它是桥接实体（bridge entity），也是 r1 的目标，并且这个隐藏表示还代表关系 r2。基本上，两个关系确实被保留了，上层确实正在执行第二阶段的知识检索。
我们想要深入了解在 grokking（领悟）过程中发生了什么。因此，我们在 grokking 期间对许多检查点进行了类似的分析，并跟踪隐藏状态与目标预测之间的因果联系。这些特征实际上展示了隐藏状态与最终预测之间的因果关系。两者之间的差异被称为在阻塞期间的变化。
同时，我们还跟踪了 r1 在第五层的隐藏表示，以及 r2 在第五层的隐藏表示。我们通过大量样本检查桥接实体（bridge entity）的排名，以及 r2 在这些成分中的关系。这些特征非常密集。
总结一下这里的关键发现：首先，我们观察到 r1 在第五层的隐藏状态与最终预测之间的因果联系显著增强，这种变化在阻塞期间非常明显。另一个有趣的现象是，r2 在第五层的隐藏表示逐渐出现，这意味着 r2 关系在阻塞期间得到了保留。此外，r1 在第五层的隐藏状态始终是桥接实体，这表明原子效应在过拟合之前已经被记忆。因此，桥接实体始终存在，只是它与最终预测之间的因果强度在不断增强。
基于这些证据，我们认为这表明模型在阻塞期间逐渐形成了操作。在 grokking 之前，模型很可能只是在进行记忆化操作，即将查询直接与目标关联。
那么，为什么会出现“grokking”现象？我们认为，在我们的模型训练初期，会形成一个记忆化电路，它直接将输入与目标预测关联起来，而无需经过中间步骤。然而，在训练的后期，随着模型逐渐泛化，会形成一个泛化路线，这个泛化路线是从记忆化路线中分化出来的。
那么，为什么会出现这种分化呢？或者，为什么记忆化路线会在训练后期被泛化路线取代？
这是因为在优化过程中，模型被激励去变得更高效。从记忆化到泛化的转变，我们可以从效率的角度来理解：记忆化路线需要存储大量的事实，而泛化路线需要支持的事实数量要少得多。
此外，我们还可以从优化过程中的权重调整来理解这一点。在 grokking 阶段，当模型达到完美的训练性能后，模型开始优化权重，其中权重项会显著减小。这表明模型试图找到一种更简洁的方式来保持相同的训练精度。
那么，为什么这两个任务并没有总是实现 OOD 泛化呢？更根本的原因是，Transformer 架构的非递归设计阻碍了跨层的记忆共享，从而限制了模型在 OOD 任务中的泛化能力。
我们还尝试了一个小规模的实验环境：我们在模型的不同部分共享参数，比如前四层和后四层使用相同的参数，然后我们重新进行训练，结果发现泛化性能有了显著提升。但我们没有等到它完全收敛，就像一个生成器达到完美性能那样。我们认为这种参数共享的方式能够解锁更好的泛化性能，但这只是潜在的一种方法，还有其他方式可以改进架构。
Meta GenAI 的田渊栋教授做了主题为“Towards a unified framework of Neural and Symbolic Decision Making”的演讲，探讨了迈向神经与符号决策的统一框架。
今天，我们仍然能看到大语言模型（LLM）存在一系列问题，关于这一问题有几种不同的方法可以解决：
首先，当然你可以将越来越多的数据输入到模型中，希望能够通过数据量的增加来帮助模型更好地学习；
第二，我们希望利用测试时扩展（test time scaling）。也就是说，我们可以使用更大的模型加上工具，或者更大的模型加上思维链。通过这种测试时扩展，使用不同的策略，我们最终可能会找到一个比单纯的大模型更好的解决方案。
最后，我会简要介绍我们最近的一些理论研究，这些研究试图将符号结构与神经网络表示统一起来。实际上，通过使用梯度上升（gradient ascent）对神经网络进行训练，我们可以发现符号结构逐渐出现。通过这种方式，我们实际上看到了符号表示和神经表示在同一框架内的统一。但目前这还处于非常初级的阶段，希望未来它能成为主流，但我们还不确定。
就像在第一种选择中，我们需要大量的计算资源、大量的数据，而且这非常昂贵。所以，我们不确定这种方法是否适用。
第二种选择是测试时扩展。接下来，我会稍微讲一下这两个部分：第一部分是工具的使用，第二部分是使用某种思维链。
对于工具的使用，我们实际上可以调用外部工具来解决推理问题。以旅行规划问题为例，我们并不是让用户直接向模型提问，而是让模型首先将用户的需求转化为符号形式。这个符号形式能够准确地描述用户的需求。然后，结合来自外部的航班和酒店信息，将这些信息整合成一个大型的优化问题，并通过混合整数线性规划（一种组合求解器）来解决。
这个求解器会给出最优行程的符号表示，然后你可以通过现有的大模型将其翻译回自然语言，从而得到由 Agents提供的答案。通过这种方式，你可以得到一个有保证的解决方案。同时，这个过程并不慢。如果你走完整个流程，它实际上是非常快的。
我们基于这个思路构建了一个演示，在两到三秒内，就能得到一个保证正确的解决方案。当然，这是在用户请求被准确翻译的前提下，大模型的翻译是相当准确的。你可以看到有一个两秒的延迟，但整个演示仍然可以很好地运行。此外，我们还让人类标注员进行了测试，他们对结果非常满意。
当然，如果你考虑到旅行规划，我们也会希望让 Agents提出澄清性的问题，也就是说，我们希望 Agents 能够真正思考用户请求中缺少的细节，并且判断 Agents 是否可以提出越来越多的问题来澄清这些细节，以确保他们理解用户的需求。
这促使我们开展了一项后续研究，探讨如何构建多轮对话，以便 Agents 能够更有效地与人类互动。
我们基本上是通过要求 Agents 遵循 Agents 章程来构建的。也就是说， Agents 需要根据几项标准进行评估。有些标准是非常客观的，而有些则是比较主观的。所谓客观，是指 Agents 最终需要得到一个准确的答案。同时， Agents 还需要积极主动地针对特定人物提出正确的问题。因此，Agents 在进入实际解决方案之前，还需要高效地完成所有问题的提问和回答。
我们基本上以一种有指导的方式进行了这种直观的 DPO（可能是某种优化方法）和项目采样，并且我们已经展示了，通过这种方式训练的 AB 模型在多轮对话的多个方面，相比没有经过这种训练的原始 700 亿参数模型要好得多。
第一部分是我们实际上可以利用工具来解决复杂的规划问题。第二部分，我会稍微讲一下更大的模型加上思维链，以及如何构建思维链来解决这些棘手的规划问题。
为了开始这个话题，让我们从第一篇论文开始，这篇论文的标题是“Searchformer”。在这篇论文中，我们利用现有的组合求解器的轨迹来构建思维链。
当我们思考导航问题时，我们有一个起点和一个终点，然后我们要求模型找出从起点到终点的最短路径。在任何阶段，我们既可以要求人工，标注也可以要求符号求解器对问题进行建模，并通过符号搜索来解决问题。A*算法（启发式搜索算法）会打开一个优先级表，这个表基本上会找到搜索中需要探索的下一个正确状态。
然后，按照探索的方式，我们最终会找到通往目的地的路径，并且它会保证给你一个最优的轨迹。因此，按照A*算法的搜索过程，我们可以构建如下所示的思维链。我们从一个提示开始，这个提示是问题规范的表示。
然后，我们可以通过像转储整个A搜索过程一样来构建一个轨迹。每次A搜索器在搜索空间中创建一个新节点时，我们实际上就在轨迹中插入一个创建操作；每次A*搜索器关闭一个节点时，我们在轨迹中插入一个关闭操作。因此，我们基本上会得到一个很长的轨迹，然后一旦开始找到目标，我们就会插入一个计划，这个计划输出最终的最优轨迹。
这基本上为你提供了一个搜索增强模型的基本框架。我们有一个作为输入的提示，同时我们还要求模型生成轨迹和计划。这与仅输出解决方案的模型形成了对比。在那些模型中，我们从一个提示开始，然后直接要求它们输出计划。
当然，生成的标记（token）数量会有很大不同。这篇论文是在 2024 年年初发表的，那时候，人们还没有充分意识到使用非常长的思维链来解决复杂规划问题的强大能力。但现在，我认为每个人都已经意识到这一点了，人们开始接受使用非常长的轨迹来解决问题。
我们发现，使用这种带有轨迹增强的搜索增强模型时，情况会有所不同。我们看到，如果你只使用仅输出解决方案的模型，那么你需要 100 万样本才能达到接近 100% 的准确率。但如果你使用搜索增强模型，你实际上只需要十分之一的数据量，同时，你也只需要十分之一的参数量，就能达到类似的性能。所以，搜索增强模型不仅更简单高效，而且在参数使用上也更加高效。
这种情况也适用于其他类型的规划任务，比如让 Agents 将箱子推到目的地，这需要非常谨慎的规划。因为如果箱子被推到角落，就没有回头路了。
一旦我们有了这些操作模型——这些模型基本上是通过模仿学习实现的——我们可以通过在这些搜索增强模型的基础上进行微调来做得更好。具体来说，我们可以通过微调这些原始模型，使其生成更短的轨迹，但仍然保持最优的计划。这其实是一个非常典型的强化学习任务，因为目标是明确的，但我们不知道如何实现这个目标。所以，我们让强化学习 Agents 去探索并找到解决方案。
通过“Searchformer”，我们发现最终得到的模型比原始的 A* 搜索模型更好，因为它具有更短的搜索轨迹。这是由于采用了“直观地址采样”（Intuitive Address Sampling），这是一种简化的强化学习版本。
从数据上看，我们发现减少后的轨迹与原始A*轨迹之间的比例越来越高，这意味着从数值上来看，这种情况确实存在。
不仅如此，我们还发现，不仅轨迹变得更短，而且经过微调后的性能也在不断提高。每次迭代后，解决方案达到最优的比例越来越高。在这种情况下，你已经可以看到，拥有 45M 个参数的模型——这里的参数指的是模型的参数数量——实际上可以与用 700M 个参数训练的模型相媲美，而后者是用一个更大的数据集进行训练的。
这非常有趣，我相信这是最早展示在测试时间和训练推理数据上存在某种“皮肤法则”（可能是指某种优化或提升性能的规律）的少数论文之一，这种法则有可能提高阅读任务的性能。
我们还有一篇论文叫作“DualFormer”。在这篇论文中，我们尝试减少用于训练的轨迹的大小和长度。你可以随机地丢弃一些搜索轨迹中的token。
论文链接：https://arxiv.org/abs/2410.09918
这种丢弃 token 的方式可以有很多种。例如，你可以丢弃所有带有成本的子句，甚至你还可以直接丢弃整个轨迹。这意味着我们实际上是在解决方案数据和搜索增强数据的混合体上进行训练。
这种训练方式非常有趣，最终得到的模型也非常强大。因此，我们最终得到了这种双模式模型，它可以自动在快速模式（即直接给出答案）和慢速模式（即通过思维链给出答案）之间切换。也就是说，你可以拥有一个同时具备这两种能力的模型，并且它在两种模式下都比单一模式的专用模型表现更好。
我们在两种模式之间切换方式非常简单——你只需要让双模式模型的第一个生成标记要么是搜索开始标记，要么是计划标记，这样模型就会直接给出最优答案。也就是说，你只需要固定第一个标记，模型的行为就会大不相同，它会表现出快速模式或慢速模式的性能。
经过训练，我们发现这种模式比单独的快速模式更好，也比单独的慢速模式更好。这是一个非常有趣的发现。
我们还注意到，DeepSeek 也表现出类似的行为。在 DeepSeek 的同步模式中，有一些技巧。如果你有两个空格，在同步 token 之后，模型生成的同步序列往往会更长一些。如果你在同步 token 之后只有一个返回，那么模型生成的内容往往会更短一些。
我认为这可能是因为他们用来训练模型的数据具有这种特定的结构，而模型在学习过程中会捕捉到这些结构，从而作为一种副作用来控制模型的行为。我们很高兴看到这种行为也出现在最先进的大型模型中。
我们也将双模式模型应用于数学问题，基线模型会有一个非常长的思维链。但一旦你随机丢弃一些句子，并用这些数据进行微调，会非常惊讶地发现，序列的长度会基本保持不变，同步标记会变得非常短，而且短得多。同时，生成的内容仍然是合理的，并且能给出正确的答案。
这种行为挺有意思的。我们是在基础模型上进行这种大规模微调。这些是基础模型，它们并不是针对特定任务优化的，所以性能并不算出色。但即便如此，你仍然会看到性能有所提升。
卡内基梅隆大学的 Graham Neubig 教授做了主题为“LLM Agents that Learn from Experience”的演讲，展示了其近期一项名为“Beyond Browsing: API-based Web Agents”的研究工作。
论文链接：https://openreview.net/forum?id=TPiJKs7ccR
我们实现了一个基础的浏览 Agent。它基于无障碍功能树运行，能够在简单布局的网页上合理地导航并填写表单。这就是我们的基线模型，也是我们在“Agents工作流记忆”论文中所使用的基线模型。
但挑战在于无障碍功能树结构的复杂性，许多语言模型对此并不熟悉。当内容并非立即可见时，导航也会变得棘手，因为你需要滚动页面、切换页面，以及其他类似的操作。
一个失败的例子是询问：“Saptaks 对 Allyproject 做了多少次提交？”于是， Agents尝试进行浏览，它试图访问 GitLab.com，使用凭据登录，点击项目，点击提交记录，然后不断向下滚动、向下滚动……最终，它耗尽了时间，并得出结论说没有找到任何提交记录，因此它认为没有提交发生，提交次数为零。
另一方面，我们还有另一种与环境交互的界面。这可以是像调用API这样的方式。它为机器与网络服务之间的通信提供了一个直接的接口，减少了操作复杂性，并且理想情况下，我们会得到更好的结果。
如果我们看看 API，它们是预定义的端点，允许计算机高效地执行任务，并通过 GET、POST、PUT 等请求实现交互，返回结构化数据，比如 JSON。有趣的是，我们在标准基准测试（比如 Web）中使用的许多网站已经提供了 API，所以在许多情况下，这些 API 已经存在。如果我们能够恰当地使用它们，我们就可以通过 API 与这些网站进行交互。
在许多情况下，我们已经这样做了。但有时，虽然有API，但文档并不完善。不过幸运的是，这也是语言模型擅长的事情。你可以直接让语言模型为 API 生成文档。
这是一个例子，在一个 API 文档中，它会告诉你属性的类型、属性的描述，以及 API 的输出会是什么，以及你可以如何执行调用。API调用本质上是通过调用代码实现的。你可以使用requests.get这样的请求，而这就是一个响应的例子。
我们考察的是，如果我们把传统上由浏览 Agent 解决的任务，让 AI Agents 通过 API 来完成，会怎么样呢？
这是我们基于 API 的 Agents。我们的实现方式是使用我们 Agents 框架中的标准编码 Agents（OpenHands），并以我接下来会讲的方式，为它提供对 API 的访问。
在过去，我们需要在网站上一步步地操作，执行许多不同的步骤，以及其他类似的操作。但在这种情况下，你只需要用三行 Python 代码就能解决任务。
那么，问题来了，你知道的鉴于 API 调用的好处，我们应该完全抛弃网页浏览吗？当然，答案是否定的。如果我们查看一百个随机抽样的任务的错误分布，当我们将 API 提供给模型时，会发现其中大约三分之一的任务实际上是正确的，但 WebArena 的验证器却判定它们是错误的，而另外 50% 的任务根本无法通过 API 解决。
原因在于，并非所有网站都提供全面的 API 支持。它们并非都有完善的 API 文档，而且网站的深度复杂性也是一个问题。
因此，我们提出的一个解决方案是创建一个混合 Agent。这种 Agent 能够交替执行浏览和 API 调用操作，并且在每一步中，它会选择与人类沟通、生成自然语言、执行 Python 代码（包括API调用）以及执行网页浏览操作。
我们根据当前可用的 API 的质量来选择操作：
我们提示 Agent，如果存在足够的 API，就应该尝试使用 API。但如果足够的 API 不存在，它就可以回到浏览模式。在其执行轨迹的最后，当它完成了所有需要做的事情后，我们要求 Agent 访问一个能够为用户提供答案的网页。这样做的想法是，它可能会使用 API 调用，但最终会将结果展示在网页上。这也符合 WebArena 评估的要求，即需要访问特定的 URL。
我们在 WebArena 上评估了我们的 Agents框架。我们使用了 OpenHands，这是我们正在开发的一种兼具编码和浏览功能的 Agent。
如果你查看 Agent 的性能，我们在多个网站类别上对其进行了评估，发现在某些特定类别上转向使用 API 后，性能有了显著提升。例如，在 GitLab 和地图上，转向使用 API 后性能大幅提升；而在 Reddit 和管理类网站上，转向使用 API 后性能提升较小，但当我们切换到使用混合 Agent 时，性能有了更大的提升。
那么，问题可能就来了，为什么会这样呢？其中一个原因是 API 的质量很重要。GitLab 和地图的 API 非常好，它们允许你完成在这些网站上需要做的大多数事情。而购物和管理类网站的 API 还算可以，但在 Reddit 风格的任务中，API 的覆盖范围非常差，这导致了在 Reddit 上使用 API 的效果不佳。
我们所做的就是查看了所有的 API，并且编写了一些新的 API。虽然数量并不多，但我们手动编写了几个，这使得在 Reddit 上使用 API 的 Agent 的准确率翻了一番。所以，拥有高质量的 API 对于网站来说是很重要的。
但就这项工作的未来方向而言，其中之一是获取或生成合适的 API。那么，我们如何能够自动生成网站的 API，以便我们能够调用一个函数，而无需 Agent 事先具备该函数、以及改进端点的检索和利用？我们可能会有非常丰富的 API，如何从中筛选出我们需要的部分呢？
未来需要我们继续探索，探索的方向如下：
加州大学伯克利分校的 Dawn Song（宋晓冬）教授做了主题为“Formal Mathematical Reasoning: A New Frontierin Al”的演讲，探讨了 AI 的新前沿——形式化数学推理。
论文链接：https://arxiv.org/abs/2412.16075
AI 在形式化数学中有广泛应用。事实上，我们可以利用各种经过形式化验证的工具，比如定理证明器等。而且，实际上存在许多不同类型的定理证明系统。
例如，在 Lean 中，当我们使用 AI 进行形式化时，本质上有一个工作流程。一旦我们有了形式化的定理陈述，我们就希望使用定理证明器来生成形式化证明。
在这一过程中，这一步是 AI 可以自动化的步骤之一。然后，生成的形式化证明和经过验证的定理可以被纳入形式化数学库。
此外，我们可以使用自动形式化（auto formalization）将非形式化的数学内容转换为形式化的数学陈述。
在这个工作流程中， AI 可以在多个步骤中提供帮助。其中一个关键步骤是，给定一个定理陈述，我们需要进行证明搜索，以遍历证明树，最终找到一个有效的证明。我们希望利用 AI ，特别是利用这些大语言模型，能够构建出 Proof Agents，从而使这一证明搜索步骤自动化。
此外， AI 还可以帮助自动形式化，即将自然语言中的非形式化数学陈述转换为形式化的数学定理陈述。例如，最新的研究和模型已经展示了如何利用大型语言模型（如 Goedel-Prover）将自然语言数学问题翻译成形式语言（如 Lean 4），并自动生成完整的证明。这种自动形式化技术为数学形式化推理提供了新的可能性，显著提升了数学问题的形式化和证明效率。
近期 AI 在形式化数学领域也取得了许多进展。例如，谷歌 DeepMind 的 AlphaGeometry 2 在解决国际数学奥林匹克竞赛（IMO）几何问题上取得了接近金牌水平的成绩。此外，Goedel-Prover 作为开源的形式化推理模型，通过将自然语言数学问题翻译成形式语言（如 Lean 4），并自动生成完整的证明，显著提升了形式化数学问题的解决效率。
尽管整个社区已经取得了非常显著的进展，但我现在想简要介绍一下一些开放性挑战和未来发展方向。
首先就是数据问题。
一般来说，在数学领域，尤其是形式化数学中，我们面临数据稀缺的问题。例如，对于训练Code Llama，其训练数据集大约有 5000 亿个 token，但当我们看这些证明时，可用的证明数据量却远远少于这个规模，甚至相差几个数量级。因此，对于这些领域，开发各种方法来解决数据稀缺问题显得尤为重要。
为了解决形式化数据的稀缺问题，幸运的是，我们确实有一些很有前景的方向，可以提升这些形式化数据的可用性。
首先是通过自动形式化来创建数据。这种自动形式化本质上是训练大型语言模型，使其能够将非形式化的数学内容自动转换为形式化的数学陈述。
鉴于我们有大量的非形式化数学内容，比如教科书和其他各种材料，通过成功的自动形式化，我们可以自动地生成这些形式化的数学陈述。我们最近在利用反馈循环来改进大型语言模型的自动形式化方面，已经看到了令人兴奋的进展。
另外，最近我也了解到，AlphaGeometry 能够支持形式化步骤，生成大约 1 亿个形式化问题陈述。这也显著促进了它在最近的国际数学奥林匹克竞赛（IMO）中取得的成功。
此外，AlphaGeometry 在 IMO 中的成功还归功于它生成合成数据的另一种方式。它通过几何规则生成了 1 亿个合成定理和证明，从而帮助它成功解决了 IMO 中具有挑战性的几何问题。这也为解决数据稀缺问题提供了一个很好的例子。
解决数据稀缺问题的另一个有前景的方向是合成数据生成，我们称之为“神经猜想”（neuro conjecturing）。
其核心思想是，可以开发模型来为定理和引理生成猜想，然后利用定理证明器尝试自动证明这些猜想。如果成功生成了证明，那么这些经过验证的猜想就成为了定理和引理，并可以被添加到陈述和证明的库中。
这可以帮助产生额外的数据，进一步帮助训练模型，使其在生成更好的猜想和证明方面表现得更好。到目前为止，我们已经在相对简单的引理和定理上看到了这方面的进展，因此未来我们可以在这方面努力，显著提高能够猜想和证明的定理的可扩展性和难度水平。
在这一领域，我们需要解决许多不同的算法挑战。例如，对于自动形式化，我们该如何扩展自动形式化？我们如何高效且有效地进行证明搜索？我们如何利用理论改进中的层次结构，以及如何真正学习数学抽象？此外，我们如何利用现有的数学知识，以及如何调和专家型和通才型方法？
首先是，我们如何真正实现大规模的自动形式化？在进行自动形式化时，实际上存在许多挑战。
因为我们进行自动形式化时，并没有后续的验证步骤，所以我们无法确切知道其他形式化的陈述是否真正正确。我们需要对它们进行评估，并且需要开发良好的指标来评估这些形式化的陈述。
此外，我们还需要能够自动验证这些自动形式化的陈述，理想情况下是利用改进的形式化步骤等。因此，我们的期望是，对于复杂的自动形式化任务，我们实际上可以将其分解为更小的步骤，然后与形式化系统进行交互以提供帮助。
对于评估自动形式化的陈述，有几个原因使其相当具有挑战性。首先，我们不能依赖人工评估，因为这种方法无法扩展。而对于其他形式化的陈述，通常存在不同的形式，即存在多种正确的方式来完成形式化，而自动等价性检查本身其实并不简单。
因此，为了应对这一挑战，我们需要利用像以太坊证明器这样的正式验证系统。我们希望借助定理证明器的反馈，迭代式地改进自动形式化。
另一个挑战是如何更高效、更有效地进行证明搜索。这当然是使用 AI 进行形式化数学的一个关键目标。对于理论改进，有许多不同的方面和组成部分。我们可以做的是，从本质上提升证明搜索的能力。
推理时间计算的扩展（即扩大推理时的计算量）对提升这些模型的通用推理能力非常有帮助。我们希望，增加测试时的计算量也能帮助加速证明搜索，这本身也是非常自然的契合。
此外，我们还希望开发更好的价值模型，以帮助评估和优先排序不同的证明目标，以及证明搜索树的不同部分。同时，我们希望系统地评估模型和搜索算法，并设置参数，以便能够开发出更适合证明搜索的模型。
到目前为止，我们已经看到，扩大测试时的计算量对于提升模型的推理能力非常有效。比如在 AlphaGeometry 和 AlphaProof 等项目中，理论改进是一个非常自然的方向。通过在证明搜索过程中增加计算量，我们可以帮助提升模型的证明搜索能力。
另一个重要话题是我们如何引导并更好地优先排序研究。特别是，我们需要开发更好的价值模型，以帮助评估和优先排序证明目标。因此，一个关键的挑战和未来方向是如何更好地训练价值模型，以及我们如何获取更好的数据并利用奖励模型（RM）来帮助解决这些问题。
目前在形式化数学中使用 AI 的方法，例如 DeepSeek Prover 等工具，通常是直接生成完整的证明，而没有充分利用证明搜索。这种方法虽然在某些情况下有效，但缺乏对不同搜索算法（如蒙特卡洛树搜索、最佳优先搜索等）的整合。因此，我们希望对这些不同的算法进行系统性评估，以开发出更好的解决方案。
另一个开放性挑战和正式的研究方向是，我们希望更好地利用定理证明中的层次结构。特别是在理论证明中，当你面对一个复杂的定理时，通常即使是数学家手动证明时，也会将这些复杂定理分解为一些不同层次的高级证明目标，以及一些不同的高级引理等。然后，这些复杂的定理会被进一步分解为更小的目标，依此类推。
这很重要——正如我们在形式化数学中应用 AI 一样，我们也需要开发具备这种能力的模型，能够逐步将高级证明目标分解为更小的目标。
所以，我们并不是主张用形式化数学的 AI 来取代非形式化数学的 AI。事实上，非形式化数学的 AI 和形式化数学的 AI 之间存在着一种自然的协同作用。重要的是将两者结合起来，本质上是将非形式化推理的灵活性与形式化推理的严谨性结合起来。
例如，对于非形式化的陈述，我们可以尝试对其进行自动形式化，然后利用形式化验证和改进等手段来验证其正确性。对于非形式化的定理陈述，以及用于非形式化数学的模型，它们可以帮助生成例如非形式化的证明草图，这些证明草图随后可以被转化为形式化的证明草图，并最终生成经过验证的形式化证明。
通过这种方式，非形式化数学部分可以帮助提升生成形式化证明的可扩展性、灵活性以及提供高层次的直觉，而形式化证明则可以为这些非形式化证明提供验证。没有这样的形式化验证，就无法真正推理并确保非形式化证明的正确性。
即使是数学论文和密码学论文等领域的非形式化证明，有时也会出现错误。而对于 AI 生成的非形式化证明，出现错误和漏洞的可能性甚至更高。因此，将非形式化和形式化结合起来，最终生成经过形式化验证的证明，是非常重要的。
通过将两者结合起来，模型可以生成多种非形式化的解决方案，最终，正确的解决方案将被形式化地验证。
另一个对于数学的可扩展性等来说也很重要的是学习数学抽象。
具体来说，无论是人类数学家还是数学系统，一般来说，这些抽象——比如开发新的定义和元素——实际上对于解决更复杂的数学问题至关重要。
我认为，这尤其是一个令人兴奋的领域和方向。对于形式化数学中的 AI 而言，这不仅是一个挑战，也是对模型创造力的考验，即模型如何学会构建这些新的定义、引理和策略，并将其应用于完整的证明辅助中，以便在未来证明中也能被利用。
最近在学习简单的证明策略方面已经取得了一些进展，这些策略是通过引导式的方法从智能体自身解决数学问题的过程中得来的。我认为这是一个非常有前景且令人兴奋的领域，即我们如何能够本质上训练模型以及证明智能体，从而使其能够更好地从自身以往的经验中发现并学习抽象。
随着我们持续推动这一正向循环，我们将继续生成新的数据，并通过自动形式化等方式，不断扩大定义、数学陈述、定理等的库。在证明搜索过程中，能够利用库中现有的知识来检索相关的定理和陈述等，对证明 Agents 来说是非常有帮助且至关重要的。因此，一个开放性挑战和未来方向是如何设计出更适合这种形式的数学以及利用这些数学库的更好的模型和检索机制。
另一个有趣的问题是，如何调和专家型和记者型的方法。记者型方法能够识别跨领域的联系，而专家型方法则在各个具体领域中表现出高效性。我们希望可以将这两种方法结合起来，例如通过为模型配备特定领域的工具等方式。
现在，我将简要谈谈两个主要应用领域的开放性挑战和未来发展方向，一个是在辅助人类数学家发展更好的数学，另一个是在程序生成、共生成和验证领域。
对于形式化数学（AFFMO），其动机和价值在于，我们希望这些工具能够真正帮助人类数学家通过解决具有挑战性的数学问题、开发新的定理和证明等，在形式化数学领域取得进展。
我们希望利用 AI 开发出更好的工具，融入数学研究的工作流程中，为人类数学家提供证明辅助，与人类数学家携手合作，共同攻克具有挑战性和前沿性的数学问题，生成相关证明等。
为了使这些工具真正发挥作用，本质上我们需要开发更好的工具，这些工具不仅用于自动化写作，生成自动化的证明步骤，还需要更好地理解数学家如何使用 AI ，比如开展行为研究来观察数学家与 AI 的互动。最终目标是为数学家开发出更好、更有用的工具。
我们希望借助这些工具，能够真正实现大规模的分布式协作，让分布在全球的数学家与 AI 工具携手合作，将大型项目分解为不同的组件，整个社区共同攻克具有挑战性和复杂性的数学问题。
另一个非常重要的应用领域是代码生成和程序验证。
它的目标不仅仅是利用 AI 来解决数学问题，更重要的是，它可以帮助从程序验证的角度来构建正确且安全的程序。
如今，与 LLaMA 相关的代码生成已经得到了广泛的应用。有估计表明，在一些公司和项目中，超过 50% 的代码现在是由LLaMA生成的。但与此同时，确保生成代码的正确性和安全性面临着巨大的挑战。例如，通过几个测试用例可以看到 AI 生成的代码不一定是正确的。
所以，我们不应该仅仅生成代码，而应该进行可验证的代码生成——即在生成代码的同时，还要生成代码的形式化规范、以及证明生成的代码符合这些形式化规范的形式化证明。
比如我想为这个问题生成代码，计算变量的绝对值函数，那么我们实际上可以生成代码的规范，同时也能生成证明。通过这种方式，就可以确保生成代码的正确性。
综上，我已经讨论了 AI 在形式化数学领域的多个不同方向和应用领域中的开放性挑战和未来发展方向。
我认为，在这个领域，接下来的五年将会非常令人激动。我们希望将整个社区凝聚在一起，共同推动 AI 在形式化数学和定理证明领域的发展。
普林斯顿大学的金驰教授做了主题为“Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving”的演讲，探讨了Goedel-Prover这一开源的大模型，通过将自然语言数学问题翻译成形式语言（如 Lean 4），并生成形式化证明，从而解决形式化数学陈述和证明稀缺的问题。
在这次演讲中，我会介绍我们开发的系统：Goedel-Prover。这个名字来源于 Gödel（哥德尔），一位在形式化系统领域非常著名的数学家。Goedel-Prover 是一个开源模型，在自动定理证明方面达到了当前的最佳性能水平。
论文链接：https://arxiv.org/abs/2502.07640
我首先会稍微谈谈评估，因为我之前提出了一个比较大胆的主张，说我们达到了最佳性能水平。所以，这就引出了一个问题：我们如何评估模型，以及我们如何判断一个模型是好的，另一个模型是不好的。
正如前述，形式化数学的一个重大挑战是数据稀缺。现有的训练数据和评估方式在某种程度上是有限的，这是开源社区中主要的数据集和基准测试。训练数据本质上是既包含 Lean 中的问题陈述，也包含 Lean 中的证明。
也就是说，我们为你提供了这些问题陈述的形式化证明，还有评估数据集，其中很多数据集只包含问题陈述，没有证明。也就是说，我们需要让模型自己生成证明，并让 Lean 编译器检查这些证明是否正确。
其中非常著名的一个是数据集 MiniF2F。很多模型都在这个数据集上进行了评估。它包含了不同难度级别的数学问题，有些非常难，有些则相对简单。
所以，很多事情都会集中在 MiniF2F 基准测试上，我们会说它包含 244 个验证问题和 244 个测试问题。这些问题涵盖了极具挑战性的数学问题，比如国际数学奥林匹克竞赛（IMO）、AIME（美国数学邀请赛）、ACM（美国计算机协会）相关问题，以及不同难度级别的代数问题（从5级到1级）和数论问题（从5级到1级），还有许多其他类型的问题。
在我们讨论完评估数据集之后，我们还会评估性能。我们还希望讨论一下在我们之前，什么是最佳模型（SOTA，State of the Art）。为了能够进行非常公平的比较，生成这种形式化数学的系统主要有两种类型：
一种是整体证明生成的风格。本质上，你有一个语言模型，它会在给定问题的情况下一次性生成整个证明。一个具有代表性的模型是 DeepSeek Prover，比如 DeepSeek v1 或 DeepSeek v1.5。评估这类模型的一个非常重要的指标是，你需要生成多少个证明（比如你采样了多少个证明），才能得到一个正确的证明。
换句话说，我们可能会说“通过率达到32次/6400”，这意味着你实际上生成了大约20万个证明，只要其中有一个证明是正确的，有一个证明通过了Lean编译器的验证，我们就可以说我们解决了这个问题。因此，“通过率”是一个在评估整体证明生成中非常重要的指标。
另一种类型是树搜索方法。与一次性生成整个证明不同，这种方法是逐步生成的。在生成一步之后，我们会使用某种树搜索算法，比如广度优先搜索或最佳优先搜索等，来搜索可能的最佳下一步。一些代表性模型，比如InternLMs 和 AlphaProof 系统（我认为它既用于几何问题，也用于代数问题），都采用了这种基于树的方法。
我们只与整体证明生成系统进行比较，因为我们的模型 Goedel-Prover是一个整体证明生成系统。不过，我们也有其他方法可以与开源的树搜索方法和内部方法进行比较。我们没有与 AlphaProof 进行比较，因为它是一个闭源系统，尽管它的性能非常好，但到目前为止，该模型并未开源。
首先，我会关注小型化数据集。我们在路径集32上进行了评估，此前的最佳水平是DeepSeek Prover，他们在经过监督微调或强化学习后有一些变体。在路径32上，这是一个相对较小的预算，比如采样推理时间，他们达到了大约50%的准确率。而我们的模型在路径32上达到了57%的准确率，比之前的最佳水平高出7个百分点。
你也可以问，当我们增加推理计算量时，我们的模型表现如何。这就是这张图展示的内容。我们可以看到一些一致的改进，我们的模型与DeepSeek Prover之间大约有7个百分点的性能差距。
第二点是，我们还希望在 PutnamBench 上评估我们的模型。这是一个包含所有永久性数学竞赛问题的基准测试，这些问题极具挑战性。我们在该基准测试中获得了第一名，解决了七个问题。我认为第二名的模型也解决了七个问题，但它不是开源的。我们排名第一，是因为我们实际上使用了更少的推理时间和计算资源，我们通过了512。
其他一些成果，比如我们之前提到的 Lean-Workbook，它是一个庞大的训练数据集，但不幸的是，其中只有很小一部分训练数据是有证明的。比如，他们提供了大量的问题陈述，但其中只有很小一部分问题陈述附有证明。
因此，以前的模型或者现有的所有工作，总共只能找到大约 1.5 万到 5 万份 Lean-Workbook 的证明，而我们的模型能够找到大约 3 万份，几乎是之前找到的证明数量的两倍。这也在我们测试的多个数据集上得到了体现，包括miniF2F、ProofNets 和 FormalNuminous，这些是我们用作基准的内部数据集。
在介绍完我们的性能之后，我还想稍微说一下我们是如何实现这一成果的。
事实证明，我们的整体方法并不复杂，这正是我喜欢的——它非常简单且清晰，我认为这作为一个起点，对于推动自动定理证明的发展是非常好的。
形式化数学中最关键的挑战之一就是数据稀缺。
尽管 DeepSeek 声称他们形式化了很多大型数据集，但不幸的是，在开源社区中，可用的数据集和数据非常稀少。你可以看到，我们大约有 1000 万非形式化的问题，但形式化的问题陈述却少得多，例如，我们只有大约 40 万形式化的问题陈述，以及仅有 1.5 万个形式化的证明，这个数量是非常非常少的。基于这样少量的数据，要训练出一个好的证明器是非常困难的。
所以，我们首先需要做的是获取更多形式化陈述，以便我们能够获得更好的训练基础，我们需要获取更多的陈述和更多的证明。对于陈述，我们采用了自动形式化的途径。因此，我们首先收集了大量既有形式化又有非形式化陈述的配对。这些是我们同时拥有形式化和非形式化陈述的数学问题。我们从 Lean-Workbook 中获取了 14 万个这样的配对，它们同时提供了形式化和非形式化的陈述；此外，我们还从云端生成了另外 17 万个配对。
第二件事是我们需要训练一个形式化器，因为仅仅 10 万个问题陈述是不够的。为了做到这一点，我们训练了我们自己的形式化器。我们从 Qwen2.5-32B 模型开始，将这些形式化和非形式化的陈述配对输入其中，最终得到了我们的形式化器。一旦我们有了形式化器，我们就可以处理一个更大规模的非形式化数据集。在这一过程中，我们特别使用了 Numina 数据集，它包含了大约 80 万个高质量的数学问题。我们将这些非形式化的问题形式化为形式化陈述。
关于直接进行自动形式化陈述，存在一些问题：
第一个问题是，它可能会产生大量语法错误。例如，我们需要在 Lean 中形式化这些陈述，但其中一些可能语法错误，无法通过 Lean 编译器的验证。因此，我们会进行编译正确性测试，本质上就是部署 Lean 编译器。如果编译器无法通过，例如返回一些错误提示，我们会要求模型进行修正。
第二个问题是，即使语法正确，形式化后的陈述可能与原始问题完全不一致。例如，非形式化的问题可能是这样的，但形式化后的问题可能缺失了一些条件，或者最终变成了一个完全不同的问题。在这种情况下，我们无法像在大学里那样部署人力去人工检查所有陈述，因为我们没有足够的人力资源。
因此，我们会使用“四重完整性测试”，本质上是要求四个大型语言模型作为独立的裁判，独立判断这些问题是否是正确的翻译，并基于一系列标准对语言模型进行提示。然后，我们会要求它们进行多数投票。经过这些流程后，我们最终得到了超过一百万条能够通过这两项测试的形式化陈述，并将这些陈述用作我们的训练数据集。
需要注意的是，这仅仅是关于问题陈述，而不涉及证明。那么在我们得到了这些问题之后，如何获取更多的证明呢？我们使用这种迭代训练的方法。这是一个获取更多证明的流程。
我们会从某个基础模型开始。当我们有了基础模型后，比如 Goedel-Prover 的第一版，它基于 DeepSeek Base 7B模型。我们将大量的形式化陈述输入其中，然后进行推理，证明器能够生成一些证明。在生成了一些证明之后，我们将它们提交给 Lean 编译器，Lean 会验证这些证明。我们会发现其中一些证明是正确的，然后将这些正确的证明加入到我们的数据集中，用于下一轮训练。
通过这种迭代训练的方式，我们可以获得越来越多的证明，并将越来越多的形式化证明加入到我们的数据集中。我们能够基于越来越多的证明进行训练，这就是我们获取更多形式化证明的方法。
表格如下：我们在进行迭代训练时，不仅在不断增加更多的证明，还在迭代地增加更多的陈述。这样，当一个模型的容量更大时，随着我们增加更多陈述，模型的表现也会更好。
我们在一开始并不会增加太多陈述，原因有两个：一是为了节省计算资源；二是为了避免让模型过于困惑。因此，我们会逐渐增加输入到数据中的陈述数量。我们把这些陈述输入到我们的证明器中生成证明，并且可以看到我们的模型持续地、稳定地解决更多问题，并基于 Lean 工作手册以及 Lumina 数据集生成更多的证明。
在多个数据集上进行训练，甚至在一些统计误差范围内，这已经被证明是一种相当有效的方法，它有点像在多次迭代中单调地提升性能。
这是我们整个模型的“配方”。这是我们推动自动形式化定理证明极限的第一步。在我们的模型的第一个版本中，我们提升了 CFR 性能，解决了多个 F2F 问题。我们还在 Putnam 基准测试中取得了第一名，并且在主要工作手册中解决了几乎两倍数量的问题
