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

Debauche, Virginie;Edwards, Alec;Jungers, Raphaël;Abate, Alessandro
(2025) 2nd International Conference on Neuro-symbolic Systems — Location: University of Pennsylvania, Philadelphia, Pennsylvania, USA (28.May.2025)

Files

paper_50.pdf
  • Open Access
  • Adobe PDF
  • 489.87 KB
Download

Details

Authors
  • Debauche, VirginieOxford University, Oxford, United Kingdom
    Author
  • Edwards, AlecAlec Edwards
    Author
  • Jungers, RaphaëlUCLouvain
    Author
  • Abate, AlessandroOxford University, Oxford, United Kingdom
    Author
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.
Affiliations

Citations

  • APA
  • Chicago
  • FWB

Debauche, V., Edwards, A., Jungers, R., & Abate, A. (2025). Formal Synthesis of Lyapunov Stability Certificates for Linear Switched Systems using ReLU Neural Networks. Published. 2nd International Conference on Neuro-symbolic Systems, University of Pennsylvania, Philadelphia, Pennsylvania, USA. https://hdl.handle.net/2078.5/267047