Marabou Input Formats

Neural Network Formats

Marabou reasons about neural networks in .nnet (via the command line) or TensorFlow's .pb format (via the Python interface).

For more information about the .nnet format see the nnet repository.

Marabou does not support all constructs of TensorFlow's format, if you run into problems, consider using converters from the .nnet repository.

Property Format

Properties can be specified as .txt file (via the command line) or using the Python interface.

The .txt file format consists of inequalities over input and output ranges, where input variables are x0 to xN and output variables as y0 to yM, where the network has N+1 inputs and M+1 outputs. Each line contains a single inequality and the lines are implicitly connected by a conjunction. Disjunctive properties need to be broken down into multiple property files and checked in separate queries.

The grammar of admitted properties:

Scalar         ::= <double>
InputVariable  ::= x<integer>
OutputVariable ::= y<integer>
Variable       ::= InputVariable | OutputVariable
Rel            ::= >= | = | <=
Coefficient    ::= + | - | <double>
Addend         ::= Coefficient Variable                              (no separating space)
Line           ::= [Addend] Rel Scalar
Property       ::= [Line]

Marabou team thanks user @MatthewDaggitt for the grammar.

Example - ACAS Property 1 in .txt format

x0 >= 0.6
x0 <= 0.6798577687
x1 >= -0.5
x1 <= 0.5
x2 >= -0.5
x2 <= 0.5
x3 >= 0.45
x3 <= 0.5
x4 >= -0.5
x4 <= -0.45
y0 >= 3.9911256459