# Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness

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

## Key facts

- Cited by 40 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 Apr 2019.

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

- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Provable Repair of Deep Neural Networks](https://mlsanity.com/paper/2104.04413/) (2021)
- [VeriX: Towards Verified Explainability of Deep Neural Networks](https://mlsanity.com/paper/2212.01051/) (2022)
- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)
- [Efficient Neural Network Analysis with Sum-of-Infeasibilities](https://mlsanity.com/paper/2203.11201/) (2022)
- [Formally Explaining Neural Networks within Reactive Systems](https://mlsanity.com/paper/2308.00143/) (2023)
- [Certifying Robustness to Programmable Data Bias in Decision Trees](https://mlsanity.com/paper/2110.04363/) (2021)
- [Scalable Verification of GNN-based Job Schedulers](https://mlsanity.com/paper/2203.03153/) (2022)
- [Convex Bounds on the Softmax Function with Applications to Robustness Verification](https://mlsanity.com/paper/2303.01713/) (2023)
- [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)
- [Toward Certified Robustness Against Real-World Distribution Shifts](https://mlsanity.com/paper/2206.03669/) (2022)
- [Incremental Verification of Neural Networks](https://mlsanity.com/paper/2304.01874/) (2023)
- [QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks](https://mlsanity.com/paper/2212.11138/) (2022)
- [Verifying Generalization in Deep Learning](https://mlsanity.com/paper/2302.05745/) (2023)
- [SyReNN: A Tool for Analyzing Deep Neural Networks](https://mlsanity.com/paper/2101.03263/) (2021)
- [Linearity Grafting: Relaxed Neuron Pruning Helps Certifiable Robustness](https://mlsanity.com/paper/2206.07839/) (2022)
- [Verification of Neural Networks' Global Robustness](https://mlsanity.com/paper/2402.19322/) (2024)
- [Safe Neurosymbolic Learning with Differentiable Symbolic Execution](https://mlsanity.com/paper/2203.07671/) (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)
- [Neural Network Branch-and-Bound for Neural Network Verification](https://mlsanity.com/paper/2107.12855/) (2021)
- [DeepCDCL: An CDCL-based Neural Network Verification Framework](https://mlsanity.com/paper/2403.07956/) (2024)
- [Reachability Analysis of Convolutional Neural Networks](https://mlsanity.com/paper/2106.12074/) (2021)
- [Self-Correcting Neural Networks For Safe Classification](https://mlsanity.com/paper/2107.11445/) (2021)
- [Sound and Complete Verification of Polynomial Networks](https://mlsanity.com/paper/2209.07235/) (2022)
- [Safe and Reliable Training of Learning-Based Aerospace Controllers](https://mlsanity.com/paper/2407.07088/) (2024)
- [A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning enabled Control Systems](https://mlsanity.com/paper/2303.05394/) (2023)
- [DelBugV: Delta-Debugging Neural Network Verifiers](https://mlsanity.com/paper/2305.18558/) (2023)

## Abstract (arXiv)

In recent years, the notion of local robustness (or robustness for short) has emerged as a desirable property of deep neural networks. Intuitively, robustness means that small perturbations to an input do not cause the network to perform misclassifications. In this paper, we present a novel algorithm for verifying robustness properties of neural networks. Our method synergistically combines gradient-based optimization methods for counterexample search with abstraction-based proof search to obtain a sound and (δ-)complete decision procedure. Our method also employs a data-driven approach to learn a verification policy that guides abstract interpretation during proof search. We have implemented the proposed approach in a tool called Charon and experimentally evaluated it on hundreds of benchmarks. Our experiments show that the proposed approach significantly outperforms three state-of-the-art tools, namely AI2 , Reluplex, and Reluval.