Reachability Analysis of Deep Neural Networks with Provable Guarantees

Abstract

Verifying correctness of deep neural networks (DNNs) is challenging. We study a generic reachability problem for feed-forward DNNs which, for a given set of inputs to the network and a Lipschitz-continuous function over its outputs, computes the lower and upper bound on the function values. Because the network and the function are Lipschitz continuous, all values in the interval between the lower and upper bound are reachable. We show how to obtain the safety verification problem, the output range analysis problem and a robustness measure by instantiating the reachability problem. We present a novel algorithm based on adaptive nested optimisation to solve the reachability problem. The technique has been implemented and evaluated on a range of DNNs, demonstrating its efficiency, scalability and ability to handle a broader class of networks than state-of-the-art verification approaches.

This is the long version of the conference paper accepted in IJCAI-2018. Github: https://github.com/TrustAI/DeepGO

References in corpus (5)

• An approach to reachability analysis for feed-forward ReLU neural networks
• Universal adversarial perturbations
• The Limitations of Deep Learning in Adversarial Settings
• Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks
• Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for the $L_0$ Norm

Cited by in corpus (14)

• Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks
• Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for the $L_0$ Norm
• Specification-Guided Safety Verification for Feedforward Neural Networks
• MR-GAN: Manifold Regularized Generative Adversarial Networks
• Fooling Object Detectors: Adversarial Attacks by Half-Neighbor Masks
• From Shallow to Deep Interactions Between Knowledge Representation, Reasoning and Machine Learning (Kay R. Amel group)
• GoTube: Scalable Stochastic Verification of Continuous-Depth Models
• A Review of Formal Methods applied to Machine Learning
• Formal methods and software engineering for DL. Security, safety and productivity for DL systems development
• Towards Identifying and closing Gaps in Assurance of autonomous Road vehicleS -- a collection of Technical Notes Part 1
• Probabilistic Safety for Bayesian Neural Networks
• Robustness Guarantees for Deep Neural Networks on Videos
• Global Robustness Verification Networks
• Failing with Grace: Learning Neural Network Controllers that are Boundedly Unsafe