DeepSplit: Scalable Verification of Deep Neural Networks via Operator Splitting
Not on the map. Why?
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.
Key facts. Cited by 8 papers in the map (data through 7 Oct 2026). Builds on 33 of its 53 references that are in the map. First posted on arXiv 16 Jun 2021.
Builds on
33 of 53 references.
References · 33
- 2017Towards Deep Learning Models Resistant to Adversarial Attackscited by 6,326
- 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 739
- 2020Fast is better than free: Revisiting adversarial trainingcited by 723
- 2017Provable defenses against adversarial examples via the convex outer adversarial polytopecited by 564
- 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 439
- 2018On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Modelscited by 322
- 2019Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networkscited by 290
- 2018Towards Fast Computation of Certified Robustness for ReLU Networkscited by 254
- 2017Formal Verification of Piece-Wise Linear Feed-Forward Neural Networkscited by 241
- 2019Towards Stable and Efficient Training of Verifiably Robust Neural Networkscited by 204
- 2020Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifierscited by 183
- 2018Semidefinite relaxations for certifying robustness to adversarial examplescited by 178
21 more
- 2019Adversarial Sensor Attack on LiDAR-based Perception in Autonomous Drivingcited by 151
- 2018Scaling provable adversarial defensescited by 141
- 2019Branch and Bound for Piecewise Linear Neural Network Verificationcited by 138
- 2017An approach to reachability analysis for feed-forward ReLU neural networkscited by 126
- 2018A Dual Approach to Scalable Verification of Deep Networkscited by 125
- 2019A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networkscited by 124
- 2019Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programmingcited by 100
- 2017Maximum Resilience of Artificial Neural Networkscited by 97
- 2020Enabling certification of verification-agnostic networks via memory-efficient semidefinite programmingcited by 65
- 2016Training Neural Networks Without Gradients: A Scalable ADMM Approachcited by 61
- 2020The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verificationcited by 50
- 2021Improved Branch and Bound for Neural Network Verification via Lagrangian Decompositioncited by 44
- 2019POPQORN: Quantifying Robustness of Recurrent Neural Networkscited by 36
- 2020Lagrangian Decomposition for Neural Network Verificationcited by 35
- 2020Scalable Polyhedral Verification of Recurrent Neural Networkscited by 20
- 2019GPU Acceleration of ADMM for Large-Scale Quadratic Programmingcited by 15
- 2020DiffRNN: Differential Verification of Recurrent Neural Networkscited by 12
- 2016Adaptive ADMM with Spectral Penalty Parameter Selectioncited by 10
- 2019Anderson Accelerated Douglas-Rachford Splittingcited by 8
- 2019Accelerating ADMM for Efficient Simulation and Optimizationcited by 7
- 2016Fast ADMM for Semidefinite Programs with Chordal Sparsitycited by 1
Built on by
Citing papers per year: 2022: 4; 2023: 1; 2024: 3.
8 papers.
- 2022General Cutting Planes for Bound-Propagation-Based Neural Network Verificationcited by 102
- 2022Zonotope Domains for Lagrangian Neural Network Verificationcited by 5
- 2022Chordal Sparsity for SDP-based Neural Network Verificationcited by 4
- 2024Ensuring Both Positivity and Stability Using Sector-Bounded Nonlinearity for Systems with Neural Network Controllerscited by 4
- 2022Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopescited by 2
- 2024Compact Optimality Verification for Optimization Proxiescited by 2
- 2024Provable Bounds on the Hessian of Neural Networks: Derivative-Preserving Reachability Analysiscited by 2
- 2023Verified Compositional Neuro-Symbolic Control for Stochastic Systems with Temporal Logic Taskscited by 0
- 2024Ensuring Both Positivity and Stability Using Sector-Bounded Nonlinearity for Systems with Neural Network Controllers18 Jun 2024
- 2024Provable Bounds on the Hessian of Neural Networks: Derivative-Preserving Reachability Analysis6 Jun 2024
- 2024Compact Optimality Verification for Optimization Proxies31 May 2024
- 2023Verified Compositional Neuro-Symbolic Control for Stochastic Systems with Temporal Logic Tasks17 Nov 2023
- 2022Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes14 Dec 2022
- 2022Zonotope Domains for Lagrangian Neural Network Verification14 Oct 2022
- 2022General Cutting Planes for Bound-Propagation-Based Neural Network Verification11 Aug 2022
- 2022Chordal Sparsity for SDP-based Neural Network Verification7 Jun 2022