A collection of DNN verification benchmarks, specified in DNNP and ONNX for use with DNNV and DNNF.
To access the benchmarks, simply clone this repo:
$ git clone https://github.com/dlshriver/benchmarks.gitWe currently include 7 benchmarks in DNNP and ONNX format.
Each one is in its own sub-directory in the benchmarks directory, and each has a README with a description of the benchmark.
We also include some useful tool scripts in the tools directory.
tools/resmonitor.py will run a command with specified memory and time limits.
tools/run_dnnv.py can run all the problems in a specified benchmark using dnnv on multiple processes with resource limits.
To check the problems in the benchmarks, first install DNNV, as well as whichever verifiers you wish to use. After installation, DNNV can be run on a single problem as follows:
$ dnnv /path/to/property --network N /path/to/network --VERIFIERFor example, to run the nnenum verifier on property 1 and network N_1_1.onnx from the ACAS Xu benchmark, run:
$ dnnv benchmarks/ACAS_Xu/properties/property_1.py --network N benchmarks/ACAS_Xu/onnx/N_1_1.onnx --nnenumTo run all of the problems in a benchmark, we provide tools/run_dnnv.py.
This tool expects both DNNV and pandas to be installed.
$ tools/run_dnnv.sh -b /path/to/benchmark/dir/ -p /path/to/problems_csv --VERIFIERFor example, to run the nnenum verifier on the ACAS Xu benchmark, run:
$ tools/run_dnnv.sh -b benchmarks/ACAS_Xu -p problems_original.csv --nnenumAdditional options (such as those for restricting the time and memory usage) can be seen by running:
$ tools/run_dnnv.sh -hAny additionally specified arguments will be passed directly to DNNV.