# Clip and Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification

We provid our code to reproduce the results—please run it on a Linux system to avoid any compatibility issues.

## Environment

Setup the conda environment:

```bash
# move to the dictionary
cd ./complete_verifier
# install all dependents into the alpha-beta-crown environment
conda env create -f environment.yaml --name clip_n_verify
# activate the environment
conda activate clip_n_verify
```

## How to Use

### Download Benckmarks

All benckmarks are opensouced VNN-COMP benckmarks. Get the benckmarks from the VNN-COMP official github:

```
git clone https://github.com/stanleybak/vnncomp2021.git

git clone https://github.com/ChristopherBrix/vnncomp2022_benchmarks.git

git clone https://github.com/ChristopherBrix/vnncomp2023_benchmarks.git

git clone https://github.com/ChristopherBrix/vnncomp2024_benchmarks.git
```

### For Input Branch-and-bound (BaB)

#### Run Clip and Verify

Remove `--enable_complete_clip_inputbab` to run vanilla α,β-CROWN.

```
# acasxu
python abcrown.py --config exp_configs/vnncomp23/acasxu.yaml --enable_complete_clip_inputbab --min_batch_size_ratio 0.1 --reorder_bab

# nn4sys
python abcrown.py --config exp_configs/vnncomp23/nn4sys.yaml --enable_complete_clip_inputbab --min_batch_size_ratio 0.1 --reorder_bab

# lsnc
python abcrown.py --config exp_configs/vnncomp24/lsnc.yaml --enable_complete_clip_inputbab --min_batch_size_ratio 0.1 --reorder_bab --initial_max_domains 100000
```

#### Clip-n-Verify, Relaxed

```
python abcrown.py --config exp_configs/vnncomp23/acasxu.yaml --min_batch_size_ratio 0.1 --enable_relexed_clip --reorder_bab

python abcrown.py --config exp_configs/vnncomp23/nn4sys.yaml --min_batch_size_ratio 0.1 --enable_relexed_clip --reorder_bab

python abcrown.py --config exp_configs/vnncomp24/lsnc.yaml --min_batch_size_ratio 0.1 --enable_relexed_clip --reorder_bab --initial_max_domains 100000
```

#### Clip-n-Verify, Relaxed w/o Reorder

```
python abcrown.py --config exp_configs/vnncomp23/acasxu.yaml --enable_relexed_clip --min_batch_size_ratio 0.1

python abcrown.py --config exp_configs/vnncomp23/nn4sys.yaml --enable_relexed_clip --min_batch_size_ratio 0.1

python abcrown.py --config exp_configs/vnncomp24/lsnc.yaml --enable_relexed_clip --min_batch_size_ratio 0.1 --initial_max_domains 100000
```

### For ReLU BaB

#### Run Clip and Verify with β-CROWN

Remove `--enable_complete_clip` to run vanilla β-CROWN.

```
python abcrown.py --config exp_configs/beta_crown/cifar_cnn_a_mix.yaml  --enable_complete_clip --initial_max_domain 200 

python abcrown.py --config exp_configs/beta_crown/cifar_cnn_a_mix4.yaml  --enable_complete_clip --initial_max_domain 200 

python abcrown.py --config exp_configs/beta_crown/cifar_cnn_a_adv.yaml  --enable_complete_clip --initial_max_domain 200 

python abcrown.py --config exp_configs/beta_crown/cifar_cnn_a_adv4.yaml  --enable_complete_clip --initial_max_domain 200 

python abcrown.py --config exp_configs/beta_crown/cifar_cnn_b_adv.yaml  --enable_complete_clip --initial_max_domain 200 

python abcrown.py --config exp_configs/beta_crown/cifar_cnn_b_adv4.yaml  --enable_complete_clip --initial_max_domain 200 

python abcrown.py --config exp_configs/beta_crown/mnist_cnn_a_adv.yaml  --enable_complete_clip --initial_max_domain 200

python abcrown.py --config exp_configs/vnncomp21/cifar10-resnet.yaml  --enable_complete_clip --initial_max_domain 200 

python abcrown.py --config exp_configs/vnncomp22/oval22.yaml  --enable_complete_clip --initial_max_domain 200 

python abcrown.py --config exp_configs/vnncomp24/cifar100.yaml  --enable_complete_clip --initial_max_domain 200 

python abcrown.py --config exp_configs/vnncomp24/tinyimagenet.yaml  --enable_complete_clip --initial_max_domain 200
```

