PV3 ⊧ Marabouchecks user-specified properties of deep neural networks

Framework for verifying deep neural networks based on SMT solving.

Application domain/field

• Deep neural networks
• Neural network verification

Type of tool

Neural network verifier

Expected input

• Neural network
• Property that should be checked

Format:

• Neural network: Tensorflow format (.pb file), .nnet format, .onnx file,
• Property: inequality over input and output variables or via the Python interface

Expected output

SAT or UNSAT indicating whether the network satisfies the property. If it does not satisfy the property then it will provide a counter-example (concrete input) for which the property is violated.

Internals

Marabou converts queries about a network into a constraint satisfaction problem. Marabou supports fully connected feed-forward and convolutional neural networks with piece-wise linear activation functions. The property/query that should be checked can be one of two types:

• Reachability queries: if the input is in a given range, the output will be 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.

Uses GLPK