-
Notifications
You must be signed in to change notification settings - Fork 49
/
Readme.txt
294 lines (215 loc) · 11.4 KB
/
Readme.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
NOTE: This repo is not maintained anymore. You can try our new tool
called Marabou, which implements the Reluplex algorithm and other
improved techniques (https://github.com/NeuralNetworkVerification/Marabou).
*** Reluplex, May 2017 ***
This repository contains the proof-of-concept implementation of the
Reluplex algorithm, as described in the paper:
G. Katz, C. Barrett, D. Dill, K. Julian and
M. Kochenderfer. Reluplex: An Efficient SMT Solver for Verifying
Deep Neural Networks. Proc. 29th Int. Conf. on Computer Aided
Verification (CAV). Heidelberg, Germany, July 2017.
The paper (with its supplementary material) may be found at:
https://arxiv.org/abs/1702.01135
This file contains instructions for compiling Reluplex and for running
the experiments described in the paper, and also some information on
the Reluplex code and the various folders.
Compilation Instructions
------------------------
The implementation was run and tested on Ubuntu 16.04.
Compiling GLPK:
cd glpk-4.60
./configure_glpk.sh
make
make install
Compiling the Reluplex core:
cd reluplex
make
Compiling the experiments:
cd check_properties
make
Running the experiments
-----------------------
The paper describes 3 categories of experiments:
(i) Experiments comparing Reluplex to the SMT solvers CVC4, Z3,
Yices and Mathsat, and to the LP solver Gurobi.
(ii) Using Reluplex to check 10 desirable properties of the ACAS
Xu networks.
(iii) Using Reluplex to evaluate the local adversarial robustness of
one of the ACAS Xu networks.
This repository contains the code for all experiments in categories
(ii) and (iii). All experiments are run using simple scripts,
provided in the "scripts" folder. The results will appear in the
"logs" folder. In order to run an experiment:
- Navigate to the main directory
- Run the experiment of choice: ./scripts/run_XYZ.sh
- Find the results under the "logs" folder.
A Reluplex execution generates two kinds of logs. The first is the
summary log, in which each query to Reluplex is summarized by a line like this:
./nnet/ACASXU_run2a_2_3_batch_2000.nnet, SAT, 12181, 00:00:12, 37, 39
The fields in each line in the summary file are:
- The network being tested
- Result (SAT/UNSAT/TIMEOUT/ERROR)
- Time in milliseconds
- Time in HH:MM:SS format
- Maximal stack depth reached
- Number of visited states
Summary logs will always have the word "summary" in their
names. Observe that a single experiment may involve multiple networks,
or multiple queries on the same network - so a single summary file may
contain multiple lines. Also, note that these files are only
created/updated when a query finishes, so they will likely appear
only some time after an experiment has started.
The second kind of log file that will appear under the "logs" folder
is the statistics log. These logs will have the word "stats" in their
names, and will contain statistics that Reluplex prints roughly every
500 iterations of its main loop. These logs will appear immediately
when the experiment starts. Unlike summary logs which may summarize
multiple queries to Reluplex, each statistics log describes just a
single query. Consequently, there will be many of these logs (a
single experiment may generate as many as 45 of these logs). The log
names will typically indicate the specific query that generated them;
for example, "property2_stats_3_9.txt" signifies a statistics log that
was generated for property 2, when checked on the network indexed by
(3,9).
- Using Reluplex to check 10 desirable properties of the ACAS Xu
networks:
These 10 benchmarks are organized under the "check_properties" folder,
in numbered folders. Property 6 is checked in two parts, and
so it got two folders: property6a and property6b. Within these
folders, the properties are given in Reluplex format (in main.cpp).
Recall that checking is done by negating the property. For instance,
in order to prove that x > 50, we tell Reluplex to check the
satisfiability x <= 50, and expect an UNSAT result.
Also, some properties are checked in parts. For example, the ACAS Xu
networks have 5 outputs, and we often wish to prove that one of them
is minimal. We check this by querying Reluplex 4 times, each time
asking it to check whether it is possible that one of the other
outputs is smaller than our target output. In this case, success is
indicated by 4 UNSAT answers.
To run Reluplex, execute the "run_peopertyi.sh" scripts, for i between
1 and 10. The result summaries will appear under
"logs/propertyi_summary.txt". The statistics from each individual
query to Reluplex will also appear under the logs folder.
- Using Reluplex to evaluate the local adversarial robustness of one of
the ACAS Xu networks:
These experiments include evaluating the adversarial robustness of one
of the ACAS Xu networks on 5 arbitrary points. Evaluating each point
involves invoking Reluplex 5 times, with different delta sizes.
The relevant Reluplex code appears under
"check_properties/adversarial/main.cpp". To execute it (after
compiling it), run the "scripts/run_adversarial.sh" script. The
summary of the results will appear as "logs/adversarial_summary.txt",
and the Reluplex statistics will appear under
"logs/adversarial_stats.txt" (the statistics for all queries will
appear under the same file).
Checking the adversarial robustness at point x for a fixed delta is
done as follows:
- Identify the minimal output at point x
- For each of the other 4 outputs, do:
- Invoke Reluplex to look for a point x' that is at most delta
away from x, for which the other point is minimal
If the test fails for all 4 other outputs (4 UNSAT results), the
network is robust at x; otherwise, it is not. As soon as one SAT
result is found we stop the test.
Information regarding the Reluplex code
---------------------------------------
The main components of the tool are:
1. reluplex/Reluplex.h:
The main class, implementing the core Reluplex algorithm.
2. glpk-4.60: (folder)
The glpk open-source LP solver, plus some modifications.
The patches applied to the pristine GLPK appear under the "glpk_patch"
folder (no need to re-apply them).
3. reluplex/SmtCore.h:
A simple SmtCore, in charge of the search stack.
4. nnet/:
This folder contains the ACAS Xu neural networks that we used, and
code for loading and accessing them.
Below are additional details about the Reluplex core.
An example of how to use Reluplex.h is provided in
reluplex/RunReluplex.h. This example is the one described in the
paper. It shows how a client specifies the number of variables for the
Reluplex class, which variables are auxiliary variables (via the
markBasic() method), which are ReLU pairs (via setReluPair()), the
lower and upper bounds and the initial tableau values. A call to the
solve() method then starts Reluplex.
Inside the Reluplex class, the main loop is implemented in the
progress() method. This loop:
A. Invokes GLPK in order to fix any out-of-bounds variables
B. If all variables are within bounds, attempts to fix a broken ReLU
constraint.
If progress() is successful (i.e., progress is made), it returns
true. Otherwise the problem is infeasible, and progress() returns
false. In this case the caller function, solve(), will have the SmtCore
pop a previous decision, or return UNSAT if there are none to pop.
Important member variables of the Reluplex class:
_tableau: the tableau.
_preprocessedTableau: the original tableau (after some
preprocessing), used for restoring the tableau in certain cases.
_upperBounds, _lowerBounds: the current variable bounds.
_assignment: the current assignment.
_basicVariables: the set of variables that are currently basic.
_reluPairs: all pairs of variables specified as ReLU pairs.
_dissolvedReluVariables: ReLU pairs that have been eliminated.
Some of the notable methods within the Reluplex class:
- pivot():
A method for pivoting two variables in the tableau.
- update():
A method for updating the current assignment.
- updateUpperBound(), updateLowerBound():
Methods for tightening the upper and lower bounds of a variable.
These methods eliminate ReLU connections when certain bounds are
discovered (e.g., a strictly positive lower bound for a ReLU
variable), as discussed in the paper.
- unifyReluPair():
A method for eliminating a ReLU pair by fixing it to the active
state. This is performed by merging the two variables in the
tableau: the method ensures that both variables are equal and
non-basic, and then eliminates the b variable from the tableau and
replaces it with the f variable.
- fixOutOfBounds():
A method for invoking GLPK in order to fix all out-of-bound
variables. The method translates the current tableau into a GLPK
instance, invokes GLPK, and then extracts the solution tableau and
assignment from GLPK.
- fixBrokenRelu():
A method for fixing a specific ReLU constraint that is currently
broken. We first try to fix the b variable to agree
with the f variable, and only if that fails attempt to fix f to
agree with b. If both fail, the problem is infeasible, and the
method returns false. Otherwise, the pair is fixed, and the method
returns true.
- storeGlpkBoundTightening():
As GLPK searches for feasible solutions, certain rows of the
tableaus that it explores are used to derive tighter variable bounds.
(see paper). These new bounds are stored (but not applied) as GLPK
runs. When GLPK terminates, all the new bounds are applied.
- performGlpkBoundTightening():
The method that actually performs bound tightening, as stored by
storeGlpkBoundTightening().
- findPivotCandidate():
A method for finding variables that afford slack for a certain
basic variable that needs to be increased or decreased.
- restoreTableauFromBackup():
A method for restoring the current tableau from the original
tableau. This is done, for example, when the round-off degradation
is discovered to be too great (see paper).
Other points of interest in the Reluplex class:
- The under-approximation technique discussed in the paper has been
implemented, although it is turned off by default. To turn it on,
call toggleAlmostBrokenReluEliminiation( true ) when setting up
Reluplex. This affects the way ReLUs are eliminated within the
updateLowerBound() and updateUpperBound() methods.
- Conflict analysis (see paper) is performed as part of bound
tightening operations. Specifically, when bound tightening leads
to a lower bound becoming greater than an upper bound, an
InvariantViolationError exception is raised. The parameter to that
error, i.e. the "violatingStackLevel", indicates the last split
that led to the current violation. This indicates how many
decisions in the stack need to be undone by the SmtCore.
Additional classes under the "reluplex" folder:
- FloatUtils: utilities for comparing floating point numbers.
- Tableau: a linked-list implementation of Reluplex's tableau.
- ReluPairs: a simple data structure for keeping information about ReLU pairs.
- RunReluplex: a small test-harness for Reluplex. Contains 2 small examples.
The "common" folder contains general utility classes.