The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification

Abstract

We improve the effectiveness of propagation- and linear-optimization-based neural network verification algorithms with a new tightened convex relaxation for ReLU neurons. Unlike previous single-neuron relaxations which focus only on the univariate input space of the ReLU, our method considers the multivariate input space of the affine pre-activation function preceding the ReLU. Using results from submodularity and convex geometry, we derive an explicit description of the tightest possible convex relaxation when this multivariate input is over a box domain. We show that our convex relaxation is significantly stronger than the commonly used univariate-input relaxation which has been proposed as a natural convex relaxation barrier for verification. While our description of the relaxation may require an exponential number of inequalities, we show that they can be separated in linear time and hence can be efficiently incorporated into optimization algorithms on an as-needed basis. Based on this novel relaxation, we design two polynomial-time algorithms for neural network verification: a linear-programming-based algorithm that leverages the full power of our relaxation, and a fast propagation algorithm that generalizes existing approaches. In both cases, we show that for a modest increase in computational effort, our strengthened relaxation enables us to verify a significantly larger number of instances compared to similar algorithms.

References in corpus (10)

• Provable defenses against adversarial examples via the convex outer adversarial polytope
• Efficient Neural Network Robustness Certification with General Activation Functions
• An approach to reachability analysis for feed-forward ReLU neural networks
• Semidefinite relaxations for certifying robustness to adversarial examples
• Efficient Formal Safety Analysis of Neural Networks
• A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks
• Training for Faster Adversarial Robustness Verification via Inducing ReLU Stability
• Deep Neural Networks as 0-1 Mixed Integer Linear Programs: A Feasibility Study
• Algorithms for Verifying Deep Neural Networks
• Improving the Tightness of Convex Relaxation Bounds for Training Certifiably Robust Classifiers

Cited by in corpus (10)

• Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond
• PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
• Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers
• Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective
• Chordal and factor-width decompositions for scalable semidefinite and polynomial optimization
• Partition-based formulations for mixed-integer optimization of trained ReLU neural networks
• Scalable Verification of GNN-based Job Schedulers
• Scaling the Convex Barrier with Sparse Dual Algorithms
• GoTube: Scalable Stochastic Verification of Continuous-Depth Models
• A Primer on Multi-Neuron Relaxation-based Adversarial Robustness Certification