Boosting Robustness Certification of Neural Networks

Authors: Gagandeep Singh, Timon Gehr, Markus Püschel, Martin Vechev

ICLR 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Experimental We evaluate the effectiveness of our approach for the robustness verification of Re LU-based feedforward and convolutional neural networks. The results show that our approach enables faster complete verification than the state-of-the-art complete verifiers: Wang et al. (2018b) and Tjeng et al. (2019), and produces more precise results than state-of-the-art incomplete verifiers: Deep Z (Singh et al., 2018) and Deep Poly (Singh et al., 2019), when complete certification becomes infeasible.
Researcher Affiliation Academia Gagandeep Singh, Timon Gehr, Markus P uschel, Martin Vechev Department of Computer Science ETH Zurich, Switzerland {gsingh,timon.gehr,pueschel,martin.vechev}@inf.ethz.ch
Pseudocode No The paper describes its approach formally but does not include any pseudocode or algorithm blocks.
Open Source Code Yes A complete end-to-end implementation of our approach in a system called Refine Zono, publicly available at https://github.com/eth-sri/eran.
Open Datasets Yes We used the popular MNIST (Lecun et al., 1998), CIFAR10 (Krizhevsky, 2009), and ACAS Xu (Julian et al., 2018) datasets in our experiments.
Dataset Splits No The paper mentions using a 'test set' for evaluation but does not provide specific details on train/validation/test dataset splits (e.g., percentages, counts, or explicit standard splits for reproduction).
Hardware Specification Yes All experiments for the 3 50 MNIST FNN and all CNNs were carried out on a 2.6 GHz 14 core Intel Xeon CPU E5-2690 with 512 GB of main memory; the remaining FNNs were evaluated on a 3.3 GHz 10 Core Intel i9-7900X Skylake CPU with a main memory of 64 GB.
Software Dependencies Yes Refine Zono uses Gurobi (Gurobi Optimization, LLC, 2018) for solving MILP and LP instances and is built on top of the ELINA library (eli, 2018; Singh et al., 2017) for numerical abstract domains.
Experiment Setup Yes We experimented with different values of the analysis parameters k MILP, k LP, k AI, θ, δ, β, T and chose values that offered the best tradeoff between performance and precision for the certification of each neural network. ... For MILP based refinement, we use θ = ω 5k 2 p where ω is the number of candidates and p is the total number of neurons in layer k. For LP based refinement, we use θ = ω 2k 5 p. We use timeout T = 1 second, β = 0.5, and δ = ω p θ for both MILP and LP based refinements.