清华沃顿师徒破解40年悬案！核心数学全是GPT写的，你上你也行

新智元报道 训练一切AI的算法，被AI自己判了「死刑」？ 就在最近，清华大学和宾大沃顿商学院的两位研究者挂出一篇新论文，给了一个优化理论界等了40年的结论—— 梯度下降想跑到最快，光调步长没用。 这是历史上第一次有人证明，梯度下降光靠设计步长序列，存在一道跨不过去的数学天花板。 而且，完成核心证明的不是人，是GPT-5.6 Sol Pro。 GPT-5.6搞定了一个40年没人答过的问题 事情是这样的。 梯度下降大家都知道，从GPT到Stable Diffusion到自动驾驶，底下跑的都是它。标准梯度下降的收敛速度是O(1/T)，跑T步，误差大概降到1/T的量级。 1983年，Nesterov给梯度下降加上动量，直接推到了 O(1/T²) 。同样跑1000步，误差从千分之一变成百万分之一，差三个数量级。至今仍是理论最优。 那一个很自然的问题就来了：不加动量、不改结构，纯靠精心设计每一步的步长大小，能不能也追上Nesterov？ 这个问题悬了整整40年。直到2023年，MIT的Altschuler和Parrilo搞出了silver stepsize。 这组步长序列不是传统的逐步递减，而是忽大忽小，呈分形自相似结构。靠它，梯度下降被推到了 O(T^{-1.2716}) 。 那么这个1.2716到底是纯步长调度的终点，还是只是个起步？ 最近，一对华人师徒接下了这个问题。 Jianhao Ma今年7月刚入职清华大学工业工程系，密歇根大学博士，在宾大做完博后回国拿到的教职。 他的博后导师Yuxin Chen是沃顿商学院的冠名教授，斯坦福博士，从普林斯顿跳到宾大，拿过SIAM最佳论文奖。 之前所有人都在做加法，设计更聪明的步长序列，看速度能提多高。 Ma和Chen的想法则是反过来去证明存在一条线，不管步长怎么设计都不可能跨过。 找一组好步长，你只需要一个成功的例子。但要证明「所有可能的步长都不行」，是对无穷多种可能性说「不」。 两个人琢磨了一阵，直接把问题丢给了GPT-5.6 Sol Pro，让AI试试。 具体来说，他们给了GPT两样东西。 一个是研究目标，证明纯步长调度无法达到O(1/T²)。另一个是高层策略，叫「resisting oracle」（对抗预言机）。 它的原理是，先构造一条让梯度下降走得最慢的对抗轨迹，再找到一个真实的光滑凸函数，让梯度下降在这个函数上走出的路径恰好就是这条慢路。 方向定好之后，GPT-5.6 Sol Pro就开始干活了。 它最终给出的核心方案是一个几何构造。 给定任意一组步长序列，先挑出其中的「长步」，也就是步长超过标准安全值1/L的那些步。然后在高维空间里放一组互相垂直的锚点，每个长步对应一个。 梯度下降在两个长步之间被迫沿同一个方向走，碰到长步就跳到下一个完全垂直的方向上去。整条轨迹由一个叫Moreau包络的光滑凸函数精确实现，严格等价。 这个构造的关键在于，它是对着你的步长序列量身定做的。不管你怎么设计步长，它都能造出一个对应的函数卡住你。 但证明到这里还没完。 最终的下界不能依赖长步出现的先后顺序，否则同一组步长换个排列就可能逃掉。 GPT-5.6又找到了一个匹配技巧，把长步按大小排列，构造一条路径，拆成奇偶两组匹配，彻底消除了时序依赖。然后引入一个Lyapunov势函数控制全局增长，配合截断论证，把局部约束汇聚成整体下界。 这套论证，是Ma和Chen反复和GPT-5.6 Sol Pro交互，碰到推导有瑕疵就指出来，GPT修正后继续往下走，经过多次迭代才完整成形。 用Ma自己的话说就是， 核心证明中没有任何非平凡的数学成分来自人类。 整套证明中有一个关键参数，同时受两个条件约束，匹配界给了下限，增长控制给了上限。 当收敛指数p下降时，两个约束越收越紧。在p = √(2+√3) ≈ 1.9319处，两条线碰到一起，参数的活动空间归零。再往下推，证明就走不通了。 GPT-5.6 Sol Pro最终给出的结论是，对任意预先确定的非负步长序列，梯度下降的收敛率下界为 Ω(T^{-1.9319}) 。 纯调步长的梯度下降，不管步长序列设计得多精巧，永远跑不过这条线。 换句话说就是，想要最快的收敛速度，必须动 算法 结构。 Lean 4终审：零sorry，零admit AI写的证明，怎么确认不是幻觉？ Ma和Chen用了数学界最硬核的验证手段，Lean 4定理证明器。 他们用Codex把GPT-5.6 Sol Pro的自然语言证明逐步转写成了Lean 4代码。 这套形式化验证系统会逐行检查每一步推导，任何逻辑跳跃或缺少依据，编译直接报错。 如果某一步实在证不下去，可以插一个sorry或admit先跳过——意思是「这步我还没证完」。 最终成绩单： 零sorry，零admit 。一步都没跳。 代码公开在GitHub，附带TRACEABILITY.md，逐行对照论文中每个定理和Lean代码中的对应证明。想查的人自己去编译就行。 项目地址：https://github.com/jianhaoma/gd-lower-bound-lean 整条验证链是三段接力。GPT-5.6 Sol Pro构造证明，Codex翻译成Lean 4，编译器逐行终审。人类全程在旁监督。 你不需要「相信」AI，让形式系统来判就行。 故事还没讲完 目前能确认的范围是这样的：silver stepsize已经把梯度下降推到了T^{-1.2716}，Ma和Chen证明了不可能超过T^{-1.9319}。 中间还差0.66。真正的极限在哪？ 长期研究这个问题的优化学者Ben Grimmer看完论文后表示，他「强烈相信」1.2716就是真正的天花板。 如果他是对的，那silver stepsize已经是纯步长调度的尽头了，Ma和Chen的下界还有继续收紧的空间。 但不管真正的极限落在哪，这篇论文已经完成了最核心的一步： 纯靠调步长， 梯度下降 跑不到满分。这件事从猜测变成了定理。 而做出这个结果的，就俩人。没有数学团队，没有Lean专家，没有专属算力预算，用的是所有人都能调用的商用版GPT-5.6 Sol Pro。 如果这种模式可以复制，全世界任何一个有好问题的研究者，都可以让AI替自己跑证明。 参考资料： https://arxiv.org/abs/2608.10418 编辑：摩西 秒追ASI ⭐ 点赞、转发、在看一键三连 ⭐ 点亮星标，锁定新智元极速推送！ 文章原文