Research map / Probabilistic and scientific modeling / Dynamical systems
Two‑Stage Learning of Stabilizing Neural Controllers via Zubov Sampling and Iterative Domain Expansion
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes a two-stage Zubov-inspired training pipeline (sampling near/outside the estimated ROA with dynamic domain expansion, then CEGIS refinement) for neural controllers and Lyapunov functions in continuous time, plus an extended α,β-CROWN verifier that bounds Jacobian operators and adjusts level sets without bisection.
Problem
Learning neural controllers with certified stability and large estimated regions of attraction for continuous-time nonlinear systems is conservative and hard to verify, since Lyapunov conditions must hold over a continuous domain and existing continuous-time verifiers (dReal, SMT) scale poorly.
Approach
Uses the Zubov PDE characterization of the true ROA to guide sampling (balanced points inside and outside the current sublevel set), dynamically expands the training domain using converging trajectories, then refines with CEGIS; verification extends α,β-CROWN to Jacobian operators (tanh, sigmoid relaxations) and adaptively shrinks level-set thresholds c1, c2 within one branch-and-bound run instead
Key results
- ROA volume on Cartpole is about 306.1 vs. 0.9266 for the best baseline (Shi et al.), roughly 330x larger as stated in the text.
- Verification with α,β-CROWN is 40–10,000x faster than dReal on 2D systems (e.g., Van der Pol 3.94 s vs 39265 s); dReal fails on Cartpole.
- Achieves 100% success on all systems, and ROA volume on 2D Quadrotor of (6.64±4.67)·10^6 and 3D Quadrotor of (1.17±0.64)·10^9 is validated by trajectory evaluation (no formal verification for the 12D system).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use the full two-stage pipeline instead of the strongest listed baseline | Cartpole · Cartpole | ROA: 0.9266 -> 306.1±54.2 | Helped |
| Use the full two-stage pipeline instead of the strongest listed baseline | 2D Quadrotor · 2D Quadrotor | ROA: 44.53±18.38 -> (6.64±4.67)·10^6 | Helped |
| Use the full two-stage pipeline instead of the strongest listed baseline | PVTOL · PVTOL | ROA: 49.87±3.91 -> (1.91±0.23)·10^4 | Helped |
| Use the full two-stage pipeline instead of the strongest listed baseline | Van-der-Pol · Van-der-Pol | ROA: 20.2±18.3 -> 57.6±3.4 | Helped |
| Use the full two-stage pipeline instead of the strongest listed baseline | Pendulum small torque · Pendulum S | ROA: 306.3±48.7 -> 1169.2±124.5 | Helped |
| Add Zubov-guided sampling to two-stage training with domain expansion (ablation) | Cartpole · Cartpole | Formal success rate: 0 -> 100% | Helped |
| Add Zubov-guided sampling to two-stage training with domain expansion (ablation) | 2-D Quadrotor · 2-D Quadrotor | Empirical-PGD success rate: 0 -> 100% | Helped |
| Add CEGIS refinement after ROA-estimation pretraining (ablation) | Cartpole · Cartpole | Formal success rate: 0 -> 100% | Helped |
| Add CEGIS refinement after ROA-estimation pretraining (ablation) | 2-D Quadrotor · 2-D Quadrotor | Empirical-PGD success rate: 0 -> 100% | Helped |
| Add ROA-estimation pretraining before CEGIS (ablation) | Cartpole · Cartpole | Trajectory success rate: 0 -> 100% | Helped |
| Add ROA-estimation pretraining before CEGIS (ablation) | 2-D Quadrotor · 2-D Quadrotor | Trajectory success rate: 0 -> 100% | Helped |
| Use α,β-CROWN instead of dReal for formal verification | Van-der-Pol · Formal verification benchmark | verification time: 39265.21 s -> 3.94 s | Helped |
Surprising findings
- Baseline checkpoints from Wang et al. did not satisfy the equilibrium condition u(x*)=u*, and Fossil 2.0 returned false positives in some cases.
- Without the ROA-estimation stage, CEGIS-only and random-sampling training yielded zero verifiable or empirically passing controllers.
Limitations
- Formal verification does not scale well to higher-dimensional systems; the 12D quadrotor and six-dimensional systems rely on PGD or trajectory-based empirical evaluation.
- CEGIS in high dimensions does not fully eliminate counterexamples.
- Several hyperparameters (loss weights, c, domain initialization) still require tuning.
Experimental setup
Datasets: simulated trajectories from continuous-time control benchmarks
Benchmarks: Van der Pol Double Integrator Inverted Pendulum Path Tracking Cartpole PVTOL 2D Quadrotor Ducted Fan 3D Quadrotor
Metrics: ROA volume training success rate verification time
Baselines: Fossil 2.0 DITL Yang et al. Shi et al. dReal
Builds on: Zubov theorem CEGIS α,β-CROWN Neural Lyapunov Control auto_LiRPA
Closest papers by meaning
- Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation (ICML 2024 · similarity 0.91)
- FESSNC: Fast Exponentially Stable and Safe Neural Controller (ICML 2024 · similarity 0.88)
- Verified Safe Reinforcement Learning for Neural Network Dynamic Models (NeurIPS 2024 · similarity 0.86)
- Certifying Stability of Reinforcement Learning Policies using Generalized Lyapunov Functions (NeurIPS 2025 · similarity 0.86)
- Analytical Lyapunov Function Discovery: An RL-based Generative Approach (ICML 2025 · similarity 0.86)
- Physics-Informed Neural Network Policy Iteration: Algorithms, Convergence, and Verification (ICML 2024 · similarity 0.86)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.