Evaluating Robustness of Neural Networks with Mixed Integer Programming

Abstract

Neural networks have demonstrated considerable success on a wide variety of real-world problems. However, networks trained only to optimize for training accuracy can often be fooled by adversarial examples - slightly perturbed inputs that are misclassified with high confidence. Verification of networks enables us to gauge their vulnerability to such adversarial examples. We formulate verification of piecewise-linear neural networks as a mixed integer program. On a representative task of finding minimum adversarial distortions, our verifier is two to three orders of magnitude quicker than the state-of-the-art. We achieve this computational speedup via tight formulations for non-linearities, as well as a novel presolve algorithm that makes full use of all information available. The computational speedup allows us to verify properties on convolutional networks with an order of magnitude more ReLUs than networks previously verified by any complete verifier. In particular, we determine for the first time the exact adversarial accuracy of an MNIST classifier to perturbations with bounded $l_{\infty }$ norm $\epsilon =0.1$: for this classifier, we find an adversarial example for 4.38% of samples, and a certificate of robustness (to perturbations with bounded norm) for the remainder. Across all robust training procedures and network architectures considered, we are able to certify more samples than the state-of-the-art and find more adversarial examples than a strong first-order attack.

Accepted as a conference paper at ICLR 2019

Cited by in corpus (135)

