Skip to content

Commit

Permalink
update README.md (#792)
Browse files Browse the repository at this point in the history 
* update readme

* Update README.md

* Update README.md
  • Loading branch information
@wu-haoze
wu-haoze authored Apr 7, 2024
1 parent ba9aa1a commit 3526396
Showing 1 changed file with 93 additions and 166 deletions.
259 changes: 93 additions & 166 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,51 +2,30 @@
[![Marabou](https://github.com/NeuralNetworkVerification/Marabou/actions/workflows/ci.yml/badge.svg)](https://github.com/NeuralNetworkVerification/Marabou/actions/workflows/ci.yml)
[![codecov.io](https://codecov.io/github/NeuralNetworkVerification/Marabou/coverage.svg?branch=master)](https://codecov.io/github/NeuralNetworkVerification/Marabou?branch=master)

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](https://aisafety.stanford.edu/marabou/MarabouCAV2019.pdf)
([slides](https://aisafety.stanford.edu/marabou/fomlas19.html)) and our [**recent work**](https://arxiv.org/abs/2203.11201)
based on Sum-of-Infeasibilities, which is now the default solving mode of Marabou.

For more information about the input formats please check the
[wiki](https://github.com/NeuralNetworkVerification/Marabou/wiki/Marabou-Input-Formats).

A guide to Split and Conquer mode is available in [resources/SplitAndConquerGuide.ipynb](resources/SplitAndConquerGuide.ipynb). The Jupyter Notebook gives on overview of SnC's parameters, discusses several runtime examples and a few rules of thumb to choose parameter values.
Deep neural networks are proliferating in many applications. 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 over networks. A typical 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).

Marabou uses ONNX as its main network format. It supports feed-forward NNs with a
wide range of activations. It also supports the .nnet and the Tensorflow NN formats.

Properties can be specified using the Python interface. In addition, Marabou also supports
the VNNLIB property format.

For more details about the design and features of version 2.0 of Marabou, check out
the latest [tool paper](https://arxiv.org/pdf/2401.14461.pdf). The initial version
of Marabou is described in a [previous tool paper](https://aisafety.stanford.edu/marabou/MarabouCAV2019.pdf).

## Research

More information about publications involving Marabou can be found
[here](https://neuralnetworkverification.github.io/).
Marabou is a research product. More information about publications involving Marabou
can be found [here](https://neuralnetworkverification.github.io/).

## Installation

Expand All @@ -61,44 +40,87 @@ The Python interface currently supports Python 3.8, 3.9, 3.10 and 3.11.

### Building from source

The current version of Marabou can be built for Linux or MacOS machines.

#### Build dependencies

The build process uses CMake version 3.16 (or later).
You can get CMake [here](https://cmake.org/download/).

Marabou depends on the Boost library, which is automatically downloaded
and built when you run make.
Library CXXTEST comes included in the repository.

#### Build Instructions for Linux or MacOS
Marabou depends on the Boost and the OpenBLAS libraries, which are automatically
downloaded and built when you run make. Library CXXTEST comes included in the
repository.

To build marabou using CMake run:
The current version of Marabou can be built for Linux or MacOS machines using CMake:
```bash
cd path/to/marabou/repo/folder
git clone https://github.com/NeuralNetworkVerification/Marabou/
cd Marabou/
mkdir build
cd build
cmake ..
cmake ../
cmake --build ./
```
For configuring to build a static Marabou binary, use the following flag
To enable multiprocess build change the last command to:
```bash
cmake .. -DBUILD_STATIC_MARABOU=ON
cmake --build . -j PROC_NUM
```
To build, run the following:
After building Marabou, the compiled binary is located at `build/Marabou`, and the
shared library for the Python API is located in `maraboupy/`. Building the Python
interface requires *pybind11* (which is automatically downloaded).

Export `maraboupy` folder to Python and Jupyter paths:
```
PYTHONPATH=PYTHONPATH:/path/to/marabou/folder
JUPYTER_PATH=JUPYTER_PATH:/path/to/marabou/folder
```
and the built `maraboupy` is ready to be used from a Python or a Jupyter script.

By default we install a 64bit Marabou and consequently a 64bit Python interface,
the `maraboupy/build_python_x86.sh` file builds a 32bit version.

#### Compile Marabou with the Gurobi optimizer (optional)
Marabou can be configured to use the Gurobi optimizer, which can replace the
in-house LP solver and enable a few additional solving modes.

Gurobi requires a license (a free academic license is available), after
getting one the software can be downloaded [here](https://www.gurobi.com/downloads/gurobi-optimizer-eula/)
and [here](https://www.gurobi.com/documentation/9.5/quickstart_linux/software_installation_guid.html#section:Installation) are
installation steps, there is a [compatibility issue](https://support.gurobi.com/hc/en-us/articles/360039093112-C-compilation-on-Linux)
that should be addressed.
A quick installation reference:
```bash
cmake --build .
export INSTALL_DIR=/opt
sudo tar xvfz gurobi9.5.1_linux64.tar.gz -C $INSTALL_DIR
cd $INSTALL_DIR/gurobi951/linux64/src/build
sudo make
sudo cp libgurobi_c++.a ../../lib/
```
To enable multiprocess build change the last command to:
Next, set the following environment variables (e.g., by adding the following to the `.bashrc` and invoke `source .bashrc`):
```bash
cmake --build . -j PROC_NUM
export GUROBI_HOME="/opt/gurobi951/linux64"
export PATH="${PATH}:${GUROBI_HOME}/bin"
export LD_LIBRARY_PATH="${LD_LIBRARY_PATH}:${GUROBI_HOME}/lib"
export GRB_LICENSE_FILE=/path/to/license.lic
```

After Gurobi is set up, follow the same build instruction of Marabou in the beginning,
except that you need to run the following command instead of `cmake ../`:
```bash
cmake ../ -DENABLE_GUROBI=ON
```
To compile in debug mode (default is release)

#### Other CMake options

The `cmake ../` command can take other options, for example:

- Compile without the Python binding:
```bash
cmake .. -DCMAKE_BUILD_TYPE=Debug
cmake --build .
cmake ../ -DBUILD_PYTHON=OFF
```
After building Marabou, the compiled binary is located at `build/Marabou`.
- Compile in debug mode (default is release):
```bash
cmake ../ -DCMAKE_BUILD_TYPE=Debug
```

#### Testing

To run tests we use [ctest](https://cmake.org/cmake/help/v3.15/manual/ctest.1.html).
The tests have labels according to level (unit/system/regress0/regress1...), and the code they are testing (engine/common etc...).
Expand All @@ -118,72 +140,21 @@ cmake ..
make check -j PROC_NUM
```

The Python bindings for Marabou are built automatically (controllable via the `BUILD_PYTHON` CMake flag).
This process will produce the binary file and the shared library for the Python API,
which is created in the `maraboupy` folder.
Building the Python interface requires *pybind11* (which is automatically downloaded).

It may be useful to set up a Python virtual environment, see
[here](https://docs.python.org/3/tutorial/venv.html) for more information.

Export `maraboupy` folder to Python and Jupyter paths:
```
PYTHONPATH=PYTHONPATH:/path/to/marabou/folder
JUPYTER_PATH=JUPYTER_PATH:/path/to/marabou/folder
```
and the built `maraboupy` is ready to be used from a Python or a Jupyter script.

### Build Instructions for Windows using Visual Studio

We no longer provide Windows support. The below instructions apply to commits up
to [0fc1d10](https://github.com/NeuralNetworkVerification/Marabou/commit/0fc1d10ff0e1859cf32abe54eb22f3ec0fec59f6).

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 `build\Release\Marabou.exe`. To build in
Debug mode, simply run "cmake --build . --config Debug", and the executables will be
written to build/Debug.

On Windows, the shared library for the Python API is written to a `Release` subfolder in `maraboupy`,
so you will need to move the `Release/\*pyd` file to the maraboupy folder:
```bash
cd path\to\marabou\repo\folder\maraboupy
move Release\*pyd .
```
You will also need to edit your environmental variables so PYTHONPATH includes the marabou folder.

#### Troubleshooting

- On Windows - Make sure the detected python ("Found PythonInterp: ....") is a windows python and not cygwin or something like that (if it is cygwin, use -DPYTHON_EXECUTABLE flag to override the default python, or manuialy download the linux pybind and locate it in the tools directory)

- 32bit Python - By default we install a 64bit Marabou and consequently a 64bit
Python interface, the `maraboupy/build_python_x86.sh` file builds a 32bit
version.
We no longer provide Windows support. Instructions to build an old version of Marabou
for Windows can be found [here](https://github.com/NeuralNetworkVerification/Marabou/tree/0fc1d10ff0e1859cf32abe54eb22f3ec0fec59f6?tab=readme-ov-file#build-instructions-for-windows-using-visual-studio).

## Running Marabou

### Run from the Command line

The `Marabou` executable can be called directly from the command line.
It takes as arguments the network to verified and the property.
It takes as arguments the network to verified and the property. `Marabou --help` would
return a list of available options.

The repository contains sample networks and properties in the *resources* folder.
For more information see [resources/README.md](resources/README.md).

To run Marabou on Linux or MacOS on such an example, you can execute the following command
To run Marabou on such an example, you can execute the following command
from the repo directory:
```bash
Marabou resources/nnet/acasxu/ACASXU_experimental_v2a_2_7.nnet resources/properties/acas_property_3.txt
Expand All @@ -193,15 +164,9 @@ i.e. `build/Marabou`).

### Run using Python

Please see our [documentation](https://neuralnetworkverification.github.io/Marabou/)
for the python interface, which contains examples, API documentation, and a developer's guide.

### Using the run script (*Recommended*)
For ease of use, we also provide a example python script (resources/runMarabou.py). The script can take the same arguments
as the Marabou binary. The difference is that the python script also supports networks in onnx format.

Moreover, instead of passing in a property file, you could define your property with the Python API
calls [here](https://github.com/NeuralNetworkVerification/Marabou/blob/master/resources/runMarabou.py#L80-L81).
The `maraboupy/examples` folder contains a list of examples. Please also see our
[documentation](https://neuralnetworkverification.github.io/Marabou/) for the python interface,
which contains examples, API documentation, and a developer's guide.

### Advanced configuration

Expand Down Expand Up @@ -239,39 +204,6 @@ build/Marabou resources/nnet/acasxu/ACASXU_experimental_v2a_2_7.nnet resources/p

A guide to Split and Conquer is available as a Jupyter Notebook in [resources/SplitAndConquerGuide.ipynb](resources/SplitAndConquerGuide.ipynb).

#### Use LP Relaxation

Marabou has an option to use LP relaxation for bound tightening.
For now we use Gurobi as an LP solver. Gurobi requires a license (a free
academic license is available), after getting one the software can be downloaded
[here](https://www.gurobi.com/downloads/gurobi-optimizer-eula/) and [here](https://www.gurobi.com/documentation/9.5/quickstart_linux/software_installation_guid.html#section:Installation) are
installation steps, there is a [compatibility issue](https://support.gurobi.com/hc/en-us/articles/360039093112-C-compilation-on-Linux)
that should be addressed.
A quick installation reference:
```bash
export INSTALL_DIR=/opt
sudo tar xvfz gurobi9.5.1_linux64.tar.gz -C $INSTALL_DIR
cd $INSTALL_DIR/gurobi951/linux64/src/build
sudo make
sudo cp libgurobi_c++.a ../../lib/
```
Next it is recommended to add the following to the .bashrc (but not necessary)
```bash
export GUROBI_HOME="/opt/gurobi951/linux64"
export PATH="${PATH}:${GUROBI_HOME}/bin"
export LD_LIBRARY_PATH="${LD_LIBRARY_PATH}:${GUROBI_HOME}/lib"
```

After installing Gurobi compile marabou as follows:
```bash
cmake .. -DENABLE_GUROBI=ON
cmake --build .
```
If you did not set the GUROBI_HOME environment variable, then use the following:
```bash
cmake .. -DENABLE_GUROBI=ON -DGUROBI_DIR=<PATH_TO_GUROBI>
```

## Developing Marabou

### Setting up your development environment
Expand Down Expand Up @@ -307,12 +239,7 @@ In the future we will run other levels of regression weekly / monthly.

## Acknowledgments

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.
The Marabou project acknowledges support from the Binational Science Foundation (BSF) (2017662, 2021769, 2020250), the Defense Advanced Research Projects Agency (DARPA) (FA8750-18-C-0099), the European Union (ERC, VeriDeL, 101112713), the Federal Aviation Administration (FAA), Ford Motor Company (Alliance award 199909), General Electric (GE) Global Research, Intel Corporation, International Business Machines (IBM), the Israel Science Foundation (ISF) (683/18, 3420/21), the National Science Foundation (NSF) (1814369, 2211505, DGE-1656518), the Semiconductor Research Corporation (SRC) (2019-AU-2898), Siemens Corporation, the Stanford Center for AI Safety, the Stanford CURIS program, and the Stanford Institute for Human-Centered Artificial Intelligence (HAI).


Marabou is used in a number of flagship projects at [Stanford's AISafety
Expand Down

0 comments on commit 3526396

Please sign in to comment.