PV3 Marabouchecks user-specified properties of deep neural networks

Framework for verifying deep neural networks based on SMT solving.

Application domain/field

Type of tool

Neural network verifier

Expected input


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.


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: Uses GLPK
DNN Neural network


Related papers

Last publication date

23 March 2021

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.