Verifying Properties of Binarized Deep Neural Networks
Authors: Nina Narodytska, Shiva Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, Toby Walsh
AAAI 2018 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | For this property, our experimental results demonstrate that our approach scales to medium-size deep neural networks used in image classification tasks. In Section 8, we present a set of experiments on the MNIST dataset and its variants. |
| Researcher Affiliation | Collaboration | Nina Narodytska VMware Research Palo Alto, USA Shiva Kasiviswanathan Amazon Palo Alto, USA Leonid Ryzhyk VMware Research Palo Alto, USA Mooly Sagiv VMware Research Palo Alto, USA Toby Walsh UNSW and Data61 Sydney, Australia |
| Pseudocode | No | The paper describes the encoding process mathematically and with examples, but it does not provide formal pseudocode blocks or algorithms. |
| Open Source Code | No | The paper does not include any explicit statements about releasing source code or provide links to a code repository. |
| Open Datasets | Yes | We trained networks on the MNIST dataset (Le Cun et al. 1998), and two modern variants of MNIST: the MNIST-rot and the MNIST-back-image (Larochelle, Erhan, and Courville 2017). |
| Dataset Splits | No | The paper mentions selecting images from the test set for experiments and discusses a 'training phase' but does not specify the explicit splits (e.g., percentages or counts) for training, validation, and test sets. It doesn't mention a validation set at all, only test. |
| Hardware Specification | Yes | We used the Torch machine learning framework to train networks on a Titan Pascal X GPU. |
| Software Dependencies | No | The paper mentions 'Torch machine learning framework' and 'SCIP solver' and 'Glucose SAT solver', but it does not provide specific version numbers for any of these software dependencies. |
| Experiment Setup | Yes | Our network consists of four internal blocks with each block containing a linear layer (LIN) and a final output block. The linear layer in the first block contains 200 neurons and the linear layers in other blocks contain 100 neurons. We use the batch normalization (BN) and binarization (BIN) layers in each block as detailed in Section 3. We experimented with three different maximum perturbation values by varying ϵ {1, 3, 5}. The timeout is 300 seconds for each instance to solve. |