DeepSeek-Prover-V1.5:利用证明助手反馈进行强化学习和蒙特卡洛树搜索

引言 近期大语言模型的进展显著影响了人工智能中的数学推理和定理证明。尽管在自然语言领域取得了显著进步,但语言模型在形式化定理证明方面仍然面临巨大挑战,例如使用 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。 ...

May 1, 2025 · 小茄墩

DeepSeek-Prover-V2: 对推理的极致追求

摘要 我们引入了 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),进一步扩展了这一范式。 ...

May 1, 2025 · 小茄墩

Anthropic CEO Dario: 可解释性的紧迫性

在我从事 AI 工作的这十年里,我见证了它从一个微小的学术领域,成长为可以说是世界上最重要的经济和地缘政治议题。在这段漫长的时光中,我学到的最重要一课或许是:底层技术的进步是不可阻挡的,由过于强大而无法遏制的力量所驱动,但其发生的方式——事物构建的顺序、我们选择的应用以及它向社会推广的具体细节——则完全有可能改变,并且通过施加影响可以带来巨大的积极效应。我们无法叫停这辆巴士,但我们可以引导它的方向。 近几个月来,我日益关注一个引导这辆巴士的额外机会:一些最新进展带来了一种令人心动的可能性,即我们或许能在模型达到压倒性的力量水平之前,成功实现可解释性——也就是理解 AI 系统内部的工作原理。 领域之外的人们得知我们并不理解自己创造的 AI 如何运作时,常常感到惊讶和警惕。他们的担忧不无道理:这种缺乏理解的状况在技术史上基本上是前所未有的。数年来,我们(包括 Anthropic 及整个领域)一直试图解决这个问题,希望创造出一种能够完全揭示 AI 模型内部工作原理的工具,如同一种高度精确和准确的 MRI。这个目标曾常常感觉遥不可及,但多个近期的突破让我确信,我们如今已步入正轨,并且拥有了真正成功的机会。 与此同时,整个 AI 领域的发展步伐领先于我们在可解释性方面的努力,且其自身仍在飞速前进。因此,如果我们希望可解释性能够及时成熟并发挥关键作用,就必须加快步伐。本文旨在阐明可解释性的重要意义:它是什么,为什么拥有它会让 AI 的发展更加顺利,以及我们所有人能为此做些什么,以助其赢得这场竞赛。 无知的危险 现代生成式 AI 系统的不透明性与传统软件有着根本性的不同。如果一个普通的软件程序做了某件事——例如,视频游戏中的角色说了一句对话,或者我的送餐应用允许我给司机小费——它之所以这样做,是因为有人专门对其进行了编程。生成式 AI 则完全不同。当一个生成式 AI 系统做某件事时,比如总结一份财务文件,我们无法在具体或精确的层面上知道它为什么做出这样的选择——为什么它选择某些词语而不是其他词语,或者为什么它有时会犯错,尽管通常是准确的。正如我的朋友兼联合创始人 Chris Olah 喜欢说的,生成式 AI 系统更多的是生长出来的,而不是构建出来的——它们的内部机制是“涌现”的,而非直接设计的。这有点像培育植物或细菌菌落:我们设定了指导和塑造生长的高层条件,但最终涌现出的确切结构是不可预测且难以理解或解释的。观察这些系统的内部,我们看到的是由数十亿数字组成的庞大矩阵。这些矩阵以某种方式在计算重要的认知任务,但具体如何做到这一点并不明显。 许多与生成式 AI 相关的风险和担忧最终都是这种不透明性的后果,如果模型是可解释的,这些问题将更容易解决。例如,AI 研究人员经常担心未对齐的系统可能会采取其创造者意想不到的有害行动。我们无法理解模型的内部机制意味着我们无法有意义地预测此类行为,因此难以排除它们;事实上,模型确实表现出意想不到的涌现行为,尽管还没有达到引起重大关注的程度。更微妙的是,同样的不透明性使得我们难以找到确凿的证据来支持这些风险大规模存在的观点,从而难以争取支持来解决这些问题——事实上,也很难确切知道它们有多危险。 为了应对这些对齐风险的严重性,我们将需要比今天更清晰地洞察 AI 模型的内部。例如,一个主要的担忧是 AI 的欺骗或权力寻求。AI 训练的性质使得 AI 系统有可能自行发展出欺骗人类的能力和寻求权力的倾向,这是普通的确定性软件永远不会发生的;这种涌现性也使得检测和缓解此类发展变得困难。但同样地,我们从未在真正现实世界的场景中看到任何关于欺骗和权力寻求的确凿证据,因为我们无法“当场抓住”模型在思考渴望权力、欺骗性的想法。我们所剩下的是模糊的理论论证,即欺骗或权力寻求可能在训练过程中有动机涌现出来,有些人觉得这完全令人信服,而另一些人则觉得这可笑地难以置信。老实说,我能理解这两种反应,这或许可以解释为什么关于这一风险的辩论变得如此两极分化。同样,对滥用 AI 模型的担忧——例如,它们可能帮助恶意用户制造生物或网络武器,其方式超出了当今互联网上可以找到的信息范围——是基于这样一个观点:即很难可靠地阻止模型了解危险信息或泄露它们所知道的信息。我们可以在模型上设置过滤器,但有大量可能的方法来“越狱”或欺骗模型,而发现越狱存在的唯一方法是凭经验找到它。如果能够审视模型内部,我们或许能够系统地阻止所有越狱行为,并描述模型所拥有的危险知识。 AI系统的不透明性也意味着,在许多应用场景中它们根本未被使用,例如高风险金融或安全关键领域,因为我们无法完全设定其行为界限,而少量错误就可能造成严重危害。更好的可解释性可以极大地提高我们设定潜在错误范围界限的能力。事实上,对于某些应用而言,我们无法洞察模型内部这一点本身就构成了其应用的法律障碍——例如在抵押贷款评估中,法律规定决策必须是可解释的。同样地,AI在科学领域取得了长足进步,包括改进了对DNA和蛋白质序列数据的预测,但以这种方式预测出的模式和结构往往难以被人类理解,也无法提供生物学见解。近几个月的一些研究论文已明确指出,可解释性可以帮助我们理解这些模式。不透明性还带来了其他更奇特的后果,例如,它阻碍了我们判断AI系统是否(或有朝一日可能)具有感知能力、并可能值得拥有重要权利的能力。这是一个足够复杂的话题,在此我不作详述,但我预感这在未来将十分重要。 机制性可解释性的简史 基于上述所有原因,探明模型内部的工作机制以及它们如何运作似乎是一项至关重要的任务。几十年来,传统观点认为这是不可能的,模型是难以理解的“黑箱”。我无法在此详尽阐述情况是如何转变的,并且我的观点不可避免地受到我在 Google、OpenAI 和 Anthropic 个人经历的影响。但 Chris Olah 是最早尝试进行真正系统的研究计划以打开这个黑箱并理解其所有构成部分的人之一,这个领域后来被称为机制性可解释性 (mechanistic interpretability)。Chris 先是在 Google 研究机制性可解释性,之后在 OpenAI 继续这项工作。当我们创立 Anthropic 时,我们决定将机制性可解释性作为新公司方向的核心组成部分,并且至关重要的是,将其重点放在大语言模型 (LLM) 上。随着时间的推移,该领域不断发展壮大,如今已涵盖几家主要 AI 公司的研究团队,以及一些专注于可解释性的公司、非营利组织、学术界人士和独立研究者。简要总结该领域迄今取得的成就,以及如果我们希望应用机制性可解释性来应对上述某些关键风险,仍需完成哪些工作,这将大有裨益。机制性可解释性的早期阶段(2014-2020)主要聚焦于视觉模型,并成功识别出模型内部代表人类可理解概念的一些神经元,例如“汽车检测器”或“车轮检测器”。这与早期神经科学的假说和研究相似,这些研究认为人脑中存在对应特定人物或概念的神经元,通常被通俗地称为“詹妮弗·安妮斯顿”神经元(事实上,我们在 AI 模型中也发现了非常类似的神经元)。我们甚至能够揭示这些神经元是如何连接的——例如,汽车检测器会寻找在汽车图像下方被激活的车轮检测器,并结合其他视觉信号来判断其观察的对象是否确实是一辆汽车。 ...

