A Domain-Specific Harness for End-to-End Automation of Optimization Research
Heechang Kim, Ernest K. Ryu, Shuvomoy Das Gupta
math.OC
2026-08-08
把「数值设计最优梯度法→猜解析式→收敛证明」整条研究流水线包进四个 agent skill,人只做审批;产出的 LemniAcc 把梯度范数最优率常数从 64 压到 47.27,ITEM-f 拿到闭式,主定理全部通过 Lean 机器检查。
设计一个「理论上最优」的梯度法,过去是一条完全靠人力的流水线:先用性能估计规划(performance estimation programming,PEP,把「某类函数上算法的最坏表现」写成一个半定规划来算)把最优步长数值解出来,再靠领域专家盯着数值猜出解析公式,然后手推收敛性证明,最后写成论文。OGM、OGM-G、ITEM 这些知名方法都是这么诞生的。BnB-PEP 把「设计算法」本身写成一个非凸 QCQP,能联合优化步长和证明,但推导和编码极其繁琐,非专家几乎用不起来。瓶颈不在计算,在每一步都要人。
这篇提出 AutoOPT,把整条流水线包成四个可复用的 agent skill,人只在每个决策边界上点头。
四段流水线,每段出口都停给人审批:
底层是一条关键洞察:PEP 对偶化后,「找最优算法」和「找它的收敛证明」是同一个优化问题的联合变量,所以数值解自带机器可查的证明骨架,LLM 做的是符号化拟合而非凭空推理。全程跑在一台 Apple M5 Max 笔记本上,agentic 部分用 GPT-5.5 和 GPT-5.6 Sol 的 200 美元/月 ChatGPT Pro 订阅,没有内部模型。
两个新算法,主定理均经 Lean 机器检查:
| 成果 | 指标 | 结果 |
| LemniAcc(光滑凸函数上压梯度范数) | 平方梯度范数率 | ≤ϖ⁴L²‖x₀−x⋆‖²/(N+1)⁴,常数 ϖ⁴≈47.27 |
| 对照:前最优(OGM 接 OGM-G 两段拼接) | 同指标 | 常数 64,LemniAcc 好约 1.35 倍 |
| ITEM-f(强凸函数上压函数值) | 单步收缩因子 | (1−√(μ/L))²,匹配复杂度下界渐近 |
| Lean 形式化 | 两个项目 | 共 15,369 行 Lean,公理审计仅三条标准公理 |
LemniAcc 的常数由双纽线常数 ϖ≈2.622(单位双纽线周长与直径之比)刻画,双纽线椭圆函数首次进入优化理论;连续时间极限是一个带时变摩擦的二阶 ODE,两端渐近行为分别贴着 OGM 和 OGM-G 的连续极限。ITEM-f 此前只有 N≤5 的数值解,这次拿到对任意 N、μ、L 成立的闭式。两个方法还都是自 H-对偶的:各自是其自身的反步长对偶。
对做优化的人,两个结果本身可用:LemniAcc 是单序列系数、无需中途切换算法的梯度范数最优法;ITEM-f 补上了强凸情形函数值收缩的闭式解。对更广的 AI 从业者,这篇是「领域专家怎么在 LLM 时代做研究」的一份具体答卷:不追求全自动 Scientist,而是把十年积累的 PEP 方法论蒸馏成 skill,让前沿模型的数学能力有落点。学术级算力(一台笔记本加订阅制 API)跑出了带 Lean 证书的新定理,这个性价比此前只有工业界的 AlphaEvolve、Aletheia 这类大预算系统才提过。
作者自认不覆盖随机优化和二阶方法。更实际的边界有三条。其一,自动化的只是「数值解到定理」这条已经高度机械化的路径,选题、猜想哪个函数类值得做、判断结果重不重要,仍然全在人手里,而后者恰恰是研究里最难的部分。其二,两个案例都落在 PEP 最成熟的固定步长一阶法这个舒适区,泛化到插值条件未知的问题类时 skill 的「领域专业知识」是否够用,论文没有给出第三个案例。其三,「八小时高强度原生推理」这类长程 LLM 环节的可复现性,论文只说证据链存档,没有第三方复跑。