来源： Invited Talk 04 · Michael R. Douglas 播客： ICML 2026 · AI4Physics 分类： 科学 原文发表： 2026-07-11 纪要生成： 2026-07-13
面对"AI 能写出千页程序/证明，但我们读不完、也不敢信"的新局面，Douglas 主张核心问题是 validation（验证）：不要让语言模型去检查另一个语言模型，而要产出算法可检验的证书（algorithm-checkable certificates）——用 Lean 等交互式定理证明器把物理论证的公理与推导形式化，从而把信任扩展到千页、百万页的解，并区分"证明被验"与"假设/陈述是否忠实编码问题"。
以自己领域的例子点题：粒子物理需要为 LHC（CERN）计算散射振幅（amplitudes），从 Feynman 图出发但早已超出 Feynman 图能算的范围，发展出各种精巧技术，最终归结为一个编程问题。若把它交给编码 agent（"问 GPT 某版本"），它给你一个千页程序——我们做完了吗？没有：我们读不了这个程序，若某处有错怎么办？要把程序理解到能依赖它的程度，花的时间远超过 AI 写它的时间。这就是 validation——工程学（尤以软件工程最贴近）里成熟的领域。AI 是统计性的、会犯错；研究本就意味着有时提出错误假设，所以每个推理 agent 都必须有发现并纠错的循环。人类科学的方法/协议只能部分迁移到 AI：若全盘迁移，就成了"AI 说服 AI"，可目标是说服我们人类。
他倡导 algorithm-checkable certificates：不是让一个语言模型检查另一个语言模型的工作，而是一个证书，声明"能被编码进证书的那部分问题是正确的"；算法可理解、可信任，且能扩展到千页、百万页的解。这是已有技术，但它正成为讨论中心，这一点是新的。
AI for math 正突飞猛进（他提及昨天 AI for science workshop 上 Madhur/相关讲者关于组合学新结果的报告——由 agent 自主或大幅辅助证明）。关键工具是交互式定理证明器（interactive theorem provers）：把数学证明表达成一种只允许可靠推演的编程语言，几乎任何数学陈述都能形式化。例子：欧几里得"素数无穷"的证明。技术成熟、非常通用，虽难读难写，但编码 agent 相当擅长（仅过去一年 agent 也获得了用这类语言编码的能力）——这就是一个证书。
不妨先问：真需要机器检查一切吗？近来最著名的成果是 OpenAI 反驳了 Erdős 的一个猜想（开放约 80 年，人们强烈相信它成立）——用了一个不算彻底革命、但对数学家而言是新的想法（数学家事后说"我们本可以做，只是没做"），且并未通过任何证书，而是九位顶尖数学家扑上去核验、确认是有效证明（此后又被改进、实验被具体化）。人类核验有效，但你无法为 AI 的每个产出都请来九位数学家——需要能规模化的技术。
Lean 4 可用。AI 已能可靠地做（形式化尚未完全解决但飞速推进）；今年有一系列论文用 agent 在 Lean 里编码大型数学框架。他预测：到 2027 年底，大部分乃至全部教科书数学（指高级研究生教科书）将基本自动地被翻译进这种语言。物理例子：Brenner 讲的渐近展开可数值验证（一种 validation 技术）。另一近例（去年底、用 Lean 完成）：推广量子 Stein 引理（quantum Stein's lemma）——量子信息的中心定理，已知原有证明有 gap，社区很关心补上，如今已由 Lean 机器验证补上，检查过程确实帮助抓出 gap，技术开始证明其价值。
Lean 等给你的是 verification（验证）：一个证书声明"假设 A、B、C 蕴含结论 X、Y、Z"，编码进语言、编译通过，你就能像对任何事一样确信（除非硬件出错）该蕴含正确。但这本身解决你的问题了吗？对 LHC 例子——还需推导该方法、写程序、定义待算结果所用的假设也正确；否则你只是相对这些假设证明了它。Validation（确认）是更大命题：不仅检查某证书正确，而且它确实忠实地编码了手头的问题/任务。两者相辅相成。
A := 定义1、B := 定义2 的顺序互换，通常会得到一个看起来很像原程序、但因定义搞乱而错误的程序；而交互式定理证明能阻止这类错误——把关于定义的大量信息塞进编译并检查，一者正确、另一者会被计算机拒绝。数学物理是真正严格的特例：可把理论物理结果证到数学家标准，再插进 Lean 形式化。但更广的应用是：物理工作看起来是数学、用数学概念表述，数学家会说"你没证明、跳了步"；物理学家可回答——我的论证基于物理假设（不是纯直觉），例如量子场论中的局域性（locality）；我不知如何从局域性证明这个推论，但若它失败我会极其震惊，因此可把它当作我的一条公理，其余部分我称之为严格、你也该认可。目标是：不仅让 AI 认可，还要有那种可检验证书说该论证可验证地正确。
他最近做了一例（语音识别把 Seiberg-Witten 记作"Cyber Witten/Cyber Goodwin"）：约 30 多年前 Seiberg-Witten 给出四维量子场论的首个精确解，且与标准模型/QCD 的 Yang-Mills 理论密切相关，其推导仅几步就说明一个类似 QCD 的理论把夸克禁闭（confine）成无色对象——粒子物理的中心结果，至今没有更好的论证（格点规范理论能看到禁闭，但那是模拟，缺乏此解的理论深度与美感）。作为演示：把该物理论文的公理用精确、准数学的术语陈述（因基于 Riemann 曲面的数学，这里较容易），在 Lean 4 中验证这些编码 Seiberg-Witten 假设的公理确实蕴含其结论。这是原理验证：原论文约 30 页、零疑义、已被其他方法确认；但方法可扩展——若它当初是 GPT 产出的 10 万页论文，仍可套用此法，"只是要花点时间真正吃透，但我们确知它正确"。
回到 LHC 对撞振幅：这源自约一个半月前在 IAS 的一个 workshop（与 David Kosower、Jesse Thaler 等专家），主题是能否用数学把此前完全超范围的 Feynman 图计算带进超算可及范围、并用编码助手写出比旧程序更好的新程序。微扰散射振幅的定义在许多教科书里、无歧义；关键在把它与那些精巧数学技巧编码进更精确的记号，再对 GPT 的千页程序不是证明程序正确、而是证明"该程序是从这组公理推导出来的"（公理你可对照教科书核验）。 错误率直觉：无论技术如何都有某个残余错误率 ε，你能写出的程序/证明长度上限约 1/ε，超过就大概率出错。三年前模型总在幻觉，两年前有时幻觉，如今相当好但仍不完美（人也不完美）。形式化能把 ε 变得很小 → 扩展你的可达范围，也决定了"科学知识形式化仓库"能有多大。
把讨论系统化：探索性研究 → 发现（概念结晶、公认有新知识）→ 成熟（获得应用）。LHC 物理明显处于成熟阶段（靠标准模型/Feynman 图预测实验）；许多物理问题仍在探索阶段。这些方法全程有用，但要依问题性质选择恰当用法。
Q1（观众）： 当前语言模型是否展现出构造前所未知的数学结构的能力（如量子力学发明后人们找到 Hilbert 空间那样）？ A1： 目前只有微光（glimmers）。OpenAI 那个 Erdős 成果是一例（数学家认可是两个想法的巧妙结合，"我们本也能做，只是没做"）；但我认为没有根本障碍，我有信心预测五年内 AI 将在各门科学中产出各种新概念，很可能远早于此。
Q2（观众）： 如何用这些工具做出好的猜想、又如何验证猜想？ A2： "是否是好猜想"与"如何验证"是两件事。验证较简单且成熟：一方面找反例（常很有成效），另一方面尝试证明它或把它约化为已知真假的陈述；定理证明器让"严格表述量子场论所需的数学"变得远为可及（过去我不敢碰、现在能碰，能像以前那样研究猜想、并用工具证出某个反例）。而"什么是好猜想"要难得多，可以是另一场报告的主题——他提到有一篇近作与"mess and bark"（合作者）以及 Mike Freedman 合写，可供参阅。（随后主持人致谢。）