An approach to reachability analysis for feed-forward ReLU neural networks

By Alessio R. Lomuscio, Lalit Maganti. 2017

387 citations recorded by the source corpus.

We study the reachability problem for systems implemented as feed-forward neural networks whose activation function is implemented via ReLU functions. We draw a correspondence between establishing whether some arbitrary output can ever be outputed by a neural system and linear problems characterising a neural system of interest. We present a methodology to solve cases of practical interest by means of a state-of-the-art linear programs solver. We evaluate the technique presented by discussing the experimental results obtained by analysing reachability properties for a number of benchmarks in the literature.

Subfields: Artificial Intelligence, Control and Systems Engineering, 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 Control and Systems Engineering

In Electrical and Electronic Engineering

In Safety, Robustness & Interpretability

Citations in the corpus

Certified Adversarial Robustness via Randomized Smoothing (2019, methodology): “Exact methods are usually based on Satisfiability Modulo Theories (Katz et al., 2017; Carlini et al., 2017; Ehlers, 2017; Huang et al., 2017) or mixed integer linear programming (Cheng et al., 2017; Lomuscio & Maganti, 2017; Dutta et al., 2017; Fischetti & Jo, 2018; Bunel et al., 2018).”
Provable defenses against adversarial examples via the convex outer adversarial polytope (2017, methodology): “We begin by considering a characterization of the exact adversarial polytope of a deep network; a very similar approach is used in Lomuscio and Maganti [2017], though we include it here for completeness, as the adversarial polytope plays a foundational role in our subsequent main contribution in…”
Reachability Analysis of Deep Neural Networks with Provable Guarantees (2018, methodology): “ive, high-level comparison of our method with several existing approaches that have been used for either range analysis or veriﬁcation of DNNs, including SHERLOCK [10], Reluplex [7], Planet [26], MIP [11, 9] and BaB [12], as shown in Fig. 8. We investigate these approaches from the following seven a”
Scaling provable adversarial defenses (2018, background): “considered in empirical works), we are still able to achieve 71% provable robust error; for comparison, the best empirical robust performance against current attacks is 53% error at = 8/255 Madry et al. [2017], and most heuristic defenses have been broken to beyond this error Athalye et al.”
Provably Robust Deep Learning via Adversarially Trained Smoothed Classifiers (2019, methodology): “Exact methods, usually based on Satisfiability Modulo Theories solvers [18, 11] or mixed integer linear programming [33, 24, 12], are guaranteed to find an adversarial example around a datapoint if it exists.”
Towards Fast Computation of Certified Robustness for ReLU Networks (2018, methodology): “Moreover, the time complexity of computing the output bounds of an m-layer ReLU network with Theorem 3.5 and Corollary 3.7 is polynomial time in contrast to the approaches in (Katz et al., 2017) and (Lomuscio & Maganti, 2017) where SMT solvers and MIO solvers have exponential time complexity.”
Output Range Analysis for Deep Feedforward Neural Networks (2018, background): “Recently, Lomuscio and Maganti present an approach that encodes neural networks into MILP constraints [18].”
Strong mixed-integer programming formulations for trained neural networks (2018, background): “Our contributions are depicted in Figure 1. It serves as a roadmapof the paper. 1.3 Relevant prior work In recent years a number of authors have used MIP formulations to model trained neural networks [19,22,24,29,40,47,54,64,66,67,70,80,81], mostly applying big-M formulation techniques to ReLU-based”
MixTrain: Scalable Training of Formally Robust Neural Networks (2018, background): “[63], [64] can provide more accurate approximations but only works for one or two layers networks.”
Efficient Neural Network Robustness Certification with General Activation Functions (2018, background): “For ReLU networks, finding the minimum adversarial distortion for a given input data point x0 can be cast as a mixed integer linear programming (MILP) problem [21, 22, 23].”
Evaluating Robustness of Neural Networks with Mixed Integer Programming (2017, methodology): “Complete verifiers typically employ either MILP solvers [10, 12, 15, 28] or SMT [6, 14, 26, 34].”
Training for Faster Adversarial Robustness Verification via Inducing ReLU Stability (2018, methodology): “Exact verification of networks has been the subject of many recent works [15, 9, 3, 30, 19, 6].”
Piecewise Linear Neural Network verification: A comparative study (2017, methodology): “Lomuscio & Maganti (2017) and Cheng et al. (2017b) advocate the use of big-M encoding to achieve this.”
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.”
Algorithms for Verifying Deep Neural Networks (2019, methodology): “NSVerify [1], [23] encodes the network as a set of mixed integer linear constraints.”
A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks (2019, methodology): “…linear networks in general), exact veriﬁers solve the robustness veriﬁcation problem (1) by typically employing MILP solvers (Cheng et al., 2017; Lomuscio & Maganti, 2017; Dutta et al., 2018; Fischetti & Jo, 2017; Tjeng et al., 2019; Xiao et al., 2019) or Satisﬁability Modulo Theories (SMT)…”
Provable Certificates for Adversarial Examples: Fitting a Ball in the Union of Polytopes (2019, methodology): “Binary networks were trained to distinguish a subset of 1’s and 7’s from the full MNIST dataset.”