Efficient Exact Verification of Binarized Neural Networks
arXiv:2005.03597
Abstract
Concerned with the reliability of neural networks, researchers have developed verification techniques to prove their robustness. Most verifiers work with real-valued networks. Unfortunately, the exact (complete and sound) verifiers face scalability challenges and provide no correctness guarantees due to floating point errors. We argue that Binarized Neural Networks (BNNs) provide comparable robustness and allow exact and significantly more efficient verification. We present a new system, EEV, for efficient and exact verification of BNNs. EEV consists of two parts: (i) a novel SAT solver that speeds up BNN verification by natively handling the reified cardinality constraints arising in BNN encodings; and (ii) strategies to train solver-friendly robust BNNs by inducing balanced layer-wise sparsity and low cardinality bounds, and adaptively cancelling the gradients. We demonstrate the effectiveness of EEV by presenting the first exact verification results for L-inf-bounded adversarial robustness of nontrivial convolutional BNNs on the MNIST and CIFAR10 datasets. Compared to exact verification of real-valued networks of the same architectures on the same tasks, EEV verifies BNNs hundreds to thousands of times faster, while delivering comparable verifiable accuracy in most cases.
arXiv commentTo be published in NeurIPS 2020
References in corpus (17)
- Adam: A Method for Stochastic Optimization
- PyTorch: An Imperative Style, High-Performance Deep Learning Library
- Estimating or Propagating Gradients Through Stochastic Neurons for Conditional Computation
- DoReFa-Net: Training Low Bitwidth Convolutional Neural Networks with Low Bitwidth Gradients
- Binarized Neural Networks
- Efficient Neural Network Robustness Certification with General Activation Functions
- Evaluating Robustness of Neural Networks with Mixed Integer Programming
- An approach to reachability analysis for feed-forward ReLU neural networks
- Semidefinite relaxations for certifying robustness to adversarial examples
- On Adaptive Attacks to Adversarial Example Defenses
- A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks
- A Unified View of Piecewise Linear Neural Network Verification
- Training for Faster Adversarial Robustness Verification via Inducing ReLU Stability
- Training verified learners with learned verifiers
- Back to Simplicity: How to Train Accurate BNNs from Scratch?
- Combinatorial Attacks on Binarized Neural Networks
- Certifying Joint Adversarial Robustness for Model Ensembles