CoVeNN: Compositional Neural Network Verification via Assume-Guarantee Reasoning

1. Installation

• Install Python 3.11+

• Install PyTorch (Stable 2.7.0):

pip3 install torch torchvision torchaudio --index-url https://download.pytorch.org/whl/cu128

• Install dependencies:

pip3 install -r requirements.txt 

2. Example

cd tools/covenn/

./vnncomp_scripts/run_instance.sh v1 resnet12 ../../benchmarks/resnet/resnet12/net/resnet12.pth ../../benchmarks/resnet/resnet12/spec/spec_idx_0_net_resnet12_eps_0.020000_seed_37.vnnlib temp.res 3600.0

./vnncomp_scripts/run_instance.sh v1 resnet18 ../../benchmarks/resnet/resnet18/net/resnet18.pth ../../benchmarks/resnet/resnet18/spec/spec_idx_0_net_resnet18_eps_0.015000_seed_37.vnnlib temp.res 3600.0

3. Experiment

export COVENN_ROOT=$(pwd)

• Run CoVeNN with NeuralSAT backend:

cd  $COVENN_ROOT/tools/covenn/
python3 ../../runner.py --tool covenn_neuralsat --backend neuralsat --benchmark vae
python3 ../../runner.py --tool covenn_neuralsat --backend neuralsat --benchmark resnet

• Run CoVeNN with alpha-beta-CROWN backend:

cd  $COVENN_ROOT/tools/covenn/
python3 ../../runner.py --tool covenn_abcrown --backend abcrown --benchmark vae
python3 ../../runner.py --tool covenn_abcrown --backend abcrown --benchmark resnet

• Run NeuralSAT:

cd  $COVENN_ROOT/tools/neuralsat/
python3 ../../runner.py --tool neuralsat --benchmark vae
python3 ../../runner.py --tool neuralsat --benchmark resnet

• Run alpha-beta-CROWN:

cd  $COVENN_ROOT/tools/abcrown/
python3 ../../runner.py --tool abcrown --benchmark vae
python3 ../../runner.py --tool abcrown --benchmark resnet