AI 中文总结
提出AutoOPT工具链，将优化研究自动化分为四阶段，通过两个案例研究验证其可发现新型加速梯度方法ITEM-f的解析描述，且相关定理已在Lean 4中形式化验证。
AI 中文摘要
我们提出AutoOPT，这是一个面向优化研究端到端自动化的领域专用工具链。AutoOPT将最优一阶方法的发现过程分为四个阶段：通过BnB-PEP方法进行数值设计；利用前沿大语言模型（LLMs）对解析描述和收敛性证明进行符号发现；在Lean 4证明助手内进行形式化验证；以及人工解读与撰写。我们在两个具有独立研究价值的案例研究中演示了该框架。第一个是双纽线加速法，这是一种用于最小化光滑凸函数梯度范数的新型加速梯度方法：经过N次梯度步骤后，它以最优的O(1/N⁴)速率降低平方梯度范数，其常数由双纽线常数ϖ（一种经典椭圆积分常数）决定。第二个是ITEM-f的解析描述，该方法此前仅为数值形式：对于L-光滑、μ-强凸最小化问题，它以加速线性速率收缩函数值间隙，每步因子为(1-√(μ/L))²。两个案例研究的收敛性定理均已在Lean 4中完成形式化并经机器验证。
英文摘要
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.
Comments66 pages, 11 figures
