Output Range Analysis for Deep Neural Networks

By Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, Ashish Tiwari. 2017

125 citations recorded by the source corpus.

Deep neural networks (NN) are extensively used for machine learning tasks such as image classification, perception and control of autonomous systems. Increasingly, these deep NNs are also been deployed in high-assurance applications. Thus, there is a pressing need for developing techniques to verify neural networks to check whether certain user-expected properties are satisfied. In this paper, we study a specific verification problem of computing a guaranteed range for the output of a deep neural network given a set of inputs represented as a convex polyhedron. Range estimation is a key primitive for verifying deep NNs. We present an efficient range estimation algorithm that uses a combination of local search and linear programming problems to efficiently find the maximum and minimum values taken by the outputs of the NN over the given input set. In contrast to recently proposed "monolithic" optimization approaches, we use local gradient descent to repeatedly find and eliminate local minima of the function. The final global optimum is certified using a mixed integer programming instance. We implement our approach and compare it with Reluplex, a recently proposed solver for deep neural networks. We demonstrate the effectiveness of the proposed approach for verification of NNs used in automated control as well as those used in classification.

Subfields: Artificial Intelligence, Computer Vision and Pattern Recognition

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

Citations in the corpus

Certified Adversarial Robustness via Randomized Smoothing (2019, methodology): “, 2017) or mixed integer linear programming (Cheng et al., 2017; Lomuscio & Maganti, 2017; Dutta et al., 2017; Fischetti & Jo, 2018; Bunel et al., 2018).”
Reachability Analysis of Deep Neural Networks with Provable Guarantees (2018, methodology): “, 2018b], output range analysis [Lomuscio and Maganti, 2017; Dutta et al., 2017], and robustness comparison.”
Will Distributed Computing Revolutionize Peace? The Emergence of Battlefield IoT (2018, background): “Preliminary results also exist on extending symbolic reasoning engines that have had signiﬁcant impact on techniques in Formal Methods, to establish safety bounds on data-driven learned models [35].”
Algorithms for Verifying Deep Neural Networks (2019, methodology): “Representative methods for search and optimization include Reluplex [30], Marabou [31], Planet [32], Sherlock [33], Venus [34], PeregriNN [35], and BaB [36] and its extensions [20], [37], [38].”
Exactly Computing the Local Lipschitz Constant of ReLU Networks (2020, background): “There is a deep body of work using mixed-integer programming to verify the robustness of a neural network (Lomuscio & Maganti, 2017; Fischetti & Jo, 2018; Tjeng et al., 2017; Dutta et al., 2017; Cheng et al., 2017; Xiao et al., 2018).”
Strong mixed-integer programming formulations for trained neural networks (2018, background): “2 Relevant prior work In recent years a number of authors have used MIP formulations to model trained neural networks [14,16,20,25,31,37,43,45,46,48,54,55], mostly applying big-M formulation techniques to ReLU-based networks.”
Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for L0 Norm (2018, background): “Moreover, [12] considers determining if an output value of a DNN is reachable from a given input subspace, and reduces the problem to a MILP problem; and [3] considers the range of output values from a given input subspace.”
Learning and Verification of Feedback Control Systems using Feedforward Neural Networks (2018, methodology): “We would like to design h so that the resulting closed loop C satisfies some desirable properties such as safety, reachability of a given target, region stability (Podelski and Wagner [2007]), or a general property defined in a suitable logic such as Signal Temporal Logic (STL) (Donzé and Maler [201”