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.