# A Dual Approach to Scalable Verification of Deep Networks

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

## Key facts

- Cited by 125 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Mar 2018.

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

- [Scalable agent alignment via reward modeling: a research direction](https://mlsanity.com/paper/1811.07871/) (2018)
- [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)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [How Deep Learning Sees the World: A Survey on Adversarial Attacks & Defenses](https://mlsanity.com/paper/2305.10862/) (2023)
- [Rethinking Lipschitz Neural Networks and Certified Robustness: A Boolean Function Perspective](https://mlsanity.com/paper/2210.01787/) (2022)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagation](https://mlsanity.com/paper/2210.07394/) (2022)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective](https://mlsanity.com/paper/2206.12227/) (2022)
- [Towards Certifying L-infinity Robustness using Neural Networks with L-inf-dist Neurons](https://mlsanity.com/paper/2102.05363/) (2021)
- [Partition-based formulations for mixed-integer optimization of trained ReLU neural networks](https://mlsanity.com/paper/2102.04373/) (2021)
- [How to Robustify Black-Box ML Models? A Zeroth-Order Optimization Perspective](https://mlsanity.com/paper/2203.14195/) (2022)
- [When Deep Learning Meets Polyhedral Theory: A Survey](https://mlsanity.com/paper/2305.00241/) (2023)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [Boosting the Certified Robustness of L-infinity Distance Nets](https://mlsanity.com/paper/2110.06850/) (2021)
- [Efficient Neural Network Analysis with Sum-of-Infeasibilities](https://mlsanity.com/paper/2203.11201/) (2022)
- [Certified Robustness Against Natural Language Attacks by Causal Intervention](https://mlsanity.com/paper/2205.12331/) (2022)
- [DNNV: A Framework for Deep Neural Network Verification](https://mlsanity.com/paper/2105.12841/) (2021)
- [Safe Control with Neural Network Dynamic Models](https://mlsanity.com/paper/2110.01110/) (2021)
- [Neural Network Repair with Reachability Analysis](https://mlsanity.com/paper/2108.04214/) (2021)
- [CC-Cert: A Probabilistic Approach to Certify General Robustness of Neural Networks](https://mlsanity.com/paper/2109.10696/) (2021)
- [Convex Bounds on the Softmax Function with Applications to Robustness Verification](https://mlsanity.com/paper/2303.01713/) (2023)
- [Make Sure You're Unsure: A Framework for Verifying Probabilistic Specifications](https://mlsanity.com/paper/2102.09479/) (2021)
- [Adversarial Robustness with Non-uniform Perturbations](https://mlsanity.com/paper/2102.12002/) (2021)
- [BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks](https://mlsanity.com/paper/2103.07224/) (2021)
- [CertiFair: A Framework for Certified Global Fairness of Neural Networks](https://mlsanity.com/paper/2205.09927/) (2022)
- [Toward Certified Robustness Against Real-World Distribution Shifts](https://mlsanity.com/paper/2206.03669/) (2022)
- [Attack as Defense: Characterizing Adversarial Examples using Robustness](https://mlsanity.com/paper/2103.07633/) (2021)

## Abstract (arXiv)

This paper addresses the problem of formally verifying desirable properties of neural networks, i.e., obtaining provable guarantees that neural networks satisfy specifications relating their inputs and outputs (robustness to bounded norm adversarial perturbations, for example). Most previous work on this topic was limited in its applicability by the size of the network, network architecture and the complexity of properties to be verified. In contrast, our framework applies to a general class of activation functions and specifications on neural network inputs and outputs. We formulate verification as an optimization problem (seeking to find the largest violation of the specification) and solve a Lagrangian relaxation of the optimization problem to obtain an upper bound on the worst case violation of the specification being verified. Our approach is anytime i.e. it can be stopped at any time and a valid bound on the maximum violation can be obtained. We develop specialized verification algorithms with provable tightness guarantees under special assumptions and demonstrate the practical significance of our general verification approach on a variety of verification tasks.