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.
Related
- A note on the convergence guarantees of RLT-based algorithms for polynomial optimization
- Monte Carlo Power Iteration Algorithms: Convergence, Analysis and Application to Reactor Criticality Calculations
- Volume of quasi-homogeneous sublevel sets: Two linear algebra deterministic algorithms with convergence rates
- Convergence of Independence Metropolis-Hastings Algorithms in High Dimensions: Iteration Lengths, Cutoff Profiles, and Diagnostic Unreliability
- Accelerated Convergence of a Second-Order Dynamical System and its Application to Splitting Algorithms for Comonotone Inclusions
BibTeX
@misc{suh2026peppy,
title = {{Peppy: An AI-Assisted Workflow for Tight Convergence Analysis of Optimization Algorithms}},
author = {Jaewook J. Suh and TaeHo Yoon and Edward Duc Hien Nguyen and Bicheng Ying and Shiqian Ma},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.35762},
eprint = {2609.35762},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.35762},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Peppy: An AI-Assisted Workflow for Tight Convergence Analysis of Optimization Algorithms
AU - Jaewook J. Suh
AU - TaeHo Yoon
AU - Edward Duc Hien Nguyen
AU - Bicheng Ying
AU - Shiqian Ma
PY - 2026
DA - 2026/09/28
PB - arXiv
DO - 10.48550/arxiv.2609.35762
UR - https://arxiv.org/abs/2609.35762
AB - 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.
ER -