# Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation

arXiv: https://arxiv.org/abs/2404.07956 · HTML: https://mlsanity.com/paper/2404.07956/

## Key facts

- Cited by 25 papers in the map (data through 14 Oct 2026).
- Builds on 29 of its 49 references that are in the map.
- First posted on arXiv 11 Apr 2024.

## Builds on (most cited first, 29 of 29)

- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [QT-Opt: Scalable Deep Reinforcement Learning for Vision-Based Robotic Manipulation](https://mlsanity.com/paper/1806.10293/) (2018)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functions](https://mlsanity.com/paper/2109.06697/) (2021)
- [Lyapunov-stable neural-network control](https://mlsanity.com/paper/2109.14152/) (2021)
- [Learning Certified Control using Contraction Metric](https://mlsanity.com/paper/2011.12569/) (2020)
- [Stability Analysis using Quadratic Constraints for Systems with Neural Network Controllers](https://mlsanity.com/paper/2006.07579/) (2020)
- [Learning Deep Control Policies for Autonomous Aerial Vehicles with MPC-Guided Policy Search](https://mlsanity.com/paper/1509.06791/) (2015)
- [Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2108.04140/) (2021)
- [Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guarantees](https://mlsanity.com/paper/2206.01913/) (2022)
- [Neural Certificates for Safe Control Policies](https://mlsanity.com/paper/2006.08465/) (2020)
- [Safe Control Under Input Limits with Neural Control Barrier Functions](https://mlsanity.com/paper/2211.11056/) (2022)
- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [Learning Lyapunov Functions for Hybrid Systems](https://mlsanity.com/paper/2012.12015/) (2020)
- [Neural Lyapunov Control for Discrete-Time Systems](https://mlsanity.com/paper/2305.06547/) (2023)
- [Safety Certification for Stochastic Systems via Neural Barrier Functions](https://mlsanity.com/paper/2206.01463/) (2022)
- [IBP Regularization for Verified Adversarial Robustness via Branch-and-Bound](https://mlsanity.com/paper/2206.14772/) (2022)
- [Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems](https://mlsanity.com/paper/2209.14076/) (2022)
- [Convex synthesis and verification of control-Lyapunov and barrier functions with input constraints](https://mlsanity.com/paper/2210.00629/) (2022)
- [Joint Differentiable Optimization and Verification for Certified Reinforcement Learning](https://mlsanity.com/paper/2201.12243/) (2022)
- [Reachable Polyhedral Marching (RPM): An Exact Analysis Tool for Deep-Learned Control Systems](https://mlsanity.com/paper/2210.08339/) (2022)
- [DRIP: Domain Refinement Iteration with Polytopes for Backward Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2212.04646/) (2022)
- [A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis](https://mlsanity.com/paper/2309.06090/) (2023)
- [Counter-Example Guided Synthesis of Control Lyapunov Functions for Switched Systems](https://mlsanity.com/paper/1509.03688/) (2015)
- [Approximate Optimal Controller Synthesis for Cart-Poles and Quadrotors via Sums-of-Squares](https://mlsanity.com/paper/2304.12533/) (2023)

## Built on by (most cited first, 25 of 25)

- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation](https://mlsanity.com/paper/2410.16281/) (2024)
- [Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification](https://mlsanity.com/paper/2512.11087/) (2025)
- [Two-Stage Learning of Stabilizing Neural Controllers via Zubov Sampling and Iterative Domain Expansion](https://mlsanity.com/paper/2506.01356/) (2025)
- [SoundnessBench: A Soundness Benchmark for Neural Network Verifiers](https://mlsanity.com/paper/2412.03154/) (2024)
- [Neural Contraction Metrics with Formal Guarantees for Discrete-Time Nonlinear Dynamical Systems](https://mlsanity.com/paper/2504.17102/) (2025)
- [Formally Verified Physics-Informed Neural Control Lyapunov Functions](https://mlsanity.com/paper/2409.20528/) (2024)
- [Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control](https://mlsanity.com/paper/2411.18235/) (2024)
- [Provably-Safe Neural Network Training Using Hybrid Zonotope Reachability Analysis](https://mlsanity.com/paper/2501.13023/) (2025)
- [Safe Domains of Attraction for Discrete-Time Nonlinear Systems: Characterization and Verifiable Neural Network Estimation](https://mlsanity.com/paper/2506.13961/) (2025)
- [Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllers](https://mlsanity.com/paper/2605.25346/) (2026)
- [Combining Neural Networks and Symbolic Regression for Analytical Lyapunov Function Discovery](https://mlsanity.com/paper/2406.15675/) (2024)
- [Kernel-Based Optimal Control: An Infinitesimal Generator Approach](https://mlsanity.com/paper/2412.01591/) (2024)
- [Analytical Lyapunov Function Discovery: An RL-based Generative Approach](https://mlsanity.com/paper/2502.02014/) (2025)
- [Neural Lyapunov Function Approximation with Self-Supervised Reinforcement Learning](https://mlsanity.com/paper/2503.15629/) (2025)
- [Learning Verifiable Control Policies Using Relaxed Verification](https://mlsanity.com/paper/2504.16879/) (2025)
- [Certifying Stability of Reinforcement Learning Policies using Generalized Lyapunov Functions](https://mlsanity.com/paper/2505.10947/) (2025)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Autonomous Wheel Loader Navigation Using Goal-Conditioned Actor-Critic MPC](https://mlsanity.com/paper/2409.15717/) (2024)
- [Verifying Closed-Loop Contractivity of Learning-Based Controllers via Partitioning](https://mlsanity.com/paper/2512.02262/) (2025)
- [Learned Lyapunov Shielding for Adaptive Control](https://mlsanity.com/paper/2605.06934/) (2026)
- [Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations](https://mlsanity.com/paper/2605.07757/) (2026)
- [A Survey on the Verification of Reinforcement Learning Policies](https://mlsanity.com/paper/2607.16210/) (2026)
- [Learning Provable Neural Network Observer for Uncertain Dynamical Systems](https://mlsanity.com/paper/2609.30819/) (2026)
- [Toward AI Trustworthiness: Finding Analytically Proven Forward-Invariant Sets for AI-Controlled Systems](https://mlsanity.com/paper/2610.05689/) (2026)

## Abstract (arXiv)

Learning-based neural network (NN) control policies have shown impressive empirical performance in a wide range of tasks in robotics and control. However, formal (Lyapunov) stability guarantees over the region-of-attraction (ROA) for NN controllers with nonlinear dynamical systems are challenging to obtain, and most existing approaches rely on expensive solvers such as sums-of-squares (SOS), mixed-integer programming (MIP), or satisfiability modulo theories (SMT). In this paper, we demonstrate a new framework for learning NN controllers together with Lyapunov certificates using fast empirical falsification and strategic regularizations. We propose a novel formulation that defines a larger verifiable region-of-attraction (ROA) than shown in the literature, and refines the conventional restrictive constraints on Lyapunov derivatives to focus only on certifiable ROAs. The Lyapunov condition is rigorously verified post-hoc using branch-and-bound with scalable linear bound propagation-based NN verification techniques. The approach is efficient and flexible, and the full training and verification procedure is accelerated on GPUs without relying on expensive solvers for SOS, MIP, nor SMT. The flexibility and efficiency of our framework allow us to demonstrate Lyapunov-stable output feedback control with synthesized NN-based controllers and NN-based observers with formal stability guarantees, for the first time in literature. Source code at https://github.com/Verified-Intelligence/Lyapunov_Stable_NN_Controllers