#### Run Clip and Verify with GCP-CROWN with mip cuts

First, cd `./cuts/CPLEX_cuts` and follow the instrction by `README.md` to complie cut solver.

Remove `--enable_complete_clip` to run vanilla GCP-CROWN.

```
python abcrown.py --config exp_configs/GCP-CROWN/cifar_cnn_a_mix.yaml  --enable_complete_clip

python abcrown.py --config exp_configs/GCP-CROWN/cifar_cnn_a_mix4.yaml  --enable_complete_clip

python abcrown.py --config exp_configs/GCP-CROWN/cifar_cnn_a_adv.yaml  --enable_complete_clip

python abcrown.py --config exp_configs/GCP-CROWN/cifar_cnn_a_adv4.yaml  --enable_complete_clip

python abcrown.py --config exp_configs/GCP-CROWN/cifar_cnn_b_adv.yaml  --enable_complete_clip

python abcrown.py --config exp_configs/GCP-CROWN/cifar_cnn_b_adv4.yaml  --enable_complete_clip

python abcrown.py --config exp_configs/GCP-CROWN/mnist_cnn_a_adv.yaml  --enable_complete_clip

python abcrown.py --config exp_configs/GCP-CROWN/cifar10-resnet.yaml  --enable_complete_clip

python abcrown.py --config exp_configs/vnncomp22/oval22.yaml  --enable_complete_clip
```

#### Run Clip and Verify with GCP-CROWN with BICCOS

Remove `--enable_complete_clip` to run vanilla BICCOS.

```
python abcrown.py --config exp_configs/BICCOS/cifar_cnn_a_mix/biccos_all_selective_mts_plus_gcp.yaml --enable_complete_clip

python abcrown.py --config exp_configs/BICCOS/cifar_cnn_a_mix4/biccos_all_selective_mts_plus_gcp.yaml --enable_complete_clip  

python abcrown.py --config exp_configs/BICCOS/cifar_cnn_a_adv/biccos_all_selective_mts_plus_gcp.yaml --enable_complete_clip  

python abcrown.py --config exp_configs/BICCOS/cifar_cnn_a_adv4/biccos_all_selective_mts_plus_gcp.yaml --enable_complete_clip  

python abcrown.py --config exp_configs/BICCOS/cifar_cnn_b_adv/biccos_all_selective_mts_plus_gcp.yaml --enable_complete_clip 

python abcrown.py --config exp_configs/BICCOS/cifar_cnn_b_adv4/biccos_all_selective_mts_plus_gcp.yaml --enable_complete_clip  

python abcrown.py --config exp_configs/BICCOS/mnist_cnn_a_adv/biccos_all_selective_mts_plus_gcp.yaml --enable_complete_clip  

python abcrown.py --config exp_configs/BICCOS/oval22/biccos_all_selective_mts_plus_gcp.yaml --enable_complete_clip  

python abcrown.py --config exp_configs/BICCOS/cifar10_resnet/biccos_all_selective_mts_plus_gcp.yaml --enable_complete_clip  

python abcrown.py --config exp_configs/BICCOS/cifar100/biccos_all_selective_mts.yaml --enable_complete_clip  

python abcrown.py --config exp_configs/BICCOS/tinyimagenet/biccos_all_selective_mts.yaml --enable_complete_clip
```
