# An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks

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

## Key facts

- Cited by 24 papers in the map (data through 14 Oct 2026).
- Builds on 43 of its 76 references that are in the map.
- First posted on arXiv 6 Jan 2022.

## Builds on (most cited first, 30 of 43)

- [Deep Residual Learning for Image Recognition](https://mlsanity.com/paper/1512.03385/) (2015)
- [Very Deep Convolutional Networks for Large-Scale Image Recognition](https://mlsanity.com/paper/1409.1556/) (2014)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Going Deeper with Convolutions](https://mlsanity.com/paper/1409.4842/) (2014)
- [Equality of Opportunity in Supervised Learning](https://mlsanity.com/paper/1610.02413/) (2016)
- [Concrete Problems in AI Safety](https://mlsanity.com/paper/1606.06565/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [Strong mixed-integer programming formulations for trained neural networks](https://mlsanity.com/paper/1811.08359/) (2018)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [Measuring Neural Net Robustness with Constraints](https://mlsanity.com/paper/1605.07262/) (2016)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [CNN-Cert: An Efficient Framework for Certifying Robustness of Convolutional Neural Networks](https://mlsanity.com/paper/1811.12395/) (2018)
- [An SMT-Based Approach for Verifying Binarized Neural Networks](https://mlsanity.com/paper/2011.02948/) (2020)
- [Perfectly Parallel Fairness Certification of Neural Networks](https://mlsanity.com/paper/1912.02499/) (2019)
- [Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness](https://mlsanity.com/paper/1904.09959/) (2019)
- [Fastened CROWN: Tightened Neural Network Robustness Certificates](https://mlsanity.com/paper/1912.00574/) (2019)
- [Parallelization Techniques for Verifying Neural Networks](https://mlsanity.com/paper/2004.08440/) (2020)
- [Abstraction based Output Range Analysis for Neural Networks](https://mlsanity.com/paper/2007.09527/) (2020)
- [Towards Scalable Verification of Deep Reinforcement Learning](https://mlsanity.com/paper/2105.11931/) (2021)
- [DeepAbstract: Neural Network Abstraction for Accelerating Verification](https://mlsanity.com/paper/2006.13735/) (2020)

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

- [Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks](https://mlsanity.com/paper/2210.13915/) (2022)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [Formally Explaining Neural Networks within Reactive Systems](https://mlsanity.com/paper/2308.00143/) (2023)
- [Neural Network Verification with Proof Production](https://mlsanity.com/paper/2206.00512/) (2022)
- [Verification-Aided Deep Ensemble Selection](https://mlsanity.com/paper/2202.03898/) (2022)
- [veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System](https://mlsanity.com/paper/2212.03287/) (2022)
- [QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks](https://mlsanity.com/paper/2212.11138/) (2022)
- [Constrained Reinforcement Learning for Robotics via Scenario-Based Programming](https://mlsanity.com/paper/2206.09603/) (2022)
- [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)
- [CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness](https://mlsanity.com/paper/2206.03044/) (2022)
- [Tighter Abstract Queries in Neural Network Verification](https://mlsanity.com/paper/2210.12871/) (2022)
- [Robustness Assessment of a Runway Object Classifier for Safe Aircraft Taxiing](https://mlsanity.com/paper/2402.00035/) (2024)
- [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)
- [Abstraction-Based Proof Production in Formal Verification of Neural Networks](https://mlsanity.com/paper/2506.09455/) (2025)
- [Safe and Reliable Training of Learning-Based Aerospace Controllers](https://mlsanity.com/paper/2407.07088/) (2024)
- [DelBugV: Delta-Debugging Neural Network Verifiers](https://mlsanity.com/paper/2305.18558/) (2023)
- [Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks](https://mlsanity.com/paper/2302.06455/) (2023)
- [Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification](https://mlsanity.com/paper/2505.00963/) (2025)
- [Expediting Neural Network Verification via Network Reduction](https://mlsanity.com/paper/2308.03330/) (2023)
- [Patch Synthesis for Property Repair of Deep Neural Networks](https://mlsanity.com/paper/2404.01642/) (2024)
- [Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees](https://mlsanity.com/paper/2507.17453/) (2025)
- [Mining Verdict Boundaries for Neural Network Verification](https://mlsanity.com/paper/2607.28954/) (2026)

## Abstract (arXiv)

Convolutional neural networks have gained vast popularity due to their excellent performance in the fields of computer vision, image processing, and others. Unfortunately, it is now well known that convolutional networks often produce erroneous results - for example, minor perturbations of the inputs of these networks can result in severe classification errors. Numerous verification approaches have been proposed in recent years to prove the absence of such errors, but these are typically geared for fully connected networks and suffer from exacerbated scalability issues when applied to convolutional networks. To address this gap, we present here the Cnn-Abs framework, which is particularly aimed at the verification of convolutional networks. The core of Cnn-Abs is an abstraction-refinement technique, which simplifies the verification problem through the removal of convolutional connections in a way that soundly creates an over-approximation of the original problem; and which restores these connections if the resulting problem becomes too abstract. Cnn-Abs is designed to use existing verification engines as a backend, and our evaluation demonstrates that it can significantly boost the performance of a state-of-the-art DNN verification engine, reducing runtime by 15.7% on average.