AutoLyap

A Python package for automated Lyapunov-based convergence analyses of first-order optimization and inclusion methods.

Overview

AutoLyap streamlines the process of constructing and verifying Lyapunov analyses by formulating them as semidefinite programs (SDPs). It supports a broad class of structured optimization and inclusion problems, providing computer-assisted proofs of linear or sublinear convergence rates for many well‑known algorithms.

A typical workflow:

Choose the class of optimization/inclusion problems.
Choose the first-order method to analyze.
Choose the type of Lyapunov analysis to search for or verify (which implies a convergence or performance conclusion).

AutoLyap builds the underlying SDP and solves it through configurable backend solvers.

Quick start

For installation instructions and first end-to-end workflows, see Quick start.

Cite this project

If AutoLyap contributes to your research or software, please cite [UDGT+26].

@misc{upadhyaya2026autolyap,
  author = {Upadhyaya, Manu and Das Gupta, Shuvomoy and Taylor, Adrien B. and Banert, Sebastian and Giselsson, Pontus},
  title = {The {AutoLyap} software suite for computer-assisted {L}yapunov analyses of first-order methods},
  year = {2026},
  archivePrefix = {arXiv},
  eprint = {2506.24076},
  primaryClass = {math.OC},
}

[UDGT+26]

Manu Upadhyaya, Shuvomoy Das Gupta, Adrien B. Taylor, Sebastian Banert, and Pontus Giselsson. The AutoLyap software suite for computer-assisted Lyapunov analyses of first-order methods. 2026. arXiv:2506.24076.

Other computer-assisted methodologies

PEPit is a computer-assisted performance estimation framework that targets worst-case analyses of first-order methods through SDP formulations. AutoLyap is complementary: it focuses on Lyapunov analyses and automates the corresponding SDP formulations. In practice, PEPit is a strong choice for tight bounds, while AutoLyap is tailored to Lyapunov-based proofs and scalable analysis patterns.