# DualApp: Tight Over-Approximation for Neural Network Robustness Verification via Under-Approximation

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 34 of its 60 references that are in the map.
- First posted on arXiv 21 Nov 2022.

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

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms](https://mlsanity.com/paper/1708.07747/) (2017)
- [Towards Evaluating the Robustness of Neural Networks](https://mlsanity.com/paper/1608.04644/) (2016)
- [DeepFool: a simple and accurate method to fool deep neural networks](https://mlsanity.com/paper/1511.04599/) (2015)
- [An overview of gradient descent optimization algorithms](https://mlsanity.com/paper/1609.04747/) (2016)
- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [Adversarial Examples Are Not Bugs, They Are Features](https://mlsanity.com/paper/1905.02175/) (2019)
- [The Limitations of Deep Learning in Adversarial Settings](https://mlsanity.com/paper/1511.07528/) (2015)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Adversarial Attacks and Defences: A Survey](https://mlsanity.com/paper/1810.00069/) (2018)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [Achieving Verified Robustness to Symbol Substitutions via Interval Bound Propagation](https://mlsanity.com/paper/1909.01492/) (2019)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [DLFuzz: Differential Fuzzing Testing of Deep Learning Systems](https://mlsanity.com/paper/1808.09413/) (2018)
- [DeepID3: Face Recognition with Very Deep Neural Networks](https://mlsanity.com/paper/1502.00873/) (2015)
- [Trustworthy AI](https://mlsanity.com/paper/2011.02272/) (2020)
- [Lipschitz Certificates for Layered Network Structures Driven by Averaged Activation Operators](https://mlsanity.com/paper/1903.01014/) (2019)
- [The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification](https://mlsanity.com/paper/2006.14076/) (2020)
- [Probabilistic Verification of Fairness Properties via Concentration](https://mlsanity.com/paper/1812.02573/) (2018)
- [Fastened CROWN: Tightened Neural Network Robustness Certificates](https://mlsanity.com/paper/1912.00574/) (2019)
- [Non-Negative Networks Against Adversarial Attacks](https://mlsanity.com/paper/1806.06108/) (2018)
- [Robustness Guarantees for Deep Neural Networks on Videos](https://mlsanity.com/paper/1907.00098/) (2019)
- [Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning](https://mlsanity.com/paper/2101.10102/) (2021)

## Abstract (arXiv)

The robustness of neural networks is fundamental to the hosting system's reliability and security. Formal verification has been proven to be effective in providing provable robustness guarantees. To improve the verification scalability, over-approximating the non-linear activation functions in neural networks by linear constraints is widely adopted, which transforms the verification problem into an efficiently solvable linear programming problem. As over-approximations inevitably introduce overestimation, many efforts have been dedicated to defining the tightest possible approximations. Recent studies have however showed that the existing so-called tightest approximations are superior to each other. In this paper we identify and report an crucial factor in defining tight approximations, namely the approximation domains of activation functions. We observe that existing approaches only rely on overestimated domains, while the corresponding tight approximation may not necessarily be tight on its actual domain. We propose a novel under-approximation-guided approach, called dual-approximation, to define tight over-approximations and two complementary under-approximation algorithms based on sampling and gradient descent. The overestimated domain guarantees the soundness while the underestimated one guides the tightness. We implement our approach into a tool called DualApp and extensively evaluate it on a comprehensive benchmark of 84 collected and trained neural networks with different architectures. The experimental results show that DualApp outperforms the state-of-the-art approximation-based approaches, with up to 71.22% improvement to the verification result.