# On the Trade-off Between Efficiency and Precision of Neural Abstraction

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 10 of its 60 references that are in the map.
- First posted on arXiv 28 Jul 2023.

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

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Neural Ordinary Differential Equations](https://mlsanity.com/paper/1806.07366/) (2018)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [On The Verification of Neural ODEs with Stochastic Guarantees](https://mlsanity.com/paper/2012.08863/) (2020)
- [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)
- [Neural Abstractions](https://mlsanity.com/paper/2301.11683/) (2023)
- [Reachability of Black-Box Nonlinear Systems after Koopman Operator Linearization](https://mlsanity.com/paper/2105.00886/) (2021)

## Abstract (arXiv)

Neural abstractions have been recently introduced as formal approximations of complex, nonlinear dynamical models. They comprise a neural ODE and a certified upper bound on the error between the abstract neural network and the concrete dynamical model. So far neural abstractions have exclusively been obtained as neural networks consisting entirely of ReLU activation functions, resulting in neural ODE models that have piecewise affine dynamics, and which can be equivalently interpreted as linear hybrid automata. In this work, we observe that the utility of an abstraction depends on its use: some scenarios might require coarse abstractions that are easier to analyse, whereas others might require more complex, refined abstractions. We therefore consider neural abstractions of alternative shapes, namely either piecewise constant or nonlinear non-polynomial (specifically, obtained via sigmoidal activations). We employ formal inductive synthesis procedures to generate neural abstractions that result in dynamical models with these semantics. Empirically, we demonstrate the trade-off that these different neural abstraction templates have vis-a-vis their precision and synthesis time, as well as the time required for their safety verification (done via reachability computation). We improve existing synthesis techniques to enable abstraction of higher-dimensional models, and additionally discuss the abstraction of complex neural ODEs to improve the efficiency of reachability analysis for these models.