reluplex 1.0

AUTHORS

@@ -0,0 +1,12 @@
+The authors, designers, and main contributors to Reluplex are listed below.
+Reluplex's copyright is held by these individuals and the affiliated
+institutions at the time of their contributions. See the file COPYING for
+details on the copyright and licensing of Reluplex.
+
+The core designers and authors of Reluplex are:
+
+  Guy Katz, Stanford University.
+  Clark Barrett, Stanford University.
+  David Dill, Stanford University.
+  Kyle Julian, Stanford University.
+  Mykel Kochenderfer, Stanford University.

COPYING

@@ -0,0 +1,43 @@
+Reluplex is copyright (C) 2016-2017 by its
+authors and contributors (see the file AUTHORS) and their institutional
+affiliations. All rights reserved.
+
+The neural network data files under the nnet folder are copyright (C)
+2016-2017 by their authors and Stanford university, and are
+distributed under the Creative Commons Attribution 4.0 International
+License (https://creativecommons.org/licenses/by/4.0/).
+
+The source code of Reluplex is open and available to study, to modify, and to
+redistribute original or modified versions; distribution is under the terms of
+the modified BSD license (reproduced below). Reluplex links against GLPK which
+is licensed under the GNU General Public License, and therefore
+its use may be restricted in non-GPL-compatible projects.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its
+   contributors may be used to endorse or promote products derived from
+   this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
+''AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+----------------------------------------------------------------------

Readme.txt

@@ -0,0 +1,285 @@
+*** 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.
+
+This file contains instructions for compiling Reluplex and for running
+the experiments described in the paper, and alsosome 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 millseconds
+ - 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 files 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 specificed 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.

check_properties/Makefile

@@ -0,0 +1,51 @@
+# \file Makefile
+# \verbatim
+# Top contributors (to current version):
+#   Guy Katz
+# This file is part of the Reluplex project.
+# Copyright (c) 2016-2017 by the authors listed in the file AUTHORS
+# (in the top-level source directory) and their institutional affiliations.
+# All rights reserved. See the file COPYING in the top-level source
+# directory for licensing information.\endverbatim
+#
+
+ROOT_DIR = .
+
+SUBDIRS = \
+	property1 \
+	property2 \
+	property3 \
+	property4 \
+	property5 \
+	property6a \
+	property6b \
+	property7 \
+	property8 \
+	property9 \
+	property10 \
+	\
+	adversarial \
+
+all:
+	rm -f bin/*
+	cp property1/property1.elf bin
+	cp property2/property2.elf bin
+	cp property3/property3.elf bin
+	cp property4/property4.elf bin
+	cp property5/property5.elf bin
+	cp property6a/property6a.elf bin
+	cp property6b/property6b.elf bin
+	cp property7/property7.elf bin
+	cp property8/property8.elf bin
+	cp property9/property9.elf bin
+	cp property10/property10.elf bin
+	cp adversarial/adversarial.elf bin
+	@echo Done
+
+include $(ROOT_DIR)/Rules.mk
+
+#
+# Local Variables:
+# compile-command: "make -C . "
+# End:
+#