Computing Preimages of Deep Neural Networks with Applications to Safety
Authors: Kyle Matoba
François Fleuret
Venue:  (2021)
Keywords: Deep neural networks
verification
interpretation
AI safety
ACAS

Abstract: To apply an algorithm in a sensitive domain it is important to understand the set of input values that result in specific decisions. Deep neural networks suffer from an inherent instability that makes this difficult: different outputs can arise from very similar inputs. 

We present a method to check that the decisions of a deep neural network are as intended by constructing the exact, analytical preimage of its predictions. Preimages generalize verification in the sense that they can be used to verify a wide class of properties, and answer much richer questions besides. We examine the functioning and failures of neural networks used in robotics, including an aircraft collision avoidance system, related to sequential decision making and extrapolation.

Our method iterates backwards through the layers of piecewise linear deep neural networks. Uniquely, we compute \emph{all} intermediate values that correspond to a prediction, propagating this calculation through layers using analytical formulae for layer preimages. 



Under review as a conference paper at ICLR 2021
COMPUTING PREIMAGES OF DEEP NEURAL NET- WORKS WITH APPLICATIONS TO SAFETY
Anonymous authors Paper under double-blind review
ABSTRACT
To apply an algorithm in a sensitive domain is important to understand the set of imput values that result in specific decisions. Deep neural networks suffer from an inherent instability that makes this difficult: different outputs can arise from very similar inputs.
We present method check that the decisions of deep neural network tended by constructing the exact, analytical preimage of its predictions. Preimages generalize verification in the sense that they can used to verify wide class of properties, and answer much richer questions besides. We examine the function- ing and fallures of neural networks used in robotics. including an aircraft collision avoidance system, related to sequential decision making and extrapolation.
in-
Our method iterates backwards through the layers of piecewise linear deep neural networks. Uniquely, we compute all intermediate values that correspond to prediction, propagating this calculation through layers using analytical formulae for layer preimages.
INTRODUCTION
Folk wisdom holds that although deep neural networks (DNNs) achieve excellent predictive accuracy, reasoning about their performance is difficult, even for experts. Our goal is to enable non- expert stakeholders, such clinical health workers, investors, or military commanders build trust a statistical model in high-stakes environments. To do this, we posit that decisionmakers want to understand a model in both directions, both from inputs outputs, but also being able to start with hypothetical outputs, and understand the inputs that lead to them.
In this paper, we develop an equivalent, but much simpler, representation of certain class of DNN classifiers. This representation, which requires only basic numeracy to productively interact with, can be used by domain experts to build intuition and trust. We apply this method to a reinforcement learning agent trained to solve the cart-pole problem, and find that DNN implementing successful policy makes particular type of mistake on 24% of the mass of the 1 1/8th of the state space for which we know the optimal action (Section 3.2). We also show how using the preimage in place of verification can yield a more efficient and interpretable end-to-end system for analyzing aircraft collision avoidance systems (Section 3.3).
1.1 PREVIOUS WORK
DNNs have the property that knowing the output tells us very little about the input it corresponds to. This is most apparent image classifiers, where totally different outputs can arise from inputs that are visually indistinguishable (Szegedy et al.) (2014)). We build upon the mathematical framework developed for verifying DNNs that grew out a desire to prove the absence of adversarial examples, for example Tjeng et al. (011)) and Wong & Kolter (2017). However, we depart from these studies along with Katz et al. (2017). being more oriented towards small DNNs that map to and from low- dimensional spaces with considerable structure. These DNNs arise especially in systems which interoperate with the physical world, for example mapping measurements positions and velocities movements. Table Jorients work to the literature.

---

