Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guarantees
Learning for control of dynamical systems with formal guarantees remains a
challenging task. This paper proposes a learning framework to simultaneously
stabilize an unknown nonlinear system with a neural controller and learn a
neural Lyapunov function to certify a region of attraction (ROA) for the
closed-loop system. The algorithmic structure consists of two neural networks
and a satisfiability modulo theories (SMT) solver. The first neural network is
responsible for learning the unknown dynamics. The second neural network aims
to identify a valid Lyapunov function and a provably stabilizing nonlinear
controller. The SMT solver then verifies that the candidate Lyapunov function
indeed satisfies the Lyapunov conditions. We provide theoretical guarantees of
the proposed learning framework in terms of the closed-loop stability for the
unknown nonlinear system. We illustrate the effectiveness of the approach with
a set of numerical experiments.