PV3 ⊧ Marabouchecks user-specified properties of deep neural networksFramework for verifying deep neural networks based on SMT solving.
- Deep neural networks
- Neural network verification
Type of toolNeural network verifier
- Neural network
- Property that should be checked
- Neural network: Tensorflow format (.pb file), .nnet format, .onnx file,
- Property: inequality over input and output variables or via the Python interface
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.
InternalsMarabou 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.