向通用人工智能发起最后的冲刺

星辰大海的入场券：为何是数学？

大家好，我是字节跳动Seed小组的一员。今天，我想和大家聊聊我们正在进行的一项激动人心的工作——教AI进行真正的数学推理。这不仅仅是让机器算得更快，而是要赋予它像人类数学家一样思考、探索和证明的能力。我们相信，这是通往通用人工智能（AGI）的漫漫征途上，一块至关重要的“敲门砖”。

为什么是数学？因为数学是逻辑的极致体现，是宇宙的通用语言。一个能够真正理解并创造数学的AI，意味着它掌握了最高级别的抽象、推理和创造能力。然而，这条路远比想象的要崎岖。过去，我们让AI解数学题，更像是让它背诵九九乘法表，它知其然，但不知其所以然。

问题出在哪里？出在“语言”上。人类数学家可以用自然语言写下证明，同行一看便知其精妙。但对机器来说，自然语言充满了模糊和歧义。“显而易见”、“不难证明”——这些词对AI来说简直是天书。我们需要一把更精确的尺子，来度量AI思维的每一步是否正确。这把尺子，就是形式化语言。

从“食谱”到“化学式”：形式化语言的力量

想象一下，自然语言的证明就像一份家常菜的食谱：“加少许盐，翻炒片刻”。“少许”是多少？“片刻”是多久？这依赖于厨师的经验和感觉。而形式化证明，则像一个精确的化学反应式：\(2\text{H}_2 + \text{O}_2 \rightarrow 2\text{H}_2\text{O}\)。每一个原子，每一个配比，都清清楚楚，不容置疑。机器可以自动、精确地验证这个过程的每一步，给出“对”或“错”的明确反馈。

我们选择的“化学式语言”，是Lean。它是一个强大的交互式定理证明器。在Lean的世界里，任何逻辑上的瑕疵都会被编译器无情地揪出来。这为我们利用强化学习训练模型提供了完美的“奖惩机制”。做对了，给奖励；做错了，给惩罚。模型在海量的试错中，逐渐学会了如何写出无懈可击的证明。

双剑合璧：Seed-Geometry与Seed-Prover

面对庞杂的数学世界，我们打造了两把利剑：专攻几何的Seed-Geometry和通晓全局的Seed-Prover。

Seed-Geometry：光速几何大师

几何问题，尤其是奥赛级别的，常常需要神来之笔的“辅助线”。人类天才或许能灵光一闪，但AI如何系统地找到它？Seed-Geometry就是为此而生。它像一位顶级的几何大师，拥有两项绝技：

• 极致的速度：我们将它的核心推理引擎用C++重写，速度飙升了近百倍。这让它能在极短时间内探索海量的可能性。
• 聪明的“直觉”：我们用一个强大的Seed大模型来“预感”最有用的辅助线应该画在哪里。这大大缩减了搜索范围，直击问题要害。

在2025年的IMO赛场上，Seed-Geometry仅用2秒就解决了那道复杂的几何题。它不是在暴力搜索，而是在用一种接近“直觉”的方式高效推理。

Seed-Prover：深思熟虑的逻辑核心

如果说Seed-Geometry是专才，那么Seed-Prover就是我们打造的通才。它负责处理代数、数论、组合等更广泛的数学领域。它的核心思想，我们称之为“引理式证明”（Lemma-Style Proving）。

传统的AI证明，像写一篇长篇大论，从头写到尾，一旦中间卡壳，就前功尽弃。而Seed-Prover不一样，它像一位建筑师，在建造一座宏伟的大厦（最终定理）之前，会先去制造和检验各种标准的砖块、钢筋和预制板（这些就是“引理”）。

这种方法的优势是巨大的：

• 模块化：每个引理都是一个独立的、可验证的单元。我们可以并行地证明它们。
• 知识复用：一个被证明的引理，就像一个经过认证的零件，可以在不同的证明路径中被反复使用。
• 进度清晰：我们能清楚地看到哪些“零件”已经合格，哪些还需要打磨，从而有效地分配计算资源。

