Towards Scalable Complete Verification of Relu Neural Networks via Dependency-based Branching
Authors: Panagiotis Kouvaros, Alessio Lomuscio
IJCAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We evaluate the method on all of the Re LU-based fully connected networks from the first competition for neural network verification. The experimental results obtained show 145% performance gains over the present state-of-the-art in complete verification. |
| Researcher Affiliation | Academia | Panagiotis Kouvaros and Alessio Lomuscio Department of Computing, Imperial College London, UK {p.kouvaros, a.lomuscio}@imperial.ac.uk |
| Pseudocode | Yes | Algorithm 1 The verification procedure. |
| Open Source Code | Yes | Venus2 is available at https://github.com/vas-group-imperial/ venus2. |
| Open Datasets | Yes | ACASXU [Julian et al., 2016] is a collection of 45 Re LU FFNNs which were developed as part of an airborne collision avoidance system to advise horizontal steering decisions for unmanned aircraft. MNIST [Le Cun et al., 1998] is a dataset comprising images of hand-written digits 0-9, each formatted as 28x28x1-pixel grayscale image. |
| Dataset Splits | No | The paper mentions using pre-trained models (MNIST2, MNIST4, MNIST6) and verifying them against robustness properties for '25 correctly classified images' but does not specify the train/validation/test splits used for the training of these networks or for the verification experiments themselves beyond the '25 images'. |
| Hardware Specification | Yes | All the experiments were carried out on an Intel Core i77700K (4 cores) equipped with 16GB RAM, running Linux kernel 4.15; the ablation experiment on the branching depth (see below) was carried out on an Intel Core i9-9900X (20 cores) equipped with 125GB RAM, running Linux kernel 5.3. |
| Software Dependencies | Yes | All MILP-based tools (Venus2, Eran, MIPVerify, Venus) rely on Gurobi 9.2 for the MILP backend. |
| Experiment Setup | Yes | Venus2 was run with the branching depth set to 4 for MNIST2 and MNIST4 and to 7 for ACASXU and MNIST6. The B&B node threshold was set to 500 for ACASXU and MNIST6, to 5000 for MNIST4 and to 10000 for MNIST2. |