对谈DeepSeek-Prover核心作者辛华剑：MultiAgent天然适合形式化数学｜BestMinds

文章来源：万象ai发布时间：2025-07-30 12:24:39

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。

……