AI的三重思考境界

面对不同难度的挑战，我们为Seed-Prover设计了三套思考模式，就像一个棋手拥有从“快棋”到“长考”的不同策略。

第一重：轻量推理 (Light Inference) - 敏捷的修正者

这就像一个学生在做完作业后快速检查一遍。Seed-Prover生成一个初步的证明草稿，然后让Lean编译器来“批改”。如果发现语法错误或者简单的逻辑断点，它会根据反馈立刻进行修改。这个过程会迭代8到16次。这种快速的“自我修正”循环，效率极高，能解决大量中等难度的问题。

生活化类比：你写了一段代码，编译器报错说“缺少一个分号”。你马上加上，再编译，通过了。这就是轻量推理的核心——快速响应，敏捷修复。

第二重：中量推理 (Medium Inference) - 专注的深潜者

当遇到真正硬核的难题时，轻量级的修改就不够了。这些难题的证明往往结构复杂，其中可能包含一两个极其困难的“引理”。这时，Seed-Prover会启动中量推理模式。它会暂停对主问题的攻击，把计算资源集中起来，对那个最难的引理启动一个“子任务”，用轻量推理模式去专门攻克它。一旦这个关键引理被证明，它就会带着这个“战利品”返回主线任务，继续前进。

生活化类比：你在写一篇博士论文，发现需要一个前人没证明过的辅助定理。于是你暂停了主论文的写作，花了一个月时间专门写了一篇短文来证明这个辅助定理。成功后，你再把这个成果引用到你的博士论文里，问题便迎刃而解了。

第三重：重量推理 (Heavy Inference) - 伟大的战略家

这是我们为最顶级的难题（比如IMO决赛的压轴题）准备的终极武器。它模拟的是人类顶级数学家解决世纪难题时的思考方式——不是一味猛冲，而是先进行广泛的、漫无目的的探索。

在这个模式下，Seed-Prover会先花上几天时间，生成数千个关于这个问题的“猜想”（Conjectures）。它会问自己：“这个函数会不会是单调的？”“这个代数结构有没有周期性？”……它像一个侦探，列出所有可能的线索，然后用轻量推理去逐一验证这些猜想。成功的猜想被放入一个“引理池”中，成为宝贵的知识储备。几天后，这个引理池里可能就积累了数千个关于这个问题的高度相关的事实。最后，Seed-Prover会带着这个庞大的“军火库”，启动中量推理，对主问题发起总攻。那些在探索阶段被证明最有价值的引理，往往就是通往最终答案的关键钥匙。

生活化类比：为了策划一场决定性战役，一位将军不会立刻出兵。他会花几周甚至几个月的时间，派出无数侦察兵，绘制地图，分析地形，研究敌人的所有可能动向，建立庞大的情报网络。当所有准备工作就绪，他才胸有成竹地发起总攻。

成果斐然，但征途依旧

凭借这套“组合拳”，我们在自动化定理证明领域取得了令人振奋的突破：

• IMO 2025: 6道题中，我们成功证明了5道，这在历史上是前所未有的。
• 饱和MiniF2F: 我们几乎完全解决了这个业界公认的、衡量形式化数学能力的标准测试集。
• 大幅超越SOTA: 在多个基准测试中，我们的表现远超之前的世界最佳水平。

然而，我们深知这只是一个开始。组合数学仍然是我们的短板，而真正的终极挑战——解决那些悬而未决的数学猜想，例如黎曼猜想——依然遥不可及。但这正是我们努力的方向。我们相信，通过将大语言模型的广阔直觉与形式化系统的严谨逻辑相结合，我们正在开辟一条通往机器智能新纪元的道路。

这条路的尽头，或许就是通用人工智能的曙光。我们很荣幸能成为这场伟大冲刺的一份子，也期待与全世界的同行者们一起，见证那个历史性时刻的到来。