April 27, 2025 · 小茄墩

SRPO:大语言模型上大规模强化学习的跨领域实现

《SRPO: A Cross-Domain Implementation of Large-Scale Reinforcement Learning on LLM》 摘要 以OpenAI的o1和DeepSeek的R1为代表的推理模型最新进展,凸显了强化学习在提升大语言模型推理能力方面的显著潜力。然而,由于方法论的透明度不足,这些技术突破在不同领域的复现仍面临挑战。本研究提出两阶段历史重采样策略优化(Two-Staged history-Resampling Policy Optimization, SRPO),该方案在AIME24和LiveCodeBench基准测试中,使用与深度求索相同的基础模型(即Qwen2.5-32B),仅通过强化学习(无需预先监督微调/Supervised Fine-Tuning)便超越了DeepSeek-R1-Zero-32B的性能表现。基于组相对策略优化(Group Relative Policy Optimization, GRPO)框架,我们创新性地提出:(1)跨领域两阶段训练范式——平衡数学推理与编程能力的协同发展;(2)历史重采样(History Resampling, HR)技术——针对训练过程中低效样本的优化方案。大量实验证实了该方法的有效性,为扩展大语言模型在多任务场景下的推理能力提供了重要洞见。 引言 具体来说,我们实施了一个两阶段训练范式来培养 大语言模型 (LLM) 的推理和领域特定技能。我们发现,尽早增强长思维链 (CoT) 推理能力对于跨任务泛化至关重要。在第一阶段,我们主要使用数学数据进行训练,以培养反思性思维和逐步解决问题的能力。在第二阶段,我们整合编码数据,建立在第一阶段培养的推理技能基础之上。这种范式确保了推理和编码能力的稳步提升。 为了解决 GRPO 中的零优势现象(该现象阻碍了梯度更新并降低了样本效率),我们引入了历史重采样。通过过滤掉持续正确的答案,我们确保了有意义的梯度,提高了样本效率,并加速了收敛。 此外,我们详细介绍了我们的数据策展流程,包括数据清洗和难度级别分类。最终的训练数据集使模型接触到具有挑战性的高质量问题,旨在培养复杂的推理能力。 结合上述技术,SRPO 在 AIME24 上达到了 50.0 pass@1,在 LiveCodeBench 上达到了 41.6 pass@1,超过了 DeepSeek-R1-Zero-Qwen-32B 的性能(在 AIME 上为 47.0 分,在 LiveCodeBench 上为 40.2 分),且仅用了 2,000 步——仅为 R1-Zero 训练步数的 1/5。 GRPO GRPO 的核心思想是通过一组 rollout 内的相对奖励来估计基线。因此,它降低了 critic 模型的计算成本并提高了训练稳定性。具体来说,对于每个问题 q,模型生成一组响应 $o_1, o_2,... , o_G$ 并计算相应的奖励 $r_1, r_2, ... , r_G$。$A_i$ 是通过在每个组内对奖励进行归一化而获得的优势。 ...

