[The GDVB Framework] Systematic Generation of Diverse Benchmarks for DNN Verification

I. Overview

The GDVB framework, which was developed for the paper titled "Systematic Generation of Diverse Benchmarks for DNN Verification," serves as a means to showcase the functionality of the proposed methods outlined in the paper and to reproduce the evaluation results presented within. This artifact encompasses several components, including 1) guidelines for installing the GDVB framework and its dependencies, 2) a tutorial on generating a small DNN verification benchmark using a toy MNIST seed problem, 3) detailed information about the configurable parameters, and 4) instructions and scripts to fully replicate the research results. It is important to note that the GDVB tool is implemented in the Python programming language, thus users are expected to possess a certain level of familiarity with Python, as well as neural network training and verification techniques.

GDVB supports generating NNV benchmarks using Fully Connected and Convolutional seed neural networks. From GDVB version 2.0.0 on, users can scale up seed verification problems. This means the benchmark instances can have more neurons, more FC and Conv layers, and more input dimensions than the original seed network. Refer to section IV for more information.

II. Installation

Acquire the Conda environment management tool. Install and activate the gdvb conda environment.
```
conda env create --name gdvb -f .env.d/env.yml
. .env.d/openenv.sh
```
Acquire the ACTS covering array generation tool and store the jar file as lib/acts.jar.
Install dependencies.

3.1 (Required) Get R4V and install it's conda environment.
```
git clone https://github.com/edwardxu0/R4V.git lib/R4V
conda env create --name r4v -f ${R4V}/.env.d/env.yml
```
3.2 (Optional) Get SwarmHost and install it's conda environment. Follow it's guide to install the tool and verifiers. Make sure to install SwarmHost in a separate conda environment named swarmhost.
```
git clone https://github.com/edwardxu0/SwarmHost.git lib/SwarmHost
conda env create --name swarmhost -f ${SwarmHost}/.env.d/env.yml
```
3.3 (Optional) Get DNNV if you wish to use the verifiers in DNNV. Follow its instructions to install the tool and verifiers. Make sure to install DNNV in a separate conda environment named dnnv.

3.4 (Optional) Get DNNF if you wish to use the falsifiers in DNNF. Follow its instructions to install the tool. Make sure to install DNNF in a separate conda environment named dnnf.
The environment variables are stored in the .env.d/openenv.sh file. Modifying the values within this file can potentially resolve certain dependency issues, such as the location of GUROBI licenses.

III. Tutorial on GDVB

In this section, we employ GDVB on the toy "MNIST_tiny" seed verification problem to produce a small DNN verification benchmark and execute the verification process within the SwarmHost framework using the abcrown verifier. Subsequently, we analyze verification results with the SCR and PAR2 metrics.

The "MNIST_tiny" seed verification problem includes a small neural network and a local robustness property. The neural network has 3 hidden layers with 50 neurons in each. The local robustness property is defined on epsilon of 0.02. The configuration file is stored as configs/mnist_tiny.toml. It defines two factors, the number of neurons and number of FC layers, where each has three evenly distributed levels, e.g., 1/3, 2/3, and 1 scaling ratio compared to the seed network.

The GDVB framework employs a command-line interface for its operations. To ensure the correct installation of GDVB, one should load the conda environment and consult the help manual.

. .env.d/openenv.sh
gdvb -h

   __________ _    ______ 
  / ____/ __ \ |  / / __ )
 / / __/ / / / | / / __  |
/ /_/ / /_/ /| |/ / /_/ / 
\____/_____/ |___/_____/  
                          
usage: GDVB [-h] [--seed SEED] [--result_dir RESULT_DIR] [--override] [--debug] [--dumb]
            configs {C,T,P,V,A,E}

Generative Diverse Verification Benchmarks for Nueral Network Verification

positional arguments:
  configs               Configurations file.
  {C,T,P,V,A,E}         Select tasks to perform, including, compute [C]A, [T]rtain benchmark
                        networks, generate [P]roperties, [V]erify benchmark instances, [A]nalyze
                        benchmark results, and [E]verything above.

options:
  -h, --help            show this help message and exit
  --seed SEED           Random seed.
  --result_dir RESULT_DIR
                        Result directory.
  --override            Override existing logs.
  --debug               Print debug log.
  --dumb                Silent mode.

Generate the verification Benchmark.

2.1) Generate the Mix Covering Array.

gdvb configs/mnist_tiny.toml C

   __________ _    ______ 
  / ____/ __ \ |  / / __ )
 / / __/ / / / | / / __  |
/ /_/ / /_/ /| |/ / /_/ / 
\____/_____/ |___/_____/  
                          
[INFO] 02/14/2024 12:19:12 PM : Computing Factors 
[INFO] 02/14/2024 12:19:12 PM : Computing Covering Array 
[INFO] 02/14/2024 12:19:12 PM : # problems: 9 
[INFO] 02/14/2024 12:19:12 PM : Computing DNN Specifications 
[INFO] 02/14/2024 12:19:12 PM : # NN: 9 
[INFO] 02/14/2024 12:19:12 PM : Spent 0.240134 seconds.

