Reachability Analysis of Deep Neural Networks with Provable Guarantees

By Wenjie Ruan, Xiaowei Huang, Marta Z. Kwiatkowska. 2018

287 citations recorded by the source corpus.

Verifying correctness for 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.

Subfields: Artificial Intelligence, Computer Vision and Pattern Recognition, Electrical and Electronic Engineering, Safety, Robustness & Interpretability

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Vision and Pattern Recognition

In Electrical and Electronic Engineering

In Safety, Robustness & Interpretability

Citations in the corpus

Simple and Principled Uncertainty Estimation with Deterministic Deep Learning via Distance Awareness (2020, background): “Distance-preserving neural networks and bi-Lipschitz condition The theoretic connection between distance preservation and the bi-Lipschitz condition is well-established [67], and learning an approximately isometric, distance-preserving transform has been an important goal in the fields of dimensiona”
Lipschitz-Margin Training: Scalable Certification of Perturbation Invariance for Deep Neural Networks (2018, methodology): “While prior work required separate analysis for slightly different components [29, 24, 7, 26], we provide a more unified analysis.”
Abduction-Based Explanations for Machine Learning Models (2018, background): “More-over and as the experimental results suggest, the approach still applies (with no conceptual modiﬁcation) if one opts to use oracles other than an ILP solver (Katz et al. 2017; Ruan, Huang, and Kwiatkowska 2018; Gehr et al. 2018; Dutta et al. 2018).”
The Marabou Framework for Verification and Analysis of Deep Neural Networks (2019, methodology): “The formal methods community has taken initial steps in this direction, by developing algorithms and tools for neural network veriﬁcation [5,9,10,12,18,20,23,24].”
Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks (2019, background): “Using Lipschitz bounds in the context of adversarial robustness and safety verification has also been addressed in several works [39, 31, 38].”
Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for L0 Norm (2018, background): “DeepGO [22, 23] shows that most known layers of DNNs are Lipschitz continuous and presents a veriﬁcation approach based on global optimisation.”
Adversarial Examples on Object Recognition (2020, background): “The publications discussed in Section 4, however, give statistical guarantees to robustness [9, 142, 171].”
Towards Trustable Explainable AI (2020, methodology): “This has given rise to a growing interest in validating the operation of ML models [Ruan et al. , 2018; Narodyt-ska, 2018; Narodytska et al. , 2018b; Katz et al. , 2017] but also motivated efforts aiming at devising approaches to ex-plainable artiﬁcial intelligence (XAI) [Ribeiro et al. , 2018;…”
Concolic Testing for Deep Neural Networks (2018, methodology): “In [20, 24], Lipschitz continuity has been shown to hold for a large class of DNNs, including DNNs for image classification.”
Feature-Guided Black-Box Safety Testing of Deep Neural Networks (2017, methodology): “alue of ‘is in [0;1], dependent on the network, and can be estimated by examining all input examples 0in the training and test data sets, or computed with provable guarantees by reachability analysis [33]. The following theorem can be seen as an instantiation of Theorem 3 by using Lipschitz continui”
A Safety Framework for Critical Systems Utilising Deep Neural Networks (2020, methodology): “Formal verification [24,27,66,21,37,64,48,65,49,30] and coverage-guided testing [61,44,59,38,60,62] currently form the two major classes of V&V techniques for DL, from which a collection of evidence may be obtained that supports the partial prior knowledge.”