Benchmark networks of the AAAI 2021 paper Scalable Verification of Quantized Neural Networks

Link to the arXiv version

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.

python3 iterate_samples.py --dataset fashion-mnist

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.

Benchmark 1	MNIST
Network size	784-64-10
Input quantization	8-bit
Network quanization (weights and activations)	6-bit
Samples	400 (100 per epsilon value)
Epsilons (L-infinity norm)	1,2,3,4
Weights	weights/mnist_mlp.h5

Benchmark 2	Fashion-MNIST
Network size	784-64-10
Input quantization	8-bit
Network quanization (weights and activations)	6-bit
Samples	300 (50/100 per epsilon value)
Epsilons (L-infinity norm)	1,2,3,4
Weights	weights/fashion-mnist_mlp.h5

Quantitative results from the paper

MNIST samples 0-99

Type	Test sample ID
Misclassified (1)	18
Timeout (0)	-
Vulnerable (0)	-
Robust (99)	Remaining

MNIST samples 100-199

Type	Test sample ID
Misclassified (1)	149
Timeout (5)	104, 119, 175, 193, 195
Vulnerable (3)	115, 151, 158
Robust (91)	Remaining

MNIST samples 200-299

Type	Test sample ID
Misclassified (4)	217, 241, 247, 259
Timeout (25)	204, 210, 211, 218, 221, 224, 227, 232, 233, 234, 235, 243, 244, 250, 251, 255, 257, 264, 266, 273, 274, 275, 289, 290, 299
Vulnerable (1)	282
Robust (70)	Remaining

MNIST samples 300-399

Type	Test sample ID
Misclassified (3)	321, 340, 381
Timeout (43)	300, 301, 303, 307, 308, 322, 324, 325, 326, 328, 329, 335, 336, 337, 339, 341, 344, 345, 349, 350, 352, 354, 357, 358, 359, 362, 366, 368, 370, 372, 373, 377, 376, 379, 383, 385, 386, 388, 389, 391, 393, 394, 397
Vulnerable (1)	320
Robust (53)	Remaining

Fashion-MNIST samples 0-99

Type	Test sample ID
Misclassified (13)	12, 17, 23, 25, 26, 29, 40, 48, 51, 66, 68, 89, 98
Timeout (11)	4, 21, 28, 42, 43, 44, 49, 57, 67, 73, 91
Vulnerable (0)	-
Robust (76)	Remaining

Fashion-MNIST samples 100-199

Type	Test sample ID
Misclassified (10)	107, 127, 145, 147, 150, 153, 163, 183, 192, 193
Timeout (17)	101, 117, 122, 129, 136, 149, 151, 157, 166, 170, 172, 181, 188, 191, 195, 197, 198
Vulnerable (1)	135
Robust (72)	Remaining

Fashion-MNIST samples 200-249

Type	Test sample ID
Misclassified (7)	222, 226, 239, 241, 244, 247, 249
Timeout (16)	203, 205, 202, 213, 217, 219, 221, 224, 228, 230, 235, 238, 243, 245, 246, 248
Vulnerable (1)	227
Robust (26)	Remaining

Fashion-MNIST samples 300-349

Type	Test sample ID
Misclassified (6)	316, 322, 324, 325, 332, 344
Timeout (26)	300, 301, 302, 304, 312, 313, 309, 308, 311, 315, 318, 319, 320, 321, 323, 326, 329, 331, 333, 334, 336, 337, 338, 341, 342, 348
Vulnerable (0)	-
Robust (18)	Remaining

Using other SMT solvers

Each benchmark SMT formula can be exported and then checked by a different SMT solver than boolector

For instance, CVC4 (note: this will not terminate)

python3 check_mnist_robustness.py --sample_id 115 --eps 2 --export
./cvc4-1.8-x86_64-linux-opt  --lang smt smt2/mnist_0115.smt2