# Abstract Neural Networks

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

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Sep 2020.

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

- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [Tighter Abstract Queries in Neural Network Verification](https://mlsanity.com/paper/2210.12871/) (2022)
- [Bisimulations for Neural Network Reduction](https://mlsanity.com/paper/2110.03726/) (2021)
- [Fully Automatic Neural Network Reduction for Formal Verification](https://mlsanity.com/paper/2305.01932/) (2023)
- [Relational DNN Verification With Cross Executional Bound Refinement](https://mlsanity.com/paper/2405.10143/) (2024)
- [Expediting Neural Network Verification via Network Reduction](https://mlsanity.com/paper/2308.03330/) (2023)
- [Inferring Data Preconditions from Deep Learning Models for Trustworthy Prediction in Deployment](https://mlsanity.com/paper/2401.14628/) (2024)
- [A Domain-Theoretic Framework for Robustness Analysis of Neural Networks](https://mlsanity.com/paper/2203.00295/) (2022)
- [Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks](https://mlsanity.com/paper/2307.10891/) (2023)
- [Verification of Neural Networks Local Differential Classification Privacy](https://mlsanity.com/paper/2310.20299/) (2023)
- [Random at First, Fast at Last: NTK-Guided Fourier Pre-Processing for Tabular DL](https://mlsanity.com/paper/2506.02406/) (2025)

## Abstract (arXiv)

Deep Neural Networks (DNNs) are rapidly being applied to safety-critical domains such as drone and airplane control, motivating techniques for verifying the safety of their behavior. Unfortunately, DNN verification is NP-hard, with current algorithms slowing exponentially with the number of nodes in the DNN. This paper introduces the notion of Abstract Neural Networks (ANNs), which can be used to soundly overapproximate DNNs while using fewer nodes. An ANN is like a DNN except weight matrices are replaced by values in a given abstract domain. We present a framework parameterized by the abstract domain and activation functions used in the DNN that can be used to construct a corresponding ANN. We present necessary and sufficient conditions on the DNN activation functions for the constructed ANN to soundly over-approximate the given DNN. Prior work on DNN abstraction was restricted to the interval domain and ReLU activation function. Our framework can be instantiated with other abstract domains such as octagons and polyhedra, as well as other activation functions such as Leaky ReLU, Sigmoid, and Hyperbolic Tangent.