Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness

Abstract

In recent years, the notion of local robustness (or robustness for short) has emerged as a desirable property of deep neural networks. Intuitively, robustness means that small perturbations to an input do not cause the network to perform misclassifications. In this paper, we present a novel algorithm for verifying robustness properties of neural networks. Our method synergistically combines gradient-based optimization methods for counterexample search with abstraction-based proof search to obtain a sound and (δ-)complete decision procedure. Our method also employs a data-driven approach to learn a verification policy that guides abstract interpretation during proof search. We have implemented the proposed approach in a tool called Charon and experimentally evaluated it on hundreds of benchmarks. Our experiments show that the proposed approach significantly outperforms three state-of-the-art tools, namely AI^2 , Reluplex, and Reluval.

References in corpus (20)

• Explaining and Harnessing Adversarial Examples
• Google's Neural Machine Translation System: Bridging the Gap between Human and Machine Translation
• Intriguing properties of neural networks
• End to End Learning for Self-Driving Cars
• A Tutorial on Bayesian Optimization of Expensive Cost Functions, with Application to Active User Modeling and Hierarchical Reinforcement Learning
• Transferability in Machine Learning: from Phenomena to Black-Box Attacks using Adversarial Samples
• DeepXplore: Automated Whitebox Testing of Deep Learning Systems
• Robust Physical-World Attacks on Deep Learning Models
• Adversarial Machine Learning at Scale
• Adversarial Perturbations Against Deep Neural Networks for Malware Classification
• Formal Security Analysis of Neural Networks using Symbolic Intervals
• BayesOpt: A Bayesian Optimization Library for Nonlinear Optimization, Experimental Design and Bandits
• An approach to reachability analysis for feed-forward ReLU neural networks
• Adversarial Examples: Attacks and Defenses for Deep Learning
• Output Range Analysis for Deep Neural Networks
• Towards Practical Verification of Machine Learning: The Case of Computer Vision Systems
• Adversarial Manipulation of Deep Representations
• DeepSafe: A Data-driven Approach for Checking Adversarial Robustness in Neural Networks
• An Overview of Vulnerabilities of Voice Controlled Systems
• Safety Verification of Deep Neural Networks

Cited by in corpus (17)

• An Abstraction-Based Framework for Neural Network Verification
• PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
• Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers
• Interval Universal Approximation for Neural Networks
• Neurosymbolic Reinforcement Learning with Formally Verified Exploration
• Towards Security Threats of Deep Learning Systems: A Survey
• Scalable Verification of GNN-based Job Schedulers
• Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees
• ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
• Towards the Quantification of Safety Risks in Deep Neural Networks
• Neural Network Branch-and-Bound for Neural Network Verification
• Reachability Analysis of Convolutional Neural Networks
• Work In Progress: Safety and Robustness Verification of Autoencoder-Based Regression Models using the NNV Tool
• BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks
• Formal Verification of Long Short-Term Memory based Audio Classifiers: A Star based Approach
• Certifying Robustness to Programmable Data Bias in Decision Trees
• Synthesizing Machine Learning Programs with PAC Guarantees via Statistical Sketching