# Neural Abstractions

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

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- Builds on 22 of its 127 references that are in the map.
- First posted on arXiv 27 Jan 2023.

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

- [Neural Ordinary Differential Equations](https://mlsanity.com/paper/1806.07366/) (2018)
- [The Expressive Power of Neural Networks: A View from the Width](https://mlsanity.com/paper/1709.02540/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (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)
- [Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guarantees](https://mlsanity.com/paper/2206.01913/) (2022)
- [JuliaReach: a Toolbox for Set-Based Reachability](https://mlsanity.com/paper/1901.10736/) (2019)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [Stability Verification in Stochastic Control Systems via Neural Network Supermartingales](https://mlsanity.com/paper/2112.09495/) (2021)
- [On The Verification of Neural ODEs with Stochastic Guarantees](https://mlsanity.com/paper/2012.08863/) (2020)
- [Learning Lyapunov Functions for Hybrid Systems](https://mlsanity.com/paper/2012.12015/) (2020)
- [Learning Control Lyapunov Functions from Counterexamples and Demonstrations](https://mlsanity.com/paper/1804.05285/) (2018)
- [Learning Safe Neural Network Controllers with Barrier Certificates](https://mlsanity.com/paper/2009.09826/) (2020)
- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)
- [Reachable Set Estimation and Safety Verification for Piecewise Linear Systems with Neural Network Controllers](https://mlsanity.com/paper/1802.06981/) (2018)
- [Reachability Analysis of a General Class of Neural Ordinary Differential Equations](https://mlsanity.com/paper/2207.06531/) (2022)
- [GoTube: Scalable Stochastic Verification of Continuous-Depth Models](https://mlsanity.com/paper/2107.08467/) (2021)
- [Sapo: Reachability Computation and Parameter Synthesis of Polynomial Dynamical Systems](https://mlsanity.com/paper/1607.02200/) (2016)
- [Automatic Dynamic Parallelotope Bundles for Reachability Analysis of Nonlinear Systems](https://mlsanity.com/paper/2105.11796/) (2021)

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

- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis](https://mlsanity.com/paper/2309.06090/) (2023)
- [Bisimulation Learning](https://mlsanity.com/paper/2405.15723/) (2024)
- [Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification](https://mlsanity.com/paper/2407.21029/) (2024)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Certified Neural Approximations of Nonlinear Dynamics](https://mlsanity.com/paper/2505.15497/) (2025)
- [On the Trade-off Between Efficiency and Precision of Neural Abstraction](https://mlsanity.com/paper/2307.15546/) (2023)
- [Correct-by-Construction Control for Stochastic and Uncertain Dynamical Models via Formal Abstractions](https://mlsanity.com/paper/2311.09786/) (2023)
- [Transfer Learning for Control Systems via Neural Simulation Relations](https://mlsanity.com/paper/2412.01783/) (2024)
- [Neural Proofs for Sound Verification and Control of Complex Systems](https://mlsanity.com/paper/2512.18389/) (2025)
- [Safety Certification is Classification](https://mlsanity.com/paper/2605.06087/) (2026)

## Abstract (arXiv)

We present a novel method for the safety verification of nonlinear dynamical models that uses neural networks to represent abstractions of their dynamics. Neural networks have extensively been used before as approximators; in this work, we make a step further and use them for the first time as abstractions. For a given dynamical model, our method synthesises a neural network that overapproximates its dynamics by ensuring an arbitrarily tight, formally certified bound on the approximation error. For this purpose, we employ a counterexample-guided inductive synthesis procedure. We show that this produces a neural ODE with non-deterministic disturbances that constitutes a formal abstraction of the concrete model under analysis. This guarantees a fundamental property: if the abstract model is safe, i.e., free from any initialised trajectory that reaches an undesirable state, then the concrete model is also safe. By using neural ODEs with ReLU activation functions as abstractions, we cast the safety verification problem for nonlinear dynamical models into that of hybrid automata with affine dynamics, which we verify using SpaceEx. We demonstrate that our approach performs comparably to the mature tool Flow* on existing benchmark nonlinear models. We additionally demonstrate and that it is effective on models that do not exhibit local Lipschitz continuity, which are out of reach to the existing technologies.