Deep neural networks are revolutionizing the way complex systems are designed. Instead of spending long hours hand-crafting complex software, many engineers now opt to use deep neural networks (DNNs) - machine learning models, created by training algorithms that generalize from a finite set of examples to previously unseen inputs. Consequently, there is a pressing need for tools and techniques for network analysis and certification. To help address that need, we present Marabou, a framework for verifying deep neural networks.
Marabou is an SMT-based tool that can answer queries about a network’s properties by transforming these queries into constraint satisfaction problems. It can accommodate networks with different activation functions and topologies, and it performs high-level reasoning on the network that can curtail the search space and improve performance. It also supports parallel execution to further enhance scalability. Marabou accepts multiple input formats, including protocol buffer files generated by the popular TensorFlow framework for neural networks.
A DNN verification query consists of two parts: (i) a neural network, and (ii) a property to be checked; and its result is either a formal guarantee that the network satisfies the property, or a concrete input for which the property is violated (a counter-example). There are several types of verification queries that Marabou can answer:
- Reachability queries: if inputs is in a given range is the output guaranteed to be in some, typically safe, range.
- Robustness queries: test whether there exist adversarial points around a given input point that change the output of the network.
Marabou supports fully connected feed-forward and convolutional NNs with piece-wise linear activation functions, in the .nnet and TensorFlow formats. Properties can be specified using inequalites over input and output variables or via Python interface.
For more details about the features of Marabou check out the tool paper and the slides.
For more information about the input formats please check the wiki.
The latest version of Marabou is available on [http://github.com/GuyKatzz/Marabou].
Pre-compiled binary for Linux is available:
Marabou depends on the Boost library, which is automatically downloaded and built when you run make. Library CXXTEST comes included in the repository.
The marabou build process uses CMake version 3.2 (or later). You can get CMake here.
Marabou can be built for Linux, MacOS, or Windows machines.
To build marabou using CMake run:
cd path/to/marabou/repo/folder
mkdir build
cd build
cmake ..
cmake --build .
To enable multiprocess build change the last command to:
cmake --build . -j PROC_NUM
The compiled binary will be in the build directory, named Marabou
To run tests we use ctest.
The tests have labels according to level (unit/regress0/regress1...), and the code they are testing (engine/common etc...).
For example to run all unit tests execute in the build directory:
ctest -L unit
First, install Visual Studio 2017 or later and select the "Desktop development with C++" workload. Ensure that CMake is installed and added to your PATH.
Open a command prompt and run:
cd path\to\marabou\repo\folder
mkdir build
cd build
cmake .. -G"Visual Studio 15 2017 Win64"
cmake --build . --config Release
This process builds Marabou using the generator "Visual Studio 15 2017 Win64". For 32-bit machines, omit Win64. Other generators and older versions of Visual Studio can likely be used as well, but only "Visual Studio 15 2017 Win64" has been tested.
The Marabou executable file will be written to the build/Release folder. To build in Debug mode, simply run "cmake --build . --config Debug", and the executables will be written to build/Debug.
Using Marabou through the Python interface requires Python 3. It may be useful to set up a Python virtual environment, see here for more information.
The Python interface requires pybind11 (which is automatically downloaded). To also build the python API on Linux or MacOS, run:
cd path/to/marabou/repo/folder
mkdir build
cd build
cmake .. -DBUILD_PYTHON=ON
cmake --build .
On Windows, run:
cd path\to\marabou\repo\folder
mkdir build
cd build
cmake .. -G"Visual Studio 15 2017 Win64" -DBUILD_PYTHON=ON
cmake --build . --config Release
This process will produce the binary file and the shared library for the Python API. The shared library will be in the maraboupy folder for Linux and MacOS. On Windows, the shared library is written to a Release subfolder in maraboupy, so you will need to move the Release/*pyd file to the maraboupy folder:
cd path\to\marabou\repo\folder\maraboupy
move Release\*pyd .
Export maraboupy folder to Python and Jupyter paths:
PYTHONPATH=PYTHONPATH:/path/to/marabou/folder
JUPYTER_PATH=JUPYTER_PATH:/path/to/marabou/folder
and Marabou is ready to be used from a Python or a Jupyter script. On Windows, edit your environmental variables so PYTHONPATH includes the marabou folder.
After building Marabou the binary is located at build/Marabou (or build\Release\Marabou.exe for Windows). The repository contains sample networks and properties in the resources folder. For more information see resources/README.md.
To run Marabou, execute from the repo directory, for example:
./build/Marabou resources/nnet/acasxu/ACASXU_experimental_v2a_2_7.nnet resources/properties/acas_property_3.txt
on Linux or MacOS, or
build\Release\Marabou.exe resources\nnet\acasxu\ACASXU_experimental_v2a_2_7.nnet resources\properties\acas_property_3.txt
on Windows.
The maraboupy/examples folder contains several python scripts and Jupyter notebooks that can be used as starting points.
In the DNC mode, activated by --dnc Marabou decomposes the problem into n0 sub-problems, specified by --initial-divides=n0. Each sub-problem will be solved with initial timeout of t0, supplied by --initial-timeout=t0. Every sub-problem that times out will be divided into n additional sub-problems, --num-online-divides=n, and the timeout is multiplied by a factor of f, --timeout-factor=f. Number of parallel threads t is specified by --num-workers=t.
So to solve a problem in DNC mode with 4 initial splits and initial timeout of 5s, 4 splits on each timeout and a timeout factor of 1.5:
build/Marabou resources/nnet/acasxu/ACASXU_experimental_v2a_2_7.nnet resources/properties/acas_property_3.txt --dnc --initial-divides=4 --initial-timeout=5 --num-online-divides=4 --timeout-factor=1.5 --num-workers=4
The Marabou project is partially supported by grants from the Binational Science Foundation (2017662), the Defense Advanced Research Projects Agency (FA8750-18-C-0099), the Semiconductor Research Corporation (2019-AU-2898), the Federal Aviation Administration, Ford Motor Company, Intel Corporation, the Israel Science Foundation (683/18), the National Science Foundation (1814369, DGE-1656518), Siemens Corporation, General Electric, and the Stanford CURIS program.
Marabou is used in a number of flagship projects at Stanford's AISafety center.
Derek A. Huang
Duligur Ibeling
Elazar Cohen
Ben Goldberger
Omri Cohen