About Marabou

Marabou is an SMT-based tool that answers queries about neural networks and their properties. Queries are transformed into constraint satisfaction problems. Marabou takes as input networks with various piece-wise linear activation functions and with fully connected topology.

Marabou first applies multiple pre-processing steps to infer bounds for each node in the network. Next it applies a combination of Simplex search over linear constraints with SMT techniques directing the search over non-linear constraints. Marabou also implements Split-and-Conquer mode, which decomposes the verification query into a set of smaller queries, which can be solved in parallel.

Marabou can be used both from the command line and via Python API. It alaccepts multiple input formats, such as .nnet, .pb and .onnx.

Getting Marabou

The source code for Marabou is available on GitHub.

Python API Documentation

To read more about the Python API, documentation and examples, see our Documentation page.