Peppy: An AI-Assisted Workflow for Tight Convergence Analysis of Optimization Algorithms

What it claims

Peppy turns numerical Performance Estimation Problem (PEP) certificates into analytic, N-independent Lyapunov proofs of tight convergence rates for first-order methods. A coding agent does work that previously needed a human expert. The authors report it closes five published conjectures:

• Taylor et al. (2017c) Conjecture 4 for FGM (y_N) and for OGM (y_N).
• Conjecture 5 for FGM (x_N).
• The Table 1 conjectures of Taylor et al. (2017a) for FGM-rational and FISTA-rational (y_N).

They describe these as the first analytic proofs of the tight FGM bounds. As a by-product, it also produced what they say is the first Lyapunov proof of the known PGM rate h(x_N)−h(x⋆) ≤ L‖x₀−x⋆‖²/(4N).

How it works

Peppy is a set of five Markdown prompt files ("commands") run in sequence. PEPFlow is the backend for building and solving the PEPs.

1. /pep-implement: turns the algorithm description into a PEPFlow setup module.
2. /pep-full-proof: solves the PEP for a fixed N, extracts the certificates (λ, d, s), and guesses closed forms. The closed forms are optional at this stage; numerical values are enough to move on.
3. /lyap-define: defines V_k as partial sums of the weighted inequalities and squares. By construction V_k is nonincreasing.
4. /lyap-vectors: finds basis vectors that express V_k as a low-rank, summation-free quadratic form. This uses the new lyapunov_utils.py, which the authors call the most novel component, following the framework of Yoon et al. (2026).
5. /lyap-closed-form: fixes the analytic coefficients, checks V_{k+1} ≤ V_k symbolically, and drafts a LaTeX theorem and proof.

Verification reduces to SymPy checks of symbolic matrix/vector identities and positivity of the coefficients. Every block runs a numerical or symbolic check on the agent's output to catch hallucinations. State is saved to a .json file, and a Jupyter notebook summary lets the user inspect progress and step in.

Evidence

The evaluation reproduced known rates for six settings, five attempts each:

• The algorithms were OGM, BPPM, FEG, Dual-FEG, and PGM, with PGM run both with and without a supplied SOS decomposition.
• Codex with GPT-6 Astra at medium reasoning both generated and evaluated the proofs.
• Runs followed a clean-room protocol: no external material and a fixed Python environment.
• All 30 trials produced verified proofs.

Mean cost per run, summed across the five blocks:

The slowest single block was Block 5 for PGM without SOS, at 23.5 ± 4.7 min.

How to use it

The code and examples are at https://github.com/pepflow-lib/PEPFlow/tree/peppy-v1. You provide:

• the function class,
• the parameters,
• the initial condition,
• the performance metric,
• the update rule,
• an optional conjectured rate.

The input can be text or a screenshot. The paper's example prompt:

/pep-implement
Function: f is convex and L-smooth
Parameters: L, R
Initial condition: ||x_0 - x_star|| <= R, where grad f(x_star) = 0
Performance metric: f(x_N) - f(x_star)
Algorithm: Gradient descent with fixed step size 1/L
For k >= 0:
x_{k+1} = x_k - (1/L) * grad f(x_k)
Conjectured rate: unknown

To advance, run /pep-full-proof gd and so on, or simply say "proceed with the next step". An auxiliary skill, \lean-from-ipynb, is provided if you want Lean formalization on top of the SymPy notebooks.

Limits

• The verification is symbolic checking in SymPy, not a formal proof. Lean formalization is optional and left to the user.
• The paper says outputs come "with varying degrees of human guidance". The fetched text cuts off before the open-problem case studies, so how much guidance the FGM, OGM, and FISTA results needed is not shown here.
• The 30-trial evaluation covers only algorithms whose tight rates were already known, and it uses a single model and agent harness (Codex with GPT-6 Astra).
• Three trials (one each for BPPM, FEG, and PGM without SOS) broke the clean-room rules by using Python/Jupyter dependencies outside the designated environment. This happened in Block 5, after correct proofs had already been generated. The authors report no prohibited mathematical exposure.
• Scope is limited to first-order methods that PEP can model in PEPFlow.