Abstract
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.
Abstract (translated)
基于学习的神经网络（NN）控制策略在机器人学和控制领域取得了令人印象深刻的实证性能。然而，对于具有非线性动力系统的NN控制器的区域吸引域（ROA）的正式（Lyapunov）稳定性保证是具有挑战性的，而且大多数现有方法依赖于昂贵的求解器，如求和平方（SOS）、混合整数规划（MIP）或满足模度理论（SMT）。在本文中，我们提出了一种新的方法，使用快速的经验性否定和战略正则化学习神经网络控制器与Lyapunov证书相结合。我们提出了一个定义了比文献中更大的可验证区域吸引域（ROA）的新颖公式，并改进了传统的Lyapunov导数的限制，仅关注可验证的ROA。后验Lyapunov条件通过基于分支和边界的不确定性规划与扩展线性边界传播技术进行严谨的验证。该方法具有高效和灵活的特点，而且在GPU上不需要使用昂贵的求解器（如SOS、MIP或SMT）进行求解。由于我们的框架的灵活性和效率，我们能够首次在文献中实现基于合成NN控制器和具有形式稳定性的NN观察器的外部反馈控制，具有Lyapunov稳定性。源代码位于此链接：https://www.osac.org/open-source-control-systems/。
URL
https://arxiv.org/abs/2404.07956
