Formal Synthesis of Lyapunov Neural Networks

Abstract

We propose an automatic and formally sound method for synthesising Lyapunov functions for the asymptotic stability of autonomous non-linear systems. Traditional methods are either analytical and require manual effort or are numerical but lack of formal soundness. Symbolic computational methods for Lyapunov functions, which are in between, give formal guarantees but are typically semi-automatic because they rely on the user to provide appropriate function templates. We propose a method that finds Lyapunov functions fully automatically$-$using machine learning$-$while also providing formal guarantees$-$using satisfiability modulo theories (SMT). We employ a counterexample-guided approach where a numerical learner and a symbolic verifier interact to construct provably correct Lyapunov neural networks (LNNs). The learner trains a neural network that satisfies the Lyapunov criteria for asymptotic stability over a samples set; the verifier proves via SMT solving that the criteria are satisfied over the whole domain or augments the samples set with counterexamples. Our method supports neural networks with polynomial activation functions and multiple depth and width, which display wide learning capabilities. We demonstrate our method over several non-trivial benchmarks and compare it favourably against a numerical optimisation-based approach, a symbolic template-based approach, and a cognate LNN-based approach. Our method synthesises Lyapunov functions faster and over wider spatial domains than the alternatives, yet providing stronger or equal guarantees.

References in corpus (3)

• Neural Lyapunov Control
• Formal Synthesis of Lyapunov Neural Networks
• Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers

Cited by in corpus (21)

• Formal Synthesis of Lyapunov Neural Networks
• Neural Operators for PDE Backstepping Control of First-Order Hyperbolic PIDE with Recycle and Delay
• Physics-Informed Neural Network Lyapunov Functions: PDE Characterization, Learning, and Verification
• Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functions
• Neural Termination Analysis
• Learning Lyapunov Functions for Piecewise Affine Systems with Neural Network Controllers
• Safe Distributed Control of Multi-Robot Systems with Communication Delays
• Actor-Critic Physics-informed Neural Lyapunov Control
• Data-driven invariant set for nonlinear systems with application to command governors
• Certifying Lyapunov Stability of Black-Box Nonlinear Systems via Counterexample Guided Synthesis (Extended Version)
• Neural Lyapunov Model Predictive Control: Learning Safe Global Controllers from Sub-optimal Examples
• Lyapunov-stable neural-network control
• Certified Inductive Synthesis for Online Mixed-Integer Optimization
• Safe Feedback Motion Planning in Unknown Environments: An Instantaneous Local Control Barrier Function Approach
• Distributed Lyapunov Functions for Nonlinear Networks
• Robustly Learning Regions of Attraction from Fixed Data
• Formal controller synthesis for hybrid systems using genetic programming
• A PAC-Bayesian Framework for Optimal Control with Stability Guarantees
• Learning Lyapunov Functions for Hybrid Systems
• Safe and Stable Neural Network Dynamical Systems for Robot Motion Planning
• Learning Region of Attraction for Nonlinear Systems