Algorithms for Verifying Deep Neural Networks

Abstract

Deep neural networks are widely used for nonlinear function approximation with applications ranging from computer vision to control. Although these networks involve the composition of simple arithmetic operations, it can be very challenging to verify whether a particular network satisfies certain input-output properties. This article surveys methods that have emerged recently for soundly verifying such properties. These methods borrow insights from reachability analysis, optimization, and search. We discuss fundamental differences and connections between existing algorithms. In addition, we provide pedagogical implementations of existing methods and compare them on a set of benchmark problems.

References in corpus (19)

• DeepXplore: Automated Whitebox Testing of Deep Learning Systems
• Provable defenses against adversarial examples via the convex outer adversarial polytope
• Certified Defenses against Adversarial Examples
• Efficient Neural Network Robustness Certification with General Activation Functions
• Formal Security Analysis of Neural Networks using Symbolic Intervals
• An approach to reachability analysis for feed-forward ReLU neural networks
• Deep Neural Network Compression for Aircraft Collision Avoidance Systems
• Efficient Formal Safety Analysis of Neural Networks
• A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks
• A Unified View of Piecewise Linear Neural Network Verification
• Verification for Machine Learning, Autonomy, and Neural Networks Survey
• Output Range Analysis for Deep Neural Networks
• Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations
• Automated Verification of Neural Networks: Advances, Challenges and Perspectives
• Abstraction based Output Range Analysis for Neural Networks
• Fast Neural Network Verification via Shadow Prices
• Reachability Analysis for Feed-Forward Neural Networks using Face Lattices
• Specification-Guided Safety Verification for Feedforward Neural Networks
• Reachable Set Estimation and Safety Verification for Piecewise Linear Systems with Neural Network Controllers

Cited by in corpus (10)

• The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification
• Parallelization Techniques for Verifying Neural Networks
• Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming
• Scaling Up Exact Neural Network Compression by ReLU Stability
• Pruning and Slicing Neural Networks using Formal Verification
• Auditing AI models for Verified Deployment under Semantic Specifications
• Evaluating the Safety of Deep Reinforcement Learning Models using Semi-Formal Verification
• Online Reachability Analysis and Space Convexification for Autonomous Racing
• Simplifying Neural Networks using Formal Verification
• Interval Deep Learning for Uncertainty Quantification in Safety Applications