清华学者用 GPT 证明优化理论 40 年难题
新智元 · wechat · 2026-08-23
清华大学与沃顿商学院研究者利用 GPT-5.6SolPro 解决了优化界悬停 40 年的问题：仅靠调整步长无法让梯度下降达到 O(1/T²) 的最优收敛速度。
核心突破：
- AI 主导证明：研究者提出「对抗预言机」策略，GPT-5.6 构造了复杂的几何证明，证明纯步长调度的收敛率上界为 Ω(T^{-1.9319})。
- Lean4 形式化验证：通过 Codex 将证明转写为 Lean4 代码，经编译器逐行终审，实现了「零 sorry，零 admit」的完美验证。
- 结论：想要达到 Nesterov 加速法的速度，必须改变算法结构而非仅调整步长。
「漫话AGI」频道最新
- 全能 Agent 市场将利好消费者，冲击中间商 — heyneighbor · 2026-08-23
- AI竞赛陷入悖论：既要长时自主又要防意外 — VraserX · 2026-08-23
- 反 AI 情绪愈发极端，媒体立场引关注 — haider1 · 2026-08-23
- ChatGPT 成交互日记：百年后历史学家该如何存档？ — romeoprico · 2026-08-23
- 回顾 Alondra Nelson 三年前提出的“Thick Alignment”理念 — arvindsatya1 · 2026-08-23
- 医疗与政务难懂，消费级 AI 实际被低估 — emollick · 2026-08-23