A Domain-Specific Harness for End-to-End Automation of Optimization Research
AuthorsHeechang Kim, Ernest K. Ryu, Shuvomoy Das Gupta
Resources
AutoOPT combines numerical search, LLM reasoning, and formal proof assistants to automatically discover and verify new optimization algorithms.
Key results
Leading constant in the squared-gradient guarantee for lemniscate acceleration.
Approximate improvement factor in the leading guarantee constant.
BnB-PEP horizons for which spatial branch-and-bound certified global optimality.
Public theorem declarations in the machine-checked LemniAcc formalization.
Public theorem declarations in the machine-checked ITEM-f formalization.
What the paper found
AutoOPT is a domain-specific harness for automating first-order optimization research while retaining human approval at each decision point. Its four-stage pipeline uses BnB-PEP to numerically optimize an algorithm and its convergence certificate, frontier LLMs to infer closed-form updates and Lyapunov proofs, Lean 4 to machine-check the mathematics, and humans to interpret the result. The experiments used OpenAI’s GPT-5.5 and GPT-5.6 Sol through ChatGPT Pro. The first discovery, LemniAcc, minimizes the final squared gradient norm for smooth convex functions at the optimal O(1/N^4) dependence; its leading constant is approximately 47.27, improving the previous OGM-plus-OGM-G guarantee by a factor of 1.35, and it connects optimization coefficients to the lemniscate constant, approximately 2.622. The second result is an analytic form of ITEM-f, previously available only numerically, for smooth strongly convex minimization. ITEM-f contracts function-value error with per-step factor (1 − √(µ/L))^2, matching the asymptotic lower-bound complexity. BnB-PEP globally certified the LemniAcc design for 5 horizons and found local optima for 20 additional horizons. Lean formalizations machine-checked both convergence theories: the LemniAcc project contains 10 public theorem declarations, while the ITEM-f project contains 14. The paper’s central claim is methodological: combining domain-specific numerical optimization with LLM symbolic reasoning and proof-assistant verification can automate the path from numerical algorithm discovery to reproducible, formally verified optimization theorems.
Original abstract
We present AutoOPT, a domain-specific harness for end-to-end automation of optimization research. AutoOPT organizes the discovery of optimal first-order methods into four stages: numerical design through the BnB-PEP methodology; symbolic discovery of the analytic description and a convergence proof through frontier large language models (LLMs); formal verification in the Lean 4 proof assistant; and human interpretation and write-up. We demonstrate the framework on two case studies, each of independent interest. The first, lemniscate acceleration, is a new accelerated gradient method for minimizing the gradient norm of a smooth convex function: after $N$ gradient steps it reduces the squared gradient norm at the optimal $O(1/N^{4})$ rate, with a constant governed by the lemniscate constant $\varpi$, a classical elliptic-integral constant. The second is the analytic description of ITEM-f, a method previously known only numerically: for $L$-smooth, $μ$-strongly convex minimization it contracts the function-value gap at an accelerated linear rate with a per-step factor $(1-\sqrt{μ/L})^{2}$. The convergence theorems of both case studies are formalized and machine-checked in Lean 4.
Read the original paperMore in Optimization
Browse all 36 papers →An $Ω(κ_y^8ε^{-6})$ Lower Bound for Stochastic NC-SC Bilevel Optimization with First-order Oracles
Zhihao Gu, Qilong Wu, Junchi Yang
This work proves that stochastic bilevel optimization fundamentally requires up to epsilon^{-6} oracle queries, showing existing methods are asymptotically optimal.
Hyper Algorithm Design Agent: Evolving Learnable Optimizer from Zero
Zipei Yu, Yue-Jiao Gong, Zeyuan Ma, Yuncheng Jiang, Zhiguang Cao
A pair of self-improving coding agents evolves new learnable optimization algorithms from a simple template, reducing the need for handcrafted optimizer design.
Tight Regret Bound for Online Inverse Linear Optimization via Multiscale Matrix Weights
Shinsaku Sakaue
A new multiscale matrix-weights algorithm learns hidden linear preferences online with provably optimal dimension-dependent regret.