The AutoLyap software suite for computer-assisted Lyapunov analyses of first-order methods

TL;DR

The core idea behind AutoLyap is to recast the verification of the existence of a Lyapunov analysis as a semidefinite program (SDP), which can then be solved numerically using standard SDP solvers.

Abstract

We introduce AutoLyap, a software suite that assists with Lyapunov analyses of a wide class of first-order methods for structured optimization and inclusion problems. Lyapunov analyses are structured proof patterns, with historical roots in the study of dynamical systems, commonly used to establish convergence results for first-order methods. Building on previous work, the core idea behind AutoLyap is to recast the verification of the existence of a Lyapunov analysis as a semidefinite program (SDP), which can then be solved numerically using standard SDP solvers. Users of the package specify (i) the class of optimization or inclusion problems, (ii) the first-order method in question, and (iii) the type of Lyapunov analysis they wish to test. Once these inputs are provided, AutoLyap handles the SDP modeling and proceeds to solve the SDP numerically. We use the package to numerically verify and extend several convergence results. AutoLyap is currently available in Python and Julia.

Figures (3)

• Figure 1: Smallest $\rho$ certifiable via AutoLyap in \ref{['eq:chambolle_pock:linear']} for the Chambolle--Pock method \ref{['eq:chambolle_pock_interface:standard']}, where $f_{1},f_{2}:\mathcal{H}\to\mathbb{R}$ are $L$-smooth and $\mu$-strongly convex with $(\mu,L)=(0.05,50)$. In the plot, we restrict to points such that $\tau=\sigma \geq 1$.
• Figure 2: Verification, via AutoLyap, of summability of the squared fixed-point residual $\mathord{( \lVert\bm{x}^{k+1} - \bm{x}^{k}\rVert^{2} )}_{k\in\mathbb{N}_0}$ for the Chambolle--Pock method \ref{['eq:chambolle_pock_interface:standard']}, which is modeled by \ref{['eq:chambolle_pock_interface:state_space']}. Here, $f_1,f_2:\mathcal{H}\to\mathbb{R}\cup\mathord{\left.\{ \pm\infty \} \right. }$ are assumed to be proper, lower semicontinuous, and convex. In the plot, we restrict to points such that $\tau=\sigma \geq 1$, and we use a few different values of the history parameter $h$ and the overlap parameter $\alpha$.
• Figure 3: Constants $c_{K}$ in \ref{['eq:nesterov_fast_iteration_dependent_bound']} for Nesterov's fast gradient method \ref{['eq:nesterov_fast_interface:standard_form']} with step size $\gamma=1$, applied to a convex and $L$-smooth function $f_{1}:\mathcal{H}\to\mathbb{R}$ with $L=1$. Values are obtained with AutoLyap and compared with the classical rates in nesterov1983fast.

Theorems & Definitions (7)

• Definition 1
• Definition 2
• Definition 3
• Definition 4
• Definition 5
• Definition 6
• Remark 1