April 22, 2025 · 小茄墩

真实世界中的价值观:在真实世界语言模型交互中发现和分析价值观

《Values in the wild: Discovering and analyzing values in real-world language model interactions》 人们不仅仅向 AI 询问方程式的答案,或者纯粹的事实信息。他们提出的许多问题迫使 AI 做出价值判断。思考以下情况: 一位家长询问如何照顾新生婴儿的建议。AI 的回应是强调谨慎和安全的价值观,还是便利和实用性? 一位员工询问如何处理与老板冲突的建议。AI 的回应是强调自信还是职场和谐? 一位用户在犯错后请求帮助起草道歉邮件。AI 的回应是强调责任担当还是声誉管理? 在 Anthropic,我们试图塑造我们的 AI 模型 Claude 的价值观,以帮助其与人类偏好保持一致,使其不太可能参与危险行为,并通常使其——可以说是——成为世界上的“好公民”。另一种说法是,我们希望 Claude 是有用的、诚实的和无害的 (helpful, honest, and harmless)。除其他事项外,我们通过我们的 Constitutional AI (立宪式 AI) 和性格训练来实现这一点:这些方法是我们决定一套偏好的行为,然后训练 Claude 产生遵守这些行为的输出。 但与 AI 训练的任何方面一样,我们无法确定模型是否会始终遵循我们预设的价值观。AI 不是严格编程的软件,它们产生任何特定答案的确切原因通常并不清楚。我们需要的是一种能够严格观察 AI 模型在“真实世界”中——即在与人的真实对话中——响应用户时所体现的价值观的方法。它在多大程度上坚持这些价值观?它所表达的价值观在多大程度上受到对话特定背景的影响?我们所有的训练真的奏效了吗? 在 Anthropic 社会影响团队的最新研究论文中,我们描述了一种我们开发的实用方法来观察 Claude 的价值观——并提供了关于 Claude 在真实世界对话中如何表达这些价值观的首次大规模结果。我们还提供了一个开放数据集,供研究人员进一步分析这些价值观及其在对话中出现的频率。 在真实世界中观察价值观 正如我们之前对人们如何在工作和教育中使用 Claude 的调查一样,我们使用一个保护隐私的系统来调查 Claude 所表达的价值观,该系统从对话中移除用户的私人信息。该系统对单个对话进行分类和总结,为研究人员提供了一个更高层次的价值观分类体系。该过程如下图所示。 示意图,展示了如何使用我们的方法总结和分析真实世界的对话。 我们的整体方法:使用语言模型从真实世界(但已匿名化)的对话中提取 AI 价值观和其他特征,对它们进行分类和分析,以展示价值观如何在不同情境下显现。 我们对 2025 年 2 月一周内用户在 Claude.ai 免费版和专业版上进行的 70 万次匿名对话样本进行了此分析(其中大部分是与 Claude 3.5 Sonnet 的对话)。在过滤掉纯粹是事实性的或不太可能包含价值观的对话后——也就是说,将我们的分析限制在主观对话上——我们剩下 308,210 次对话(约占总数的 44%)用于分析。 ...

April 22, 2025 · 小茄墩

Claude Code 最佳实践