• On Evaluating Adversarial Robustness
• Fast is better than free: Revisiting adversarial training
• Optimization Problems for Machine Learning: A Survey
• Robustness May Be at Odds with Accuracy
• On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models
• Provably Robust Deep Learning via Adversarially Trained Smoothed Classifiers
• Minimally distorted Adversarial Examples with a Fast Adaptive Boundary Attack
• RobustBench: a standardized adversarial robustness benchmark
• Machine Learning Testing: Survey, Landscapes and Horizons
• Training for Faster Adversarial Robustness Verification via Inducing ReLU Stability
• Verification of Neural Network Behaviour: Formal Guarantees for Power System Applications
• Recent advances for quantum classifiers
• Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond
• Adversarial Robustness Against the Union of Multiple Perturbation Models
• 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
• Reachability Analysis of Neural Feedback Loops
• Tight Certificates of Adversarial Robustness for Randomly Smoothed Classifiers
• Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks
• Certified Adversarial Robustness for Deep Reinforcement Learning
• Reinforcement Learning with Combinatorial Actions: An Application to Vehicle Routing
• Overfitting in adversarially robust deep learning
• Understanding and Improving Fast Adversarial Training
• The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results
• Solving Mixed Integer Programs Using Neural Networks
• Robustness Verification of Quantum Classifiers
• Robustness Verification of Tree-based Models
• Provably Robust Boosted Decision Stumps and Trees against Adversarial Attacks
• Formal Verification of Input-Output Mappings of Tree Ensembles
• Robustness Verification for Transformers
• DNNV: A Framework for Deep Neural Network Verification
• Certified Robustness for Top-k Predictions against Adversarial Perturbations via Randomized Smoothing
• Randomized Smoothing of All Shapes and Sizes
• Efficient Exact Verification of Binarized Neural Networks
• Learning Certified Individually Fair Representations
• Opportunities and Challenges in Deep Learning Adversarial Robustness: A Survey
• Learning Security Classifiers with Verified Global Robustness Properties
• Lipschitz Bounded Equilibrium Networks
• ASNets: Deep Learning for Generalised Planning
• Interval Universal Approximation for Neural Networks
• Semialgebraic Optimization for Lipschitz Constants of ReLU Networks
• Verifying Individual Fairness in Machine Learning Models
• Improving adversarial robustness of deep neural networks by using semantic information
• Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition
• Robust Deep Reinforcement Learning through Adversarial Loss
• Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming
• Learning Lyapunov Functions for Piecewise Affine Systems with Neural Network Controllers
• CAQL: Continuous Action Q-Learning
• Deep Learning-powered Iterative Combinatorial Auctions
• Partition-based formulations for mixed-integer optimization of trained ReLU neural networks
• A Survey of Recent Scalability Improvements for Semidefinite Programming with Applications in Machine Learning, Control, and Robotics
• Equivalent and Approximate Transformations of Deep Neural Networks
• Manifold Regularization for Locally Stable Deep Neural Networks
• Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees
• Improved, Deterministic Smoothing for L_1 Certified Robustness
• Correctness Verification of Neural Networks
• Neural Networks for Encoding Dynamic Security-Constrained Optimal Power Flow
• Lagrangian Decomposition for Neural Network Verification
• Understanding Adversarial Robustness: The Trade-off between Minimum and Average Margin
• Local Repair of Neural Networks Using Optimization
• Monotone-Value Neural Networks: Exploiting Preference Monotonicity in Combinatorial Assignment
• Robust Models Are More Interpretable Because Attributions Look Normal
• ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
• Verification of Neural Networks: Enhancing Scalability through Pruning
• Improving Certified Robustness via Statistical Learning with Logical Reasoning
• Learning a Large Neighborhood Search Algorithm for Mixed Integer Programs
• TSS: Transformation-Specific Smoothing for Robustness Certification
• On Training Robust PDF Malware Classifiers
• Refactoring Neural Networks for Verification
• Scaling the Convex Barrier with Sparse Dual Algorithms
• Towards the Quantification of Safety Risks in Deep Neural Networks
• QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking
• Data-Dependent Randomized Smoothing
• Enhancing Certified Robustness via Smoothed Weighted Ensembling
• Scaling Up Exact Neural Network Compression by ReLU Stability
• On the verification of Embeddings using Hybrid Markov Logic
• CROP: Certifying Robust Policies for Reinforcement Learning through Functional Smoothing
• DeepSearch: A Simple and Effective Blackbox Attack for Deep Neural Networks
• NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation
• Scalable Verification of Quantized Neural Networks (Technical Report)
• Accelerating Robustness Verification of Deep Neural Networks Guided by Target Labels
• Provable robustness against all adversarial $l_p$-perturbations for $p\ge 1$
• On the Tightness of Semidefinite Relaxations for Certifying Robustness to Adversarial Examples
• Understanding the Intrinsic Robustness of Image Distributions using Conditional Generative Models
• A Review of Formal Methods applied to Machine Learning
• Certifying Joint Adversarial Robustness for Model Ensembles
• Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs
• Certifiable Robustness to Adversarial State Uncertainty in Deep Reinforcement Learning
• GoTube: Scalable Stochastic Verification of Continuous-Depth Models
• Towards Certifying L-infinity Robustness using Neural Networks with L-inf-dist Neurons
• Traversing the Local Polytopes of ReLU Neural Networks: A Unified Approach for Network Verification
• Tight Second-Order Certificates for Randomized Smoothing
• Probabilistic Verification of Neural Networks Against Group Fairness
• Neural Network Branch-and-Bound for Neural Network Verification
• ANCER: Anisotropic Certification via Sample-wise Volume Maximization
• Constrained Discrete Black-Box Optimization using Mixed-Integer Programming
• Insta-RS: Instance-wise Randomized Smoothing for Improved Robustness and Accuracy
• Fast and Stable Interval Bounds Propagation for Training Verifiably Robust Models
• Incorrect by Construction: Fine Tuning Neural Networks for Guaranteed Performance on Finite Sets of Examples
• Relaxing Local Robustness
• IPBoost -- Non-Convex Boosting via Integer Programming
• Reachability Analysis of Convolutional Neural Networks
• SOCRATES: Towards a Unified Platform for Neural Network Analysis
• Exploring Model Robustness with Adaptive Networks and Improved Adversarial Training
• Universal Approximation with Certified Networks
• Attack as Defense: Characterizing Adversarial Examples using Robustness
• Lyapunov-stable neural-network control
• Towards Evaluating and Training Verifiably Robust Neural Networks
• Scalable and Modular Robustness Analysis of Deep Neural Networks
• Rethinking Empirical Evaluation of Adversarial Robustness Using First-Order Attack Methods
• Verifying Quantized Neural Networks using SMT-Based Model Checking
• Simplifying Neural Networks using Formal Verification
• Deep Probabilistic Accelerated Evaluation: A Robust Certifiable Rare-Event Simulation Methodology for Black-Box Safety-Critical Systems
• NeVer 2.0: Learning, Verification and Repair of Deep Neural Networks
• BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks
• Certifying Strategyproof Auction Networks
• Adversarial Examples for $k$-Nearest Neighbor Classifiers Based on Higher-Order Voronoi Diagrams
• Dynamic Defense Approach for Adversarial Robustness in Deep Neural Networks via Stochastic Ensemble Smoothed Model
• Investigating the Robustness of Artificial Intelligent Algorithms with Mixture Experiments
• A Sequential Framework Towards an Exact SDP Verification of Neural Networks
• ReLU activated Multi-Layer Neural Networks trained with Mixed Integer Linear Programs
• Recent Advances in Large Margin Learning
• Robust Machine Learning via Privacy/Rate-Distortion Theory
• Hidden Cost of Randomized Smoothing
• A Primer on Multi-Neuron Relaxation-based Adversarial Robustness Certification
• Training Provably Robust Models by Polyhedral Envelope Regularization
• MadNet: Using a MAD Optimization for Defending Against Adversarial Attacks
• Neural Network Repair with Reachability Analysis
• Identifying and Exploiting Structures for Reliable Deep Learning
• Learning Region of Attraction for Nonlinear Systems
• Efficient and Robust Mixed-Integer Optimization Methods for Training Binarized Deep Neural Networks
• Deterministic Certification to Adversarial Attacks via Bernstein Polynomial Approximation
• Generate and Verify: Semantically Meaningful Formal Analysis of Neural Network Perception Systems
• Learning Lyapunov Functions for Hybrid Systems
• Expected Tight Bounds for Robust Training