AI for Research 进展综述（基于 ICML 2026 AI4Research Workshop）

来源： AI4Research · 进展综述 播客： ICML 2026 · AI4Research 分类： AI 研究 原文发表： 2026-07-10 纪要生成： 2026-07-13

本文把本届 6 场 invited talk + 1 场结构化辩论横向打通，按主题而非按人，提炼"把 AI 当作数学/CS/ML 研究工具当前的具体进展、共识与未决问题"。方括号标注支撑该论点的讲者。本 workshop 的立场很明确——聚焦"AI 帮助人类做研究的工作流"，而非"自主 AI 研究"（后者是隔壁 AI4Math 的重心）。

---

一、AI 数学能力的真实坐标：已达研究生级，离最难问题仍极远

Gukov 以纯数学家视角给出坐标系：AI 已达研究生级数学（FrontierMath Tier 4 一年内到约 50%），但离 Riemann 假设那类最难问题仍差"数十亿倍"。他认为真正瓶颈不在知识而在算法——长视野 + 稀疏奖励（如 Andrews–Curtis 猜想需约 10^10000 步）及随之而来的 reward hacking；并指出这类挑战与聚变、气候控制在结构上同构 [Sergei Gukov]。Sawhney 从另一端补上"能力已跃升"的证据（见第四节）。

二、形式化（Lean）：把"昂贵的人工评分"换成"廉价的正确性检查"

Degenne（mathlib 五年维护者）系统讲了 Lean 作为研究加速器的价值与短板：Lean 能把昂贵的人工评审换成廉价的自动正确性检查，AI 已能"从 mathlib 出发"自动形式化新证明；但产出冗长、重复、缺一般性、且永不学习。他反复强调一个与 AI4Math 呼应的要害——"证明被验 ≠ 陈述正确"（P 可能被悄悄定义成恒真）。当前最缺的是两样东西：信任大规模 AI 代码库的事后（post-hoc）工具，以及让 AI 自己写 tactics 做自动化 [Remy Degenne]。

三、Agentic 工作流：能解真实开放问题，但"配最强模型才值得"

• ProofCouncil（Gehrunger）：面向数学家的开源 harness（offer + 双 critic + LLM council + compute worker）；在 First Proof 竞赛第二批 9 题解 6，成本约为单次 GPT-5.5 Pro 查询的 30 倍，但把解题数从 4 提到 6。结论：agentic 确能解真实开放问题、超过单查询，但只有配最强模型时才划算 [Tim Gehrunger]。
• 教育范式实验（Niao He）：约 35 名零优化基础的本硕生，一学期用 AI 攻真实开放问题，9 题解 3（含 Lean 验证）、2 题实质进展（heavy ball 一维非加速、Nesterov 弯曲流形加速）。AI 强于跨域联想与套模板、弱于简化；工作流为 generator / auditor / verifier / orchestrator。教育上开创"开放问题 + AI 的 productive failure（有效失败）主动学习"范式，新瓶颈变成问题设计 [Niao He]。

四、数学家视角：AI 能力的三档跃升，已独立攻克重大猜想

Sawhney 用过去九个月的真实定理串起三档能力跃升：

1. 文献定位：帮你在文献里找到"其实已解"的问题（与 Mark Sellke 找到 10 个 Erdős 问题）；
2. 给关键点子：为 minor 开放问题提供解决的关键 idea；
3. 独立攻克重大猜想：Ramsey 数 l^(k−1) 上下界（OpenAI 内部模型，dependent random choice）、单位距离猜想 n^(1+δ) 推翻 80 年猜想（含约百万行 Lean 证明，并外溢推翻和积猜想）、Talagrand 猜想、在线向量平衡最优界。

关键观察：这些多为无数学专训的通用模型，能在"违反数学家直觉"的区域坚持、并跨领域组合 [Mehtaab Sawhney]。（注：单位距离猜想的百万行 Lean 证明与 de Moura、AI4Math 的叙述互相印证，是本届跨 workshop 的共同标志性事件。）

五、人-AI 协作而非自主：ideation–execution gap 与多样性坍缩

Diyi Yang 以 NLP"自动化研究"做三段式现实检验：

1. 创意评测（2024）：AI 生成的研究创意在 novelty / excitement / overall 上比人类 PhD 更被看好；
2. 执行评测（盲测、2–3 个月人工实现）：暴露 ideation–execution gap——人类创意评分稳定，AI 创意落地后显著下滑；
3. 接成闭环（进化搜索 + RL，仅更新 ideator、用自动执行器作奖励）：在 GRPO 后训练与 nanoGPT 25 分钟预训练上刷到 SOTA/超 baseline，但暴露"极端调参"与"多样性坍缩"（平均奖励涨、最大奖励饱和，而科学要的是最大化最大奖励）。

落点与本 workshop 主题一致：研究的核心仍是研究者，用 AI 做平庸研究、把好奇心与品味留给人 [Diyi Yang]。