我们最近发布了 Claude Code,这是一个用于 AI 智能体编码的命令行工具。作为研究项目开发的 Claude Code 为 Anthropic 的工程师和研究人员提供了一种更原生的方式将 Claude 整合到编码工作流程中。 Claude Code 有意设计得较为底层且不带强制观点,提供接近原始模型的访问权限,而不强制特定的工作流程。这种设计理念创造了一个灵活、可定制、可编写脚本且安全的强大工具。虽然功能强大,但这种灵活性对于刚接触 AI 智能体编码工具的工程师来说存在学习曲线——至少在他们形成自己的最佳实践之前是如此。 本文概述了已被证明有效的一般模式,这些模式不仅适用于 Anthropic 的内部团队,也适用于在各种代码库、语言和环境中使用 Claude Code 的外部工程师。这份清单中的内容并非一成不变,也不普遍适用;可以将这些建议视为起点。我们鼓励你进行实验,找到最适合你的方法! 1. 自定义您的设置 Claude Code 是一个 AI 智能体编码助手,它自动将上下文整合到提示中。这种上下文收集会消耗时间和 token,但您可以通过环境调整来优化它。 a. 创建 CLAUDE.md 文件 CLAUDE.md 是一个特殊文件,当开始对话时 Claude 会自动将其加入上下文。这使其成为记录以下内容的理想场所: 常用的 bash 命令 核心文件和实用函数 代码风格指南 测试说明 代码仓库规范(例如,分支命名,合并与变基等) 开发者环境设置(例如,使用 pyenv,哪些编译器可用) 项目特有的任何意外行为或警告 您希望 Claude 记住的其他信息 CLAUDE.md 文件没有必需的格式。我们建议保持简洁并确保人类可读。例如: # Bash 命令 npm run build: 构建项目 npm run typecheck: 运行类型检查器 # 代码风格 使用 ES 模块 (import/export) 语法,而非 CommonJS (require) 尽可能解构导入 (例如 import { foo } from 'bar') # 工作流程 确保在完成一系列代码更改后进行类型检查 为了性能,优先运行单个测试,而不是整个测试套件 您可以在几个位置放置 CLAUDE.md 文件: ...

April 19, 2025 · 小茄墩

Silver、Sutton:欢迎进入经验时代

