$N^3V$ - A Non-linear Neural Network Verifier

This repository contains the non-linear neural network verifier $N^3V$ (and its evaluation).

Installation

Requirements

We require an installation of Julia 1.10. Moreover, if the installation fails it may be necessary to install Conda (we use Conda.jl to manage a python environment). This tool has a dependency on PicoSAT.jl which is only compatible with the platforms listed here

Setup

The setup script can be run via ./build.sh <path to julia 1.10 executable>.

This should run Julia and build the tool. Beware: Julia's building process may take 10-20 minutes. This is, because Julia's building system requires us to execute trace runs for determining the functions that will be precompiled.

Reproducing Experiments

To start of, you can run ./run_example.sh which should run the verification of an ACC controller. This process takes about 130 seconds on a 16 core AMD Ryzen 7 PRO 5850U CPU and returns that there exist counterexamples.

The logs of experiments can be found in the corresponding sub-folders of ./experiments. To rerun all experiments, you can use the script ./run_experiments.sh (Beware: This takes approx. 2 days!) which will write the experimental results into the corresponding log files.

Verifying your own NN.

To verify a model we need four things:

• A specification given as a formula (see e.g. ./test/parsing/examples/acc/formula)
• A description of variables that should be fixed (see e.g. ./test/parsing/examples/acc/fixed)
• A mapping from variables in the formula to input/output variables (see e.g. ./test/parsing/examples/acc/mapping)
• An NN to verify in ONNX format

After building the tool (see above), you can then run the following bash command to verify a model:

OPENBLAS_NUM_THREADS=1 OMP_NUM_THREADS=1 ./deps/NCubeV/bin/NCubeV <formula> <fixed vars> <mapping> <onnx file> <file-prefix to save results to>

To save memory for large verification tasks, it is necessary to provide a file prefix (!), e.g. /tmp/my-ncubev-results, as the tool may save results intermittently (e.g. /tmp/my-ncubev-results-100.jld).

Further options of the tool can be found via ./deps/NCubeV/bin/NCubeV; for very complicated arithmetic (square roots, high degree polynomials etc.) it may be worthwhile to switch of core reasoning with --no-cores.

Interpreting results

After completion, the tool will tell you if it found counterexamples. If there are counterexamples the model is generally unsafe. The counterexample regions can be found in the .jld files saved during execution. For an example how such regions can be analyzed see ./experiments/acas/Analysis-leveled.ipynb (and the associated julia file Analysis.jl).

Naming

$N^3V$ (pronounced "N Cube V") stands for Non-linear Neural Network Verifier.
Incidentally, interpreted as a unit $N^3V$ corresponds to $m^5kg^4A^{-1}s^{-9}$ which signifies the CPS mission of the tool: "making autonomy safer (which in turn has $5+4+1+9=19$ letters).

Citation

Please refer to our upcoming NeurIPS publication:

@inproceedings{NCubeV,
	title        = {Provably Safe Neural Network Controllers via Differential Dynamic Logic},
	author       = {Teuber, Samuel and Mitsch, Stefan and Platzer, Andr\'{e}},
	year         = {2024},
	booktitle    = {Advances in Neural Information Processing Systems},
	publisher    = {Curran Associates, Inc.},
	editor       = {A. Globerson and L. Mackey and A. Fan and C. Zhang and D. Belgrave and J. Tomczak and U. Paquet}
}