Source Code

Source Code are avaible at : https://anonymous.4open.science/r/Olive-5C2C

OLIVE Code Structure

├── Compare

│ ├── alpha-beta-CROWN

│ ├── nets

│ └── vnncomp

├── data

│ ├── boxplotS

│ ├── histo_distribution

│ ├── MNIST

│ ├── output

│ ├── ParameterAnalysis

│ ├── scatterplotss

│ └── treeSpecification

├── nnverify

│ ├── attack

│ ├── bnb

│ ├── common

│ ├── domains

│ ├── nets

│ ├── proof_transfer

│ ├── __pycache__

│ ├── smoothing

│ ├── specs

│ ├── tests

│ └── training

├── olive.py

├── olive_util.py

├── olive_runall.py

├── olive_execute.py

└── olive_demo.py

Annotation:

The "\Compare" directory contains configuration files for AB-CROWN and Marabou.
The "\data" folder holds all datasets used in the paper.
The "\nnverifier" directory contains the baseline implementation of the branch-and-bound algorithm using the IVAN framework.

--------------------------------------------

olive.py: Contains the full implementation of Order Leading Incremental Verification (OLIVE).

olive_runall.py: A script to execute all experiments.

olive_execute.py: Runs a single verification instance.

olive_demi.py: Implements the motivational example described in the paper.

Our experimental data is all available in /data folder:

To check the distribution of our data, please refer to ./data/RQ0_data_histo_distribution.ipynb
To check the over all results, please refer to ./data/RQ1&4_statiscal.ipynb
To check the speedup, please refer to ./data/RQ3_scatterplot.ipynb
To check the violated and certified verification, please refer to ./data/RQ2&3_boxplot.ipynb and ./data/RQ2&3_boxplot2.ipynb
To check the hyper-parameter analysis, please refer to ./data/RQ4_heatMapHyper.ipynb

Usage of Olive

Now we are supporting MNIST and CIFAR-10 with OVAL21 models, we will support more dataset and model verification problems in the future. The incremental verification supports quantize 8, 16 bits, and weight pruning. For detailed installation, please refer to https://anonymous.4open.science/r/Olive-5C2C/README.md

# Use Prune for mnistL2 (default behavior)

python olive_execute.py mnist mnistL2 0 0.1 12 2000

# Use Quantize for mnistL4

python olive_execute.py mnist mnistL4 0 0.1 12 2000 true

# A use case for mnist dataset mnistL2 model with 92 image index under eps = 0.01568627450980392 with pruning 7% within 2000 seconds

python olive_execute.py mnist mnistL2 92 0.01568627450980392 7 2000

Results are shown as

Results for MNIST case (net_type: mnistL2, image_index: 92, eps: 0.01568627450980392, timeout: 2000, approx: Prune):

Reuse: Time: 15.375141620635986, Visited: 3, Output: Status.ADV_EXAMPLE

Greedy: Time: 7.9392383098602295, Visited: 1, Output: Status.ADV_EXAMPLE

Balance: Time: 7.573286533355713, Visited: 1, Output: Status.ADV_EXAMPLE

Baseline: Time: 13.422738075256348, Visited: 3, Output: Status.ADV_EXAMPLE

Google Sites

Report abuse