Tao Lab

← 返回 Dashboard

主题演讲

Tim Gowers：用「有动机的证明」让 AI 的数学发现变得透明

Tim Gowers: Motivated Proofs Making AI Mathematical Discovery Transparent
主题演讲🎤 Tim Gowers（蒂姆·高尔斯，菲尔兹奖得主、剑桥大学数学家）⏱ 20:24👁 NA
▶ 在 YouTube 观看
高尔斯先用一个几天前的真实案例展示 LLM 已能独立做出博士论文级别的组合数学新结果，再剖析当前 AI 证明在透明度、原创性、教育性和算力效率上的不足，并介绍其剑桥团队正在打造的「有动机证明」平台与数据库。

核心要点

分章详解

一个真实案例：从指数到多项式上界

  • 近期关于 AI 解决 Erdős 问题的报道很多，但那只是数学中很小的一类；高尔斯认为组合数学论文中作者来不及深究的开放问题更适合用来测试 AI。
  • 他向获授权使用的 ChatGPT 5.5 Pro 提交了 Melvin Nathanson 一篇关于和集（sum sets）可能大小的论文中的问题，模型很快把一个指数级上界改进为多项式上界；他仔细核验以排除幻觉，证明成立且并不算太难。
  • 紧接的第二个相关问题也被轻松解决；第三个更难，其已知结果来自 MIT 学生 Isaac Rajagopal 的一篇漂亮工作，原界是指数级。
  • ChatGPT 先把界改进到「根号上的指数」，并在结尾主动建议沿某些思路或可降到多项式；经 Nathanson 转给 Rajagopal、再回到模型，经过两三轮高尔斯仅说「这听起来有意思，试试看」的迭代，模型给出了多项式上界的完整证明。

如何评价这一成果及其冲击

  • Rajagopal 评估认为这不只是对其工作的显然优化，其中有他不知道、文献里也没有的额外想法；但论证大部分仍紧密建立在他的工作之上，因此他应得大量功劳。
  • 高尔斯强调该结果在 LLM 出现前足以构成一篇不错 PhD 论文的一章，而现在约一个半小时即可产出，这在一年前是不可想象的。
  • 这会显著降低进入该领域的门槛、也加大了竞争；一个关键开放问题是：借助 LLM，初学者能否做出 LLM 自身都难以独立完成的工作——目前无人知道答案。

为何不应对 LLM 现状百分百满意

  • 透明度问题：很难从 LLM 套出它「怎么想到」某个想法；思维链未必反映真实过程，也看不到它走过多少无果的死胡同。
  • 原创性难判断：除非作者明确说明某论证模仿自他人，否则即便受他人想法启发也常无从知晓，LLM 同理。
  • 理解胜于答案：被直接告知答案的学习收获远小于得到精心设计的提示；高尔斯试着扮演「不太聪明的学生」让 AI 讲解，发现它总把解释定位在「已经懂的人」的层次，因为它训练自只负责灌输的教科书，而缺乏优秀教师课堂的互动语料。
  • 算力效率：LLM 解题所用计算量远超人脑用于模拟该计算的那一小部分；人类只需极少计算就能解复杂数学，这是高尔斯仍想理解的核心。

与《苦涩的教训》的张力

  • 高尔斯声明自己确实读过 Rich Sutton 的《苦涩的教训》（Bitter Lesson），也认同其观点，但对相反立场仍抱同情。
  • 他主张在不忽视 LLM 强大力量的前提下，仍以「略带老派」的方式追求对底层机制的理解。
  • 对国际象棋等任务，只要够强就行；但对数学，他认为若能让 AI 以「类人」的方式擅长定理证明，会带来额外的价值。

剑桥团队：从 Polya 到可点击的证明平台

  • 团队的工作承接 Polya 等人对数学解题过程的研究传统，但做得细致得多——细到原则上可在计算机上实现，弥补 Polya 建议「过于笼统、难以真正提升解题能力」的缺陷。
  • 团队比 ChatGPT 早约半年成立，最初忽视 LLM 并因「LLM 做不到某些事」而自我宽慰，但这种宽慰已不复存在。
  • 策略从「自底向上（由易到难）」转为「自顶向下」：因为 LLM 已能做简单题，现在的目标是把略超 LLM 当前能力的难题，拆解为 LLM 能回答的问题。
  • 他们在构建一个实现各种通用「证明发现动作」（proof discovery moves）的平台，梦想是只靠点击选择动作（如推广、应用 modus ponens 等）就能找出证明，无需手写；并试图把看似无限的动作空间约化为有限的动作空间。

