# Two-Stage Learning of Stabilizing Neural Controllers via Zubov Sampling and Iterative Domain Expansion

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 37 of its 61 references that are in the map.
- First posted on arXiv 2 Jun 2025.

## Builds on (most cited first, 30 of 37)

- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Multi-Task Learning Using Uncertainty to Weigh Losses for Scene Geometry and Semantics](https://mlsanity.com/paper/1705.07115/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Control Barrier Function Based Quadratic Programs for Safety Critical Systems](https://mlsanity.com/paper/1609.06408/) (2016)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods](https://mlsanity.com/paper/2202.11762/) (2022)
- [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [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)
- [Learning Control Barrier Functions from Expert Demonstrations](https://mlsanity.com/paper/2004.03315/) (2020)
- [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)
- [Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guarantees](https://mlsanity.com/paper/2206.01913/) (2022)
- [Safe Control Under Input Limits with Neural Control Barrier Functions](https://mlsanity.com/paper/2211.11056/) (2022)
- [Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation](https://mlsanity.com/paper/2404.07956/) (2024)
- [Learning Lyapunov Functions for Hybrid Systems](https://mlsanity.com/paper/2012.12015/) (2020)
- [Learning Safe, Generalizable Perception-based Hybrid Control with Certificates](https://mlsanity.com/paper/2201.00932/) (2022)
- [Neural Contraction Metrics for Robust Estimation and Control: A Convex Optimization Approach](https://mlsanity.com/paper/2006.04361/) (2020)
- [Neural Lyapunov Control for Discrete-Time Systems](https://mlsanity.com/paper/2305.06547/) (2023)
- [Formal Synthesis of Stochastic Systems via Control Barrier Certificates](https://mlsanity.com/paper/1905.04585/) (2019)
- [Control Barrier Functions for Unknown Nonlinear Systems using Gaussian Processes](https://mlsanity.com/paper/2010.05818/) (2020)
- [Physics-Informed Neural Network Lyapunov Functions: PDE Characterization, Learning, and Verification](https://mlsanity.com/paper/2312.09131/) (2023)
- [Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models](https://mlsanity.com/paper/2311.09793/) (2023)
- [Convex synthesis and verification of control-Lyapunov and barrier functions with input constraints](https://mlsanity.com/paper/2210.00629/) (2022)
- [LyZNet: A Lightweight Python Tool for Learning and Verifying Neural Lyapunov Functions and Regions of Attraction](https://mlsanity.com/paper/2403.10013/) (2024)
- [Actor-Critic Physics-informed Neural Lyapunov Control](https://mlsanity.com/paper/2403.08448/) (2024)

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

- [Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification](https://mlsanity.com/paper/2512.11087/) (2025)
- [TorchLean: Formalizing Neural Networks in Lean](https://mlsanity.com/paper/2602.22631/) (2026)
- [Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllers](https://mlsanity.com/paper/2605.25346/) (2026)
- [The FABRIC Strategy for Verifying Neural Feedback Systems](https://mlsanity.com/paper/2603.08964/) (2026)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Learning Aligned Stability in Neural ODEs Reconciling Accuracy with Robustness](https://mlsanity.com/paper/2509.21879/) (2025)

## Abstract (arXiv)

Learning-based neural network (NN) control policies have shown impressive empirical performance. However, obtaining stability guarantees and estimates of the region of attraction of these learned neural controllers is challenging due to the lack of stable and scalable training and verification algorithms. Although previous works in this area have achieved great success, much conservatism remains in their frameworks. In this work, we propose a novel two-stage training framework to jointly synthesize a controller and a Lyapunov function for continuous-time systems. By leveraging a Zubov-inspired region of attraction characterization to directly estimate stability boundaries, we propose a novel training-data sampling strategy and a domain-updating mechanism that significantly reduces the conservatism in training. Moreover, unlike existing works on continuous-time systems that rely on an SMT solver to formally verify the Lyapunov condition, we extend state-of-the-art neural network verifier α,!β-CROWN with the capability of performing automatic bound propagation through the Jacobian of dynamical systems and a novel verification scheme that avoids expensive bisection. To demonstrate the effectiveness of our approach, we conduct numerical experiments by synthesizing and verifying controllers on several challenging nonlinear systems across multiple dimensions. We show that our training can yield region of attractions with volume 5 - 1.5· 105 times larger compared to the baselines, and our verification on continuous systems can be up to 40-10,000 times faster compared to the traditional SMT solver dReal. Our code is available at https://github.com/Verified-Intelligence/Two-StageNeuralControllerTraining.