Branch and Bound for Piecewise Linear Neural Network Verification
Authors: Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip H.S. Torr, Pushmeet Kohli, M. Pawan Kumar
JMLR 2020 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We use the data sets to conduct a thorough experimental comparison of existing and new algorithms and to provide an inclusive analysis of the factors impacting the hardness of verification problems. The last two sections conduct detailed experimental studies of verification methods on our comprehensive data sets. |
| Researcher Affiliation | Collaboration | Rudy Bunel EMAIL Ilker Turkaslan EMAIL Philip H.S. Torr EMAIL M. Pawan Kumar EMAIL Department of Engineering Science University of Oxford Oxford OX1 3PJ Jingyue Lu EMAIL Department of Statistics University of Oxford Oxford OX1 3LB Pushmeet Kohli EMAIL Deepmind London N1C 4AG |
| Pseudocode | Yes | Algorithm 1 Branch and Bound |
| Open Source Code | Yes | All code and data necessary to replicate our analysis have been released. |
| Open Datasets | Yes | We introduce comprehensive data sets consisting of trained as well as synthetic networks with fully connected and/or convolutional layers. Our curated convolutional data sets differ from these data sets and are able to bring new insights by verifying properties on range of epsilon values on the same network. All code and data necessary to replicate our analysis have been released. The Collision Detection data set (Ehlers, 2017a) ... The Airborne Collision Avoidance System (ACAS) data set, as released by Katz et al. (2017a) ... The Robust MNIST Network ... PCAMNIST and Twin Stream |
| Dataset Splits | Yes | For MNIST networks, the natural properties to verify are whether the predicted label changes if each input image is allowed to be perturbed within an epsilon-infinity norm ball.4 Since each combination of an image in the MNIST test set and an epsilon constitute a valid property, we randomly select test images and verify properties at a set of pre-specified epsilons ranging from 0.14 to 0.175 for Robust MNIST Network and from 0.11 to 0.14 for reduced Robust MNIST Network. |
| Hardware Specification | Yes | on a single core of a machine with an i7-5930K CPU. |
| Software Dependencies | No | The paper mentions "Gurobi solver", "GLPK solver", "Python", and "C++" as software used. However, it does not provide specific version numbers for any of these components, which is required for a reproducible description of ancillary software. |
| Experiment Setup | Yes | We use a timeout of two hours for each experiment, unless otherwise stated. and a maximum allowed memory usage of 20GB, on a single core of a machine with an i7-5930K CPU. For our experiments, we have used the complete version of ERAN with refinepoly domain and 10 seconds MILP timeout, as suggested in Singh et al. (2019b). All the rest of hyper-parameters are set as default values. |