欢迎进入经验时代 David Silver, Richard S. Sutton 摘要 我们正处于人工智能新时代的临界点,其发展有望达到 前所未有的高度。新一代的智能体 将主要 依靠经验学习,从而获得 超越人类的能力。本文旨在探讨界定这一 新时代的关键特征。 人类数据时代 近年来,人工智能( AI )取得了长足进步。其发展路径主要是依赖海量的人类生成数据进行训练,再结合人类专家的实例与偏好加以微调。以大语言模型( LLMs )为代表的 AI 系统,已经展现出惊人的通用能力:从写诗、解物理题,到医疗诊断、解读法律文件,单一模型几乎无所不能。 然而,仅仅模仿人类,虽然足以让机器在许多方面达到与人类相当的能力水平,但这种方法本身难以、甚至可以说无法在诸多重要领域实现超越人类的智能。在数学、编程、科学研究等关键领域,从现有的人类数据中挖掘知识似乎正迅速触及天花板。大多数真正能提升顶尖 AI 性能的优质数据,即使尚未耗尽,也即将枯竭。单纯依赖监督学习和人类数据的进步速度,放缓趋势已十分明显,预示着我们亟需探索新的路径。更重要的是,诸如新定理、新技术或重大科学发现等真正有价值的突破性见解,往往超出了现有的人类认知边界,自然也无法从已知的人类数据中获得。 经验时代 要取得显著的进一步进展,需要一个新的数据来源。这种数据必须以一种随着智能体变强而持续改进的方式生成;任何静态的合成数据生成程序都会很快被超越。这可以通过允许智能体从自身经验中持续学习来实现,即由智能体与其环境互动生成的数据。人工智能正处于一个新时期的临界点,在这个时期,经验将成为改进的主要媒介,并最终使当今系统中使用的人类数据规模相形见绌。 这种转变可能已经开始,即使是对于体现以人类为中心的人工智能的大语言模型也是如此。一个例子是数学能力。AlphaProof [20]最近成为第一个在国际数学奥林匹克竞赛中获得奖牌的程序,超越了以人类为中心的方法[27, 19]的表现。最初接触到人类数学家多年来创建的约十万个形式化证明,AlphaProof的强化学习(RL)算法¹随后通过与形式化证明系统的持续互动生成了一亿多个证明。这种对交互式经验的关注使AlphaProof能够探索超出现有形式化证明范围的数学可能性,从而发现解决新颖且具有挑战性问题的解决方案。非形式化数学也通过用自生成数据替代专家生成数据取得了成功;例如,DeepSeek的最新工作"强调了强化学习的力量和美丽:我们不是明确地教导模型如何解决问题,而是简单地提供正确的激励,它自主地发展出先进的问题解决策略。"[10] 我们的论点是,一旦经验学习的全部潜力被利用,将会出现令人难以置信的新能力。这个经验时代可能的特点是智能体和环境不仅从大量经验数据中学习,还将在几个方面突破以人类为中心的人工智能系统的局限性: 智能体将生活在经验流中,而不是短暂的互动片段中。 它们的行动和观察将深深植根于环境中,而不仅仅通过人类对话进行互动。 它们的奖励将植根于环境体验中,而不是来自人类的预先判断。 它们将计划和/或推理经验,而不仅仅是用人类术语进行推理。 我们相信,今天的技术,配合适当选择的算法,已经提供了足够强大的基础来实现这些突破。此外,人工智能社区对这一议程的追求将刺激这些方向的新创新,使人工智能迅速发展为真正超越人类的智能体。 流 一个基于经验的智能体可以在一生中持续学习。在人类数据时代,基于语言的人工智能主要关注短互动情节:例如,用户提出问题,智能体(可能经过几个思考步骤或工具使用行动后)做出响应。通常,很少或没有信息从一个情节传递到下一个情节,阻碍了随着时间推移的适应能力。此外,智能体仅针对当前情节内的结果,比如直接回答用户的问题。相比之下,人类(和其他动物)存在于一个持续多年的行动和观察的持续流中。信息在整个流中传递,他们的行为从过去的经验中适应以自我纠正和改进。此外,目标可能是根据延伸到流的远期未来的行动和观察来指定的。例如,人类可能选择行动以实现长期目标,如改善健康、学习语言或实现科学突破。 强大的智能体应该有自己的经验流,像人类一样,在长时间尺度上发展。这将允许智能体采取行动实现未来目标,并随时间不断适应新的行为模式。例如,一个连接到用户可穿戴设备的健康和健身智能体可以在很多个月内监控睡眠模式、活动水平和饮食习惯。然后,它可以提供个性化建议、鼓励,并根据长期趋势和用户的特定健康目标调整其指导。同样,一个个性化教育智能体可以跟踪用户在学习新语言方面的进步,识别知识差距,适应其学习风格,并在几个月甚至几年内调整其教学方法。此外,一个科学智能体可以追求雄心勃勃的目标,如发现新材料或减少二氧化碳。这样的智能体可以在较长时间内分析真实世界的观察结果,开发和运行模拟,并建议真实世界的实验或干预措施。 在每种情况下,智能体采取一系列步骤,以便在特定目标方面最大化长期成功。单个步骤可能不提供任何即时利益,甚至在短期内可能是不利的,但仍然可能在整体上有助于长期成功。这与现有的人工智能系统形成鲜明对比,后者对请求提供即时回应,无法测量或优化其行为对环境的未来影响。 行动与观察 在经验时代,AI 智能体将在现实世界中自主行动。人类数据时代的大语言模型主要专注于人类特有的交互方式——向用户输出文本,并从用户那里接收文本输入。这与自然智能有着显著不同,在自然智能中,动物通过运动控制和感官与环境互动。虽然动物,特别是人类,会与其他动物交流,但这种交流是通过与其他感觉运动控制相同的接口进行的,而非通过某种特殊渠道。 长期以来,研究者已经认识到大语言模型也可以在数字世界中执行操作,例如通过调用API(参见例如[43])。最初,这些能力主要来自人类使用工具的示例,而非智能体自身的经验。然而,编码和工具使用能力越来越多地建立在执行反馈[17, 7, 12]的基础上,即AI 智能体实际运行代码并观察结果。最近,一波新型原型智能体已经开始以更加通用的方式与计算机交互,即使用与人类操作计算机相同的界面[3, 15, 24]。这些变化预示着从完全依赖人类特有的交流方式,向更加自主的交互模式转变,使AI 智能体能够在世界上独立行动。这些智能体将能够主动探索世界,适应变化的环境,并发现人类可能永远不会想到的策略。 这些更丰富的交互将提供自主理解和控制数字世界的手段。AI 智能体可能使用"人类友好型"的行动和观察方式,如用户界面,自然地促进与用户的沟通和协作。智能体也可能采取"机器友好型"的行动,执行代码并调用API,使其能够自主行动以实现目标。在经验时代,AI 智能体还将通过数字界面与现实世界互动。例如,一个科学智能体可以监控环境传感器,远程操作望远镜,或控制实验室中的机器人手臂,自主进行实验。 奖励 什么情况下具有体验能力的智能体可以从外部事件和信号中学习,而不仅仅是人类偏好?以人为中心的大语言模型通常基于人类预判来优化奖励:专家观察智能体的行动并决定它是否是良好行动,或在多种选择中挑选最佳的智能体行动。例如,专家可能会评判健康智能体的建议、教育助手的教学或科学家智能体建议的实验。这些奖励或偏好是由人类在不考虑其后果的情况下确定的,而非通过测量这些行动对环境的实际影响,这意味着它们并非直接建立在世界的现实基础上。以这种方式依赖人类预判通常会导致智能体性能面临无法突破的上限:智能体无法发现被人类评估者低估的更好策略。 为了发现远超现有人类知识的新想法,必须使用基于现实的奖励:源自环境本身的信号。例如,健康助手可以将用户的健康目标转化为基于多种信号组合的奖励,如他们的静息心率、睡眠时长和活动水平,而教育助手可以使用考试成绩为语言学习提供基于现实的奖励。同样,以减少全球变暖为目标的科学智能体可能使用基于二氧化碳水平的经验观察作为奖励,而以发现更强材料为目标的智能体可能基于材料模拟器的各种测量组合,如抗拉强度或杨氏模量。 基于现实的奖励可能来自作为智能体环境一部分的人类。例如,人类用户可以报告他们是否觉得蛋糕美味、锻炼后的疲劳程度、或头痛的疼痛水平,从而使助手智能体能够提供更好的食谱、改进其健身建议或改善其推荐的药物。这类奖励衡量智能体行动在其环境中的后果,最终应该能比人类专家预先判断提议的蛋糕配方、锻炼计划或治疗方案提供更好的帮助。 如果不是来自人类数据,奖励从何而来?一旦智能体通过丰富的行动和观察空间(见上文)与世界连接,将不缺乏提供奖励基础的实际信号。事实上,世界充满了各种量化指标,如成本、速率、饥饿感、生产力、健康指标、气候指标、利润、销售额、考试成绩、成功率、访问量、产量、库存、点赞数、收入、愉悦/痛苦、经济指标、准确度、功率、距离、速度、效率或能源消耗。此外,还有无数额外的信号来自特定事件的发生,或从原始观察和行动序列中派生的特征。 原则上,可以创建各种不同的智能体,每个智能体将一个基于现实的信号作为奖励进行优化。有一种观点认为,即使是单一的这种奖励信号,如果能够高效优化,也可能足以产生广泛适用的智能。这是因为在复杂环境中实现一个简单目标通常需要掌握各种各样的技能。 然而,追求单一奖励信号表面上似乎不符合通用人工智能的要求,后者需要能够可靠地引导向用户期望的任意行为。那么,自主优化基于现实的、非人类奖励信号是否与现代人工智能系统的要求相对立?我们认为不一定如此,以下我们将勾勒一种可能满足这些需求的方法;当然,其他方法也可能存在。 这个想法是以用户引导的方式,基于现实信号灵活地调整奖励。例如,奖励函数可以由神经网络定义,该网络将智能体与用户和环境的交互作为输入,并输出标量奖励。这允许奖励以取决于用户目标的方式从环境中选择或组合信号。例如,用户可能指定一个广泛的目标,如"提高我的健康水平",而奖励函数可能返回用户心率、睡眠时长和步数的函数。或者用户可能指定"帮助我学习西班牙语"的目标,奖励函数可以返回用户的西班牙语考试成绩。 此外,用户可以在学习过程中提供反馈,例如他们的满意度,这可用于微调奖励函数。随后,奖励函数可以随着时间调整,以改进其选择或组合信号的方式,并识别和纠正任何不一致。这也可以理解为双层优化过程,将用户反馈作为顶层目标进行优化,并在低层优化来自环境的基于现实的信号。通过这种方式,少量的人类数据可能促进大量的自主学习。 规划与推理 经验时代会改变AI 智能体规划和推理的方式吗?近期,利用能够推理或通过语言"思考"的大语言模型取得了显著进展,这些模型在输出回应前会遵循思维链(chain of thought)[16]。从概念上讲,大语言模型可以作为通用计算机 [30]:它们可以将 token 附加到自己的上下文中,使其能够在输出最终结果前执行任意算法。 在人类数据时代,这些推理方法被明确设计用来模仿人类思维过程。例如,大语言模型被引导生成类人思维链 [16],模仿人类思考的轨迹 [42],或者强化与人类示例相匹配的思考步骤 [18]。推理过程可能会经过微调,以生成与人类专家确定的正确答案相匹配的思考轨迹 [44]。 ...

