# Zonotope Domains for Lagrangian Neural Network Verification

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 25 of its 47 references that are in the map.
- First posted on arXiv 14 Oct 2022.

## Builds on (most cited first, 25 of 25)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Obfuscated Gradients Give a False Sense of Security: Circumventing Defenses to Adversarial Examples](https://mlsanity.com/paper/1802.00420/) (2018)
- [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)
- [Lipschitz regularity of deep neural networks: analysis and efficient estimation](https://mlsanity.com/paper/1805.10965/) (2018)
- [Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks](https://mlsanity.com/paper/1906.04893/) (2019)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [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)
- [Exactly Computing the Local Lipschitz Constant of ReLU Networks](https://mlsanity.com/paper/2003.01219/) (2020)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [Neural Network Branching for Neural Network Verification](https://mlsanity.com/paper/1912.01329/) (2019)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [Lagrangian Decomposition for Neural Network Verification](https://mlsanity.com/paper/2002.10410/) (2020)
- [Provable Certificates for Adversarial Examples: Fitting a Ball in the Union of Polytopes](https://mlsanity.com/paper/1903.08778/) (2019)
- [Certifying Incremental Quadratic Constraints for Neural Networks via Convex Optimization](https://mlsanity.com/paper/2012.05981/) (2020)
- [DeepSplit: Scalable Verification of Deep Neural Networks via Operator Splitting](https://mlsanity.com/paper/2106.09117/) (2021)
- [Provable Lipschitz Certification for Generative Models](https://mlsanity.com/paper/2107.02732/) (2021)

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

- [On the Robustness of Removal-Based Feature Attributions](https://mlsanity.com/paper/2306.07462/) (2023)
- [Parameterized Hardness of Zonotope Containment and Neural Network Verification](https://mlsanity.com/paper/2509.22849/) (2025)
- [Learning from Uncertain Data: From Possible Worlds to Possible Models](https://mlsanity.com/paper/2405.18549/) (2024)
- [Hybrid Robustness Verification for Spatio-Temporal Neural Networks](https://mlsanity.com/paper/2606.09746/) (2026)
- [Matrix Zonotopic Attention: A Context-Adaptive Value Projection for Set Transformers](https://mlsanity.com/paper/2608.05472/) (2026)

## Abstract (arXiv)

Neural network verification aims to provide provable bounds for the output of a neural network for a given input range. Notable prior works in this domain have either generated bounds using abstract domains, which preserve some dependency between intermediate neurons in the network; or framed verification as an optimization problem and solved a relaxation using Lagrangian methods. A key drawback of the latter technique is that each neuron is treated independently, thereby ignoring important neuron interactions. We provide an approach that merges these two threads and uses zonotopes within a Lagrangian decomposition. Crucially, we can decompose the problem of verifying a deep neural network into the verification of many 2-layer neural networks. While each of these problems is provably hard, we provide efficient relaxation methods that are amenable to efficient dual ascent procedures. Our technique yields bounds that improve upon both linear programming and Lagrangian-based verification techniques in both time and bound tightness.