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
AutoOPT wraps the design-analyze-verify pipeline for optimal gradient methods into four agent skills with human approval gates. It produced LemniAcc, which cuts the optimal gradient-norm constant from 64 to 47.27, and a closed-form ITEM-f, with all main theorems machine-checked in Lean 4.
Designing a theoretically optimal gradient method used to be an all-manual pipeline: solve for the optimal stepsizes numerically with performance estimation programming (PEP), stare at the numbers until an analytic formula suggests itself, hand-derive the convergence proof, write the paper. OGM, OGM-G, and ITEM were all born this way. BnB-PEP later turned the design itself into a nonconvex QCQP that optimizes stepsizes and proof jointly, but formulating and coding it is tedious enough that only PEP specialists could use it. The bottleneck was never compute. It was that every step needed a person.
AutoOPT wraps the pipeline into four reusable agent skills, with a human approving every hand-off.
Four stages, each with a stop for human approval:
The load-bearing insight is that after dualization, the algorithm and its proof are joint variables of one optimization problem, so the numerical solution ships with a machine-checkable proof skeleton. The LLM fits symbols to it; it does not reason from nothing. Everything ran on an Apple M5 Max laptop, with the agentic parts on GPT-5.5 and GPT-5.6 Sol through a $200-per-month ChatGPT Pro subscription. No internal models.
Two new algorithms, both with Lean-machine-checked main theorems:
| Result | Metric | Value |
| LemniAcc (gradient norm, smooth convex) | squared gradient rate | ≤ϖ⁴L²‖x₀−x⋆‖²/(N+1)⁴, constant ϖ⁴≈47.27 |
| Prior best (OGM then OGM-G) | same | constant 64, so LemniAcc is 1.35x better |
| ITEM-f (function value, strongly convex) | per-step contraction | (1−√(μ/L))², matching the lower-bound asymptotics |
| Lean formalization | two projects | 15,369 lines of Lean, axiom audit clean |
The LemniAcc constant is governed by the lemniscate constant ϖ≈2.622, the perimeter-to-diameter ratio of the unit lemniscate; this is the first time lemniscate elliptic functions have appeared in optimization theory. The continuous-time limit is a second-order ODE with time-varying friction whose endpoints asymptotically match the continuous limits of OGM and OGM-G. ITEM-f was previously known only numerically for N≤5; the closed form now holds for all N, μ, and L. Both methods are additionally self-H-dual, each its own anti-diagonal transpose.
For optimization people, both results are directly usable: LemniAcc is a single-sequence method with no mid-run algorithm switch, and ITEM-f closes the closed-form gap for function-value contraction in the strongly convex setting. For the broader audience, the paper is a concrete answer to how domain experts stay useful in an AI-driven workflow: instead of a fully autonomous Scientist, distill a decade of PEP methodology into skills that give a frontier model's mathematical intelligence something to grip. Academic-scale compute, one laptop plus a subscription, produced new theorems with Lean certificates, territory previously claimed only by big-budget industry systems like AlphaEvolve and Aletheia.
The authors state it does not cover stochastic or second-order methods. Three boundaries stand out on a close read. First, what got automated is the already-mechanical path from numerical solution to theorem; picking the problem class and judging whether a result matters remain human work, and that is the hard part of research. Second, both case studies sit in the comfort zone of fixed-step first-order methods where PEP theory is most mature; whether the skill's encoded expertise survives problem classes without known interpolation conditions is untested, and no third case study appears. Third, reproducibility of the long-horizon LLM stages (the native route runs at least eight hours) rests on archived evidence trails, with no third-party rerun reported.