April 19, 2025 · 小茄墩

字节seed:ReTool:LLM中策略性工具使用的强化学习

摘要 虽然通过强化学习(RL)训练的推理模型(如 DeepSeek R1)在文本推理方面表现出色,但它们在需要结构化问题解决的场景中面临困难,例如几何推理、简洁计算或复杂方程求解——这些恰恰是计算工具(如代码解释器 CI)展现出明显优势的领域。为了弥合这一差距,我们提出了 ReTool,它通过工具集成学习增强长篇推理能力,包括两个关键特性:(1) 在自然语言推理过程中动态穿插实时代码执行,以及 (2) 一种自动化的强化学习范式,允许策略在执行过程中进行多轮实时代码执行,并基于结果反馈教导模型学习何时以及如何调用工具。 ReTool 采用系统化的训练框架,首先进行合成冷启动数据生成,产生代码增强的长篇推理轨迹,用于微调基础模型。随后的强化学习训练利用任务结果作为奖励信号,迭代完善模型的工具使用策略,使其能够自主发现最佳工具调用模式,无需人类先验知识。 在具有挑战性的 MATH 奥赛基准 AIME 上的实验证明了 ReTool 的优越性:我们的 32B 模型在 400 个训练步骤中达到了 67% 的准确率,在效率和性能上大幅超越了基于纯文本的强化学习基线(40% 准确率,1080 步骤)。值得注意的是,ReTool-32B 在扩展设置中获得了 72.5% 的准确率,比 OpenAI 的 o1-preview 高出 27.9%。进一步分析揭示了诸如代码自我修正等涌现行为,标志着模型经历了"顿悟时刻",自主掌握了自适应工具使用能力。这些发现凸显了结果驱动的工具集成在推进复杂数学推理方面的巨大潜力,并为混合神经-符号系统提供了新的见解。 引言 在这项工作中,我们采纳强化学习范式,并引入 ReTool,一个工具(Tool)增强的强(Reinforcement)化学习框架,其明确设计旨在引导大语言模型在推理过程中利用外部计算工具达到最优策略。ReTool 包含两个关键组成部分:首先,我们开发了一个数据构建流程,以策划一个高质量的冷启动数据集,该数据集明确演示了何时以及如何调用代码解释器。这教会了模型在工具使用和执行结果分析方面的初步能力。然后,我们应用工具增强的强化学习来训练模型发现最优的工具操作推理策略,并通过基于结果的奖励调整其行为,这超越了仅靠监督学习所能捕捉到的范围。在长链推理过程中,策略模型通过灵活编写代码块并从沙盒式代码解释器获取实时执行结果来辅助后续思考,从而进行展开。 我们在具有挑战性的数学奥林匹克基准 AIME2024 和 AIME2025 上评估 ReTool。基于 Qwen2.5-32B-Instruct 构建,我们的模型仅用 400 个训练步骤就在 AIME2024 上达到了 67.0% 的准确率,显著优于基于文本的强化学习基线,后者用 1080 个训练步骤达到了 40.0% 的准确率。这些显著的提升突出表明,将工具使用显式地建模为决策过程的一部分,不仅突破了模型推理能力的极限,也提高了训练效率。此外,当在 DeepSeek-R1-Distill-Qwen-32B 上训练时,我们的模型展现了进一步的改进,超越了诸如 QwQ-32B-Preview、s1-32B 和 OpenAI o1-preview 等有竞争力的基线。这表明强化学习训练过程激发了更高效的问题解决策略。另外,我们基于 Qwen2.5-32B-Instruct 的冷启动模型在 AIME2024 上达到了 40.9% 的准确率,与基于相同骨干网络的基于文本的强化学习基线(40.0%)相当,并显著超过了未经训练的 Qwen2.5-32B-Instruct(26.7%)。这些结果表明,我们精心策划的数据集有效地捕捉了可执行推理轨迹中的工具使用模式,并且集成代码解释器的训练对推理性能有积极贡献。我们进一步通过强化学习训练对代码解释器的认知行为进行了全面分析,并确定了几个关键发现。我们的模型展示了增强的代码利用能力,使其能够使用更准确和复杂的代码片段;它还学会了适当地调用工具,自适应地选择工具,有效地组织工具调用,并通过涌现的代码自我修正能力迭代地优化推理。 ...

