GPT-5.6用提示词攻克凸优化30年难题

背景

Hacker News 上的一篇帖子显示，OpenAI 的 GPT-5.6 Sol Pro 模型在一次 148 分钟的连续会话中，通过一个精心设计的提示（prompt），成功证明了一个凸优化领域自 1996 年就存在的复杂度间隙下界。该结果随后在 Lean 定理证明器中得到了形式化验证。作者 Phillip Kerger 是加州大学伯克利分校工业工程与运筹学系（IEOR）的教学教授，拥有应用数学博士学位，并已将该预印本和相关 Lean 代码公开。

该问题属于确定性零阶凸优化：对于定义在 ℝᵈ 中单位球上的凸 1-Lipschitz 函数，算法只能查询函数值（不能获得梯度），且查询次数受限于最坏情况下的 oracle 复杂度。1996 年 Protasov 给出了一种需要 O(d²) 次函数值查询的算法，但此前已知的下界仅为 Ω(d)（来自更强的一阶 oracle 模型，即同时获得函数值和梯度）。这意味着我们无法确定梯度是否真的对优化有帮助——因为函数值查询模型和一阶模型的下界相同，两者之间存在 d 的线性间隙。GPT-5.6 Sol Pro 证明了该间隙是紧的，即 Protasov 的 d² 次查询是必要的，无法改进到 d 线性量级。

核心内容

作者在得知 OpenAI 用 GPT-5.6 Sol Pro 证明了 Cycle Double Cover（CDC）猜想后，借鉴了其提示方法，将该方法论应用于自己多年来未能解决的凸优化复杂度下界问题。他编写了一个约十页长的详细提示（附在预印本末尾），结构完全模仿 OpenAI 的 CDC 提示风格。在 148 分钟不间断的工作后，模型返回了一个证明方案，解决了在 d⁻³ 精度下二次维度依赖的下界问题（作者原本要求的是 d⁻⁴ 精度）。作者随后在 Lean 中完成了形式化验证，证明通过。

该问题的核心是：在零阶凸优化中，算法可以任意选择查询点，只获得精确函数值，但知道函数是凸且 1-Lipschitz 的。这种问题在物理实验或模拟器评估目标函数时自然出现（例如选择 d 个工程参数，仅观察模拟返回的成本值）。若评估昂贵，需要知道最少需要多少次查询。作者证明，对于精度 ε = O(d⁻³)，下界为 Ω(d²)，与 Protasov 的上界 O(d²) 匹配，从而关闭了间隙。

模型构造了一族困难的凸函数（形如多个仿射函数的最大值），并设计了一个对抗性 oracle 策略，使得任何算法在 d² 次查询内都无法找到 ε-最优解。构造和主要不变量与凸优化复杂度中的经典结果（如 Nemirovsky 和 Yudin 对一阶凸优化的紧界）密切相关。

作者指出，该结果并未使用全新的凸几何或优化理论技术，而是利用了已有的方法。从 AI 能力角度看，这表明如果一个问题可以通过现有技术解决，现代 AI 方法就能找到该方案。但数学/理论计算机科学的研究者不会因此被淘汰，而是需要转向那些真正需要全新方法的难题。

关键要点

• 问题：确定性零阶凸优化中，仅使用精确函数值查询的 oracle 复杂度。自 1996 年起，上界为 O(d²)（Protasov 算法），下界仅为 Ω(d)，存在 d 线性间隙。
• 模型与提示：GPT-5.6 Sol Pro（非 Ultra）在 148 分钟连续会话中，按照 OpenAI 用于 CDC 证明的提示方法，生成了完整证明。提示约十页，包含方法论和具体策略。
• 结果：在精度 ε = O(d⁻³) 下，证明了 Ω(d²) 的下界，与已知上界匹配，从而关闭了 30 年的复杂度间隙。该证明在 Lean 中通过形式化验证。
• 作者角色：作者是预印本和 Lean 代码的作者，此前曾与 GPT-5.4 和 GPT-5.5 尝试解决该问题未果，直到看到 CDC 结果后调整提示成功。
• 技术细节：构造使用了一类困难函数（多个仿射函数的最大值）和对抗性 oracle 策略，与凸优化复杂度中的经典结果（如 Nemirovsky 和 Yudin 的紧界）相关。
• AI 能力启示：作者认为，对于可以用现有技术解决的问题，现代 AI 能够找到解决方案；但未来数学/理论计算机科学的研究者应专注于需要真正新颖方法的困难问题，而非低垂或中垂的果实。
• 公开资源：预印本、Lean 代码、完整提示、证明地图和构建说明已发布在 GitHub；原始 148 分钟聊天记录和后续改进聊天记录也已公开。

意义与影响

• 理论贡献：该结果彻底解决了凸优化中一个基础但长期悬而未决的复杂度下界问题，确认了零阶（仅函数值）与一阶（函数值+梯度）模型之间存在本质差异：当只允许函数值查询时，最优算法需要的查询次数与维度平方成正比，而非线性。这为理解不同 oracle 模型下的优化复杂度提供了关键闭合。
• AI 辅助研究的范式验证：这是继 OpenAI 的 CDC 证明之后，又一个大型语言模型在数学/理论计算机科学中产生可验证突破性结果的案例。它表明，通过精心设计的提示（尤其是模仿成功案例的方法论），AI 可以在需要数小时连续推理的复杂问题上发挥实质性作用，而不仅仅是生成简单答案。
• 对研究者的启示：作者明确指出了 AI 能力的边界——它擅长从现有技术中挖掘合适的构造和证明，但尚未创造全新的数学工具。这意味着未来研究者应聚焦于需要真正原创性方法的“硬骨头”，而将基于已有方法的中等难度问题交给 AI 辅助解决。这可能会加速某些领域的进展，同时改变科研工作的优先级。
• 可复现性与开放性：作者公开了完整的提示、聊天记录、Lean 形式化验证代码和预印本，使得该结果可以被独立验证和复现。这种透明性有助于社区评估 AI 在数学研究中的真实能力，并促进后续研究。