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 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.