Computer-assisted proofs for Lyapunov stability via Sums of Squares certificates and Constructive Analysis
Grigory Devadze, Victor Magron, Stefan Streif
TL;DR
This work addresses certifying the stability of polynomial dynamical systems through computer-assisted proofs that combine sums-of-squares (SOS) Lyapunov certificates with constructive, formally certified verification in the Minlog proof assistant. The approach first constructs SOS Lyapunov functions via semidefinite programming and then upgrades numerical certificates to exact, rational ones using the RealCertify/intsos framework, yielding exact certificates for $V$ and $V- V\circ f$. These certificates are then embedded in a constructive framework, and Minlog is extended to formalize real numbers, vectors, and multivariate maps, enabling machine-checked stability proofs and program extraction. The paper demonstrates the workflow on a two-dimensional example and discusses scalability and possible extensions, including sparsity exploitation and alternative nonnegativity certificates, with open-source libraries provided for reproducibility and future work in certified nonlinear control.
Abstract
We provide a computer-assisted approach to ensure that a given continuous or discrete-time polynomial system is (asymptotically) stable. Our framework relies on constructive analysis together with formally certified sums of squares Lyapunov functions. The crucial steps are formalized within of the proof assistant Minlog. We illustrate our approach with various examples issued from the control system literature.