清华大学工业工程系研究者 Jianhao Ma 与宾夕法尼亚大学沃顿商学院教授 Yuxin Chen 近日发布一篇新论文，给一个持续约 40 年的优化理论问题给出结论：标准梯度下降如果只调整步长序列、而不引入动量或改变算法结构，就存在无法跨越的收敛速度上限。
论文的核心结论是，对任意预先确定的非负步长序列，梯度下降的收敛率下界为 Ω(T^-1.9319)。按文中表述，这意味着纯粹依赖步长调度，无法把标准梯度下降推进到 Nesterov 动量法达到的 O(1/T²) 速度。
问题起点：只改步长，能否追上动量方法
报道指出，梯度下降是大量 AI 系统使用的基础优化方法，包括 GPT、Stable Diffusion 和自动驾驶相关训练过程。标准梯度下降的收敛速度通常写作 O(1/T)，即运行 T 步后，误差降到约 1/T 的量级。
1983 年，Nesterov 在梯度下降中引入动量机制，把收敛速度提升到 O(1/T²)。按照文中的例子，在相同步数下，误差量级可从千分之一降到百万分之一，相差 3 个数量级。报道称，这一结果至今仍被视为理论最优。
由此引出的长期问题是：如果不加动量、不改算法结构，只靠精细设计每一步的步长，标准梯度下降能否达到同样的速度。
直到 2023 年，MIT 的 Altschuler 和 Parrilo 提出 silver stepsize。报道称，这组步长并非传统的逐步递减，而是呈现忽大忽小的分形自相似结构，并把梯度下降推进到 O(T^-1.2716)。这也让问题进一步收缩为：1.2716 是纯步长调度的起点，还是它的极限。
研究者与 AI 的分工
接手这一问题的是 Jianhao Ma 和 Yuxin Chen。报道显示，Ma 于今年 7 月入职清华大学工业工程系，此前在密歇根大学获得博士学位，并在宾大完成博士后工作后回国任教。Chen 是沃顿商学院的冠名教授，拥有斯坦福博士背景，曾从普林斯顿转至宾大，并获得过 SIAM 最佳论文奖。
与此前尝试继续设计更优步长序列的路线不同，两人的思路是反过来证明一条不可逾越的边界：无论步长如何设计，都不可能把标准梯度下降提升到 O(1/T²)。
报道称，他们随后把这个问题交给 GPT-5.6 Sol Pro 处理，并向模型提供两项输入：一是研究目标，即证明纯步长调度无法实现 O(1/T²)；二是一个高层策略——「resisting oracle」对抗预言机。
这一策略的思路是，先构造一条让梯度下降尽可能慢的对抗轨迹，再找到一个真实的光滑凸函数，使得梯度下降在该函数上的运行路径与这条慢轨迹严格对应。
核心证明如何构造
按照报道，GPT-5.6 Sol Pro 最终给出的核心方案是一种几何构造。
给定任意一组步长序列，先从中挑出「长步」，也就是步长超过标准安全值 1/L 的部分。随后，在高维空间中放置一组彼此正交的锚点，每个长步对应一个锚点。这样一来，梯度下降在两个长步之间会被限制在同一方向上前进，而每次遇到长步时，又会被切换到下一个完全垂直的方向。
报道称，这条轨迹可以由一个名为 Moreau 包络的光滑凸函数精确实现，并与前述构造严格等价。这个设计的关键在于，它会针对给定的步长序列量身定制。也就是说，不论步长怎样安排，都能构造出一个对应函数，使算法被卡在这条路径上。
不过，证明并未到此结束。文中提到，最终得到的下界不能依赖长步出现的先后顺序，否则同一组步长若改变排列方式，就可能绕开结论。
为处理这个问题，GPT-5.6 Sol Pro 又给出了一套匹配技巧：先按大小排列长步，再构造路径，并拆成奇偶两组匹配，以此消除时序依赖。之后再引入一个 Lyapunov 势函数控制全局增长，并配合截断论证，把局部约束汇总为整体下界。
报道写道，这套论证并非一次成型，而是 Ma 和 Chen 与 GPT-5.6 Sol Pro 多轮交互的结果。研究者在发现推导瑕疵后提出修正，模型再继续补完证明。Ma 的原话是，核心证明中「没有任何非平凡的数学成分来自人类」。
下界为何落在 1.9319
整套证明里有一个关键参数，同时受到两个条件约束。报道称，其中匹配界给出下限，增长控制给出上限。当收敛指数 p 下降时，这两个约束会逐步收紧。
在 p = √(2+√3) ≈ 1.9319 时，两条约束线相交，参数可活动空间归零，证明也无法再往下推进。由此，GPT-5.6 Sol Pro 最终给出的结论是，对任意预先确定的非负步长序列，梯度下降的收敛率下界为 Ω(T^-1.9319)。
按报道的解释，这意味着单纯依靠步长设计，标准梯度下降无论调度多么复杂，都无法越过这条线；若想达到最快收敛速度，必须调整算法结构。
Lean 4 形式化验证：零 sorry，零 admit
对于 AI 生成的证明，论文作者采用了 Lean 4 定理证明器做形式化验证。报道称，他们使用 Codex 将 GPT-5.6 Sol Pro 输出的自然语言证明逐步转写成 Lean 4 代码，再由形式化系统逐行检查推导。
在 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 代码，编译器则完成逐行终审，人类研究者全程监督。
上界与下界之间仍有 0.66 的空白
目前能够确认的区间是：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。
论文参考地址为：https://arxiv.org/abs/2608.10418。
本文来自微信公众号「新智元」，作者为「ASI启示录」，编辑为「摩西」。MarsBit 页面信息显示，文章发布时间为 2026 年 8 月 24 日。