When using or adapting the code and benchmarks, please cite
@inproceedings{henzinger2021scalable,
title={Scalable Verification of Quantized Neural Networks},
author={Henzinger, Thomas A and Lechner, Mathias and {\v{Z}}ikeli{\'c}, {\DJ}or{\dj}e},
booktitle={Proceedings of the AAAI Conference on Artificial Intelligence},
volume={35},
number={5},
pages={3787--3795},
year={2021}
}
Setup
Installing boolector
git clone https://github.com/boolector/boolector
cd boolector
./contrib/setup-cadical.sh
./contrib/setup-btor2tools.sh
./configure.sh --python --py3
cd build
make
Running the Bit-vector SMT encodings on the benchmarks
# Checking MNIST test set sample 1 with epsilon=1
python3 check_mnist_robustness.py --sample_id 1 --eps 1
# Checking MNIST test set sample 115 with epsilon=2
python3 check_mnist_robustness.py --sample_id 115 --eps 2
# Checking MNIST test set sample 200 with epsilon=3
python3 check_mnist_robustness.py --sample_id 200 --eps 3 --dataset fashion-mnist
Using the benchmarks for other method
The file iterate_samples.py shows how to load and use the networks.
It also iterates over the exact samples of the benchmark and output the corresponding epsilons to use.
When implementing some verification method of the networks of these benchmarks,
make sure they exactly match the bit-exact quantized rounding semantics in each layer.
The files quantization_layers.py and quantization_utils.py should serve as a good starting point.
Benchmark description
The benchmark consists of robustness verification queries.