This paper describes a method for turning tight, computer-assisted convergence proofs for optimization algorithms into concise, human-readable Lyapunov-style proofs. Lyapunov-style proofs show a single number that never increases through the algorithm’s steps and so give a clear quantitative convergence rate. Until now, such translations were done case by case by experts and often relied on hand-chosen templates. The authors provide a general recipe and code that automate much of that work.

The researchers give a mathematical characterization of when a convergence proof can be rewritten in Lyapunov form, and they present a concrete procedure for building the Lyapunov function when it is possible. Concretely, their implementation pairs a performance estimation problem (PEP) toolbox — a computer method that searches for worst-case convergence rates — with elementary linear algebra and symbolic verification. They package this into a single Jupyter notebook so a user can run the search and derivation on their own algorithm without needing to read the implementation details.

At a high level, PEP casts the task of finding the worst-case rate of a first-order method as a semidefinite program (SDP). The SDP’s dual solution produces algebraic certificates for the rate. Lyapunov-style proofs instead demonstrate a sequence of scalar quantities that decreases at each step. The authors’ procedure starts from the PEP-style certificate and systematically converts it, by algebraic manipulation, into an explicit Lyapunov function and a short, checkable proof that it is nonincreasing.

This work matters because Lyapunov proofs are often easier for people to read and to reuse in related analyses. By automating the conversion, the authors unify several prior Lyapunov analyses under one framework and reduce the manual effort needed to produce human-friendly proofs. Using their tool they recovered many existing results and discovered four new analytic Lyapunov-style proofs. One of those discoveries yields a new exact, minimax-optimal proximal algorithm for strongly monotone inclusion problems, labeled Dual-OC-Halpern in the paper.