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.

CAISAR uses Marabou for solving complex queries.