有动机证明的数据库与展望

  • 平台上能录入的证明在某种意义上都是「有动机的」「透明的」，能看清导向该证明的思维过程；高尔斯认为称之为「透明证明」或「把发现过程摊开的证明」更贴切。
  • 团队获 Renaissance Technologies 与 XTX Markets 通过「AI for Math Fund」资助，用以建设平台并构建「有动机证明」数据库，该库可用于训练 LLM 更高效、更透明地做数学。
  • 效率的意义不仅在于速度与进一步扩展的潜力，也在于环保——减少解题所需资源。
  • 原型已存在但仍较初级，未来一个月左右会大幅重新设计；待能录入足够有趣的问题后将公开，期待大家来玩并吸引外部合作者。
  • 高尔斯提到将于十月与 SAIR（SER）基金会展开合作。

关键引述

“我什么都没做，只是说「这听起来有意思，对，也许你可以试试那个」，经过两三轮迭代，它就给出了这个更难问题的多项式上界的完整证明。”— Tim Gowers
“这种结果在 LLM 出现之前，足以轻松构成一篇还不错的博士论文的一章——而它现在是被 ChatGPT 在一个半小时左右产出的。一年前这是不可想象的。”— Tim Gowers
“我们想要的是对数学的洞见，而不只是正确的证明。如果别人直接告诉你答案，你学到的远比给你精心选择的提示要少。”— Tim Gowers
“我向你保证我读过 Rich Sutton 的《苦涩的教训》。尽管如此，我对相反的观点仍有些同情——我想稍微以老派的方式做事，不忽视 LLM 的力量，但更好地理解究竟发生了什么。”— Tim Gowers
“我们的目标，是把刚好超出 LLM 当时能力的问题，约化为 LLM 能够回答的问题；并把证明发现的过程从一个看似无限的动作空间，化为一个有限的动作空间。”— Tim Gowers

术语 / 人物

Tim Gowers（蒂姆·高尔斯） — 1998 年菲尔兹奖得主，剑桥大学与法兰西公学院数学家，泛函分析与组合数学专家，长期推动「人本式」自动定理证明研究。
Motivated Proof（有动机的证明） — 高尔斯团队提出的概念：每一步都有可理解动机、不靠「从帽子里变兔子」的魔术式技巧，能把证明发现的思路完全摊开、可复现。
和集（sum sets） — 加性组合数学中的对象，研究集合 A 中元素两两相加所得集合 A+A 的可能大小，本视频案例即来自 Nathanson 关于和集大小的论文。
指数 / 多项式上界 — 刻画量随规模增长速度的界；把指数级上界改进为多项式上界是显著且更有价值的进步，本案例即实现了这一改进。
Bitter Lesson（苦涩的教训） — Rich Sutton 提出的观点：在 AI 历史中，依赖大规模计算与通用搜索/学习的方法，长期上往往胜过依赖人类领域知识的精巧方法。
George Polya（波利亚） — 著名数学教育家，《How to Solve It》等著作系统总结解题启发法；高尔斯团队试图将其思想细化到可在计算机上实现的程度。
AI for Math Fund — 由 Renaissance Technologies、XTX Markets 等支持（经 Renaissance Philanthropies 发起）的基金，资助 AI 与数学方向项目，高尔斯团队的「有动机证明数据库」为入选项目之一。

背景补充

Tim Gowers 是 1998 年菲尔兹奖得主，剑桥大学三一学院与法兰西公学院教授，以泛函分析、组合数学及 Polymath 协作数学项目闻名。自 2022 年起，他在剑桥领导一个「人本式自动定理证明」研究组（最初由 Astera Institute 资助），追求让计算机以接近人类的方式发现证明，并提出「有动机证明」概念——即不靠魔术式技巧、每步都有清晰动机的证明。其团队近年获 AI for Math Fund 资助，建设「结构化有动机证明」数据库；这项研究可追溯到他与 Mohan Ganesalingam 早年合作的「具人类风格输出的自动解题器」工作。

适合谁看

适合关注 AI 与数学交叉、自动定理证明、LLM 推理能力与可解释性的研究者、研究生及科技从业者，也适合对前沿数学如何被 AI 改变感兴趣的广泛读者。