arXiv · 2609.35762
Peppy: An AI-Assisted Workflow for Tight Convergence Analysis of Optimization Algorithms
Abstract
This paper presents Peppy, an AI-assisted workflow for discovering tight, analytic convergence proofs for first-order optimization algorithms. Generic approaches to using LLMs to conduct mathematical research target an unspecified, broad spectrum of problems and sometimes use the Lean 4 proof assistant for formalization. On the other hand, Peppy leverages domain-specific knowledge more heavily and is thereby capable of constructing the proofs in a more structured manner, which allow a minimal and accessible verification through SymPy. We experimentally demonstrate through examples that Peppy provides a rigorous, practical, and reproducible paradigm for AI-assisted theorem synthesis in optimization. We further highlight its capability of closing several open problems on tight convergence analysis of first-order optimization algorithms, including conjectures for Nesterov's FGM. Overall, Peppy is designed to turn the art of optimization algorithm analysis into a science.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Jaewook J. Suh, TaeHo Yoon, Edward Duc Hien Nguyen, Bicheng Ying, Shiqian Ma. 2026-09-28. Peppy: An AI-Assisted Workflow for Tight Convergence Analysis of Optimization Algorithms. https://arxiv.org/abs/2609.35762
Cite the original work for its findings. Save a collection to share your selection of sources.