A Unified View of Piecewise Linear Neural Network Verification

Authors: Rudy R. Bunel, Ilker Turkaslan, Philip Torr, Pushmeet Kohli, Pawan K. Mudigonda

NeurIPS 2018 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Experimental We use the benchmark to provide the first experimental comparison of existing algorithms and identify the factors impacting the hardness of verification problems.
Researcher Affiliation Collaboration Rudy Bunel University of Oxford rudy@robots.ox.ac.uk Ilker Turkaslan University of Oxford ilker.turkaslan@lmh.ox.ac.uk Philip H.S. Torr University of Oxford philip.torr@eng.ox.ac.uk Pushmeet Kohli Deepmind pushmeet@google.com M. Pawan Kumar University of Oxford Alan Turing Institute pawan@robots.ox.ac.uk
Pseudocode Yes Algorithm 1 Branch and Bound
Open Source Code Yes All code and data necessary to replicate our analysis are released.
Open Datasets Yes The Collision Detection data set [6] attempts to predict whether two vehicles with parameterized trajectories are going to collide.
Dataset Splits No The paper refers to using datasets like Collision Detection, ACAS, and PCAMNIST, but does not provide specific details on how these datasets were split into training, validation, or test sets (e.g., percentages, sample counts, or explicit references to standard splits used).
Hardware Specification Yes We attempt to verify each property with a timeout of two hours, and a maximum allowed memory usage of 20GB, on a single core of a machine with an i7-5930K CPU.
Software Dependencies No The paper mentions software like 'Python', 'Gurobi', and 'GLPK library' but does not provide specific version numbers for these software dependencies, which are necessary for full reproducibility.
Experiment Setup Yes The base network has 10 inputs and 4 layers of 25 hidden units, and the property to prove is True with a margin of 1000. Each of the plot correspond to a variation of one of this parameters.