Marabou Neural Network Verification

Maraboupy is the Python interface for Marabou, an SMT-based neural network verification tool. It allows users to verify properties of neural networks by supplying them in TensorFlow, ONNX, or NNet formats.

Users can add piecewise-linear constraints to network variables to encode properties for verification. Maraboupy leverages pybind11 to interface with the core C++ implementation of Marabou.

When running a query, the solver returns one of two primary results:

• UNSAT: No assignment of values to all network variables can satisfy all equations and constraints.
• SAT: A satisfying assignment exists.

The CxxTest sample workspace for Visual Studio consists of three interdependent projects designed to automate the testing lifecycle:

1. CxxTest_3_Generate: Runs cxxtestgen to produce runner.cpp.
2. CxxTest_2_Build: Compiles the generated runner.cpp.
3. CxxTest_1_Run: Executes the compiled binary.

Prerequisites

You must define an environment variable PERL or PYTHON pointing to the executable path (e.g., PERL=c:\perl\bin\perl.exe) before running the projects.

Running Tests

When building the workspace, tests are executed automatically. If any assertions fail, they are displayed as compilation errors, which can be browsed using the F4 key in Visual Studio.

set PERL=c:\perl\bin\perl.exe

Maraboupy is the Python API for the C++ Marabou engine. Both must be built from source using CMake.

Prerequisites

• CMake: Version 3.2 or later.
• Python: Tested on versions >3.5 and >2.7. The build process prefers Python 3.
• Dependencies: Boost and pybind11 are automatically downloaded during the build process.

Installation Steps

1. Clone the repository:

git clone https://github.com/NeuralNetworkVerification/Marabou.git

2. Follow the platform-specific build instructions below.

After building Marabou, you can verify the installation by running tests via ctest from your build directory. There are three types of tests available:

1. Unit tests: Test specific small components. Run with -L unit.
2. System tests: Test end-to-end use cases with access to internal functionality. Run with -L system.
3. Regression tests: Test end-to-end functionality through the API. These are divided into 6 levels (0-5) to manage execution time. Run with -L regress[LEVEL] (e.g., -L regress0).

You can speed up test execution by running them in parallel using the -j flag followed by the number of processes.

ctest -L unit -j 4
ctest -L system -j 4
ctest -L regress0 -j 4

New example files added to the maraboupy/examples folder are automatically included in the documentation generated in maraboupy/docs. To ensure the documentation renders correctly with alternating text and code blocks, follow these formatting rules:

1. Title Block: Start the file with a comment block containing the title, followed by a line of = characters.
2. Text Blocks: Use # %% at the beginning of a comment line to denote a new text block.
3. Subsections: Create subsections by writing the subsection title followed by a line of - characters.
4. Ordering: Prefix the filename with a number (e.g., 01_example.py) to control the order in which files appear in the documentation.

You can replace the in-house LP solver with Gurobi to enable additional solving modes and improve performance.

1. Install Gurobi and follow the specific compilation steps for the C++ library (as described in the Gurobi documentation).
2. Set the required environment variables: GUROBI_HOME, PATH, LD_LIBRARY_PATH, and GRB_LICENSE_FILE.
3. Build Marabou using the -DENABLE_GUROBI=ON CMake flag.

# After setting up Gurobi environment variables
cmake ../ -DENABLE_GUROBI=ON

To build both the Marabou binary and the Maraboupy Python API on Linux or MacOS, use CMake from within a build directory.

Build Commands

cd path/to/marabou/repo/folder
mkdir build 
cd build
cmake .. -DBUILD_PYTHON=ON
cmake --build .

Build Options

• Multiprocess build: Speed up compilation by using multiple cores: cmake --build . -j PROC_NUM (replace PROC_NUM with your number of cores).
• Debug mode: Compile with debug symbols (default is Release): cmake .. -DCMAKE_BUILD_TYPE=Debug -DBUILD_PYTHON=ON

Post-Build

• The Marabou binary will be located in the build directory.
• The Maraboupy shared library will be placed in the maraboupy directory.
• Important: Add the Marabou root directory to your PYTHONPATH environment variable to use the Python API.