This step will generate the MCA at ./results/mnist_tiny.0/cas/ca_*.txt. This file contains the factor-level description of the benchmark instances. Below are the first few lines of the generated covering array. For each test case, the parameters are the verification performance factors and their assignments are chosen the levels, which are 0 indexed. For more detailed information, please consult the ACTS documentation.

# Degree of interaction coverage: 2
# Number of parameters: 2
# Maximum number of values per parameter: 3
# Number of configurations: 9
------------Test Cases--------------

Configuration #1:

1 = neu=0
2 = fc=0

-------------------------------------

Configuration #2:

1 = neu=0
2 = fc=1

2.2) Train the neural networks.

gdvb configs/mnist_tiny.toml T

   __________ _    ______ 
  / ____/ __ \ |  / / __ )
 / / __/ / / / | / / __  |
/ /_/ / /_/ /| |/ / /_/ / 
\____/_____/ |___/_____/  
                          
[INFO] 02/14/2024 01:30:37 PM : Computing Factors 
[INFO] 02/14/2024 01:30:37 PM : Computing Covering Array 
[INFO] 02/14/2024 01:30:37 PM : # problems: 9 
[INFO] 02/14/2024 01:30:37 PM : Computing DNN Specifications 
[INFO] 02/14/2024 01:30:37 PM : # NN: 9 
[INFO] 02/14/2024 01:30:37 PM : Training ... 
Training ... :   0%|                                             | 0/9 [00:00<?, ?it/s]
[INFO] 02/14/2024 01:30:37 PM : Training network: neu=0.3333_fc=0.3333_idm=1.0000_ids=1.0000_SF=0.6667 ... 
Training ... :  11%|█████                                        | 1/9 [03:05<24:45, 185.68s/it]
[INFO] 02/14/2024 01:33:43 PM : Training network: neu=0.3333_fc=0.6667_idm=1.0000_ids=1.0000_SF=0.6667 ... 
Training ... :  22%|██████████                                   | 2/9 [06:26<22:43, 194.76s/it]
[INFO] 02/14/2024 01:37:04 PM : Training network: neu=0.3333_fc=1.0000_idm=1.0000_ids=1.0000_SF=0.3333 ... 
Training ... :  33%|███████████████▎                             | 3/9 [09:45<19:39, 196.56s/it]
[INFO] 02/14/2024 01:40:23 PM : Training network: neu=0.6667_fc=0.3333_idm=1.0000_ids=1.0000_SF=1.3333 ... 
Training ... :  44%|████████████████████▍                        | 4/9 [13:09<16:37, 199.47s/it]
[INFO] 02/14/2024 01:43:47 PM : Training network: neu=0.6667_fc=0.6667_idm=1.0000_ids=1.0000_SF=1.3333 ... 
Training ... :  56%|█████████████████████████                    | 5/9 [16:17<13:01, 195.42s/it]
[INFO] 02/14/2024 01:46:55 PM : Training network: neu=0.6667_fc=1.0000_idm=1.0000_ids=1.0000_SF=0.6667 ... 
Training ... :  67%|██████████████████████████████               | 6/9 [19:43<09:56, 198.81s/it]
[INFO] 02/14/2024 01:50:20 PM : Training network: neu=1.0000_fc=0.3333_idm=1.0000_ids=1.0000_SF=2.0000 ... 
Training ... :  78%|███████████████████████████████████          | 7/9 [22:54<06:32, 196.39s/it]
[INFO] 02/14/2024 01:53:32 PM : Training network: neu=1.0000_fc=0.6667_idm=1.0000_ids=1.0000_SF=2.0000 ... 
Training ... :  89%|████████████████████████████████████████     | 8/9 [26:03<03:13, 193.94s/it]
[INFO] 02/14/2024 01:56:41 PM : Training network: neu=1.0000_fc=1.0000_idm=1.0000_ids=1.0000_SF=1.0000 ... 
Training ... : 100%|█████████████████████████████████████████████| 9/9 [29:28<00:00, 196.50s/it]
[INFO] 02/14/2024 02:00:06 PM : Spent 1768.792314 seconds.

The R4V configurations, as specified by the MCA, will be generated in this stage and the neural networks will be distilled accordingly. The distilled neural network models in ONNX format will be stored in the directory results/mnist_tiny.0/dis_model/, while the training logs will be saved in results/mnist_tiny.0/dis_log/.

2.3 (Optional) Generate properties.

configs/mnist_tiny.toml P

   __________ _    ______ 
  / ____/ __ \ |  / / __ )
 / / __/ / / / | / / __  |
/ /_/ / /_/ /| |/ / /_/ / 
\____/_____/ |___/_____/  
                        
[INFO] 02/14/2024 11:16:31 PM : Computing Factors 
[INFO] 02/14/2024 11:16:31 PM : Computing Cover

GDVB

Install / Use

README

[The GDVB Framework] Systematic Generation of Diverse Benchmarks for DNN Verification

I. Overview

II. Installation

III. Tutorial on GDVB