六、结构化辩论：超人 AI 之后，还要不要大比例资助人类研究？

辩题：Even after AI surpasses humans in research ability, humans should continue to fund a significant proportion of today's human research workforce to conduct research.（anti-debate 形式，力求建设性综合。）

• 正方 Mireshghallah（保留 ~80%）：研究是一组任务，10% 的人类环节按 Amdahl 定律会成瓶颈；验证者必须"先做过"才能验证、要保住 pipeline；人类多样性/冗余是保险；在可逆性风险下不该骤降 [Niloofar Mireshghallah]。
• 反方 Schmidt（≤20%）：更便宜更好就该让 AI 做，把人转去模型尚不擅长的物理/生物；降到 20% 只是回到 2015 年 ICML 的规模 [Ludwig Schmidt]。
• 建设性共识：当前"模型/方法改进型"研究若 AI 做得更好就交给 AI；ICML 重心应转向 oversight/治理、AI for science、评测与科学传播，且应由独立于 AI 公司的公共资金支持；分歧收窄为"从多少起步、多快 taper 到多低"——反方接受最终 ~20–30%，正方坚持因全球风险/可逆性保留高于 20% 并缓降。民调 71–29 → 64–36（略向反方）。赛后 Gukov（乐观、认为资助会增长）与 Gehrunger（质疑公共开源 AI，举 Apertus 失败）补充点评。

七、共识信号与未决问题

已成共识：

• AI 是研究工具：加速文献、形式化、点子生成、agentic 求解；但"研究者/品味/问题设计"更值钱。
• 验证（Lean）是关键杠杆，且要区分"证明被验"与"陈述正确"。
• 改进型研究可交 AI，领域重心应转向 oversight / AI4science / 评测 / 传播，并靠独立公共资金。

公认瓶颈 / 开放问题：

• 算法瓶颈：长视野 + 稀疏奖励 + reward hacking，是通往最难问题的拦路虎 [Gukov]。
• AI 代码可信度：缺信任大规模 AI 形式化代码的事后工具；AI 产出冗长、不学习 [Degenne]。
• 成本：agentic 只有配最强模型才划算 [Gehrunger]。
• ideation–execution gap 与多样性坍缩：科学要"最大奖励"，而 RL 优化"平均奖励" [Diyi Yang]。
• 问题设计成为新瓶颈：谁来出好的开放问题 [Niao He]。
• 治理与资助：超人 AI 后人类研究规模、可逆性、资金独立性 [Debate]。

---

一页速览（Highlights）

维度	现状	代表证据
能力坐标	研究生级，离最难问题差数十亿倍	FrontierMath Tier4 50% [Gukov]
形式化	Lean 换廉价检查；证明≠陈述正确	mathlib 自动形式化 [Degenne]
Agentic	能解真实开放问题，需最强模型	ProofCouncil 9 解 6 [Gehrunger]
教育	零基础学生 + AI 攻开放问题	9 解 3 + productive failure [Niao He]
数学突破	独立推翻 80 年猜想	单位距离猜想 n^(1+δ)、百万行 Lean [Sawhney]
人-AI 协作	ideation–execution gap、多样性坍缩	创意→执行→闭环 [Diyi Yang]
治理辩论	超人 AI 后人类研究资助之争	民调 71→64 [Debate]
瓶颈	算法/可信/成本/问题设计/治理	多场

---

附：本综述引用人员现职

姓名	现职（机构 / 角色）
Sergei Gukov	Caltech 理论物理与数学 John D. MacArthur 讲席教授、Merkin 纯与应用数学中心主任；American Institute of Mathematics (AIM) 顾问主任
Remy Degenne	Inria（里尔中心 Scool 团队）终身研究员；Lean mathlib 维护者
Tim Gehrunger	ETH Zurich 算术几何博士后；IMProofBench 组织团队成员
Niao He	ETH Zurich 计算机科学系副教授，Optimization & Decision Intelligence Group 负责人
Diyi Yang	Stanford 计算机科学系助理教授（Stanford NLP / HCI / SAIL / HAI）
Mehtaab Sawhney	Columbia University Clay Research Fellow、tenure-track 助理教授；OpenAI
Niloofar Mireshghallah（辩论正方）	humans& 技术成员；2026 秋起任 CMU（工程与公共政策系 EPP + 语言技术研究所 LTI）助理教授
Ludwig Schmidt（辩论反方）	Stanford 计算机科学系助理教授；Anthropic 技术成员（亦 LAION 成员）

说明：以上职位以本届 workshop（2026-07）讲者自述与官网信息为准；提及的合作者另有 Mark Sellke、Tatsunori Hashimoto (Stanford)、Chenglei Si (Stanford) 等，未在讲者之列故不逐一列。

原文发表：2026-07-10  ·  纪要生成：2026-07-13