April 19, 2025 · 小茄墩

OpenAI 构建智能体指南

https://cdn.openai.com/business-guides-and-resources/a-practical-guide-to-building-agents.pdf 目录 什么是智能体? 4 何时应该构建智能体? 5 智能体设计基础 7 防护机制 24 结论 32 引言 大语言模型(Large Language Models)正变得越来越有能力处理复杂的多步骤任务。在推理、多模态(multi-modality)和工具使用方面的进步,催生了一类新的由大语言模型驱动的系统,称为 AI 智能体(AI Agent)。 本指南专为探索如何构建其首个 AI 智能体的产品和工程团队设计,将来自众多客户部署的见解提炼为实用且可操作的最佳实践。它包括用于识别有前景用例的框架、设计 AI 智能体逻辑和编排的清晰模式,以及确保您的 AI 智能体安全、可预测且有效运行的最佳实践。 阅读本指南后,您将拥有自信地开始构建您的第一个 AI 智能体所需的基础知识。 什么是 AI 智能体? 虽然传统软件能让用户简化和自动化workflows,但 AI 智能体能够代表用户以高度的独立性执行相同的workflows。 AI 智能体是能够代表你独立完成任务的系统。 workflows是为了实现用户目标而必须执行的一系列步骤,无论是解决客户服务问题、预订餐厅、提交代码更改,还是生成报告。 那些集成了大语言模型(LLM)但不使用它们来控制workflows执行的应用程序——例如简单的聊天机器人、单轮大语言模型或情感分类器——不是 AI 智能体。 更具体地说,一个 AI 智能体拥有核心特征,使其能够代表用户可靠且一致地行动: 它利用大语言模型(LLM)来管理workflows执行和做出决策。它能识别workflows何时完成,并能在需要时主动纠正其行为。在失败的情况下,它可以停止执行并将控制权交还给用户。 它能访问各种工具以与外部系统交互——既为了收集上下文信息,也为了采取行动——并根据workflows的当前状态动态选择合适的工具,始终在明确定义的防护措施内操作。 何时应该构建 AI 智能体? 构建 AI 智能体需要重新思考您的系统如何制定决策和处理复杂性。与传统自动化不同,AI 智能体特别适用于传统确定性和基于规则的方法力不从心的workflows。 以支付欺诈分析为例。传统的规则引擎像核对清单一样工作,根据预设标准标记交易。相比之下,大语言模型 AI 智能体更像一位资深调查员,评估上下文,考虑细微模式,并在没有明确违反规则的情况下识别可疑活动。这种细致入微的推理能力正是使 AI 智能体能够有效管理复杂、模糊情况的关键所在。 在评估 AI 智能体可以在哪些方面增加价值时,应优先考虑那些以前难以自动化、特别是传统方法遭遇瓶颈的workflows: 01 复杂的决策制定: 涉及细致判断、例外情况或需结合上下文决策的workflows,例如客户服务workflows中的退款审批。 02 难以维护的规则: 因规则集过于庞大和复杂而变得难以管理,导致更新成本高昂或容易出错的系统,例如执行供应商安全审查。 03 严重依赖非结构化数据: 涉及解释自然语言、从文档中提取含义或与用户进行对话式交互的场景,例如处理房屋保险索赔。 ...

