E9 和DeepSeek-Prover作者辛华剑聊「形式化数学」：数学的工业化，Agentic AI，Benchmark
01:40:56 Share

Era of Experience 这篇在 AI 社区讨论度很高的文章中提出：如果想实现 AGI，构建通用 Agent，就必须依靠“经验”，也就是模型和 Agent 在强化学习过程中自主积累的、人类数据集中没有的高质量数据。

DeepMind 的 AlphaProof 就被认为是这样一个典型案例，它靠 RL 算法自行“做题练习”，最终在数学领域，达到了超越人类的水平。以 AlphaProof 为开端，OpenAI 的 o1、DeepSeek 的 Prover-V2 等模型不断推动数学领域的进展，让数学证明成为了 AI 突破的新高地。

为什么 AI 研究中要特别关注数学证明能力？一方面数学领域的突破是模型能力提升的直接表现；另一方面，数学和代码类任务一样，不仅有严格的规则和格式，明确的推理路径，还有着对逻辑性、可验证性的高要求，这让数学类任务成为 RL 理想的训练环境。

这期内容我们请到了 DeepSeek-Prover 系列核心作者辛华剑，邀请华剑来和我们讲解数学和 AGI 之间的关系。华剑本科毕业于中山大学逻辑学，现在是爱丁堡大学人工智能方向的博士生，他目前专注于大模型在数学定理证明中的创新应用。

***友情提示：**这期内容同时涉及 AI 和数学领域的硬核干货，点击查看对谈全文*文字内容)

本期拓展阅读

• 86 条 DeepSeek 的关键思考 ｜Best Ideas 开源)
• 对 DeepSeek 和智能下半场的几条判断)
• The Second Half：一位 OpenAI 科学家的 AI 下半场启示录)
• o3 深度解读：OpenAI 终于发力 tool use，agent 产品危险了吗？)
• Claude 4 核心成员：Agent RL，RLVR 新范式，Inference 算力瓶颈)

讨论中被提及的相关名词：

• **DeepSeek Prover：**DeepSeek Prover 是 DeepSeek 开发一系列开源数学推理大模型，专注于形式化定理证明，支持将自然语言问题转化为 Lean 4，并通过逻辑严谨的定理验证来解决数学问题。
• **Ilya sutskever：**是 OpenAI 联合创始人和前首席科学家，在 GPT 系列模型的开发中扮演了关键角色，Ilya 在 AI 研究领域有很强的影响力，业界认为他的技术品味很好，在技术方向的选择上具有很强的预判性。
• **形式化数学：**形式化数学是指利用精确的符号语言来表达数学概念、定理及其证明，以消除传统数学推理中的模糊性，建立严谨且透明的框架。
• 人月神话：“人月神话”最初来源于软件工程领域，指的是一种普遍的误区，即错误地认为增加人手可以线性地提升项目进度。
• **MATH 数据集：**这是一个数学推理数据集，包含约 12500 道数学竞赛的题目，涵盖代数、几何、组合、数论等领域。它专为评估和提升 LLM 在逐步数学推理任务中的能力而设计。
• **Autoformalization：**自动形式化，指将用自然语言表达的数学内容（如定义、定理和证明）自动转换为可被计算机验证的形式化语言的过程。
• **AlphaProof：**AlphaProof 是由 Google DeepMind 开发的模型，以 Lean 语言自动生成数学定理的形式化证明，是第一个在 IMO 获奖的 AI 模型。
• **Mathlib 数据库：**这是基于 Lean 形式化证明系统构建的一个大型数学库，包含丰富的定义、定理和证明，用于支持数学知识的形式化与自动验证。
• **从“HumanEval” 向 “SWE-bench”跨越：**HumanEval 测试模型写单个函数的能力，侧重小规模代码生成；SWE-bench 要求模型在完整代码库中修复 bug，考察跨文件和系统级改动能力。两者区别在于前者侧重原子级能力，后者重视工程级能力。
• **DeepSeek Generative Reward Model：**这是 DeepSeek 与清华大学提出的奖励建模方法，通过生成结构化文本反馈（如评价原则与点评）来替代传统数值评分，提升大 LLM 的推理与 RL 效果，同时支持推理时的灵活扩展与优化。