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

TL;DR

AutoLyap is a software suite that automates Lyapunov analysis for first-order optimization methods by formulating the problem as a semidefinite program, enabling numerical verification and extension of convergence results.

Contribution

The paper introduces AutoLyap, a novel software tool that automates Lyapunov analyses for optimization algorithms using SDP formulations, streamlining convergence verification.

Findings

Successfully verified existing convergence results.

Extended convergence analysis to new classes of problems.

Demonstrated usability in Python and Julia environments.

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.