Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming
arXiv:2010.11645
Abstract
Convex relaxations have emerged as a promising approach for verifying desirable properties of neural networks like robustness to adversarial perturbations. Widely used Linear Programming (LP) relaxations only work well when networks are trained to facilitate verification. This precludes applications that involve verification-agnostic networks, i.e., networks not specially trained for verification. On the other hand, semidefinite programming (SDP) relaxations have successfully be applied to verification-agnostic networks, but do not currently scale beyond small networks due to poor time and space asymptotics. In this work, we propose a first-order dual SDP algorithm that (1) requires memory only linear in the total number of network activations, (2) only requires a fixed number of forward/backward passes through the network per iteration. By exploiting iterative eigenvector methods, we express all solver operations in terms of forward and backward passes through the network, enabling efficient use of hardware like GPUs/TPUs. For two verification-agnostic networks on MNIST and CIFAR-10, we significantly improve L-inf verified robust accuracy from 1% to 88% and 6% to 40% respectively. We also demonstrate tight verification of a quadratic stability specification for the decoder of a variational autoencoder.
References in corpus (19)
- Adam: A Method for Stochastic Optimization
- PyTorch: An Imperative Style, High-Performance Deep Learning Library
- Auto-Encoding Variational Bayes
- Obfuscated Gradients Give a False Sense of Security: Circumventing Defenses to Adversarial Examples
- Adversarial Risk and the Dangers of Evaluating Against Weak Attacks
- Evaluating Robustness of Neural Networks with Mixed Integer Programming
- On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models
- Safe Exploration in Continuous Action Spaces
- Semidefinite relaxations for certifying robustness to adversarial examples
- A Dual Approach to Scalable Verification of Deep Networks
- Towards Fast Computation of Certified Robustness for ReLU Networks
- A Unified View of Piecewise Linear Neural Network Verification
- A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks
- Learning perturbation sets for robust machine learning
- Algorithms for Verifying Deep Neural Networks
- Toward Scalable Verification for Safety-Critical Deep Networks
- Efficient First-Order Methods for Linear Programming and Semidefinite Programming
- An Optimal-Storage Approach to Semidefinite Programming using Approximate Complementarity
- Verification of Non-Linear Specifications for Neural Networks