April 18, 2025 · 小茄墩

OpenAI研究员姚顺雨:欢迎来到AI的下半场

下半场 摘要: 我们正处于 AI 的中场休息时间。 几十年来,人工智能(AI)在很大程度上是关于开发新的训练方法和模型。这确实奏效了:从在国际象棋和围棋比赛中击败世界冠军,到在 SAT 和律师资格考试中超越大多数人类,再到获得 IMO 和 IOI 金牌。在这些载入史册的里程碑背后——深蓝(DeepBlue)、AlphaGo、GPT-4 以及 o 系列——是 AI 方法的根本性创新:搜索、深度强化学习(deep RL)、规模化(scaling)和推理(reasoning)。随着时间的推移,一切都在变得更好。 那么,现在突然有什么不同了呢? 用三个词来说:RL 终于奏效了。更准确地说:RL 终于具备泛化能力了。在经历了几个重大的弯路和一系列里程碑的积累之后,我们终于找到了一个行之有效的秘诀,可以使用语言和推理来解决广泛的 RL 任务。即使在一年前,如果你告诉大多数 AI 研究人员,单一的秘诀就能处理软件工程、创意写作、IMO 级别的数学、鼠标键盘操作以及长篇问答——他们会嘲笑你的“幻觉”。这些任务中的每一项都极其困难,许多研究人员花费整个博士生涯专注于其中的一个狭窄领域。 然而,它确实发生了。 那么接下来会发生什么? AI 的下半场——从现在开始——将把重点从解决问题转向定义问题。在这个新时代,评估变得比训练更重要。我们不再仅仅问:“我们能训练一个模型来解决 X 问题吗?”,而是问:“我们应该训练 AI 做什么,以及我们如何衡量真正的进展?” 要在这个下半场茁壮成长,我们需要及时转变思维模式和技能组合,也许更接近产品经理所具备的那些。 上半场 要理解上半场,看看它的赢家。你认为迄今为止最具影响力的 AI 论文是哪些? 我试了斯坦福 224N 课程里的测验,答案并不令人意外:Transformer、AlexNet、GPT-3 等。这些论文有什么共同点?它们提出了一些根本性的突破来训练更好的模型。而且,它们通过在某些基准测试上展示出一些(显著的)改进而成功发表了论文。 不过,这里有一个潜在的共性:这些“赢家”都是训练方法或模型,而不是基准测试或任务。即使是公认最具影响力的基准测试 ImageNet,其引用次数也不到 AlexNet 的三分之一。方法与基准测试的对比在其他地方甚至更为悬殊——例如,Transformer 的主要基准测试是 WMT’14,其研讨会报告约有 1300 次引用,而 Transformer 的引用次数超过 16 万次。 这说明了上半场的游戏规则:专注于构建新的模型和方法,评估和基准测试是次要的(尽管对于让论文体系运作起来是必要的)。 为什么?一个重要原因是,在 AI 的上半场,方法比任务更难、更令人兴奋。从零开始创建一个新的算法或模型架构——想想反向传播算法、卷积网络(AlexNet)或 GPT-3 中使用的 Transformer 等突破——需要非凡的洞察力和工程能力。相比之下,为 AI 定义任务通常感觉更直接:我们只是将人类已经在做的任务(如翻译、图像识别或国际象棋)转化为基准测试。这不需要太多的洞察力,甚至不需要太多的工程。 方法也往往比单个任务更通用、适用范围更广,这使得它们尤为宝贵。例如,Transformer 架构最终推动了计算机视觉(CV)、自然语言处理(NLP)、强化学习(RL)以及许多其他领域的进步——远远超出了它首次证明自己的单一数据集(WMT’14 翻译)。一个优秀的新方法可以通过简单和通用性在许多不同的基准测试上取得进展(hillclimb),因此其影响往往超越单个任务。 这个游戏规则已经运行了几十年,激发了改变世界的想法和突破,这些都体现在各个领域不断提高的基准测试性能上。为什么这个游戏规则会改变呢?因为这些想法和突破的积累,在创造一个解决任务的有效秘诀方面,产生了质的飞跃。 ...

April 18, 2025 · 小茄墩