# DeepSplit: Scalable Verification of Deep Neural Networks via Operator Splitting

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 33 of its 53 references that are in the map.
- First posted on arXiv 16 Jun 2021.

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

- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Fast is better than free: Revisiting adversarial training](https://mlsanity.com/paper/2001.03994/) (2020)
- [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)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks](https://mlsanity.com/paper/1906.04893/) (2019)
- [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)
- [Towards Stable and Efficient Training of Verifiably Robust Neural Networks](https://mlsanity.com/paper/1906.06316/) (2019)
- [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)
- [Adversarial Sensor Attack on LiDAR-based Perception in Autonomous Driving](https://mlsanity.com/paper/1907.06826/) (2019)
- [Scaling provable adversarial defenses](https://mlsanity.com/paper/1805.12514/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [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)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [Training Neural Networks Without Gradients: A Scalable ADMM Approach](https://mlsanity.com/paper/1605.02026/) (2016)
- [The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification](https://mlsanity.com/paper/2006.14076/) (2020)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [POPQORN: Quantifying Robustness of Recurrent Neural Networks](https://mlsanity.com/paper/1905.07387/) (2019)
- [Lagrangian Decomposition for Neural Network Verification](https://mlsanity.com/paper/2002.10410/) (2020)
- [Scalable Polyhedral Verification of Recurrent Neural Networks](https://mlsanity.com/paper/2005.13300/) (2020)
- [GPU Acceleration of ADMM for Large-Scale Quadratic Programming](https://mlsanity.com/paper/1912.04263/) (2019)
- [DiffRNN: Differential Verification of Recurrent Neural Networks](https://mlsanity.com/paper/2007.10135/) (2020)
- [Adaptive ADMM with Spectral Penalty Parameter Selection](https://mlsanity.com/paper/1605.07246/) (2016)

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

- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Zonotope Domains for Lagrangian Neural Network Verification](https://mlsanity.com/paper/2210.08069/) (2022)
- [Chordal Sparsity for SDP-based Neural Network Verification](https://mlsanity.com/paper/2206.03482/) (2022)
- [Ensuring Both Positivity and Stability Using Sector-Bounded Nonlinearity for Systems with Neural Network Controllers](https://mlsanity.com/paper/2406.12744/) (2024)
- [Provable Bounds on the Hessian of Neural Networks: Derivative-Preserving Reachability Analysis](https://mlsanity.com/paper/2406.04476/) (2024)
- [Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes](https://mlsanity.com/paper/2212.07553/) (2022)
- [Compact Optimality Verification for Optimization Proxies](https://mlsanity.com/paper/2405.21023/) (2024)
- [Verified Compositional Neuro-Symbolic Control for Stochastic Systems with Temporal Logic Tasks](https://mlsanity.com/paper/2311.10863/) (2023)

## Abstract (arXiv)

Analyzing the worst-case performance of deep neural networks against input perturbations amounts to solving a large-scale non-convex optimization problem, for which several past works have proposed convex relaxations as a promising alternative. However, even for reasonably-sized neural networks, these relaxations are not tractable, and so must be replaced by even weaker relaxations in practice. In this work, we propose a novel operator splitting method that can directly solve a convex relaxation of the problem to high accuracy, by splitting it into smaller sub-problems that often have analytical solutions. The method is modular, scales to very large problem instances, and compromises operations that are amenable to fast parallelization with GPU acceleration. We demonstrate our method in bounding the worst-case performance of large convolutional networks in image classification and reinforcement learning settings, and in reachability analysis of neural network dynamical systems.