Efficient Formal Safety Analysis of Neural Networks

Abstract

Neural networks are increasingly deployed in real-world safety-critical domains such as autonomous driving, aircraft collision avoidance, and malware detection. However, these networks have been shown to often mispredict on inputs with minor adversarial or even accidental perturbations. Consequences of such errors can be disastrous and even potentially fatal as shown by the recent Tesla autopilot crash. Thus, there is an urgent need for formal analysis systems that can rigorously check neural networks for violations of different safety properties such as robustness against adversarial perturbations within a certain $L$-norm of a given image. An effective safety analysis system for a neural network must be able to either ensure that a safety property is satisfied by the network or find a counterexample, i.e., an input for which the network will violate the property. Unfortunately, most existing techniques for performing such analysis struggle to scale beyond very small networks and the ones that can scale to larger networks suffer from high false positives and cannot produce concrete counterexamples in case of a property violation. In this paper, we present a new efficient approach for rigorously checking different safety properties of neural networks that significantly outperforms existing approaches by multiple orders of magnitude. Our approach can check different safety properties and find concrete counterexamples for networks that are 10$\times$ larger than the ones supported by existing analysis techniques. We believe that our approach to estimating tight output bounds of a network for a given input range can also help improve the explainability of neural networks and guide the training process of more robust neural networks.

arXiv commentAccepted to NIPS'18

Cited by in corpus (85)

• Provably Robust Deep Learning via Adversarially Trained Smoothed Classifiers
• Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond
• How to Certify Machine Learning Based Safety-critical Systems? A Systematic Literature Review
• Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers
• Security and Privacy Issues in Deep Learning
• Software Engineering for AI-Based Systems: A Survey
• Practical Solutions for Machine Learning Safety in Autonomous Vehicles
• Certified Adversarial Robustness for Deep Reinforcement Learning
• The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification
• Branch and Bound for Piecewise Linear Neural Network Verification
• Towards Stable and Efficient Training of Verifiably Robust Neural Networks
• A Survey on Scenario-Based Testing for Automated Driving Systems in High-Fidelity Simulation
• Robust Deep Reinforcement Learning against Adversarial Perturbations on State Observations
• Provably Robust Boosted Decision Stumps and Trees against Adversarial Attacks
• Denoised Smoothing: A Provable Defense for Pretrained Classifiers
• Formal Verification of Input-Output Mappings of Tree Ensembles
• DNNV: A Framework for Deep Neural Network Verification
• Robustness Verification for Transformers
• Algorithms for Verifying Deep Neural Networks
• Certified Robustness for Top-k Predictions against Adversarial Perturbations via Randomized Smoothing
• HYDRA: Pruning Adversarially Robust Neural Networks
• Randomized Smoothing of All Shapes and Sizes
• Learning Security Classifiers with Verified Global Robustness Properties
• Parallelization Techniques for Verifying Neural Networks
• Towards Compact and Robust Deep Neural Networks
• Provable Certificates for Adversarial Examples: Fitting a Ball in the Union of Polytopes
• Verifying Individual Fairness in Machine Learning Models
• Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition
• Resilient Cyberphysical Systems and their Application Drivers: A Technology Roadmap
• Robust Deep Reinforcement Learning through Adversarial Loss
• Evaluations and Methods for Explanation through Robustness Analysis
• Learning Lyapunov Functions for Piecewise Affine Systems with Neural Network Controllers
• Towards Understanding the Adversarial Vulnerability of Skeleton-based Action Recognition
• Towards Verifying Robustness of Neural Networks Against Semantic Perturbations
• Improved Adversarial Robustness by Reducing Open Space Risk via Tent Activations
• Evaluating the Robustness of Nearest Neighbor Classifiers: A Primal-Dual Perspective
• Defending Against Physically Realizable Attacks on Image Classification
• A Survey of Recent Scalability Improvements for Semidefinite Programming with Applications in Machine Learning, Control, and Robotics
• Case Study: Verifying the Safety of an Autonomous Racing Car with a Neural Network Controller
• Enhancing Gradient-based Attacks with Symbolic Intervals
• Reachability Analysis for Feed-Forward Neural Networks using Face Lattices
• Enhancing Certifiable Robustness via a Deep Model Ensemble
• Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees
• A Systematic Mapping Study on Testing of Machine Learning Programs
• Security and Machine Learning in the Real World
• Fast Certified Robust Training with Short Warmup
• Refactoring Neural Networks for Verification
• On Training Robust PDF Malware Classifiers
• Boosting the Certified Robustness of L-infinity Distance Nets
• ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
• Scaling the Convex Barrier with Sparse Dual Algorithms
• QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking
• Enhancing Certified Robustness via Smoothed Weighted Ensembling
• Adversarial robustness via robust low rank representations
• Scalable Verification of Quantized Neural Networks (Technical Report)
• An efficient nonconvex reformulation of stagewise convex optimization problems
• NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation
• Interpretable and Trustworthy Deepfake Detection via Dynamic Prototypes
• A Review of Formal Methods applied to Machine Learning
• Statistically Robust Neural Network Classification
• Accelerating Robustness Verification of Deep Neural Networks Guided by Target Labels
• Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs
• Certifiable Robustness to Adversarial State Uncertainty in Deep Reinforcement Learning
• Neural Network Branch-and-Bound for Neural Network Verification
• Auditing AI models for Verified Deployment under Semantic Specifications
• Attack as Defense: Characterizing Adversarial Examples using Robustness
• Fast Falsification of Neural Networks using Property Directed Testing
• Evaluating the Safety of Deep Reinforcement Learning Models using Semi-Formal Verification
• Non-Stochastic Information Theory
• SOCRATES: Towards a Unified Platform for Neural Network Analysis
• Universal Approximation with Certified Networks
• Not All Features Are Equal: Feature Leveling Deep Neural Networks for Better Interpretation
• Towards Evaluating and Training Verifiably Robust Neural Networks
• Verifying Quantized Neural Networks using SMT-Based Model Checking
• NeVer 2.0: Learning, Verification and Repair of Deep Neural Networks
• Grand Challenges in Resilience: Autonomous System Resilience through Design and Runtime Measures
• On ${\ell }_p$-norm Robustness of Ensemble Stumps and Trees
• Incremental Verification of Fixed-Point Implementations of Neural Networks
• Adaptive Verifiable Training Using Pairwise Class Similarity
• Expected Tight Bounds for Robust Training
• Training Provably Robust Models by Polyhedral Envelope Regularization
• Deterministic Certification to Adversarial Attacks via Bernstein Polynomial Approximation
• Hidden Cost of Randomized Smoothing
• Is the Rush to Machine Learning Jeopardizing Safety? Results of a Survey
• Towards Assessment of Randomized Smoothing Mechanisms for Certifying Adversarial Robustness