Lyapunov-stable neural-network control
arXiv:2109.14152
Abstract
Deep learning has had a far reaching impact in robotics. Specifically, deep reinforcement learning algorithms have been highly effective in synthesizing neural-network controllers for a wide range of tasks. However, despite this empirical success, these controllers still lack theoretical guarantees on their performance, such as Lyapunov stability (i.e., all trajectories of the closed-loop system are guaranteed to converge to a goal state under the control policy). This is in stark contrast to traditional model-based controller design, where principled approaches (like LQR) can synthesize stable controllers with provable guarantees. To address this gap, we propose a generic method to synthesize a Lyapunov-stable neural-network controller, together with a neural-network Lyapunov function to simultaneously certify its stability. Our approach formulates the Lyapunov condition verification as a mixed-integer linear program (MIP). Our MIP verifier either certifies the Lyapunov condition, or generates counter examples that can help improve the candidate controller and the Lyapunov function. We also present an optimization program to compute an inner approximation of the region of attraction for the closed-loop system. We apply our approach to robots including an inverted pendulum, a 2D and a 3D quadrotor, and showcase that our neural-network controller outperforms a baseline LQR controller. The code is open sourced at \url{https://github.com/StanfordASL/neural-network-lyapunov}.
arXiv commentPublished at Robotics: Science and Systems (RSS) in July, 2021
References in corpus (12)
- Trust Region Policy Optimization
- Learning agile and dynamic motor skills for legged robots
- QT-Opt: Scalable Deep Reinforcement Learning for Vision-Based Robotic Manipulation
- Evaluating Robustness of Neural Networks with Mixed Integer Programming
- A Unified View of Piecewise Linear Neural Network Verification
- Neural Lyapunov Control
- Formal Synthesis of Lyapunov Neural Networks
- Learning Control Lyapunov Functions from Counterexamples and Demonstrations
- The Lyapunov Neural Network: Adaptive Stability Certification for Safe Learning of Dynamical Systems
- ContactNets: Learning Discontinuous Contact Dynamics with Smooth, Implicit Representations
- Partition-based formulations for mixed-integer optimization of trained ReLU neural networks
- A Differentiable Augmented Lagrangian Method for Bilevel Nonlinear Optimization