Paper: On the Soundness and Completeness of Neural Network Verifiers

Framework:

There are two major steps in CGE. $f$ and $\varphi = {\Phi, \Psi}$ denote an NN and a verification specification, where the pair $\Phi $ and $ \Psi$ denote the input and output specifications. $\mathbf{x}_{ce}$ denotes a counterexample generated by the verifier. For our collaborative evaluation, there are $m$ numbers of verification instances and $n$ numbers of verifiers. After step 1, $m'$ instances' are confirmed as ground truths including violations and desirables. Step 2 is to evaluate the soundness and completeness of verifiers by comparing the $m' \times n$ numbers of filtered verification results with ground truths. FN and FP denote false negative and false positive.

Soundness and Completeness

Please note that to download this repository, your Git installation requires Git Large File Storage

Firstly, clone the rep:

git lfs clone https://github.com/fengxxu/cge.git
cd cge
mkdir results
unzip benchmarks.zip
unzip verification_results.zip

Secondly, create a new environment and install environment using conda:

(Install conda (How to install) if necessary)

Install environments

conda env create -f environments.yml

Lastly, open the main.ipynb, select the correct kernel for the notebook, following instructions in the notebook to replicate the experiment