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

Virginie Debauche, Alec Edwards, Raphael M. Jungers, Alessandro Abate
Proceedings of the International Conference on Neuro-symbolic Systems, PMLR 288:352-364, 2025.

Abstract

This paper presents a neural network-based algorithm with soundness guarantees to study the stability of discrete-time linear switched systems. This algorithm follows a counterexample guided inductive synthesis (CEGIS) architecture: an iterative process alternating 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 for its expressivity 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. Several examples demonstrate the algorithm’s efficacy.

Cite this Paper

BibTeX
@InProceedings{pmlr-v288-debauche25a, title = {Formal Synthesis of Lyapunov Stability Certificates for Linear Switched Systems using ReLU Neural Networks}, author = {Debauche, Virginie and Edwards, Alec and Jungers, Raphael M. and Abate, Alessandro}, booktitle = {Proceedings of the International Conference on Neuro-symbolic Systems}, pages = {352--364}, year = {2025}, editor = {Pappas, George and Ravikumar, Pradeep and Seshia, Sanjit A.}, volume = {288}, series = {Proceedings of Machine Learning Research}, month = {28--30 May}, publisher = {PMLR}, pdf = {https://raw.githubusercontent.com/mlresearch/v288/main/assets/debauche25a/debauche25a.pdf}, url = {https://proceedings.mlr.press/v288/debauche25a.html}, abstract = {This paper presents a neural network-based algorithm with soundness guarantees to study the stability of discrete-time linear switched systems. This algorithm follows a counterexample guided inductive synthesis (CEGIS) architecture: an iterative process alternating 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 for its expressivity 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. Several examples demonstrate the algorithm’s efficacy.} }
Endnote
%0 Conference Paper %T Formal Synthesis of Lyapunov Stability Certificates for Linear Switched Systems using ReLU Neural Networks %A Virginie Debauche %A Alec Edwards %A Raphael M. Jungers %A Alessandro Abate %B Proceedings of the International Conference on Neuro-symbolic Systems %C Proceedings of Machine Learning Research %D 2025 %E George Pappas %E Pradeep Ravikumar %E Sanjit A. Seshia %F pmlr-v288-debauche25a %I PMLR %P 352--364 %U https://proceedings.mlr.press/v288/debauche25a.html %V 288 %X This paper presents a neural network-based algorithm with soundness guarantees to study the stability of discrete-time linear switched systems. This algorithm follows a counterexample guided inductive synthesis (CEGIS) architecture: an iterative process alternating 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 for its expressivity 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. Several examples demonstrate the algorithm’s efficacy.
APA
Debauche, V., Edwards, A., Jungers, R.M. & Abate, A.. (2025). Formal Synthesis of Lyapunov Stability Certificates for Linear Switched Systems using ReLU Neural Networks. Proceedings of the International Conference on Neuro-symbolic Systems, in Proceedings of Machine Learning Research 288:352-364 Available from https://proceedings.mlr.press/v288/debauche25a.html.

Related Material