Abstract
Learning-based neural network (NN) control policies have shown impressiveempirical performance in a wide range of tasks in robotics and control.However, formal (Lyapunov) stability guarantees over the region-of-attraction(ROA) for NN controllers with nonlinear dynamical systems are challenging toobtain, and most existing approaches rely on expensive solvers such assums-of-squares (SOS), mixed-integer programming (MIP), or satisfiabilitymodulo theories (SMT). In this paper, we demonstrate a new framework forlearning NN controllers together with Lyapunov certificates using fastempirical falsification and strategic regularizations. We propose a novelformulation that defines a larger verifiable region-of-attraction (ROA) thanshown in the literature, and refines the conventional restrictive constraintson Lyapunov derivatives to focus only on certifiable ROAs. The Lyapunovcondition is rigorously verified post-hoc using branch-and-bound with scalablelinear bound propagation-based NN verification techniques. The approach isefficient and flexible, and the full training and verification procedure isaccelerated on GPUs without relying on expensive solvers for SOS, MIP, nor SMT.The flexibility and efficiency of our framework allow us to demonstrateLyapunov-stable output feedback control with synthesized NN-based controllersand NN-based observers with formal stability guarantees, for the first time inliterature. Source code athttps://github.com/Verified-Intelligence/Lyapunov_Stable_NN_Controllers.