Efficient Exact Verification of Binarized Neural Networks
Authors: Kai Jia, Martin Rinard
NeurIPS 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We demonstrate the effectiveness of EEV by presenting the first exact verification results for ℓ -bounded adversarial robustness of nontrivial convolutional BNNs on the MNIST and CIFAR10 datasets. Our experimental results show that, compared to exact verification of robustly trained real-valued networks with the same architectures, EEV delivers several orders of magnitude faster verification of BNNs with comparable verifiable accuracy in most cases. |
| Researcher Affiliation | Academia | Kai Jia MIT CSAIL 32 Vassar St, Cambridge, MA 02139 jiakai@mit.edu Martin Rinard MIT CSAIL 32 Vassar St, Cambridge, MA 02139 rinard@csail.mit.edu |
| Pseudocode | No | The paper describes various algorithms and methods (e.g., CDCL, Bin Mask, CBD loss, adaptive gradient cancelling) but does not present any of them in a structured pseudocode block or an explicitly labeled 'Algorithm' section. |
| Open Source Code | Yes | Our source code is available at https://github.com/jia-kai/eevbnn. |
| Open Datasets | Yes | We demonstrate the effectiveness of EEV by presenting the first exact verification results for ℓ -bounded adversarial robustness of nontrivial convolutional BNNs on the MNIST and CIFAR10 datasets. |
| Dataset Splits | Yes | We evaluate the performance of EEV on the task of verifying robustness of BNNs against ℓ -bounded input perturbations on the MNIST and CIFAR10 benchmarks. |
| Hardware Specification | No | The paper does not provide specific hardware details (e.g., GPU/CPU models, memory, or cloud instance types) used for conducting the experiments. It only discusses the theoretical aspects and software implementations. |
| Software Dependencies | No | Mini Sat CS extends Mini Sat 2.2 which is a highly optimized and minimalistic SAT solver... and ...the Glucose SAT solver [3] with the sequential counters encoding. While it mentions these, it does not provide a comprehensive list of software dependencies with specific version numbers (e.g., Python version, ML framework version, CUDA version) needed to fully replicate the environment. |
| Experiment Setup | Yes | We set τ = 5 in our experiments because it is an empirically good choice among a few values that enables fine control of the accuracy-speed tradeoff by tuning η. We present details of the experimental settings in the supplementary material. |