Augmented Neural Lyapunov Control
Davide Grande, Andrea Peruffo, Enrico Anderlini, Georgios Salavasidis
Abstract
Machine learning-based techniques have recently been adapted to solve control problems. The Neural Lyapunov Control (NLC) method is one such example. This approch combines Artificial Neural Networks with Satisfiability Modulo Theories (SMT) solvers to synthesise stabilising control laws and to prove their formal correctness. The formers are trained over a dataset of state-space samples to generate candidate control and Lyapunov functions, whilst the SMT solvers are tasked with certifying their correctness over a continuous domain or returning a counterexample. Despite the approach attractiveness, issues can occur due to subsequent calls of the SMT module oftentimes returning similar counterexamples, turning out to be uninformative and leading to dataset overfitting. Additionally, the control network weights are usually initialised with pre-computed gains from state-feedback controllers, e.g. Linear-Quadratic Regulators. This initialisation requires user time and control expertise. In this work, we present an <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">Augmented</i> NLC method that alleviates these drawbacks, removes the need for the control initialisation and further improves the counterexample generation. As a result, the approach allows to synthesise nonlinear (as well as linear) control laws requiring solely the knowledge of the system dynamics. The proposed method is tested over challenging benchmarks such as the Lorenz attractor, outperforming existing techniques in terms of successful synthesis rate. The developed framework is released open-source at https://released upon acceptance.