# DeepAbstract: Neural Network Abstraction for Accelerating Verification

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

## Key facts

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

## Built on by (most cited first, 30 of 31)

- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)
- [Pruning and Slicing Neural Networks using Formal Verification](https://mlsanity.com/paper/2105.13649/) (2021)
- [Verification-Aided Deep Ensemble Selection](https://mlsanity.com/paper/2202.03898/) (2022)
- [BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks](https://mlsanity.com/paper/2103.07224/) (2021)
- [Minimal Multi-Layer Modifications of Deep Neural Networks](https://mlsanity.com/paper/2110.09929/) (2021)
- [Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning](https://mlsanity.com/paper/2101.10102/) (2021)
- [QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks](https://mlsanity.com/paper/2212.11138/) (2022)
- [Distributionally Robust Statistical Verification with Imprecise Neural Networks](https://mlsanity.com/paper/2308.14815/) (2023)
- [Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks](https://mlsanity.com/paper/2207.00759/) (2022)
- [Verifying Generalization in Deep Learning](https://mlsanity.com/paper/2302.05745/) (2023)
- [Shared Certificates for Neural Network Verification](https://mlsanity.com/paper/2109.00542/) (2021)
- [On Neural Network Equivalence Checking using SMT Solvers](https://mlsanity.com/paper/2203.11629/) (2022)
- [QEBVerif: Quantization Error Bound Verification of Neural Networks](https://mlsanity.com/paper/2212.02781/) (2022)
- [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)
- [On Optimizing Back-Substitution Methods for Neural Network Verification](https://mlsanity.com/paper/2208.07669/) (2022)
- [Fully Automatic Neural Network Reduction for Formal Verification](https://mlsanity.com/paper/2305.01932/) (2023)
- [DeepCDCL: An CDCL-based Neural Network Verification Framework](https://mlsanity.com/paper/2403.07956/) (2024)
- [Abstraction-Based Proof Production in Formal Verification of Neural Networks](https://mlsanity.com/paper/2506.09455/) (2025)
- [DelBugV: Delta-Debugging Neural Network Verifiers](https://mlsanity.com/paper/2305.18558/) (2023)
- [Bridging the Gap between Artificial Intelligence and Artificial General Intelligence: A Ten Commandment Framework for Human-Like Intelligence](https://mlsanity.com/paper/2210.09366/) (2022)
- [Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks](https://mlsanity.com/paper/2302.06455/) (2023)
- [Verification of Bit-Flip Attacks against Quantized Neural Networks](https://mlsanity.com/paper/2502.16286/) (2025)
- [Mini-Batch Robustness Verification of Deep Neural Networks](https://mlsanity.com/paper/2508.15454/) (2025)
- [Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits](https://mlsanity.com/paper/2512.20755/) (2025)
- [Scaling Model Checking for DNN Analysis via State-Space Reduction and Input Segmentation (Extended Version)](https://mlsanity.com/paper/2306.17323/) (2023)
- [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)
- [AGNES: Abstraction-guided Framework for Deep Neural Networks Security](https://mlsanity.com/paper/2311.04009/) (2023)
- [Patch Synthesis for Property Repair of Deep Neural Networks](https://mlsanity.com/paper/2404.01642/) (2024)

## Abstract (arXiv)

While abstraction is a classic tool of verification to scale it up, it is not used very often for verifying neural networks. However, it can help with the still open task of scaling existing algorithms to state-of-the-art network architectures. We introduce an abstraction framework applicable to fully-connected feed-forward neural networks based on clustering of neurons that behave similarly on some inputs. For the particular case of ReLU, we additionally provide error bounds incurred by the abstraction. We show how the abstraction reduces the size of the network, while preserving its accuracy, and how verification results on the abstract network can be transferred back to the original network.