AI for Math 进展综述（基于 ICML 2026 AI4Math Workshop）
来源： AI4Math · 进展综述
播客： ICML 2026 · AI4Math
分类： AI 研究
原文发表： 2026-07-11
纪要生成： 2026-07-13
本文把本届 8 场报告（Dawn Song 开场主旨 + 7 场 invited talk）横向打通，按主题而非按人，提炼"AI for Math 这个学科当前的具体进展、共识与未决问题"。方括号标注支撑该论点的讲者。全场基调呼应本届主题 "Toward Self-Evolving Scientific Agents"（迈向自我演化的科学 agent）。
参会规模本身也是进展信号：投稿 346 篇（逐年翻倍 30→172→346），其中形式化相关（定理证明、自动形式化、形式验证）合计超 40%，是社区重心 [开场]。
一、证明范式：从"整证/分步"走向"agentic"
过去两年形式定理证明的主线是证明生成范式的迭代：
- Whole-proof（整证）：一次生成完整 Lean 证明——小错即被整体拒绝、难生成长链、且浪费证明助手的交互反馈 [Junqi Liu]。
- Step prover（分步）：每步一个 tactic + 搜索（MCTS 等），2024 年 DeepMind 借此达 IMO 银牌；但搜索开销大、tactic 空间固定、难泛化、且不会像人那样试特例/引理 [Junqi Liu]。
- Agentic（当前前沿）：让模型先生成小引理、复用引理往上搭，配"propose→prove→summarize errors→refine"循环，实现长程推理 [Zheng Yuan/Seed Prover]；或直接把通用 coding agent 接上 Lean 工具、由 agent 自主决定调用时机 [Junqi Liu/Numina Agent]。
一个明确的架构共识正在形成：基座模型与 harness（工具集 + 系统提示）解耦，且"模型改进 > harness 改进、少给控制、多给上下文" [Zheng Yuan]。Numina Agent 用 Claude/DeepSeek 作基座、以约 1/8 成本达到接近顶配效果，佐证了这一解耦 [Junqi Liu]。
里程碑级战绩（说明范式已能打硬仗）：Seed Prover 在 IMO 2025 证 5/6、历届 IMO 约 80%、MiniF2F 近全解 [Zheng Yuan]；Numina Agent 在 Putnam 2025 12/12 全解，为首个对齐闭源 SOTA 的开源系统 [Junqi Liu]；Boris 用 Lean+ChatGPT 从新手到提交约 100 万行证明、证否单位距离猜想 [de Moura]。
二、训练方法：RL、课程、依赖感知、模型多样性
- 大规模 RL 成为主力：Lean 是做 RL 的理想场所——有无限数据的清晰 ground-truth 奖励。Seed Prover 用带 value 预训练的 PPO、稀疏奖励（+1/−1，无过程奖励）、课程式难度（过易丢弃、过难分解或生成易变体），1200 步内训练准确率 50%→~90%，且随能力提升"工具调用次数与序列长度下降" [Zheng Yuan]。Dawn Song 亦强调 RL/前沿 AI 已到"自动化定理证明的拐点" [开场]。
- 冷启动 + SFT 教会 agent 用工具与多轮交互，是 RL 能 rollout 出正信号的前提 [Zheng Yuan]。
- 依赖感知训练：premise selection 不再只看"语义相似"，而是利用 mathlib/Blueprint 的依赖图（跳数、边方向、邻居类型、子图多样性），在小预算与分布外仍有效 [Yinya Huang]。
- 模型多样性作为资源：与其追一个"最优模型"，不如让多样模型协作——union 预测提升约 20% 证明率、能让弱模型组合达到最佳单模型水平；共享子目标快 50%；这在有"Oracle（证明器）"的形式场景尤其可行 [Emily First]。
- 神经符号结合：用 LLM 生成模板、符号引擎实例化引理（Lemonade），在引理猜想上稳定优于纯神经与纯符号（QuickSpec）[Emily First]。
三、非形式 ↔ 形式：鸿沟正在被系统性地弥合
这是本届反复出现的中枢议题：
- 为什么要形式化：非形式（自然语言）数学只看最终答案、无法保证过程正确；形式系统能逐步自动检查、展示证明状态 [Junqi Liu]。
- 自动形式化的忠实性成为独立研究对象：定义"对齐"（保留全部约束、逻辑一致、不引入额外约束），建 28 类错误 + "判定→归类→定位→纠正"四子任务；发现前沿 LLM 判定尚可但归类/定位/纠正弱，而 1.7B 小模型经训练即可胜任评测 [Yinya Huang]。
- 两种推理互相促进：形式推理常被非形式推理卡住，反之非形式又可被形式改善——因此需联合提升 [Zheng Yuan]。
- premise selection 把"非形式问题"接入形式证明技术，并反哺下游非形式证明（IMO ProofBench）[Yinya Huang]。
四、基础设施与生态：可扩展、可信、可协作
形式数学的"操作系统层"正在成型，且这是很多进展的隐性前提：
- Lean + mathlib：既是语言也是证明助手；可扩展、可扩到大规模（10 亿行级）、可信（多内核交叉验证，如 nanoda / arena.lean-lang.org）；mathlib 700+ 贡献者、200 万+ 行，是费马大定理等项目的地基 [de Moura]。
- 面向 AI 的工具链：Verso（可交互文档）、Blueprint（理解人/AI 完成的大项目）、Lean Verbose（点选式、教育）、Workbench（零安装、浏览器内、预配 AI）、Lean 的 MCP 标准化 [de Moura]。
- 成果共享与协作：TaoSet（AI 写/审代码、人定路线图，含 PDE 支持推进）[de Moura]；CSLib 把这套范式延伸到计算机科学（算法/数据结构的正确性与复杂度验证，Time Monad 把复杂度当"副作用"与正确性解耦）[Sorachai]。
五、评测在"军备竞赛"式演进
- 旧基准快速饱和："有基准，几个月内就会被解"——MiniF2F 近全解、PutnamBench 被解、Verina 一年内饱和 [Zheng Yuan / Dawn Song]。
- 走向 repo 级 / 工程化：APE-Bench 把任务从"证一个孤立定理"升级为"在真实 GitHub commit 上做证明工程"（"Lean 版 SWE-bench"，编译器 + LLM-judge 双层评测），下一步是多文件、"自动化库构建 agent" [Zheng Yuan]。
- 验证"陈述"而非只验证"证明"：用 Lean 证开放猜想时，Lean 只验证明、不验陈述正确性——需 comparator、"Validating a Lean Proof"、LeanEval（211 题、持续加题，Seed 已证约一半）来兜底 [de Moura / Zheng Yuan]。
- Challenge 化：本届 4 条 challenge track（自动形式化忠实性 FormalRx、TCS proving、视觉物理 SeePhys、端到端形式化 ShadowBench），506 参赛者、2300+ 提交 [开场]。
六、应用与外溢：AI4Math 不止于"解题"
- 可证明安全的系统：把定理证明 + 程序合成用于"secure by construction"，生成可证明安全代码，扭转网络安全攻防不对称（Verina 已饱和、repo 级 Vero 仍难）[Dawn Song]。
- 计算机科学形式化：CSLib 迈向"CS 领域的 mathlib"（含把 Rust 等真实代码翻成中间语言 Boo 做验证）[Sorachai]。
- 理论视角回看学习本身：用理论物理"最小作用量原理"统一看学习动力学，稳态解对应学习算法（数据规划 / 贝尔曼最优 / MLE）——一种"AI for Math 反哺 ML 理论"的尝试 [Siyuan Guo]。
七、共识信号与未决问题
已成共识：
- Lean/形式化是当前 AI for Math 的主战场；agentic + 大规模 RL 是当红范式；基座与 harness 解耦、"少控制多上下文"。
- 评测必须持续升级（repo 级、验陈述、challenge），否则很快饱和。
- 非形式与形式必须协同，自动形式化的忠实性是关键卡点。
公认瓶颈 / 开放问题：
- mathlib 覆盖缺口：想形式化最新猜想却发现所依赖的项不在库里——大规模形式化传统定理回馈 mathlib 是关键瓶颈 [Zheng Yuan]。
- 长程 RL 的 credit assignment（跨天任务）尚无标准解 [Zheng Yuan]。
- 可解释性/机理：多样模型表现相同但内部机理不同，鲁棒性差异只在 OOD 显现 [Emily First]；协作"为何有效"难解释。
- 能耗与数据效率：与人脑（20W / 1.15 亿词）相比，ML 仍极不高效，呼唤更根本的学习原理 [Siyuan Guo]。
- 学术界算力受限下如何贡献：转向"通用、可迁移、非纯 SOTA 竞争"的研究问题 [Yinya Huang]。
一页速览（Highlights）
| 维度 |
现状 |
代表证据 |
| 范式 |
agentic（引理式 + 工具 + 循环）成为前沿 |
Numina Agent、Seed Prover 1.5 |
| 训练 |
大规模 RL + 课程 + 稀疏奖励；依赖感知；模型多样性 |
Seed Prover、Yinya、Emily First |
| 战绩 |
IMO 2025 5/6、Putnam 12/12、百万行证明 |
Seed、Numina、de Moura |
| 非形式↔形式 |
autoformalization 忠实性评测（28 类错误）；premise selection |
Yinya Huang |
| 基础设施 |
Lean/mathlib/多内核 + Verso/Blueprint/Workbench/TaoSet/CSLib |
de Moura、Sorachai |
| 评测 |
从 MiniF2F/Putnam（饱和）→ APE-Bench（repo 级）→ 验陈述 |
Zheng Yuan、de Moura |
| 外溢 |
可证明安全代码、CS 形式化、ML 理论 |
Dawn Song、Sorachai、Siyuan Guo |
| 瓶颈 |
mathlib 覆盖、长程 credit assignment、机理可解释、能耗/数据效率 |
多场 |
附：本综述引用人员现职
| 姓名 |
现职（机构 / 角色） |
| Dawn Song |
UC Berkeley 计算机科学教授；Berkeley Center for Responsible Decentralized Intelligence 主任 |
| Junqi Liu |
中科院数学与系统科学研究院 (AMSS) 博士生；Project Numina 形式化团队负责人、Kimina-Prover 贡献者 |
| Leonardo de Moura |
AWS 自动推理组 Senior Principal Applied Scientist；Lean FRO 首席架构师与联合创始人（Lean/Z3 主要设计者） |
| Siyuan Guo |
Prior Labs AI 科学家（剑桥大学 + Max Planck 智能系统所联合博士） |
| Sorrachai Yingchareonthawornchai |
ETH Zurich 理论研究所 Junior Fellow；CSLib 技术负责人 |
| Yinya Huang |
ETH Zurich AI Center 博士后 fellow（中山大学博士） |
| Emily First |
Rutgers University 计算机科学助理教授 |
| Zheng Yuan |
ByteDance Seed 研究员（清华大学博士）；主导 Seed Prover |
说明：以上职位以本届 workshop（2026-07）讲者自述与官网信息为准。
原文发表：2026-07-11 · 纪要生成：2026-07-13