This is an experimental branch of NeuroCodeBench written specifically for VNN-COMP'25.
Currently, it contains only SAT-ReLU: a synthetic benchmark for neural network verification tools.
The idea behind this benchmark is to take arbitrary CNF formulae and embed them inside a feedforward neural network in ONNX format and a safety property in VNN-LIB format. Details of the algorithm will be released soon.
Crucially, the verdict of each verification instance (either SAT or UNSAT) is known in advance.
Clone the repository and run install.sh. This will install the following Python dependencies:
- numpy
- pytorch
- onnx
Different versions of the benchmark can be generated by running "generate_properties.py [SEED]" with arbitrary seed values.
See the file generate_properties.py:
- N_BENCH_PAIRS controls the number of generated instances
- N_VAR controls the number of input variables, extracted uniformly at random from the [min,max] range
- X_CLAUSE controls the range of clauses in the CNF formula as n_clauses = n_var * x_clauses
Preliminary results show that Marabou solves all SAT instances instantly, while struggling on UNSAT ones. For the latter, we observe timeouts as soon as the number of variables grows beyond 2.