Era of Experience 这篇文章中提到：如果要实现 AGI， 构建能完成复杂任务的通用 agent，必须借助“经验”这一媒介，这里的“经验”就是指强化学习过程中模型和 agent 积累的、人类数据集中不存在的高质量数据。
强化学习是 AGI 的关键解法。从 OpenAI o1 到 DeepSeek R1，我们不断在看到强化学习的潜力：DeepMind AlphaProof 被认为是“经验时代”初露端倪的一个例子，作为第一个在 IMO 获奖的 AI，AlphaProof 借助 RL 算法自行“做题”，积累经验，AlphaProof 的案例表明，在像数学这样人类高水平知识接近极限的领域，RL 通过互动试错可以突破瓶颈，取得超人类的成果。
以 AlphaProof 为开端，整个数学证明领域也在最近半年迎来了 AI 突破的密集期：除了 AlphaProof ，OpenAI 的 o1 模型在数学推理上展现出了惊人表现，DeepSeek-Prover 三部曲也在形式化数学证明上不断创造新纪录。
为了理解数学和 AGI 的关系，海外独角兽访谈了 DeepSeek-Prover 系列的核心作者辛华剑：
• 为什么 AI 研究中要特别关注数学证明能力？RL 和数学领域的研究进步会如何带来智能泛化？
• 无论是在数学还是代码领域，要让 RL 能够有效工作，最关键的一点就在于 verification 或 evaluation 的设定，今天的模型是很好的“锤子”，但我们却缺少足够好的“钉子”。
• 形式化数学和 Agent 探索天然适配当前的形式化工具需要从静态的 Theorem Prover 转向具备自我规划、自我修复和自我知识积累能力的 Proof Engineering Agent。
• 作为 GenAI 的下一步，Certified AI 强调：我们不仅需要生成能力，更需要对生成质量有良好的控制。
• 下一个 GPT-4 时刻是实现具备自主规划、执行和反思能力的 Agent。
……
💡 目录 💡
01 AGI 是 Agent 的 AGI
02 当代数学研究面临“分布式挑战”
03 DeepSeek Prover 三部曲
04 形式化数学和 Multi-Agent 天然契合
05 好的 benchmark 是给模型“找钉子”
06 GenAI 的下一步是 Certified AI
07 RL，数学，智能泛化
08 下一个 GPT-4 时刻是实现自主 Agent
01.
AGI 是 Agent 的 AGI
海外独角兽：先请华剑介绍一下自己。
华剑：我叫辛华剑，现在是爱丁堡大学人工智能专业的一年级博士生，我的研究方向是使用大语言模型进行形式化数学定理自动证明的任务。我本科就读于中山大学哲学系逻辑学专业，深入学习了这类形式化方法的理论基础，后来在中山大学梁小丹老师的指导下开始以 AI 研究的视角切入这个问题，随后分别在华为诺亚方舟实验室和 DeepSeek AI 做了一系列探索性的工作，现在在读博士的同时也在字节跳动 Seed 团队继续进行这一方向的研究实习。
DeepSeek Prover 在这个领域算是一个比较典型的工作：在 DeepSeek Prover 之前，几乎每一个工作都有独特的名字，但在 DeepSeek Prover 之后，几乎所有的模型都叫什么什么 Prover，比如 Goedel-Prover，Kimina-Prover。基本上 DeepSeek Prover 已经作为这个领域的一种固定的研究范式了，我个人对这件事也比较开心。接下来，我也会在这方面做进一步的探讨，包括从单一定理的证明推广到定理库，对一个完整的数学库进行形式化等。
海外独角兽：华剑在不同的世界一流的组织里做 research 有没有什么不一样的感受？
华剑：DeepSeek 是一个非常年轻的团队，从 2023 年开始组建，我在那工作的时间是 2024 年上半年。DeepSeek 的年轻一方面体现在它的历史不长，Infra、组织、工作方式等都在一个不断演进的过程；另一方面体现在年龄上，DeepSeek 喜欢招应届生，团队年龄整体比较低，团队成员会把很多学校里的工作方式和生活气氛带到公司，这会和一般的创业公司，甚至大公司，有一个比较大的差别。但字节是一个相对来说体系架构更加成熟的企业。各家各有所长。
如果我们处于一个全新的领域，初创公司工作可以快速切入并迅速地成长起来，有针对性地调整人力和技术上的投入。但如果这个领域在技术、工程和商业模式上已经有了很明确的复杂模式，那字节这样的大公司会在面对复杂处境时，有一个更加稳健和全面的打法。
至于学校，目前我能明显感觉到在大模型研究上已经慢慢有一点脱节。许多大的实验很难在学校的计算集群上进行，这种算力上的硬性限制很大程度上影响或决定了研究上的风格，往往局限于在具体的细节上雕花，可能会陷入见木不见林的误区。这一问题在强调规模效应的大模型研究中更加严重，因为往往具体的技术可能只在小模型上效果明显，但这种效果上的收益会随着模型规模的增大而被逐渐淡化。如果学界的团队只能在小规模的实验上进行验证，那就无法确认同样的方法推广到更大规模时是否还能奏效，也就无法对于智能边界的扩张提供有效的指导。
这就是为什么一流的研究范式总是在头部的企业中提出，不仅仅是好的想法无法通过最好的实验证明的，而且是无法进行最好的实验决定了难以提出好的想法。
因此对我个人而言，爱丁堡大学主要还是给我提供了一个可以更好吸收传统知识和进行自由交流的机会，但在前沿问题的探索上，我主要还是依靠企业进行工作。
海外独角兽：从你对 AGI 的理解出发，你今天的研究主线在实现 AGI 的道路上，会起到什么作用？
华剑：AGI 包含很多层面上的意义，语言模型、多模态和机器人等不同领域对这个问题也会给出不同回答。
从语言模型角度，在知识层面上，一方面是 AGI 要能够理解所有人类的知识，并以一种正确的方法，像人类一样成功运用知识；另一方面在于 AGI 能够像人一样运用知识推理，主动生产和积累知识，这是我们之前的研究不太能覆盖到的。
AI 的发展离不开评测，评测的设计很大程度上反映了我们对 AI 的理解和预期。之前只是通过具体的问答等二元结构的任务来对模型进行测评，比如让模型进行一次代码编写，一个知识问答。之前我们认为如果模型能在这样的形式上与人类能力匹配，就是 AGI 了。
但到了 2025 年，我们对 AGI 的要求更高了，实际上是向更 Agent 的方向提出了要求，我们希望 AGI 不但是个知识的使用者，而且能够像人一样是知识的发现者、整理者。这会带来很多额外的挑战。
这个挑战也会反映到数学中的一些具体问题上。在基础数学上，我们想要 AGI 能以更好的方式拆解复杂问题，能提出引理和假设来指导思考方向，能对人类已有的数学知识进行整理、编排，从而找到能够更好概括很多相互独立的数学结论之间的统一结构，我们也希望 AGI 能解决一些开放问题，而这些开放问题可能会引导我们不断想要对已有数学的知识结构进行调整、扩充，甚至这些开放问题都是能够让模型自己提出来的。
比如人类提出了费马大定理之后，发现这不仅仅是一个初等数论的问题，还需要很多高等的知识才能解决。如何提出更好的问题，对于科学研究来说是比较重要的，我们希望模型或者 Agent 能够像人类一样满足知识生产的完整流程，而不仅仅是一个验证流程，这才是能够真正符合我们需求的 AGI。
也只有这样的 AGI 才能真正在各个流程环节上做到人机协作、解决复杂问题，而不是我们把问题整理好后，模型来解决我们已经非常干净地约定和限制好的问题。后者不是一个符合人类水平的 Agent 体系。
总而言之，现在所有对 AGI 的刻画和想象，实际上已经和大家现在对 Agent 的追求非常相近，我认为对 AGI 的讨论如果不涉及其他模态以及和世界的交互的话，我们说的 AGI 就是 Agent 的 AGI。
02.
当代数学研究
面临“分布式挑战”
海外独角兽：你的研究领域是 LLM 加形式化数学，能否先解释下形式化数学是什么？和大家熟悉的纸笔演算，自然语言表示的数学有什么不同？
华剑：大家日常做 LLM 的过程中，其实不太会用到形式化方法，比如测试一段代码的正确性，传统的方法是编写单元测试，看输入输出是否符合预期，而从 70 年代开始，形式化会用更严格的方法来对系统进行建模，尝试描述每个函数确切的行为性质，用证明来阐述它会做什么、不会做什么，而不是简单地测试会不会有意外输出。总的来说，形式化方法就是用符号化的方式对整个系统进行建模和推理。
这种方法并不局限于使用特殊的形式化语言来进行系统描述，实际上可以用一种更宽泛的方式来理解这种想法。
逻辑规则其实就是对推理的建模，很多正确的推理都有稳定的形式，这种形式作为一种普遍模式，超越了具体事例的限制，对它进行建模就是逻辑学。
比如在对算法建模上，我们会具体落实到每一个算法到底对哪一个变量或实体进行怎样操作，实际上代码的实现也是对抽象算法的建模，所有这些建模的想法其实都是一种更加宽泛的形式化方法。
而我们想要把它应用在 LLM 中，其实就是为了想要用这种符号的推理工具来约束和引导概率模型的行为：比如现在 LLM 可以生成大量的不可控的内容，但我们可以以这种方式对它进行内容的筛选，从中抽出正确的内容来作为最终的回答。这也是目前 Meta-Generation 等算法中比较常用的方法，也是形式化的具体应用。
Meta-generation 是 Welleck 等人于 2024 年在 From Decoding to Meta‑Generation: Inference‑time Algorithms for Large Language Models 提出的一种推理阶段生成算法，区别于逐 token 解码，它在序列级别进行优化，融合外部信息与回退机制，提升生成质量。
总的来说，形式化方法能够用符号化的方式对整个系统进行建模和验证，而形式化数学就是使用形式化方法来对数学推理进行建模和验证。
例如我们可以精确地将数学推理归结为利用公理系统和推理规则进行的活动，数学推理的正确性就是判断结论是否可以通过推理规则正确地从前提中得出，而这种活动我们可以用形式化方法在程序语言中建模，从而将数学推理的正确性归结为代码编译的正确性。
海外独角兽：所以在 Coding 领域，大家对于形式化方法已经比较熟悉了，那在数学领域，形式化是否就是把数学建模或翻译成一个比较确定的、计算机和大语言模型可以理解的语言？
华剑：是的。所以一个引入形式化数学的典型动机是论文评审。
为了聚焦主线，数学论文往往只会将最核心的思路写到论文里，但一些具体的推理细节，很多时候依赖于作者表达和读者理解之间的默契，作者只要展示结论在原则上可以用更严格更具体的推演即可。
但现代数学中往往有几百页长的一个大定理证明，对于人工评审来说是一个非常具有挑战性的事情，要将每一个这样的细节尝试手工地进行实际的补全来确认它的正确性意味着非常巨大的工作量。
但对于计算机来说，它可以很低的成本快速地执行大量繁琐的证明搜索的任务，可以为严格的证明检查提供彻底的解决方案。唯一的问题在于计算机程序无法直接处理模糊笼统的自然语言描述，它需要对每一个方面都有非常严格的确认和理解，这就需要我们以一种更加严格的符号方法来对它进行描述。这样做的好处在于我们可以用计算机来检查所有的具体情况和具体的边界条件，使得它能够可以以超越人类的水平对严格性进行把握，来对一个大规模数学证明进行检查和验证。
因此我们要首先对数学进行形式化，以一种更加严格的符号方法来对它进行描述，进行完善全面的形式化建模，才能发挥算法的力量。这也是当前陶哲轩在推广形式化数学这种范式的关键动机。
另一个例子是程序验证。
为了测试一段代码的正确性，目前主要的方法就是编写单元测试，看输入输出是否符合预期。但是测试的问题在于它至多能够证明一个系统在一组有限的输入下会出现错误的行为，却无法证明一个系统在任何输入下都将会正确表现。而形式化的方法希望能用更严格的方法来对系统进行完善的建模，在数学上证明每一个函数在任意输入下会做什么、不会做什么，从而提供全面彻底的系统描述。
海外独角兽：现在有了形式化语言，才能让当代数学能够工程化，解决更复杂的问题，如果没有这个语言，那我们想要证明一些定理，或者想让数学更进一步，是会有很多困难的？
华剑：当代数学面临的挑战类似于分布式系统中的关键问题，比如我们要让 10 万个 GPU 进行统一运算，困难主要来自通信，因为每个 GPU 可以计算一部分内容，而我们需要把这些内容聚合，再进行分发，这对于通信的要求很高，通信的上限限制了我们能够使用分布式系统进行大规模计算的可能性。
数学研究也面临类似的困境。目前的困惑不仅在于对前沿数学理解不到位，更在于前沿数学家之间的成果理解需要花费大量的沟通和讨论时间。这导致人类数学研究作为一个整体活动时，会产生工程瓶颈。
也就是说，大家花费太多时间来互相传达对前沿数学的理解和掌握，导致整体数学进展变慢。这种变慢并非因为不够聪明，而是因为团队协作面临着类似“人月神话”的工程化挑战。
我们可能会寄希望于可以通过合作加速数学研究，例如，对于一个人需要做 10 年的问题，我们尝试让 10 个人花一年时间做完，但这往往是不现实的。不同的人对于同一个问题会有不同的理解和解决方法，对进展进行沟通、对结论交叉验证都会耗费大量的时间和精力，同样也面临着“人月神话”的挑战。
“人月神话”最初来源于软件工程领域，指的是一种普遍的误区，即错误地认为增加人手可以线性地提升项目进度。
而计算机可以作为一种中心化的“Oracle”，能够判断哪些是对的、哪些是错的。我们只要相信它的判断，就可以继续前进。
形式化之后的结果会成为一个统一的知识库，研究者可以中心化地贡献和提取信息。这使得我们可以用更加统一、更加连贯的方式来进行整体化的数学研究，这是形式化数学的一个核心愿景。
海外独角兽：形式化语言让计算机能够作为一个中心处理器，去沟通不同参与者或研究者的工作。在 Alphapoof 和 DeepSeek 的 Prover 论文中，都把 Lean 作为训练语言的标准，Lean 的优势是什么？
华剑：我们选择 Lean 作为形式化语言，主要是因为它对当代前沿数学的支持非常好，它的社区最活跃，社区不断有新的成员加入，覆盖的数学范围也在快速增长。
数学是对复杂思维推理进行系统化设计的理想训练场。数学里充满了高阶抽象，比如对具体演算实例的抽象，以及对这些抽象之上的再抽象，如果 AI 能够精确而严格地对这类高级抽象进行形式化建模和推理，那么处理一般现实世界中的具体问题可能会更加得心应手。
这可以看作是将数学作为科学皇冠上的明珠，进行专门研究和形式化建模的基本动机。而 Lean，正是在这个背景下，因为它对数学的良好支持和活跃的社区生态而被选中。此外，Lean 的开发环境相对现代，很多工程上的问题可以得到迅速解决。
海外独角兽：数学和 Coding 是在模型训练，包括在 RL 中，是一个比较适合做验证的领域，选择数学作为研究对象，对其他任务的泛化，或者对 LLM 的推理能力、抽象能力，会有什么影响？
华剑：形式化方法可以对数学定理、代码进行建模，比如可以对一个复杂软件进行形式化建模，从而判断它是否面临内存泄露、并发竞争等问题。我们如果能实现用语言模型来做数学推理，那泛化到代码上做形式化建模的方式也是类似的。
从问题结构来说，数学难点在于比较抽象，但规模一般没有代码那么大。代码主要的问题在于规模复杂性比较大，在一个复杂软件工程的项目上，有十万行、几十万行代码都是常见的，但这在数学并不常见。如果我们要把数学的这套方法推广到代码验证的话，我们需要以某个非常好的方式在规模上进行泛化，即使这可能会导致在具体功能、方法上的抽象程度并不高。
此外，我们希望能够对更一般的场景进行形式化支持，无论是普通知识问答的推理，还是法律、医疗领域的推理，很多推理也是演绎推理的系统，凡是这种系统，往往就可以用形式化方法来做。
比如在法律领域，逻辑学上有专门的法律逻辑学科，我们在大语言模型进行法律推理的时候，也可以用同样的方式来进行建模和验证，来保证对法律条文的理解和运用是符合正确的规则的。
总而言之，形式化不会局限在数学和代码领域，对于更一般的领域也会有贡献，将具有生成能力的 LLM 和具有验证能力的形式化系统进行结合，可能会是下一步范式。
下一步的看点在于，模型的能力除了当前简单的工具调用和 Deep Research 信息检索之外，还能对自己的生产能力进行约束和控制。
海外独角兽：前面提到数学领域率先出现了类似 Test Time Scaling、Online Training 这样的信号，那在形式化数学领域，有没有哪个具体的技术是从形式化数学衍生到其他领域的？
华剑：目前最典型的就是 autoformalization，也就是自动形式化，把数学内容从自然语言翻译到形式化语言，从而弥补数据不充分的问题。
这在其他领域也有比较好的对应，比如 Llama 3 的技术报告里，有把用 Python 编程的数据代码翻译到用更加不常见的语言编程的代码中，来进行数据合成的工作。这个方式类似我们在 Prover 里做的，就是从一个数据更加充分的领域推广到数据不充分的领域，但在知识内容和逻辑结构上有继承作用。
海外独角兽：在DeepSeek Prover 之后，这个领域里的几乎所有模型都以 Prover 命名，Prover 是什么意思？
华剑：Prover 就是定理证明器的意思，不同于 DeepSeek-Math 这样的数学解题模型，后者往往是用在问答题或者填空题，也就是说我们想要通过数学推理来拿到一个具体的答案，通过这个答案来判断模型在这个题目上的数学推理是否正确。
但对于 Prover 来说，数学命题是一个封闭形式的数学定理，我们希望模型提供一个正确的数学证明，每个推理的步骤都是以合理的方式从前提或者公理中严格推出来的，最终可能并不会到达一个确定的结果。
要实现这个目标，意味着 Agent 的每一步都是符合逻辑和数学直觉的，这也说明这天然是一个过程监督的任务，而不像一般的数学解题那样，是一个结果监督的任务。因此，这个定理证明模型在任务形式上和以前的模型有本质差别，因此我们把它单独命名为 Prover。
03.
DeepSeek Prover 三部曲
海外独角兽：从 2024 年的 AlphaProof 和 AlphaGeometry，到 DeepSeek Prover V1.5 和今年的 Prover V2，AI 在数学领域取得了怎样的进展？
华剑：从 Prover V1 到 V1.5 到 V2，一个显著的进步是在模型 Scaling 上取得了更好的效果。
DeepSeek Prover V1 的主要贡献在于验证了在合成数据上做 Scaling 会有很明显的效果。
DeepSeek Prover V1.5 验证了利用自然语言推理引导形式化代码编写是有益的。
而 V2 则将更多精力放在了更高层次、更抽象的内容上，比如对一个复杂问题进行拆解和规划。这种高层次的抽象推理任务，更能发挥大模型参数量多、通用推理能力强的优势。
DeepSeek Prover V2 验证了在模型规模上做 Scaling 能够实现高层次的数学推理和规划。
将复杂的证明任务分解为具体可实现的目标是我从三年前就开始尝试探索的技术路线，在 DeepSeek Prover V2 上我们成功地在 671B 的规模上实现了非常有效的证明分解和实现策略，最终充分验证了这个路线的有效性。
这也是 V2 相比之前 RL 工作的一个主要区别。比如围棋这样的传统 RL 任务虽然状态空间巨大，但其动作空间相对固定和有限，就是棋盘上的落子点。但数学不一样，理论上我们可以无限地提出任意复杂度的猜想、定义和中间引理，其动作空间是开放且无界的。
这就是为什么过去那种依赖简单直觉或即时映射的 RL Agent 在数学领域难以取得突破的原因，而具有推理能力的 LLM 在经过 RL 的进一步训练之后，确实能完成一些以前难以做到的任务，比如代码和数学，这也是目前为什么 LLM 能取得那么大进展的一个主要原因。
在 DeepSeek Prover 三部曲的发展过程中，我们也看到使用 LLM 进行自动定理证明的研究领域也开始越来越活跃，在测试基准上的表现不断取得新的突破，这都证明了这个领域的长期前景。
海外独角兽：在 AlphaGo 和 AlphaFold 发布时还没有 LLM，仅靠 RL 就取得了很好的效果。而 RL 解决数学问题却是在 LLM 出现后才取得进展，除了操作空间不同之外，还有什么原因？LLM 在这几个重要研究中分别扮演了什么角色？
华剑：另外一个比较重要的差异在于对思维链的使用。一些理论工作证明，在回答问题前进行长链条的推理，相当于在效果上扩展了模型的规模，允许模型为不同问题分配不同的计算预算。
那我们对于更复杂的问题，就可以等效地将模型放大，让模型有更充裕的时间来思考和判断，这包括长链条推理、大目标分解、与已有知识的回忆等。
在 LLM 出现之前，这些复杂的计算和推理步骤就是一个即时的输入和输出，都必须在神经元传播当中进行，这使得训练模型处理复杂任务非常困难。现在，通过思维链，这些复杂的目标和生成过程可以在一个更大的框架内，利用更充分的计算预算逐步实现。
这也是为什么 OpenAI 的 GPT-o1 到 GPT-o3，在投入更多推理预算后，能在推理结果上获得持续且可靠的提升，这表明对于解决推理问题，Test Time Scaling 是一个可靠的长期发展方向。
海外独角兽：LLM 在数学中，不仅起到了拆解任务的角色，更重要的对思维链的增强起到了很大作用。数学领域的思维链和我们平时使用语言模型解决普通问题的思维链，有什么不一样吗？
华剑：数学有许多层面。在简单层面，MATH 这个数据集是偏重于测试计算和简单推理问题，难点在于对数学技巧的使用，比如对一些比较微妙的数学结构进行专门归纳、和以往策略进行简单对应，这是在高中竞赛水平上的特点。
MATH 是一个数学推理数据集，包含约 12500 道数学竞赛的题目，涵盖代数、几何、组合、数论等领域。它专为评估和提升 LLM 在逐步数学推理任务中的能力而设计。
在研究层面，往往需要投入大量时间去深入理解和迁移抽象概念。理解这些概念常常需要将其置于更广阔的语境中，甚至依赖大量具体例子来辅助推理。这种过程使得人们必须花费大量精力去把握各个定义之间的联系，以及如何从基础推理出发，推广或类比到更复杂的模式。这与通用推理的区别在于，它要求在更高层次的抽象领域中展现出更复杂的推理能力。
在日常推理中，比如 Manus 现在能做的事情，更多是对信息的处理和综合，但对数学来说，更多推理性的内容是放在了抽象的理解和运用上。虽然都是使用推理的概念，但是具体使用过程中，其实是不一样的模式。
海外独角兽：在这几个数学论文中还有一个比较有意思的点是，LLM 有时还承担了产生数据的作用，比如在 Prover 里面，LLM 其实产生了一些用来做 SFT 冷启动的数据。在 AlphaProof 的训练过程中，也是首先收集 100 万道自然语言描述的数学问题，然后用神经网络将其转换成 1 亿道形式化数学问题，最后用 RL 不断训练这个神经网络来证明数学题。从 100 万道题扩展到 1 亿道题，这个增量是怎么实现的？这是否表明数学领域的合成数据问题已经解决了？
华剑：在 Prover 这类形式化数学模型的研究中，我们之所以密集地使用合成数据，甚至比其他领域更早地这样做，很大程度上是不得已而为之。因为用于训练模型的自然数据是非常少的，能熟练使用 Lean 这类语言进行编码本身就很少，并且这些人还需要在数学、代码和逻辑方面有专精的理解，才能贡献出一些能满足机器验证的有意义代码。
这导致在 pre-training 阶段，我们远没有足够的数据来训练一个专门的大模型。这也说明 Prover 相对于一般的代码和数学来说，是一个非常特殊的领域。这就提出了一个问题：当人类没有大规模产生自然数据的话，模型应该怎么进行复杂的推理、对环境的理解和掌握？
因此，我们提出了 autoformalization，从数据相对更充足的领域进行知识和内容的迁移，比如从自然语言描述的习题、教科书、论文开始，将它们翻译或整合到数据量较小的形式化数学领域。这是进行数据合成比较好的出发点，这更像是一个翻译工作，而非从零开始的创造，因此相对更容易实现高质量的数据合成。
相比之下，在代码领域上做合成数据，是需要语言模型独立提出问题，根据这个问题编写相应代码和测试样例，并用这个样例来衡量代码质量，这会导致大家在用语言模型的时候，是一个从零开始的状态，这个难度也更高。
AlphaProof 团队从 100 万道题扩展到 1 亿道题，其增量主要来自几个方面：首先，同一个自然语言数学问题，可以翻译成多种不同的形式化表达方式。
第二，AlphaProof 团队花了很多时间来做 Test Time Training，这是他们在去年 7 月提出的一个想法，甚至比 o1 这种 Test Time Scaling 概念还要早。基本思路是，当模型要解决一个极端困难的问题，比如 IMO 级别的题目，可以先对问题进行变形或拆解，比如具体化条件或放宽约束，形成一些相对简单些的子问题。让模型先尝试证明这些子问题。
如果成功了，AlphaProof 团队就把这些成功的证明加入到训练数据中，让模型在聚焦解决这个原始难题的过程中，不断加深对问题的理解和对之前尝试的记忆。随着能力的提升，模型就能解决更难的子问题，最终攻克核心问题。
这个想法已经非常接近现在讨论的 Online Learning 的设置了，比如我们怎么解决一个问题，如何进行在线交互，如何能通过拆解和规划的方式来探索解决问题的结构和形式等等。
海外独角兽：我们也经常会想 AGI 或者 ASI 是否可以先在代码或数学领域实现，Test Time Training 和 Online Learning 都是我们认为的 LLM 下一个范式，这个范式是否可以先在数学或代码领域探索出来？
华剑：我认同这个观点，这个观点和在逻辑学里探讨问题的方法是一致的，比如在如何发展出现代逻辑学的这个问题上，一开始也是尝试对数学进行推理建模，因为数学是一个比较干净的领域，不需要和物理世界有昂贵且危险的交互，只需要在纯粹思维世界进行实验就可以了。
在思维空间里，我们已经可以得到一些想法是对的或错的，可以根据这些想法和公理之间的矛盾进行判断。这就为我们带来了非常好的实验环境，就像机器人可以在虚拟环境里做 simulation 的数据采样和训练，而不是一开始就让真实的机器人进行抓碗等操作。
也就是说我们先在一些形式和内容上比较整洁、可以更好建模和探索的场景下，进行成本较低地大规模探索，再推广到一般的、更加接近于日常生活、更加靠近物理世界的复杂场景。这会是接下来的大致方向。
海外独角兽：相比于 AlphaProof，DeepSeek Prover 是这个领域第一个开源的重要里程碑式的工作，除了 LLM 做拆解，还有哪些比较有创新意义的？
华剑：同样聚焦于任务拆解，Prover 实际上更接近于 Multi-Agent，或者说让不同模型分工协作。比如在训练数据的构造过程中，我们同时使用了 DeepSeek V3 和 DeepSeek V1.5 来进行数据构造。
对于一个大的任务，我们使用大模型进行任务拆解和规划，用小模型进行细致的目标补全。这种方法的优势在于既能在宏观层面利用大模型的推理能力，也能在需要快速、高频交互场景下，利用小模型的快速推理、低成本优势。
这带来一个比较有意思的点在于，以后如果我们想要在复杂推理任务中使用大模型，我们是否还需要像现在这样使用单一大模型来完成所有任务？还是可以用更加 Agent 的 workflow 来组织任务，进行模型之间的合作？
虽然现在在不断增加 training 的前提下，我们可以拿到更好的推理效果，但这给推理 Infra 带来了很大的挑战，这也是现在很多厂家在研究 Test Time Scaling 或 long CoT 的 token 控制的原因。比如在小问题上就不要过度思考，让模型主动进行一些及时问答，在大问题上再进行长链条的推理。
我们需要整个推理系统，包括不同模型、工具，能对任务难度进行感知，从而对不同任务设置不同的算力需求。这样做的话，一方面，对于 Test Time 算力推理会是一个更加复杂的调度问题，另一方面，我们能够以更加持续的方式来使用模型解决更多的任务，同时避免对推理系统的算力需求不断膨胀。
总而言之，我希望能够实现模型之间混合、模型和工具之间混合这样一种更加灵活、复杂的 Agent workflow，来解决不同难度、不同领域、不同方法的推理任务。这并不局限于使用现在的专家模型、MoE 模型来进行并行训练，混合系统也是一个比较好的机会。
04.
形式化数学
和 Multi-Agent 天然契合
海外独角兽：这个观点和陶哲轩的一个观点类似，数学，尤其是复杂数学证明问题，比大部分人想的更像是一个复杂系统，如果有计算机和形式化数学的帮助，甚至可以让几百个甚至上千个人一起合作，每个合作者只负责自己的部分。这是不是天然很适合 Agent 或者 Multi-Agent 的思路？
华剑：是的。现在形式化数学的基本方式就是把一个复杂任务进行蓝图拆解，把这个蓝图中的具体每一个任务交给不同的人来做，而不同的人做出的结果，只要它能通过计算机的验证，就认为是可靠的、正确的，我们把它聚合在一起，实际上就已经得到了一个完整任务框架的全面实现，这是可以非常方便快捷地变成 Multi-Agent 的想法，甚至有人机协作的想法。
在对一个任务进行拆解时，如果这个任务足够简单，我们完全可以让模型独立探索和简单尝试，而复杂问题则让人工进行参与，这可以有一种更自动化做数学的方式，而这种人机协作的模式，理论上可以推广到其他形式，比如代码，人和 Agent 进行协作，甚至其他领域。这是一个非常值得期待的场景。
海外独角兽：关于这个复杂系统，你提出过一个观点，“当前的形式化工具需要从静态的 Theorem Prover 转向具备自我规划、自我修复和自我知识积累能力的 Proof Engineering Agent”， 自我规划、自我修复和自我知识积累能力的这几个能力，听起来都像是我们对未来 Agent 的一个想象。
华剑：这也是我为什么认为形式化数学是我们发展和探索 Agent 一个比较好的场景，这也是我做 APE-Benchmark 这个新测试基准的想法来源。
我们其实是将软件工程当中的一些 Agent 探索模式迁移到了数学当中来，做一个类似于 SWE-Bench 的标准化基准测试，为后续的工作流和模型开发工作提供指导。如果我们想在数学领域像处理代码一样，对数千个文件进行修改、提取关键内容并处理，应该怎么做？
这个在形式化数学中有一个相应的概念叫 Proof Engineering，这意味着我们面对的不仅仅是一个传统意义上的软件工程项目，而是一个以证明为中心的工程项目。和软件工程项目一样，证明工程项目可能会有几万甚至几十万行代码，因此我们需要用软件工程的视角来训练大语言模型，进行大规模长文本的推理和修改。但除此之外，证明工程项目还包括丰富的数学内容，还涉及到与计算机验证工具的交互，是一个含义丰富、有挑战性的研究领域。
我们需要 Agent 能够提出数学上更强大的抽象，能够统领和聚合对各方面问题的理解，并在这个框架中给出通用的解释。这也是 Proof Engineering 相比 Software Engineer 来说，需要额外关注的。这使得问题更有深度和具有抽象要求，也为探索 Agent 提供了很好的环境。同时，一旦这样的场景能够有非常好的 Agent 解决方案，这对人类数学走向形式化来说，也是一种契机。
目前，形式化数学仍局限于学术探索，未成为数学家的日常工作，主要因为形式化本身是困难且缓慢的任务，需要专家长期努力，导致像 Mathlib 这样的数学库扩展缓慢，远未达到我们希望能够对全体人类数学知识进行编码和整理的梦想。
Mathlib 是基于 Lean 形式化证明系统构建的一个大型数学库，包含丰富的定义、定理和证明，用于支持数学知识的形式化与自动验证。
如果这样的 Agent 能实现，会加速这个梦想。以及，未来 10 年我们做数学的方式可能会完全改变，不再是简单的纸笔推演，而是直接用自然语言与具备形式化能力的 Agent 交互，我们告诉它我们想要处理的问题、想要得到的结果，它自动把任务目标和基础的数学概念翻译到形式化领域，并进行推理、思考和验证，最后将解答翻译回自然语言。
这会对数学研究有比较大的影响，比如当数学家想要确定一下简单的具体猜想的正确性的话，就不需要把这些任务交给人类去做，而可能交给 Agent 来做，这对于成本、规模、速度上，都有较好的优化。
可能接下来大家做数学的速度会越来越快，因为我们可以很快判断猜想的正确和错误，并能够相信模型的正确性。更进一步，如果我们在数学上能够达到这样一种非常便捷的程度，我们就可以在更多领域来使用这个 Agent，比如在软件工程项目上推测一些业务程度和代码，在运筹优化问题上做一些计算上的优化和整理。
海外独角兽：你提到形式化语言在实际数学家和其他研究者中，使用频率并不高，因为还有大量人类现存的数学题没有被翻译过去，那现在已经被形式化的数学占人类高质量数学数据的百分之几？
华剑：现在数学专业里，本科一二年级及以下的知识已经有一个非常好的表示，而前沿数学，比如研究者级别的数学，只有一些非常零散的形式化结果。
海外独角兽：AI 和 Agent 要发展到什么情况下，才能取得超出人类最顶级数学的贡献？
华剑：这个问题有两个方面，一方面是现在很多问题人类数学家已经有了非常好的结果，有了具体的证明，我们希望形式化能够覆盖这方面，另一方面是我们想要让具有形式化推理能力的模型 Agent 可以开拓新的数学教育，比如解决人类提出的开放问题，甚至提出一些新的数学想法，也是更高层面的追求。
第一个方面的一个例子是帝国理工大学正在进行的形式化费马大定理的项目，这需要投入大量人力和时间。我们现有的机会，就是在这样的大项目中融入我们的 Agent，帮助数学家更快地进行形式化工作。目前的技术已经能在一定程度上提供帮助，比如让模型用 Embedding 从基础库中抽取相关的引理和定义，或者用像 DeepSeek Prover 这样的模型来补全一些具体的形式化步骤。
接下来的进展，是发展出具备 Proof Engineering 能力的 Agent，能够梳理和扩展人类正在编写的文件。更进一步，我们希望 Agent 能具备高层次的理解能力，能够像人类一样独立地提出形式化的策略选项，并自主实验筛选出足够好的方案来辅助人类进行自动化。虽然目前已有工作像 LEGO-Prover、STP Prover 在尝试提出和验证猜想，但距离主动提出足够好的猜想来解决足够难的问题，仍有一定距离，有一定的挑战。
第二个方面需要更加复杂的推理和对数学的理解能力，我们希望将自然语言的数学推理能力和形式化的验证能力结合起来，让 GPT-o3 或 GPT-o4 这样强大的推理模型，通过长链条推理，发现可能有用的数学结构或抽象，然后由形式化 Agent 将这些中间产物翻译到形式化领域进行验证。
这种验证可以为探索过程提供非常好的监督和引导。通过这种方式将自然语言数学的发展和形式化数学的 Agent 验证框架结合起来，可能在接下来的两三年时间里就会看到不错的工作成果。
05.
Evaluation benchmark
是给模型“找钉子”
海外独角兽：现在的模型能力已经可以部分实现第一方面的工作，而在第二个方面，让模型开辟新的领域，或者提出更高阶的数学问题上，现在的模型能力还做不到，现在主要欠缺的能力是什么？
华剑：这样的欠缺需要在自然语言上有一个更好的解决，比如需要在模型的 pre-training 阶段引入更强的数学推理能力，配合能够满足高复杂度推理需求的数据合成与筛选机制，以及通过 RL，实现对模型从简单到复杂任务的逐步训练，从而持续提升模型的推理能力。这是和现在在推理模型的训练问题上所需要解决的主流问题是一脉相承的。
海外独角兽：在用 RL 进行训练的过程中，有几个组件可能是特别重要的，比如环境、Verification、RL 算法等。相比代码，这几个组件在数学领域有什么异同点？
华剑：现在无论是在数学还是代码领域，要让 RL 能够有效工作，最关键的一点就在于 Verification 或 Evaluation 的设定。 之前 RLHF 能够成功，很大程度上是因为它基于一些非常好的、rule-based 的验证设计，这种反馈机制不容易被 hack，并且能提供精确可靠的反馈结果。只要模型足够大，RL 算法足够好，就能不断地与这样的结果进行匹配和交互，从而实现能力的增长。
这也就引出了一个关键问题：如果在某些场景下，我们没有现成可用的评估方法该怎么办？ 这正呼应了姚顺雨提出的“Evaluation 相比 Training 更重要”的论断。
我们现在的模型就像是很好的“锤子”，但我们却缺少足够好的“钉子”。 RL 需要与环境进行任务中心型的交互，也就是说，需要环境能给模型提供足够的奖励信号，并且稍稍高于模型当前的能力，才会对训练结果有较好的提升。如果任务太简单，模型只要简单 sampling 就能解决，那它就得不到本质的锻炼；如果任务太难，模型拿不到任何正向奖励信号，也就没有明确的优化方向。
因此，如何提出更好的 Evaluation Benchmark 就成了一个非常关键的任务。 以数学为例，我们需要在难度、涉及领域，甚至具体技巧和解题策略上，都有足够完备和充分的测试任务与环境。 只有在这样的环境下，我们才能用现有的 RL 算法更好地训练模型。 这就是为什么说 Evaluation 比 Training 更重要。
我们的 Benchmark 设计或者 RL 训练中的 Prompting 设计，必须更加符合实际应用的需求。 只有当我们的 Evaluation 环境能够全面、可靠、准确地覆盖我们下游测试时的推理需求时，RL 才能够真正发挥作用。 我认为，这无论是对于代码还是数学来说，都是一个核心的场景和任务。
海外独角兽：很赞同你说的 benchmark 既不能太简单，也不能太难。在 benchmark 领域，你最近新发了一个工作叫做 APE-bench，这个设计思路是什么样子的？
华剑：APE-Bench 的设计思路非常接近 Proof Engineering 的想法，希望 Agent 能够对大规模的文本进行修改，并能与验证系统交互来判断修改的正确性，使得 Agent 能够完善一个大规模的数据库，而不仅仅是完成单个孤立的任务，也就是说我们希望在形式化数学领域也能实现从 “HumanEval” 向 “SWE-bench” 模式的跨越。
HumanEval 测试模型写单个函数的能力，侧重小规模代码生成；SWE-bench 要求模型在完整代码库中修复 bug，考察跨文件和系统级改动能力。两者区别在于前者侧重原子级能力，后者重视工程级能力。
APE-Bench 强调模型不仅要完成任务，还要能从中学习、思考，并将这些收获以形式化的方式沉淀到统一的知识库中，以便在后续任务中利用这些经验解决更复杂的问题。我们希望这个 benchmark 能评测和引导模型在长文本处理、大规模定理库管理和知识积累方面的能力。
海外独角兽：有没有更直观的方式说明这个 benchmark 考量的任务和方式是什么样的？
华剑：目前 APE-Bench 的第一阶段聚焦于单文件的修改，这要求 Agent 理解特定数学分支中现有的编码风格和结构，并将自然语言描述的数学结果融入其中。此外，它还包含重构工作，比如将冗长的证明进行合理拆解和模块化，这非常接近软件工程的思想，我们需要引入新的代数结构，并与现有定义结合，以方便证明一些目标灵活的场景。这是这个 benchmark 想要解决的问题。
如果想要在 APE-Bench 上取得好成绩，模型需要同时具备对形式化数学的代码、数学本身以及它们之间互动的深刻理解，我们希望这能帮助大家判断模型是否接近人类使用者的实际需求。
海外独角兽：相比于之前可能更侧重于解题能力的 benchmark，APE-Bench 更侧重于考察模型综合运用代码、工具，甚至通过多步骤、跨文件来解决复杂问题的能力。
华剑：这也是我们想象中数学领域的 Agent 想要达到的能力，我们也是先分析了这些能力，再落实到 benchmark。
海外独角兽：现在有专门做数学的模型，也有专门做 Coding 的模型，但它们的基座都是 LLM。未来会不会出现一个融合模型，在数学、代码及其他领域都很强，我们不再需要单独的专业模型？
华剑：我觉得理想情况下是这样的。以形式化数学为例，模型就同时需要代码能力和数学能力，才能解决复杂问题。即使在数学研究上，很多时候我们也是需要用仿真建模的方法，用专门的代码工具进行结果验证。也就是说，如果我们想要模型在数学上做得好，随着模型做的任务越来越难，模型的代码能力是不断提升的。
在数学、金融等领域的很多论文都是基于非常大、非常复杂的代码库，才能完成结论的仿真和计算。在代码上，很多时候我们需要对一个常用程序，尤其是字段密集型程序，进行复杂度、计算效率的估计，也需要用离散数学的工具来做。如果希望模型不仅能生成代码，还能够分析代码，并进一步优化代码，那数学能力也是必要的。
除了代码和数学，在一般的科学领域，这会更加常见，比如物理领域会用很多数学工具等。我们需要对各个领域都有一个触类旁通的模型，才能对具体场景有一个比较好的应用结果。
我认为最后人类会有一个全才模型，而不是现在的专才模型。后者是一个时代的特殊产物，因为我们无法在 post training 阶段兼顾各个领域之间的长处和特性，比如在 SFT 阶段，不同领域的数据混合后的效果无法兼顾。如果这些基础问题能够解决，以后会有一个通才模型出现的，这也是大家的共同需求。
06.
GenAI 的
下一步是 Certified AI
海外独角兽：你提到形式化验证与动态学习机制的结合将催生出新型的生成式智能 Certified AI，可以解释下“Certified AI”是什么？
华剑：Certified AI 的概念主要是相对于 Generative AI 而言的。现在的模型在生成方面能力很强，能快速生成大量看似高质量的代码，它们符合人类编码习惯，审查时可能看不出问题。但在长期部署和应用中，可能会暴露安全性、效率或可维护性等不符合人类需求的问题。
而 “Certified AI” 强调的是，我们不仅需要生成能力，更需要对生成质量有良好的控制。以数学为例，我们不仅需要模型生成长篇复杂的推理，更需要它的每一个步骤都是正确的，全面满足数学工作的要求。这需要模型对自己的生成结果进行验证或检测，也就是 Certification。
在我们的研究中，这是通过形式化方法实现的：我们将生成结果翻译到形式化领域，然后用计算机辅助方法进行验证。只有通过这种验证，我们才认为这是一个通过了质量认证的结果，这样的模型就是 Certified AI。
模型不仅要有生成能力，还要有质量控制和检测能力，它必须通过外部工具调用，完全确认其生成方法满足所有需求后，才将其返回给用户。这样，人类使用者就可以完全可靠地相信它的结果。我们认为，这对于当前只管生成不管质量的 AI 来说，是一个比较好的补充和革新。
海外独角兽：这个想法的提出，主要是对数学的研究，还是说可能能泛化到其他领域？
华剑：这和前述讨论类似，在数学上我们有形式化方法，在代码上我们有类似的程序化验证的方法。在一般场景下，我们有很多工具调用，比如在完成文本论述后，调用 Deep Research 这样的工具对事实细节进行检查，并进一步修正和反思，最后在多轮迭代后有一个最终完全可靠的结果反馈给人类用户。
我认为只要是能够使用外部工具对模型生成结果进行纠正和修改，都算是 Certified AI 的理念。
07.
RL，数学，智能泛化
海外独角兽：数学是 LLM 应用和研究的一个分支，反过来看，RL 和数学的突破，对 LLM 本身起到什么作用？能否举例说明数学能力是否带来了泛化的迹象？
华剑：我个人倾向于认为具体场景还是要具体分析。很多这样的结果，其实是 pre-training 厂家通过不断实验、调整数据配比和使用基于规则的数据筛选机制探索出来的。
一个比较早期的例子是 GPT-3.5，它的推理能力得到较好提升，很多时候被认为是因为它在 pre-training 中使用了更高比例的代码数据。这让大家倾向于认为代码数据对于提升通用推理能力有帮助。
但同样是代码数据，它包含怎样的内容、以何种形式提供，是纯代码还是带有解释，都可能对模型的学习产生不同结果。所以这其实是一个模型训练中的工程问题。一般来说，这种泛化现象的出现，往往是基于不同领域之间存在共同的推理模式，使得这些模式能够在不同的语料中相互印证。也就是说，我们还是需要通过对语料进行控制，来促成这样的泛化。
海外独角兽：AI 对数学研究的突破是否能借鉴到其他学科，比如化学、生物、医疗等，从而真正帮助科学研究和科学突破？形式化语言在别的科学领域是否有可能出现？
华剑：对于形式化本身来说，现在有很多尝试是把它推广到一些同样使用数理结构、演绎推理的方法来进行工作的领域，这都表明，形式化的理念并不仅限于数学研究，还对其他领域有一个知识整理和综合的作用。
当然，对于一般的科学领域，它们往往涉及到实验，需要通过具体实验来把握世界，这与纯思维推理有所不同。但即便如此，数学方面的成果和方法在一定程度上也可以推广。
在数学中我们非常依赖“提出假设-验证假设-将成功结果加入知识体系”的思维模式，这在所有学科中都普遍存在。一旦我们能够开发出具备自主提出猜想、自主验证猜想以及进行知识积累能力的 AI 模型，那么这种方法论上的探索就可以很快地应用到其他学科领域中去。虽然在这些领域可能需要在机器与物理世界的实际交互方面进行进一步的补充。
海外独角兽：模型在数学证明的过程中，代码能力也会有很大提升，因为在涉及复杂定理证明的时候，所需要的是一个代码库，你对于复杂数学和复杂代码库之间的联系怎么看？
华剑：这两方面是非常接近的。我们现在想要在一个非常长的数学论证的文章编写中去修改一些具体问题，比如放松条件或引入新概念，都非常接近大家在代码软件工程里实践的基本策略。
所以如果将这个问题上升到对大规模知识进行完善和补充的话，无论是数学、代码，还是其他领域，都是一个非常有共通之处的研究场景。大家的主要困难已经不在于对数学概念、代码执行逻辑的理解，而是在对大规模工程的理解，而后者在领域之间是共通的。
08.
下一个 GPT-4 时刻
是实现自主 Agent
海外独角兽：接下来 AI 和 LLM 如果要进一步发展，可能要突破哪些瓶颈？
华剑：首先，一个非常现实且具体的困难在于如何提出更好的问题，以及如何对模型生成的回答进行有效的 evaluation。训练一个好的 reward model 是非常困难的，尤其是在判断复杂问题的回答的时候。
很多时候，即使模型在代码库中提出了一些修改，而且生成的代码通过了所有单元测试，我们仍然难以判断它是否真正满足我们的需求，比如代码风格、使用规范、安全性等方面，这时我们往往需要依赖 LLM 进行软性判断。
当我们无法使用 rule-based 的方法时，如何训练一个可靠的观察员模型，是一个核心挑战。这会是 2025 年一个核心点。之前 DeepSeek 提出了一个 Generative AI 的设计，也是希望在更加通用的场景上有一个训练得比较好的 reward model。
DeepSeek Generative Reward Model 是 DeepSeek 与清华大学提出的奖励建模方法，通过生成结构化文本反馈（如评价原则与点评）来替代传统数值评分，提升大 LLM 的推理与 RL 效果，同时支持推理时的灵活扩展与优化。
而在 APE-bench 中，它一方面需要对通过编译来对语法层进行判断，另一方面也需要使用语言模型来笼统判断是否正确的遵循自然语言指令，这个目前我们是直接只用了 Claude Sonnet 来进行了简单的推理，但这个问题事实上是比较复杂的。人类的代码检察员在面对具体的 commit 或 pull request 的时候，也需要对已有代码进行比较审查，甚至进行更加新颖的测试，才能判断正确性。
对生成结果的审查本身就是一项 Agent 的任务，我们需要的不仅仅是生成式的 reward model，甚至需要 reward agent，我们需要让模型自主收集更多信息，利用这些信息判断模型自己的生成是否正确，这可能需要调用一些外部工具来判断一些细节。
也就是说，我们为了训练 Agent，我们需要训练另一个 Agent 来对它进行判断，一整个训练的 workflow 可能是一种非常复杂的场景，其中有许多开放性问题，比如如何提出具体的方法来解决这种复杂性的控制等。
海外独角兽：也就是说这个 reward 不再是一个提前固定好的 model，而是一个动态的 Agent，这个 Agent 还要自己去学习如何能更好地判断，更好地给奖励信号？
华剑：是的。如果用固定的数据训练出一个一次性判断的 reward model 的话，这个效果很大程度上是局限于我们的数据的，也就是说模型的生成一旦超出了我们提供的训练数据范围，效果会急剧下降。
而在 Agent 设定下，Agent 在遇到不熟悉的领域时，它可以主动获取更多的信息和知识，来进行判断，这样会更加鲁棒、不易被 hack，也更准确可靠，用这种方法训练 RL 可能会是一个比较好的补充，甚至彻底的提升。
海外独角兽：除了 reward agent，大家提到比较多的模型能力提升需要的要素还包括 long Context，或者说 Long Horizon Reasoning，还有未来可能实现 Online Learning，你对这两个要素怎么看？
华剑：Long Context 基本上是工程问题，关键在于如何通过更好的数据工程，来收集高质量的长文本推理数据，并处理好多轮交互的过程。
无论是人类用户在交互中展现出对模型上一轮回答的偏好，促使模型在后续作出调整，还是 Agent 在任务执行中通过与工具持续互动，来完成复杂的长链条操作与规划，这些场景所依赖的数据构建与筛选机制，我认为将会逐步走向成熟。但这一方面可能并不一定有很多概念性或技术性的 insight，很多时候就是工程化的努力。
Online Learning 与 Agent 的想法非常接近，现在 Agent 主要想法是不断积累上下文，通过将新获得的信息加入到上下文中，来辅助下一轮的决策和执行。Online Learning 主要想法在于用新的信息和尝试来训练模型，利用训练结果来对下一轮或者同一轮的任务有一个更好地执行。
我认为这仍然是一个工程性的问题。主要瓶颈在于 Infra 支持，如何平衡推理和训练的需求，在推理和训练异步执行后，怎么对模型变化进行控制等，都是对训练技术和 Infra 系统的挑战。这方面一定会取得进展，如果有厂家能够实现的话，Online Learning 将会非常有前景，可能带来意想不到的收获。
海外独角兽：你认为下一个像 GPT-4 级别的智能技术跨越最可能会出现在什么方向？
华剑：我认为，下一个重大的技术跨越将是实现一个具备自主规划、执行和反思能力的 Agent。如果这样一个 Agent 能够拥有上下文理解能力、长链条思考能力，并且具备 Online Learning 的能力，那么这样一套系统一旦能够商业化部署，就将是一个非常震撼的结果。
比如在用户的使用过程中，模型能够不断解决复杂问题，并且用户能感受到其能力在探索过程中持续优化，这本身就是一个非常好的商业产品，足以对现有产品形成差异化的打击。
海外独角兽：你认为全球范围内可能第一家会实现 AGI 的公司会是哪家？
华剑：我认为这很难说，因为我们对每家公司的了解非常有限，大家往往会有很多压箱底的技术出现爆出来。但我总体认为，那些拥有足够充分的模型训练经验、大规模 Infra 支持，并且已经推出足够稳定的大模型商业产品的公司，往往会是下一个赢家。
也就是说，大概率不会是新的、意料之外的赢家，而是在现有赢家之间进行内部角逐的结果。像北美的 Google、OpenAI、Anthropic，以及国内的 DeepSeek，都可能是这个结果的贡献者。
我个人认为，这个领域已经慢慢到了一个垄断和赢家通吃的阶段。因为要进行下一步的探索和增长，必须在第一阶段有很好的基础。新入局者需要补全太多技术、Infra、人才和研究上的长期积累，才能在这样一个基础密集且工程密集的环境下取得突破，这会非常困难。所以，我个人认为，Big name 仍然会是 Big name。
海外独角兽：有观点认为 pre-training 遇到瓶颈，在 O 系列模型出来之后，未来半年到一两年可能出现技术发展真空期，你对此怎么看？
华剑：我认为像从 GPT-3 到 GPT-4 那样的跨越，在历史上一定是比较罕见的事情，我们不能一直指望这样的事情不断涌现。我们必须接受技术发展有快速期，也有慢慢积累期，然后才能等待下一个突破。现在，我们可能正处在一个有新东西不断涌现，但不会那么令人激动的阶段。
虽然 o1 模型在推理上带来了震撼，但在日常使用中，并不一定会对已有的方法有一个彻底的革新或代替作用，现在大多数人仍然在密切使用 4o 这样的老模型，这是推理时代之前的模型，而推理时代之后的模型往往和 4o 形成互补，而非彻底的代替或代际跨越，这反映了我们当前的状况。
至于说 pre-training 遇到瓶颈，我们需要仔细探讨瓶颈是什么意思。这可能意味着仅仅在 pre-training 阶段进行 Scaling，已经不足以支撑下一步的大规模跨越。但这并不意味着 pre-training 本身不重要。例如，Agent 能力扩展、工具调用等过程中产生的新数据和新方法，可能还是需要在 pre-training 阶段进行融合。
大家说 pre-training 不再那么重要，可能是因为它不再带来全新的技术革新，但这绝不意味着我们可以完全不做 pre-training，或者在一个完全稳定的模型上就能实现新进展。我认为这没那么乐观，我们仍然需要在技术密集、资源密集的 pre-training 阶段不断加入新东西，才能为下一阶段的稳定基础突破做准备。
海外独角兽：Pre-training 仍然非常重要，很多 post training 其实也是在激发 pre-training 的能力。从时间线上看，如何看待 AGI 实现的 timeline？有可能在 2027 年实现吗？
华剑：我个人对此也没有很好的判断。但我认为，到 2027 年之前，在我们之前讨论过的这些内容上，应该会有一个比较好的进展。
然而，一个可能的问题是，即使我们拥有了具备这些能力的模型，我们可能会发现一些新的问题，或者发现它们仍然不能满足我们对于 AGI 的想象。实际上我们对 AGI 的理解是不断演进的——看到新的东西，我们才知道我们真正想要的是什么。
海外独角兽：从你个人的角度，接下来的研究重点会如何演进？什么时候会从数学这个分支领域转向更通用的方向？
华剑：我个人认为，数学方面一直会是一个比较好的研究案例，它根植于人类智慧中最精华的一部分，有非常丰富的内容和结构，就像一个钉子，我们可以不断地用它来尝试新的锤子。
发现哪些方法将会在数学上取得本质上的突破，或许相关的思路也可以迁移到其他领域上。我们可以不断地把通用的、可以借鉴的方法在形式化数学这个领域进行探索和实验。至于形式化方法，我认为可能会是接下来几年的一个范式性的重要机会。
因此，我个人在接下来的几年时间里，应该还是会在形式化数学上进行更深入的研究，这也是我博士阶段研究的主线，会更关注形式化数学如何去满足不同场景需求、能力。
海外独角兽：作为一个年轻的 researcher，有没有学术领域的 Role Model？
华剑：如果局限在当下的 AI 研究而言，我认为可以称得上 role model 就是 Ilya，他能够敏锐地理解到 scaling law 就是推广智能的核心动力，并且能够看到它在技术和工程上都达到了一个条件成熟的阶段。技术积累是一个长期的过程，研究者在已有的方向上继续前进可以成为一个优秀的贡献者，但真正困难的在于整合具体技术在系统结合之后的潜力，提供完整可实现、具有长期成长空间的愿景和构想。科学革命往往不是渐进的结论积累，而且是剧烈的范式转变，这才是英雄真正的用武之地。
在这一语境下，Ilya 是一个非常典型的榜样，能够非常敏锐地感受到我们这个时代在哪个方面有非常明确的、可以立刻工程化和商业化的机会。
但这样的历史时机并不是均匀地出现的，AI 发展到现在也有数次高潮和低谷，也是一个时势造英雄的领域。如果抛开 AI 不谈，在这一语境下我的 role model 就是亚里士多德，“他出生，他思考，他工作，他死去”，这也是目前我想要的。
文章来自于微信公众号“海外独角兽”，作者是“拾象”。
