Formal Synthesis of Lyapunov Stability Certificates for Linear Switched Systems using ReLU Neural Networks

Debauche, Virginie [UCL] Jungers, Raphaël M. [UCL] et al.

This paper presents a neural network-based algorithm with soundness guarantees to study the stability of discrete-time linear switched systems. This algorithm is cast as a counterexample guided inductive synthesis (CEGIS) architecture: an iterative structure which alternates between the learner, which provides a candidate Lyapunov function, and the verifier which checks its validity over the whole domain. We choose a ReLU neural network as learner to take advantage of its expressivity power and flexibility, and a satisfiability module theories (SMT) solver as verifier. In addition, we introduce a post processing step to leverage a valid Lyapunov function from the neural network in case of failure of the CEGIS loop. We provide several examples to illustrate the entire algorithm.