Certifying Lyapunov Stability of Black-Box Nonlinear Systems via Counterexample Guided Synthesis (Extended Version)
Chiao Hsieh, Masaki Waga, Kohei Suenaga
TL;DR
This work tackles the problem of certifying Lyapunov stability for black-box nonlinear systems without access to explicit dynamics. It introduces a counterexample-guided inductive synthesis (CEGIS) framework that directly bounds the Lie derivative using Lipschitz constants, together with a regional verification strategy and lazy sampling to efficiently certify stability region-by-region. The method is backed by termination guarantees via Analytic Center Cutting-Plane Method (ACCPM) when formulated as a convex feasibility problem, and a practical prototype demonstrates orders-of-magnitude sample efficiency over prior data-driven approaches. The approach enables reliable stability certification for learning-enabled controllers in safety-critical contexts and suggests scalable extensions, including richer Lyapunov templates and applicability to switched/hybrid dynamics.
Abstract
Finding Lyapunov functions to certify the stability of control systems has been an important topic for verifying safety-critical systems. Most existing methods on finding Lyapunov functions require access to the dynamics of the system. Accurately describing the complete dynamics of a control system however remains highly challenging in practice. Latest trend of using learning-enabled control systems further reduces the transparency. Hence, a method for black-box systems would have much wider applications. Our work stems from the recent idea of sampling and exploiting Lipschitz continuity to approximate the unknown dynamics. Given Lipschitz constants, one can derive a non-statistical upper bounds on approximation errors; hence a strong certification on this approximation can certify the unknown dynamics. We significantly improve this idea by directly approximating the Lie derivative of Lyapunov functions instead of the dynamics. We propose a framework based on the learner-verifier architecture from Counterexample-Guided Inductive Synthesis (CEGIS). Our insight of combining regional verification conditions and counterexample-guided sampling enables a guided search for samples to prove stability region-by-region. Our CEGIS algorithm further ensures termination. Our numerical experiments suggest that it is possible to prove the stability of 2D and 3D systems with a few thousands of samples. Our visualization also reveals the regions where the stability is difficult to prove. In comparison with the existing black-box approach, our approach at the best case requires less than 0.01% of samples.