A Dual Approach to Scalable Verification of Deep Networks

Abstract

This paper addresses the problem of formally verifying desirable properties of neural networks, i.e., obtaining provable guarantees that neural networks satisfy specifications relating their inputs and outputs (robustness to bounded norm adversarial perturbations, for example). Most previous work on this topic was limited in its applicability by the size of the network, network architecture and the complexity of properties to be verified. In contrast, our framework applies to a general class of activation functions and specifications on neural network inputs and outputs. We formulate verification as an optimization problem (seeking to find the largest violation of the specification) and solve a Lagrangian relaxation of the optimization problem to obtain an upper bound on the worst case violation of the specification being verified. Our approach is anytime i.e. it can be stopped at any time and a valid bound on the maximum violation can be obtained. We develop specialized verification algorithms with provable tightness guarantees under special assumptions and demonstrate the practical significance of our general verification approach on a variety of verification tasks.

References in corpus (4)

• Obfuscated Gradients Give a False Sense of Security: Circumventing Defenses to Adversarial Examples
• Adversarial Risk and the Dangers of Evaluating Against Weak Attacks
• Adversarial vulnerability for any classifier
• Analyzing the Robustness of Nearest Neighbors to Adversarial Examples

Cited by in corpus (46)

• Robustness May Be at Odds with Accuracy
• Formal Security Analysis of Neural Networks using Symbolic Intervals
• On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models
• Provably Robust Deep Learning via Adversarially Trained Smoothed Classifiers
• ReLU Networks as Surrogate Models in Mixed-Integer Linear Programs
• How Deep Learning Sees the World: A Survey on Adversarial Attacks & Defenses
• Scaling provable adversarial defenses
• Adversarial Attacks Against Medical Deep Learning Systems
• Verification of Neural Network Behaviour: Formal Guarantees for Power System Applications
• On Recurrent Neural Networks for learning-based control: recent results and ideas for future developments
• Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond
• Verification for Machine Learning, Autonomy, and Neural Networks Survey
• The Limitations of Adversarial Training and the Blind-Spot Attack
• Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective
• Tutorial: Safe and Reliable Machine Learning
• Robust Deep Reinforcement Learning against Adversarial Perturbations on State Observations
• Robustness Verification for Transformers
• Learning Security Classifiers with Verified Global Robustness Properties
• AI Research Considerations for Human Existential Safety (ARCHES)
• Towards Understanding Fast Adversarial Training
• Formal Verification of CNN-based Perception Systems
• Resilient Cyberphysical Systems and their Application Drivers: A Technology Roadmap
• Towards Understanding the Adversarial Vulnerability of Skeleton-based Action Recognition
• Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming
• Towards Robust Detection of Adversarial Examples
• Reachability analysis of neural networks using mixed monotonicity
• Fine-grained Synthesis of Unrestricted Adversarial Examples
• On Training Robust PDF Malware Classifiers
• Improving the Tightness of Convex Relaxation Bounds for Training Certifiably Robust Classifiers
• PROVEN: Certifying Robustness of Neural Networks with a Probabilistic Approach
• QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking
• DeepSearch: A Simple and Effective Blackbox Attack for Deep Neural Networks
• An efficient nonconvex reformulation of stagewise convex optimization problems
• NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation
• Certified Robustness of Graph Neural Networks against Adversarial Structural Perturbation
• On the Minimal Adversarial Perturbation for Deep Neural Networks with Provable Estimation Error
• Taking Care of The Discretization Problem: A Comprehensive Study of the Discretization Problem and A Black-Box Adversarial Attack in Discrete Integer Domain
• Connecting Lyapunov Control Theory to Adversarial Attacks
• Towards Adversarial Patch Analysis and Certified Defense against Crowd Counting
• nn-dependability-kit: Engineering Neural Networks for Safety-Critical Autonomous Driving Systems
• Attack as Defense: Characterizing Adversarial Examples using Robustness
• On ${\ell }_p$-norm Robustness of Ensemble Stumps and Trees
• Affine Multiplexing Networks: System Analysis, Learning, and Computation
• Verifying Quantized Neural Networks using SMT-Based Model Checking
• Reachability Analysis of Neural Networks with Uncertain Parameters
• A general framework for defining and optimizing robustness