Learning-based neural network (NN) control policies have shown impressive
empirical 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 to
obtain, and most existing approaches rely on expensive solvers such as
sums-of-squares (SOS), mixed-integer programming (MIP), or satisfiability
modulo theories (SMT). In this paper, we demonstrate a new framework for
learning NN controllers together with Lyapunov certificates using fast
empirical falsification and strategic regularizations. We propose a novel
formulation that defines a larger verifiable region-of-attraction (ROA) than
shown in the literature, and refines the conventional restrictive constraints
on Lyapunov derivatives to focus only on certifiable ROAs. The Lyapunov
condition is rigorously verified post-hoc using branch-and-bound with scalable
linear bound propagation-based NN verification techniques. The approach is
efficient and flexible, and the full training and verification procedure is
accelerated on GPUs without relying on expensive solvers for SOS, MIP, nor SMT.
The flexibility and efficiency of our framework allow us to demonstrate
Lyapunov-stable output feedback control with synthesized NN-based controllers
and NN-based observers with formal stability guarantees, for the first time in
literature. Source code at
this https URL

学习型神经网络控制策略在机器人学和控制领域的广泛任务中显示出令人印象深刻的实证性能，然而，对于具有非线性动力系统的神经网络控制器而言，关于吸引域（ROA）内的 Lyapunov 稳定性保证是具有挑战性的，并且现有的大多数方法都依赖于昂贵的求解器，例如 SOS、MIP 或 SMT。本文提出了一种新的框架，利用快速经验性推翻和战略正则化来学习具有 Lyapunov 证明的 NN 控制器。