Under review as a conference paper at ICLR 2021
Commonly called
What is computed
Examples
Verification
(S, X.YY + +1-----==== s(x)n==))
Wong & Kolter (2017
Reachability
f(X)
Yang et al. (2020)
Inversion
- (1Y)+
Carlsson al. 2017
Preimage
This paper
Table 1: A laxonomy of previous work on inversion and verification. Here f 1 R is
DNN, X S R E R" Y - ER,, and E R f-1 is its inverse in the sense that f = {x fY)
We have phrased verification in this unusual fashion facilitate comparison with the other points. Stated in the familiar application to image classifiers X would be epsilon ball around an input, and Y would be the halfspace where one coordinate is higher than all others.
Verification ultimately amounts to simple yes no, and so answering higher-level questions typ- ically requires many verifications: for example, Katz et al. (2017) describes a suite of 45 tests, and image classifiers often wish to verify the absence of adversarial examples around the entire train- ing set. Yang et al. (2020) is an interesting extension to verification in that it computes the entire image of, say, epsilon ball around data point, and not just whether it intersects with decision boundary.
Reasoning forward, about the outputs that can arise from inputs, is only half of the picture. Carlsson jet al.] (2017) and [Behrmann et al.] (2018) are oriented backwards, they attempt to reconstruct the inputs that result in an output. These related papers study the statistical invariances that nonlinear layers encode. [Behrmann et al. (2018) examines the preimage of a single point through a single ReLU layer, analyzing stability via analyzes the preimage of single point through the repeated application of a nonlinearity, purely theoretically. Our paper looks at the preimage of non-singleton subsets of the codomain, which is much more practically useful, and requires considerable extension to their approaches.
ixproximation-baseee experiment. Carlsson et al. (2017)
2
METHOD
Our method is easily stated: build up the preimage of DNN from the preimage of its layers, using simple analytical formulae. We start by developing some properties of the preimage operator, then we describe the class of sets that we compute the preimage of, and finally discuss the class of DNNs that our algorithm addresses.
2.1 PROPERTIES PREIMAGES
Lemma shows how to build up the preimage of DNN from the preimages of its constitutent layers.
Lemma 1 (Preimage of composition reversed composition of preimages). For functions f, R"y + 174+1
(fe+ o o........
o...o fātk- fetR-
Secondly, we mention an intuitive property of 1-1 that handy for building up the preimage of any set from the preimages of any partition of that set.
Lemma 2 (Preimage of union is union of preimages).
f-1 (U) = (
2.2 POLYTOPES
Our method is not applicable to arbitrary sets Y, but rather sets that, roughly, have piecewise linear boundaries. The basic building block of these polytopes.
2

---

Under review as a conference paper at ICLR 2021
Definition 1 (Polytope). A polytope in R" is that can be written {a R : Ar 2 0} for some m E N, b E RRt,, and E I
Put more simply: polytope the intersection of half-planes. Definition does not require that polytopes be bounded, but polytopes are convex. Sets with linear boundaries, though they may be non-convex, can decomposed into the union of polytopes. We term such sets region-unions. and the set of polytopes which comprise them, regions.
Definition 2 (Region and region-union). For N E N, E R" A Imxx, with my E N, region
(1 : b, - A -0 LI.
(2)
A region-union is a set UrER r for some region R.
Region-unions are interesting because the preimage polytopes under piecewise linear functions are regions-unions. However, we need to also keep information on how to form region-union, hence the notion of a region. It is trivial observe that R2 and Rg are regions, then R2 R2 likewise region, and correspondingly for region-unions,
2.3 LINEAR AND RELU POLYTOPE PREIMAGES
In this section, give formulae for the preimage of linear and ReLU functions, giving significant The preimage of polytopes under linear mappings are polytopes:
content to Lemma I|
Lemma (Preimage of Linear layer).
(x Wx+ ({x Ax 2 0}) = fx (b Aa)
AWx 2 0}.
(3)
ReLU is a piecewise linear function, so we carefully treat the portions of the domain on which exhibits different behavior, obtain a similar formulation for each:
Lemma 4 (Preimage of ReLU layer).
ReLU
(fx b Ar 2 0})
U tx: b Adiag(v)x 2 0, -diaga - v) 2 0, diag(()) 0}.
(4)
(0.0)))
To understand Lemma 4 let (ar) be the vector given by s(x); = if 2 0 and zero otherwise. Then diag(s(z))> = (x) This expression separates æ ++ ReLU(z) into a pattern signs over its coordinates and itself. This means that once restrict attention to set which the sign does not change, we can apply familiar linear algebra routines to compute the preimage set, akin to Lemma 3 The nonnegative values denoted by {0. 13 in the above, and the set of x such that 24 2 +> P; = 1 is given by diag(v)r > 0. Similarly, x; < 0 + Vi = 0 for i 1,2,......... .,, and only if diag(1 v)x Equation fooloow by partitioning R. into the 2 sets where each coordinate is nonnegative not.
Computing the preimage of ReLU layer unavoidably intractable scale, though the problem exhibits considerable structure. We expect that it is possible to compute the preimage of networks of a similar scale to those that can be completely verified, such small image-scale networks. Preimages are most insightful and useful when the inputs and outputs have definite interpretation application areas where the need for massive networks less.
2.4 THE SUFFICIENCY OF LINEAR AND RELU LAYERS
In familiar terms DNN classifier might consist of some "feature building" modules, say composed of alternating convolution and maxpooling, then flattened, and passed onto the prediction logic consisting of alternating linear and ReLU layers, possibly including dropout or batch normalization, and concluding with softmax function to normalize the predictions to probability distribution. Resnets (He et al. (2016)) do not strictly fit this pattern, bu can be handled with similar reasoning (see Appendix B).
3

---

Under review as a conference paper at ICLR 2021
How do the results of Section 2.3 suffice to invert such DNNs? Firstly, under convention that layers operate on flat tensors, flattening is superfluous. Next, dropout affects inference only through the weights this layer be omitted entirely in computing the preimage. Convolution is sentially linear. Maxpool is straightforwardly rewritten in terms of the ReL.U and linear function. {x: (softmax(2z) 0} is not polytope. However, if the classification alone suffices then the softmax layer can be elided entirely since arg max, Iz = arg max, softmax(z)).
EXPERIMENTS
3.1 TWO MOONS CLASSIFICATION
To cultivate some intuition about the preimage of DNN we start by examining a classic test prob- lem in nonlinear classification. We fit DNN [-3, +3)² R² consisting of two nonlinear layers with eight neurons each on an instance the "two moons" dataset. This data is shown in Figure Ta (further details of details of f and the data in (Section D.I). Figure 1b plot the corresponding
logits, along with the sets to be inverted {x 21 & x2) C R Figure Ic shows the correspond-
ing preimages, with different hues of the same color corresponding to different sign patterns in Equation 4
(a)
(b)
Figure 1: Inversion of a simple DNN ?R2 + R2 fit to the "two moons" data shown in Figure la In Figure lb are the logits from simple DNN corresponding each data point computed with an inference pass, along with the decision boundary. Figure Ic shows the preimages comprised of polytopes that form the region-union.
3.2 CART-POLE REINFORCEMENT LEARNING AGENT
In the "cart pole" control problem pole is balanced atop cart which moves along a one dimen- sional track (Figure 2}. Gravity pulls the pole downward, the falling of the pole pushes the cart, and external movement of the cart pushes the pole in turn. The control problem is to keep the pole upright by accelerating the cart.
In the formulation of Brockman et al. (2016) controller inputs are: the position of the cart, æ, ve- locity of the cart á, the angle of the pole 0 from upright, and the angular velocity of the pole ú. Possible actions are accelerate the cart in the positive or negative direction. The reward envi- ronment encourages balancing by unit reward per period before failure, where failure means that the pole is not sufficiently upright (0 I-x/15, + /15)), or the cart near enough the origin (ar 2.4, 2.4)). have no prescribed limits for and Ó, but via a methodology described in Section 1 we interpret these states taking values in [-00, +3.0 [-3.5, +3.5).
Consider still cart and pole (i 0 0), with the cart left of zero (x < 0) and the pole left of vertical (0 < 0). Keeping I and 9 near zero is preferable, since these are further from failure, so moving left will steady 0 but worsen ar. Nonzero velocities make this reasoning
complicated, but configuration is unambiguous: if x 0, < 0, > 0, 2 0, then pushing right is clearly

---

Under review as a conference paper at ICLR 2021
-2.0
-1.0
+0.0
+1.0
+2.0
+0.2
+0.1
+0.0
T
-0.1
-0.2
T
The state space of the cart pole prob- lem, schematically. Here S (the cart is left of the origin), & < (the cart is moving left- ward), 2 0 (the pole is right of vertical), and i 2 0 (the pole is moving rightward).
Figure 2:
Projection of subsets of the domain where the wrong action taken, with the hue of the area being proportional to the volume of the wrong sets, divided by the volume the projec- tion.
Figure 3:
the correct action. Figure 2 gives depicts value in this orthant. Let D+1 = (-oc, 0J² x o0) and correspondingly, let D [0, ) x (-00, 0J2.
We fit one hidden layer neural network control function f R² - I22 using policy gradient reinforcement learning. Details of this calculation of balancing the pole: in 1000 trials of 200 periods, (x. B) remains uniformly in [-.75, +.75 x [-.05,+.4 +-05 with very low velocities. Nonetheless there are many states for which pushing right clearly the correct action, but for which the DNN controller predicts -1: 1: in the same simulation of 1000 trials 200 steps, roughly 7% of actions performed by the agent fail this sanity check. This behavior not numerical fluke it holds if we consider states only nonnegligibly interior to D+1 and D- and also if we only count predictions that are made with probability greater than ,51. One such pockets of counterintuitive behavior is
Seccion D.2] This agent achieves goal
[-2399 1.442] x 1-2.922, 2.262 [+1.798 10- +0.1166] [+1.399, +1.728] n R x2))-
We find this box large for example the first coordinate comprises almost 20% of that dimension of the state space. The size this box is even more suprising because is inscribed within larger polytope (using the algorithm of Bemporad et al. 2204)) that has volume about 40 times larger. The total volume in R of these sets 3% of the state space volume, and thus 24% of the volume of D_, D+1- Figure 3 parses this surprising fact bit further by plotting the projection of the four-dimensional domain onto the (x, 0) plane. The hue the gray is proportional to the volume of darker
the four-dimen nour-dimensional polytope divided by the volume of the two-dimensional projection,
areas mean more ( 0) mass that is wrong. Since the entirety of the second and fourth quadrants
grey at every (x, 0) 2-2.4 +2.4 I-m/15, + /15 there are some (#, 0) where the wrong action will be taken.
3.3 COLLISION AVOIDANCE SYSTEMS
The final application shows how to use domain knowledge to anticipate dangerous behavior of DNN in complex modelling domain.
5

---

Under review as a conference paper at ICLR 2021
3.3.1 BACKGROUND
Aircraft automated collision avoidance systems (ACAS) are navigational aids that use data on air- craft positions and velocities to issue guidance evasive actions to prevent collisions with intrud- ing aircraft. The ACAS developed in Kochenderter & Chryssamhaccoooloss (201T) uses dynamic programming formulate the optimal control of partially observed Markov process, and issues advisories to optimize a criterion that penalizes near collisions and raising false or inconsistent warnings. Unfortunately, evaluating the policy function is too resource-intensive run on certified avionics hardware. Small DNNs have been been found to be adequate approximators that require little storage and can perform inference quickly. downside of this approximation that even accu- rate DNNs can give very wrong predictions that when another aircraft is nearby and approaching from the left, a DNN- approximation need not advise the correct action of turning right aggressively.
some inputs Katz et al. (2017), for example show
Verification can check that one-step behavior in DNN-based ACAS behaves as intended. However, it cannot answer higher level questions like "will near-collision occur if this policy is followed?" The idea ofliia & Kochenderfer (2019) is to verify dynamic properties of such systems by com- bining single-step verification with worst-case assumptions about randomness in state transitions and (constrained) behavior of other aircraft.
3.3.2 DISCRETIZE AND VERIFY: JULIAN & KOCHENDERFER 2019
In Julian & Kochenderfer 2019). the state con- sists of x and y distances between the two aircraft, and an angle of approach angle between them, th. The actions are five turning advisories: (1) "clear of conflict" (COC), (2) weak left [turn] (WL), (3) strong left (SL., (4) weak right (WR), and (5) strong right (SR). The initial condition is given by the boundary of the domain where the distance of the intruding aircraft are at their maxima. Transi- tion dynamics are denoted by (a, S). a set-valued function which gives the set of states that are reach- able from states in S under action a. encom- passes both randomness in the transition, and be- havior of the other aircraft. The change in (ar, y) controlled by the angle between the crafts, and the update to the angle is the difference between the turning of the two crafts, with some randomness. To compute the states that can arise under a pol- icy, the idea is to begin from an initial set of states that are known to be reachable, and to iteratively
9
Volume fraction
40
0.05128
80
0.02532
120
0.01681
160
0,01267
200
0.01005
Table 2:
Quantifying the inefficiency of dis- cretization: Each of the three dimensions, (z, y. v) is discretized into grid of size g, so that the domain is partitioned into g" cubes. We present the fraction of the cubes for which all eight corners of this cube do not evaluate to the same prediction, which is sufficient con- dition for the cell to intersect with a decision boundary.
append states that reachable from any of those states, until fixed point is reached. U denotes the set of states that we wish to preclude.
This idea formalized by Julian & Kochenderfer (2019) Algorithm Because multiple advi- sories will be issued whenever a cell straddles the decision boundary, the discretized algorithm will wrongly include some states as reachable since a worst-case analysis needs take account of all reachable states. [able 2 gives an indication of the magnitudes of overestimation, presenting how much of the state space will lead to multiple advisories under a simple discretization scheme.
Julian & Kochenderfer (2019) do not use an equispaced grid, but the basic point that discretization error cannot be made negligible- is an inescapable feature of this approach. And any false positives in single-step decision function will be amplified in the dynamic analysis, more reachable states at one point time lead to even more reachable points at the next step, so a 1% overestimation at one step may be compounded to considerably more through the dynamics. Coincidentlly, Julian & Kochenderfer (2019) are able to reach a usable solution, but are unable to guarantee the absence of near collisions under some realistic parameter configuations.
Note how the cells can be traversed in any order. This is a simple way to see that this algorithm is not fully using the spatial structure of the problem. Next, incorporate this knowledge.

---

Under review as a conference paper at ICLR 2021
Data: Maximum distance Ro, policy f, "unsafe set" U, transition dynamics V, encounter length T.
Result: Guaranteed to not reach unsafe state from Rg under policy f?
initialization: t = 0, done = False;
Partition the state space into cells с C:
while not done do
t ++++:
R. 0;
for e E such that c RA-1 + do
for i such that [(e) n {x 2 xj for + + do
for d' C such that (i, # do
R₂ R2 Ud
end
end
end
done= R2 = - or #ort
end
Return R, nu
Algorithm 1: Algorithm from Julian & Kochenderfer (2019) for computing whether unsafe
set U can be reached under a policy /' beginning from Rg under transition dynamics
3.3.3 OUR PREIMAGE-BASHI ALTERNATIVE
Rather than looping first the domain, then over actions those points, Algorithm loops over actions and, using the preimage, computes all reachable points under that action.
Data: Ru, U, V, T.
Result: Guaranteed to not reach an unsafe state from Rg under policy f?
initialization: / = 0, done False;
for i = 1, 1,2,..., n2 do
E, = f(x xa 2 ny for j + i1)
end
while not done do 1= 1 1+;;; 1;
R2 0;
for i 1,2. 7 do
R, - R, (i RR-1):
end
done= = Rr = - Un
end
Return U UnR, R2 == 0.
Algorithm 2: Our preimage-based based, exact algorithm for computing the dynamically reachable states an ACAS.
While Algorithm is exact will never wrongly say that a state can be reached the accuracy of Algorithm is ultimately controlled by the number of cells, |C]. This is because is necessary to perform ni verifications for each reachable cell, and the number of reachable cells proportional to Cl. Let V denote the cost of verification. Verification is known to be NP-complete (Katz et al. 2017 ) so dominates all others calculation such as computing intersections or evaluating (tt c). Thus, the computational cost of Alggorihmm ii V((CVVn)) In Algorithm 2 must initially compute ny preimages which dominates the entire calculation, which consists of relatively fast operations applying the dynamics and computing intersections up 7 times, for T a number around 40.
Let P denote the cost of computing a preimage, then Algorithm 2 is O(Pn)). So whilst dispenses with the need to solve O( [C) verifications, but may be more intractable if P is significantly higher than V. Let the dimensions of the nonlinear layers in a DNN be ny, then because in the worst case it necessary check each nonlinearity, each of which be independently in a negative or positive configuration, V 0 nc, Exact verification for even single cell is impossible present for

---

Under review as a conference paper at ICLR 2021
+25
+20
+15
COC
SR
+10
SL
WR
WL
+5
0
A
-5
-5
+5
+10
+15
+20
+25
+30
Figure 4: An encounter plot showing the optimal action at each (ar, y) distance configuration for a fixed angle of approach, indicated by the perpendicular orientation of the red (intruder) aircraft. Distances are measured in kilofeet.
large networks. We believe that preimages be computed roughly (within small constant factor) as easily as a verification - P OVV). We are currently developing this conjecture formally, the idea is that, as shown in Lemmmma 4| each nonlinear layer generates up 2n sets, the preimage of which must be computed through earlier layers.
In any case, is true of any exponentially hard problem, the practical tractability of both P and V hinges importantly upon theoretical arguments showing that not all 2 configurations of the nonlin- carities of an n-dimensional layer be achieved (Serra et al. (2017) Hanin & Rolnick (201i (2019), and clever implementations that take account of the structure of the problems (e.g. TTjeng et al. (2017)
Katz al. (017
The distinction between the two algorithms is made clearer by examining an encounter plor such as Figure 4 Encounter plots are concise summarizations of the policy function, here depicting the possible advisories, for a fixed angle of approach (which is here conveyed by the orientation of the aircraft relative the black). This figure, which replicates Figure of Julian Kochenderfer 2019), differr from it in crucial respect: it is depicts the malytically-compptie five sets where each the advisories are issued (details of the experiment are in |Section D.3). The shaded areas arise from plotting polytopes, in Algorithm 2] Julian & Kochenderfer (2019), the other hand, produce such plots by evaluating the predictions the network on a fine grid. The different manner in which the plots are produced is exact analogue of the different way that the networks are summarized and analyzed through time.
preimage of the
4 CONCLUSION
In many areas, safety and interpretation inhibit the use of DNNs, because their use still requires a good deal of indirect experimentation and oversight to have confidence that it will not act in an unintuitive way. This paper has proposed computing the preimage of the decisions of DNN as an intuitive diagnostic that can help to anticipate problems and help domain experts gain trust a DNN, even if they are unable to formally articulate what makes DNN trustworthy. In order to do this, developed the preimage utility of the preimage to understand counterintuitive behavior from cart pole agent, and to more precisely characterize the set of states that would be reachable in an existing application of DNNs to aircraft automated collision avoidance systems.
DNN and presented an algorithm to compute We demonstrated the
8

---

Under review as a conference paper at ICLR 2021
REFERENCES
David Avis. A Revised Implementation of the Reverse Search Vertex Enumeration Algorithm, pp. 177-198. Birkhäuser Basel, Basel, 2000. URL https://daat /ttpp:s://ee...o1111.00000 00t.//..//000007.700
C. Bradford Barber, David P. Dobkin, David Dobkin, and Hannu Huhdanpaa. The quickhull algorithm for convex hulls, ACM Trans. Math. Softw. 22( 483, December 1996. ISSN 0098-3500. URL (tRt:t/:://dee
acm.
Jens Behrmann, Sören Dittmer, Pascal Fernsel, and Peter Maaß. Analysis of Invariance and Ro- bustness via Invertibility of ReLU-Networks, arXiv e-prints, Jun 2018. URL http:://axxxx
brg/aba/1806.0 09730
Alberto Bemporad, Carlo Filippi. and Fabio D. Torrisi. Inner and outer of using boxes. Computational Geometry, 27(2):151 - 178, 2004. URL https://doi..o.
of
IO0.0016/0025-7711 (03) 00048-8
Greg Brockman, Vicki Cheung, Ludwig Pettersson, Jonas Schneider, John Schulman, Jie Tang, and Wojciech Zaremba. Openai gym. 2016.
01540
Benno Büeler, Andreas Enge, and Komei Fukuda. Exact Volume Computation for Polytopes: A Practical Study, pp. 131-154. Birkhäuser Basel, Basel, 2000.
Stefan Carlsson, Hossein Azizpour, and Ali Sharif Razavian. The preimage of rectifier network activities. 2017. URL
Komei Fukuda. Lecture: Polyhedral computation, 2014. URL https: /inf//iinfffaa ethe. /h.
Komei Fukuda and Alain Prodon. Double description method revisited. In Michel Deza, Rein- hardt Euler, and loannis Manoussakis (eds.), Combinatorics and Computer Science, pp. 91-111, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. URL https:///dci.org/10..
3-540-61576- 87
Boris Hanin and David Rolnick. Deep ReLU Networks Have Surprisingly Few Activation Patterns. arXiv e-prints, Jun 2019. ott.://pp.../aarr....rr///////00
00904
Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun. Deep residual learning for image recog- nition. In 2016 IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pp- 770-778, 2016. URL /tttps://doi.oro
11199//.....99/.R..... 2016.90
Kyle Julian, Jessica Lopez, Jeffrey Brush, Michael Owen, and Mykel Kochenderfer. Policy compres- sion for aircraft collision avoidance systems. 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC), pp. 1-10, 09 2016. |
wttpthtt:///mm http://///oo...////....//// wttpg////11.10//SS..... 2016
[7778091
Kyle D. Julian and Mykel Kochenderfer. Guaranteeing safety for neural network-based aircraft collision avoidance systems. IEEE/AIAA 38th Digital Avionics Systems Conference (DASC), 2019. /RLLattps://oi. wwt./oii.rrrrgg// 101./11100//155555 2019. 9081748
Guy Katz, Clark Barrett, David I.. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In Rupak Majumdar and Viktor Kunčak (eds.), Computer Aided Verification. Springer International Publishing, 2017. URL https::/
doi. www.oorgg..... 00007777883-319-638777
Diederik P. Kingma and Jimmy Ba. Adam: A Method for Stochastic Optimization. arXiv e-prints, Dec 2014. WtRlpptt:///axxtti
oo //tgg//////// /atb///1/11. 1412. 6980
Mykel J. Kochenderfer and James P. Chryssantaacopollos. Robust Airbore Collision Avoidance
through Dynamic Programming. Massachusetts Instinute of Technology, Lincoln Labo-
ratory, Project Report ATC-371, 2011. URL https:: htttps::/www...
11. 11. .it. wwt.edidusssss....
def defaultt Coffaut//e httaaa//iieee/ppaaaaaatoooootooo htt.a//a....aa/ao/00//---////aea 2011 ATC-371.
WW- 21458. 458.pdf

---

Under review as a conference paper at ICLR 2021
Thiago Serra, Christian Tjandraatmadja, and Srikumar Ramalingam. Bounding and Counting Linear Regions Deep Neural Networks. arXiv e-prints, Nov 2017. RRLpttp::/ /arxiv. orq/ abs/ / 17 1711 02114
Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna Estrach, Dumitru Erhan, lan Goodfellow, and Robert Fergus. Intriguing properties of neural networks. January 2014. URL http://arxiv www.vvvorggbbbb///bee 61 99 2nd International Conference on Learning Repre- sentations, ICLR 2014; Conference date: 14-04-2014 Through 16-04-2014.
Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating Robustness of Neural Networks with Mixed Integer Programming. arXiv e-prints, Nov 2017. URL http:::/axxv..rg/////o 07356
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. arXiv e-prints, Nov 2017. URL http::/aaxxiv..rgabbss//// 00851
Kai Y. Xiao, Vincent Tjeng. Nur Muhammad Shafiullah, and Aleksander Madry. Training for Faster Adversarial Robustness Verification via Inducing ReLU Stability. ICLR 2019, Sep 2018. URL
http:///axiv..rrgabbsse
Xiaodong Yang. Hoang- Dung Tran, Weiming Xiang, and Taylor Johnson. Reachability Analysis for Feed-Forward Neural Networks using Face Lattices. arXiv e-prints, art. arXiv:2003.01222 2020.
01226
Hao Zhou, Jose M. Alvarez, and Fatih Porikli. Less is more: Towards compact CNNs. In European Conference Computer Vision, pp. 662 677, Amsterdam, the Netherlands, October 2016. URL 400
10

---

Under review as a conference paper at ICLR 2021
A PROOFS
A.1
PROOF OF LEMMA
Proof. Unroll Equation
Let S Ri- be arbitrary.
(fe+x o fetk-10.. .... fi) (S)
= (fe+* fe+k-1 .... ft)(z) E 5}
fx: Setx((ee+x-1 fetk-20... ft)(z)) e
(x: (Jeth-1 o.... (z) E (5)
(5)
=:
{ (fe+1 fi)(2) (Fe22 o... 0 (S)
f f((x) E (föt o fe-2 ....o (
-sz .... (/)
A.2
PROOF OF LEMMA 2
Proof.
DE f- (U =
f(z) E S +
f(z) S₁ or f(x) S2 or ... or f(x) E SN =
E (Si) or x (S)) E S2or or o =
x E (
Note that an identical argument shows that / ( (S.). This can useful in some applications where where S; can be wrtten V/ / E, writing U.S: as Vu,EE, may be more efficient.
B THE INVERSE OF A RESIDUAL BLOCK
The key function in residual block is
x + WWRr + x.
Combining arguments similar to Lemma and Lemma 4
we have that
Lemma (Preimage of residual block).
(2 + W2ReLU((12) 2) (fz b Ax 2 07)
=(x A(W.ReLU((i1x) + + 2 0}
(6)
U ( A(Wadiag(v)W: Z) 2 0, -diag(1 w) 2 0, diagg())Wir 2
(0(11))
C COLLECTING THIS ALL UP
Section 2.1 Section 2.2 Section 2.3 and Section 2.4 together give recipe for inverting wide class of image sets (region-unions) unions) for a wide class of DNNs (those which can be written as the composition of linear and ReL.U functions). To summarize the steps are:
11

---

Under review as a conference paper at ICLR 2021
1. Put the network into "standard form":
(a) Embed any transformations that are "off" at inference time, such as dropout or batch normalization into the weights.
(b) Rewrite the network in flattened form, for example replacing 3 x 32 x 32 tensors by 3072 x vectors. This is convention to facilitate polytope formulation.
(c) Rewrite all transformations as compositions of linear and ReLU functions. For exam- ple, convolution and average pooling are linear functions. Maxpooling, hard tanh, and leaky ReLU can be written as the composition of linear and ReL.U functions.
2. Let f = fr fL-1 ....o fi denote the network in this form.
3. Let R₁, U,A, be the image set that we wish to invert, for example Rr. A fx
21 2 x2) C TR22 a binary classifier.
4. Compute fi (A;) for all using Lemma or Lemma 4
5. Each term above a region-union, thus UzfZ'(A)
region-union.
6. By Lemma 2 R fL" (RL) = u.ff
7. Rr.-1 regiion-uioon union, so apply the same argument to compute R₁.-2 - (R
(7.
f2 o... 8. Repeat for = I 2, ...., to compute Rs = (R1) ... =si
= 02
fT (RL).
9. Appeal to Equation to conclude that Ry = f-
D DETAILS OF EXPERIMENTS
D.1 SECTION 3.1
The dataset of 500 observations is generated using the scikit-learn function sklearn. datasets make_moons moons with noise .2
Weights initialized according uniform (-vin features, in features distribution (the Py- Torch default), and were run for 1000 epochs of with a batch size of 128. Gradient steps were chosen by the adam optimizer (Kingma & Ba (2014)) with learning rate of 0.005 and (31,32) (0.9, 0.999).
D.2 SECTION 3.2
Our experiment is based upon the "CartPole-vI" environment from Brockman et al. (016). The fitting procedure is based upon the Monte Carlo policy gradient vignette from the Torch project with a considerably simplified control policy, consisting of DNN wih only five hidden units.
D.2.1 VELOCITY MAGNITUDE
As far as we can tell, there is no single best methodology for computing limits on the velocities (i: 8) in the cart pole problem. In premise, very high velocities could be supported by the discretization scheme, but these are unlikely to be achieved by any feasible sequence of actions. attention to limits described by actions, how should characterize the set of actions consider? For example, should we simply observe the behavior some non-optimized agent? Should we deliberate construct agents to pursue meleeity-maxmizing strategies? Should force agents to have the same initialization as that prescribed in the fitting?
we restrict
We concluded that an interpretable baseline which gave quantitative bounds robust details of parameterizations would be best. For this, we chose our limits on 9 the values that answer the question "how fast can the cart and pole be moving if we start from rest with the cart all the
httpp::///github.commmmm
Teaming/reiiforee..pp
12

---

Under review as a conference paper at ICLR 2021
T
2.4
0.5
2.3
1.0
2.2
1.5
2.0
2.1
2.5
5
10
5
10
0
0.2
3
0.1
2
0.0
0.1
0.2
5
10
0
5
10
Figure 5: The evolution of the cart pole state under a policy which continually accelerates left until failure (when 2 T 7/15), starting from rest, with the cart near the right boundary and the pole near its right boundary ((x, f 0, 0) = (2.39, 0, 220 0)).
way to the right, and the pole all the way to the left, and continually push left until failure?". This experiment is plotted in ingiurrre 5) where that the implied limits +3.0 and +3.5 for & and 0, respectively.
In addition to being easy to envision and interpret, a policy that pushes in uniform direction is natural boundary between benigh "dumb" policies and those that more actively seek to exercise worst-case scenarios through some deliberately degenerate behavior.
These limits largely agree with three the other candidates considered:
The same experiment, although constrained to obey the same initialization as in Brockman al. (006)) (these limits are tighter, understandably, roughly 2.25, 2.75 respectively).
A simple one- me-parameter agent which (starting from an initialization near the origin) seeks out high velocities by beginning to push in uniform direction, then switches to the oppo- site direction.
The most extreme values emitted from a small (and hence exhibitting more erratic behavior early the in the fitting) DNN that is able eventually achieve good performance.
13

---

Under review as a conference paper at ICLR 2021
D.3
SECTION 3.3
The analysis presented in Section 3.3 is based entirely on data generated by JJuiinn & Kochenderfer (2019)'s system that formulates and solves dynamic programs to deliver lookup tables of optimal collision avoidance behavior in the same manner as the FAA's proprietary software. Our DNN modelling somewhat different, however, and whilst we think that our results can be interpreted within their framework, in this section we detail the aspects of our analysis that differ from Julian & Kochenderfer (2019)s.
D.3.1 FITTING OPTIMIZATION CRITERION
The first manner in which our approach is different is the fitting criterion: Julian & Kochender- fer 2019) issue advisories as a function of position and velocities indirectly: by first fitting the continuation value to taking each action, and then choosing the action with the highest predicted continuation value. This oblique approach is understandable: this work is the continuation of an extended project to build [Kochenderfer & Chryssanthacopoulls (201T) and compress the Q-table (Julian et al. (2016), Katz et al. (2017)).
And although the Q-values themselves have some interpretation, issuing advisories requires only knowing the greatest. We hypothesize that it is easier to solve a problem which recognizes an invariance of the prediction to any increasing transformation. And that what we find-by replacing Julian et al. (016)) mean- rrean-squared-eeee cereede-err--bbee error-based criterion with cross entropy loss to directly model the optimal decision, we are able achieve better performance with smaller networks. One statement of the improvement is Julian & Kochenderfer (20e) use five layer fully connected layers with 25 neurons each to achieve an accuracy of 97% 98%. We are able to achieve comparable accuracy with two layer 25 neuron fully connected network (a network of the same size targetting MSE loss only attains an accuracy around 93%).
Why is anything less than complete fidelity to the Q-table acceptable in approximation? The answer seems to be twofold: firstly the Q-table is itself not perfect, because of discretization artifacts. One can observe physically implausible sawtooth-lit -iie decision boundaries that arise from coarse grid in the top plot of Dulian & Kochenderter (2019) Figure 4. The second is that accuracy alone does not capture the genuine metric of goodness, for example in the bottom plot of Figure 4 of Julian & Kochenderferi (2019) we see a highly accurate network that exhibits unusual "islands" of SR completely encompassed by region of WR that are both not present in the ground truth, and also prescibe a conceptually wrong relationship (a pilot could be initially advised a strong right turn, then after some period of lessened danger have downgraded to weak right, only have re-upgraded to strong right, seemingly although the danger continues to lessen). The correct metric seems to rather be plausibility of the prescribed encounter plot. These observation leads us not worry too much about small differences in model accuracies in favour of plausibility of the encounter plots.
D.3.2 FITTING SYMMETRY
The second manner in which our approach differs from Julian & Kochenderfer (2019) is in the domain being fitted. Julian & Kochenderfer (2019) fixed lookup table over (,, v/)
[-56000, +56000)2 x [-m, +T). However, we let Q R3 - R denote the Q-function as a function of the state (x, v, v), then the physics of the problem insure that
0
0
0
0
+1
0
0
+1
0
Q(Tis) T,Q(s) where 7, =
0
1
and To
0
+1
0
0
0
0
0
+1
0
+1
0
This relationship clearly only works for aprev = COC, but similar symmetries will exist more gen- erally. Thus, strictly speaking, half of the lookup table is unneeded, and moreover it would seem wasteful to ask a network to learn (what we already know to be) the same thing twice. Thus, our method is only fit ff over (z, ()) E [-56000, 2 [0, -T,, and when needed to infer f() = T,f (T,s) for s = (æ, y. 15) with e < O. In so doing, we halve the data set size, but leave other data fitting parameter unchanged.
14

---

Under review as a conference paper at ICLR 2021
To continue the analysis above describing comparable performance from smaller networks, exploit- ing symmetry enables us to achieve accuracy above 97% from one layer. 24 neuron network. For computational ease, Figure 4ss computed on 16 neuron network that achieves about 96% accuracy.
D.3.3 INVERSION PROJECTION
Figure 4 was formed by taking the fitted no DNN, fixing & to given value, and inverting the resultant no DNN (if W1, bj denote the weights and bias the original DNN, then projecting
()
onto the Wi Wi
0 84 = b, + Wi
0
E ADDITIONAL COMPUTATIONAL DETAILS
Definition as well as Lemma and Lemma worked with what known as the H representation of polytope. What Fukuda (2014) terms the "Minkowski-Wil Weyl Theorem" states that there is an equivalent representation, as the Minkowski sum of (1) a convex combination of vertices, and (2) conic combination of some rays.
Definition (Polytope (V representation), polytope in Rn is a set that can be written as
Σ Aees
for some vs E 12" rr R
The Minkowski Weyl Theorem assures us that Definition 3 is equivalent to Definition
To introspect DNNs it is handy have both the H and V representation of the preimage. Unfor- tunately, computing the V representation from the H representation is computationally challenging, both theoretically and practically. Analyzing formally the computational complexity of the problem is technical, and also complicated by host of special cases, but roughly speaking:
Evidently the complexity of the problem depends not only on the size of the input, but also the output.
Small inputs have large outputs. For example, cube in d dimensions has an H repre- sentation with 2d rows, but 2d vertices.
In general, there are no known algorithms that have polynomial time complexity in the input and output size.
For some polytopes, there are algorithms that have polynomial time and space complexity in the input and output. However, but this is still exponentially large in the dimension of the polytopes, again because output size can be exponentially large in the input size.
The more precise statements of this summary can found Fukuda 2014)) Section
Our problem may lie in some more easily-solved subclass of problems (though the fact that even simple geometric objects like cubes exhibit exponential growith of the output as function of the input dimension makes this perhaps less likely). Our review of the theoretical literature was unsuc- cessful int this regard, and empirically we observed empirically that the runtime of our calculation did rise at exponential-like rate with the dimension of the input. Thus: we did not find the naïve approach of computing the H representation of the preimage, then computing from that the representation to be practical.
Happily, when W is full rank, we can give the V representation corollary Lemma
15

---

Under review as a conference paper at ICLR 2021
Lemma 6. Suppose that W is full full-rank, and let W be its preudoinverse and W be a basis for the nullspace (with kth column W then. X 2 0, vj 2 0, i,
Wx+a Σ UiA= +
Σ rzy 5
E(w -a]di E(wiry)es + Σ Wi
k
(7)
Σ (Wiv; aa) E(wtry)os EW
Wh Th
where 7k 2 0, 7 2 0.
This is V representation with vertices (Wiv; - a) and rays (Wiry), W -1 W
Checking the rank of W, computing the pseudoinverse, and computing basis for the nullspace all quick and standard linear-algebraic routines.
For example, in our experiments were were unable come anywhere near computing the V rep- resentation of a an MNIST classifier (ne = 784) directly using a standard software such as cdd (Fukuda Prodon| (1996). However, for networks with 71-11 2 ny for all é 2 (which in our simple fitting procedure, was sufficient to insure that W would be full-rank), it was quite possible using Lemma 6) (1) compute the V representation of the polytopes to be inverted (these will be ten dimensional, and highly structured), then (2) apply Equation 7 7Jiteaaivvely backwards.
E. POLYTOPE DIMENSION
One slightly subtle point is that the terms in Equation 4 overlap at the boundaries, for example if b > then the origin is in fact contained in every term in the union. In this work, we only form full dimensional polytopes, roughly those which have strictly positive n-dimensional volume. Removing lower-dimensional sets does not change the union, so this does not substantively change the preimage. A study which was more explicitly interested in the details of decision boundaries might not want do make such a restriction. Some more discussion this point Secciin E.
We mentioned in Section 2.4tthat our analyses restrict attention to polytopes that have full dimension. Formally, the dimension of polytope is the maximum number of affinely independent points that polytope, minus one. And full dimensional polytop in Rd is one with dimension d. Geometrically, sets which are not full dimensional lie on the boundary between sets, and if they have a nonempty preimage, it will lie on boundary shared by another polytope, which does have full dimension.
This idea is made clearer by explaining how we check if a polytope has full-dimension. Algorithm 8.4 from Section 8.3 of Fukuda (2014) states that {x b Ar 0} is full-dimensional iff the optimization problem
maximize x subject to Ax + 1x S 5 x,
(8)
achieves positive criterion. Here 1 is conformable column vector of ones, representing the intuition that possible to loosen all inequality conditions by a strictly positive amount, meaning that there is some volume interior to the polytope. The ancillary condition that x S 1 is used to keep the problem well-conditioned.
Empirically, most sets in the region-union comprising Equation 4 are not full dimensional, and as soon as we know that an element of a preimage region is not full dimensional, we need not consider anymore. Future will will use more careful analysis to detect analytically when sets must necessarily be less than full dimensional, but for now we query each of the 2" subsets of the region-union. Thus most of computational time is spent in calculations of the form of Eqqution 8) We tested both Mosek and Gurobi as software for solving linear programs such as Equation 8 and found Gurobi to be faster.
16

---

Under review as a conference paper at ICLR 2021
Hidden layer widths
Accuracy
parameters
Storage (MB)
Time (s)
0.973
42
1.105
0.205
12
0.975
62
35,256
2.907
16
0.974
82
985.767
52.912
4
0,972
42
0.260
0.269
6 6 6
0.967
74
6.764
3.205
8
0,971
114
42.089
26.256
4 4 +
0.969
62
3.125
1,802
6 6 6
0.968
116
279.138
117.248
4 4
0.973
82
43.695
27.253
E.2 POLYTOPE VOLUME
In low dimensions, computing the volume of polytope from its V form is fast and space efficient. In the analysis presented in Section 3.2 we used the Qhull software which implements the Quickhull algorithm (Barber et al. (1996)) via scipy. spat ConvexHull, This computation scales poorly with dimension, however, for instance in our experiments it stopped being usable around ten dimensions. Büeler al. (2000) gives some "why" and "how" about this difficulty.
In high dimensions analysis of volumes seems difficult. However, if we already plan to compute the representation of the preimage also a highly complex operation we may be able to compute the volume "for free". Avis (2000) shows how to compute the volume rithm for converting between and V representation (solve the vertex enumeration problem), and seems quite plausible that the same ideas could be adapted to other algorithms that solve the vertex enumeration problem as well. We hope to investigate this further and possibly incorporate into software.
byproduct of his algo-
E.3 CLOCK TIME TO SOLVE PROBLEMS VARYING SIZES
In this section, we give sense of the computational difficulty of inverting a DNN. The general finding that for simple problems, one layer networks of around neurons, two layer networks of about 8 neurons apiece, or three layer networks of about six neurons apiece are easily inverted on a low-powered laptop, but the rate of growth empirically very fast. Certainly even the five layer, 25 neurons apiece networks employed in Julian & Kochenderfer (2019) are out of reach under the current implementation.
We do not use any multiprocessing, though the essential computation, checking polytope emptiness, embarassingly parallel.
We perform ten fittings and compute preimages per size, and report the average model accuracy, time to compute the preimage, and standard deviation each. To get a sense of the space complexity, also present the disk storage necessary to hold both the H and V forms of complete preimage partitiion (pickled dense numpy arrays float 64s). Since we do not re-tune hyperparameters across runs, accuracy is solely indicative.
All timings were performed on a 1.6 GHz Dual-Core Intel Core i5 CPU.
A more formal analysis of the complexity of the computation will follow in future work, will speed improvements from a more sophisiticated logic for handling empty preimage regions, along with further experimentation
"tricks" such sophisticated regularization clever initialization schemes that might enable greater modelling capacity without increasing the scale of the network (e.g. Zhou et (2016) Xiao et (2018)).
The problem is as described in Section 3.1 with further detail given in Section D.
17


Reviews:
[{"review_id": "jc6Zkbt-3q7", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The paper details a way of investigating the space of pre-images that lead to a particular output from a ReLU layer, with the goal of using the inverted representations as a way to understand the deep neural networks. Three experiments are proposed where the authors claim that the computed pre-images help interpret the network decision making. \n\nOverall the paper is interesting, however I am not certain of the novelty as some related work is not discussed. Additionally, although the practical application of the method is interesting, the clarity could be improved for the last experiment. \n\nPositives:\n* Understanding the invariances of neural networks can potentially lead to more interpretable models, and one way to investigate this is by looking at the preimages for a network. \n* The paper is a nice mix of theoretical results which lead to practical applications\n\nQuestions and Concerns:\n* The authors state that maxpool can be rewritten in terms of a linear component and a ReLU, but this is non obvious. If this is true, a mathematical formulation should be explicitly included in the paper. \n* The paper is missing some potentially related references. Previous work has investigated how multiple stimuli can get mapped onto (approximately) the same point in recognition networks by inverting the representations via iterative gradient descent (Mahendran & Vedaldi 2015, and recent work including invarianced based adversarial examples in Jacobsen et al. 2019 or model metamers in Feather et al. 2019). How does the proposed preimage computation help improve model interpretability beyond this previous work, especially given the authors statement that the method is intractable for large networks? \n* The paper does not discuss invertible networks which have a bijective mapping between the input and output (ie Invertible Residual Networks in Behrmann et al. 2019). Discussing this work seems relevant if the goal is to make models such that one can start with hypothetical outputs and understand the inputs that lead to them. \n* The final example of using this method in practice for ACAS systems is interesting, but it is difficult to follow what “success” would mean for this experiment\n\nMinor points: \n* The following sentence on page 3 seems to be missing something “Preimages are most insightful and useful when the inputs and outputs have definite interpretation – application areas where the need for massive networks is less.”.\n* There it a typo in the last sentence of page 3 (“bu”->”but”)\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "ZxXY6zONJnk", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The paper presents a method to verify if a NN is performing as expected in sensitive applications. Although the general area is very important in machine learning, the paper is not very well presented: The problem is not well stated, the approach is not very clear, and the results are not well justified.\n\n- The presentation and the writing of the paper should be improved. Unfortunately, with the current format it is hard to glean the idea of the paper. There are some typos (e.g., 'bu' in page 3, 'plot' in page 4, etc.).\n- There are some concepts that are not defined early on and maybe never in the paper. For example, what is the problem that the paper tries to solve mathematically? It is not very clear. What is the mathematical definition of a preimage?\n- The authors say: \"Preimages are most insightful and useful when the inputs and outputs have definite interpretation –\napplication areas where the need for massive networks is less\". Its hard to fully understand but it seems that the method suffers scalability issues. Can this be formally analyzed? What is the complexity of the algorithm in time and space? Why is there a scalability issue? Is it a fundamental problem? How does this limit the scope and applicability of the method? Also, what does \"definite interpretation\" mean?\n- The NN used in the experiments are very tiny. I would consider experiments that reflect more realistic situations in the real-world. Current setup significantly limits the scope of the method.\n- It is not clear how to verify the performance of the method. Results in Figure 1 and 2 does not show us the quality of the method, is it doing good or bad? I found the results in Figure 1 surprising as the moon data is fairly symmetric while the preimage is biased towards one class. Is there a reason for that?", "extra_scores": {}, "extra_text": {}}, {"review_id": "YIgezrKe4y_", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "There are many issues in the paper that can be improved.\n\nThe title is not appropriate, this work does not address safety applications. It is worth noting that the word safety is not defined and not used in the main body of the paper.\n\nIt is difficult to follow the presentation of the paper since mainly the applications are presented and then some contributions given, in the same presentation as the abstract.\n\nA major issue it that the paper is missing some important theoretical analysis. Of particular interest is the existence of the preimages, because not all outputs have inputs. Moreover, the uniqueness of the solution needs to be studied. These properties should depend on the used nonlinearities and architecture of the neural network.\n\nThere are many spelling and grammatical errors, such as “suprising”, “have been been”, “Coincidentlly”, “configuations”", "extra_scores": {}, "extra_text": {}}, {"review_id": "NoE09WESWRZ", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 2, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "Deep neural networks are known to be brittle, and can lead to dangerous consequences if left unverified. Forward reach set computation can be used as a basic primitive to verify properties of deep neural networks used in a robotic setting. There has been a rising interest in verifying larger neural networks used in safety critical setting. \n In this paper,  the authors propose a way to compute reachable sets for a neural network in a backward sense. Starting from the outputs of the neural network, and  then work it's way to the inputs. This is an interesting way to look at the problem itself,  but as the authors point out it is an intractable problem.\n\nMy concern about this paper is I don't see the use of a pre-image computation algorithm as being very useful. A forward reachability tool works pretty well for the size of neural networks considered in the paper. Pre-image computation does not provide any advantage in terms of scalability, as is apparent from the experiments. Moreover, almost any safety constraint that needs to be verified with system dynamics in the loop always should ideally work forward in time. Thus for the neural network controller from the inputs to the outputs. \n\nCartpole example : The authors come up with rules about, which output behaviors are correct for a few of the input regions. Then use this as a specification for the verification algorithm. But the very specifications, comes from reasoning about the forward behavior of the system dynamics itself. The idea of forward reach sets computation would generalize much better to a wide range of examples therefore.  Without the need to come up with such handcrafted rules. \n\nThe authors do make a convincing case for the ACASXu example. But this example is less interesting given the amount of attention it has received recently. ", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: Thank you for your submission to ICLR.  The reviewers and I unanimously felt, even after some of the clarifications provided, that while there was some interesting element to this work, ultimately there were substantial issues with both the presentation and content of the paper.  Specifically, the reviewers largely felt that the precise problem being solved was somewhat poorly defined, and the benefit of the proposed preimage technique wasn't always clear.  And while the ACAS system was a nice application, it seems to be difficult to quantify the real benefit of the proposed method in this setting (especially given that other techniques can similarly be used to verify NNs for this size problem).  The answer that this paper provides seems to be something along the lines of "ease of visual interpretation" of the pre-image conditions, but this needs to be quantified substantially more to be a compelling case.
Decision: Reject