|
1 | | -# NPAQ |
2 | | -Neural Property Approximate Quantifier |
| 1 | +# NPAQ: Quantitative Verification for Neural Nets |
3 | 2 |
|
4 | | -## Setup & Requirements |
| 3 | +NPAQ (Neural Property Approximate Quantifier) is a quantitative verification |
| 4 | +tool that can quantify robustness, fairness and trojan attack success for |
| 5 | +binarized neural networks (BNNs). This work is by Teodora Baluta, Shiqi Shen, |
| 6 | +Shweta Shinde, Kuldeep S. Meel and Prateek Saxena, as published in [CCS |
| 7 | +2019](https://www.comp.nus.edu.sg/~teodorab/papers/NPAQ.pdf). NPAQ relies on |
| 8 | +approximate model counting and uses the latest version of |
| 9 | +[ApproxMCv3](https://github.com/meelgroup/ApproxMC). |
| 10 | + |
| 11 | +## How to Build |
| 12 | + |
| 13 | +To build on Linux you need the following: |
5 | 14 |
|
6 | 15 | - Python 2.7 |
7 | | -- (currently z3 requirement but will this dependency will be eliminated) |
8 | | -- (optional) scalmc (unless only encoding mode is used, you need to have scalmc installed) |
| 16 | +- (currently z3 requirement but will this dependency will be eliminated when we |
| 17 | + cleanup more of the code) |
| 18 | +- ApproxMC |
9 | 19 |
|
| 20 | +First, compile the encoder: |
| 21 | + |
| 22 | +``` |
| 23 | +cd mlp2cnf; make |
| 24 | +``` |
10 | 25 |
|
11 | | -First, compile the encoder `cd mlp2cnf; make`. |
| 26 | +Next, install the other requirements in a virtualenv (here, `npaq`): |
12 | 27 |
|
13 | | -We recommend you use a virtualenv |
| 28 | +``` |
| 29 | +mkvirtualenv npaq |
14 | 30 |
|
15 | | -`mkvirtualenv npaq |
16 | 31 | pip install -r requirements.txt |
| 32 | +
|
17 | 33 | ./setup.sh |
| 34 | +``` |
18 | 35 |
|
19 | | -### BNN Training |
| 36 | +Unless you want NPAQ to only encode your problem to a CNF formula and not do any |
| 37 | +quantification (for whatever reason) you will not need `approxmc`. Otherwise, |
| 38 | +please follow the setup instructions for ApproxMC |
| 39 | +[here](https://github.com/meelgroup/ApproxMC#how-to-build) and make sure |
| 40 | +`approxmc` is in your path. |
20 | 41 |
|
21 | | -We used the PyTorch implementation of the binarized neural networks available at |
22 | | -<https://github.com/itayhubara/BinaryNet.pytorch>, hence there might be |
23 | | -differences in the API between current PyTorch versions and the older versions |
24 | | -`torch==1.0.1.post2` and `torchvision==0.2.2.post3`. To use GPU you should make |
25 | | -sure you have the right version for cuda and cuDNN (these should ship with the |
26 | | -pytorch installation). If there are any issues with running on GPU, you may use |
27 | | -the `--no-cuda` flag to disable GPU. |
| 42 | +## Usage Example |
28 | 43 |
|
29 | | -For example, you may write the following command to train a BNN on the MNIST |
30 | | -dataset: |
| 44 | +It is always a good idea to check the options with `python npaq --help` from the |
| 45 | +project's root directory but we will go over the options below. |
31 | 46 |
|
32 | | -`python npaq bnn --dataset mnist train --no-cuda` |
| 47 | +### Selecting the Architecture, Dataset and Input Size |
33 | 48 |
|
34 | | -See training help menu with `python npaq bnn train --help`. |
| 49 | +- Architecture: You can specify the number of blocks and neurons per |
| 50 | +block either as a JSON file (see [1]) or you can select from the predefined |
| 51 | +ones: `{1blk_100, 2blk_100_50}` |
| 52 | +See `npaq/models/bnn.py` for the definitions and project page for details on the [BNN models in |
| 53 | +the benchmark](https://teobaluta.github.io/npaq/#bnn_models). |
| 54 | + |
| 55 | +- Dataset: By default, the dataset is MNIST (`--dataset mnist`), you can select UCI Adult dataset |
| 56 | + using the option `--dataset uci_adult`. |
| 57 | + |
| 58 | +- Input size: The input size is a pair _width,height_ where (`--resize`) and the |
| 59 | +dataset (`--dataset`). |
| 60 | + |
| 61 | + |
| 62 | +### Quantifying Properties |
35 | 63 |
|
36 | | -## Example Usage |
| 64 | +- Encoding to CNF formulas: `encode`. This just encodes the BNN to a CNF |
| 65 | + formula. The encode option assumes there is a trained model in `models/mnist/` in the |
| 66 | +format of a `.pt` file (PyTorch model). For example, for a BNN with architecture |
| 67 | +of 3 internal blocks with 200 neurons and an output block with 100 neuron-input |
| 68 | +trained over an input of 28x28 (the default MNIST input) the file name should be |
| 69 | +in the following format `bnn_784_3blks_200_100.pt`. |
| 70 | +Example query: |
37 | 71 |
|
38 | | -It's always a good idea to check the options with --help. |
| 72 | +`python npaq bnn --arch 1blk_100 --dataset uci_adult --resize 10,10 encode` |
39 | 73 |
|
40 | | -The general structure is to first specify that we are dealing with BNNs, next to specify neural network architecture (`--arch`), input size (`--resize`) and the dataset (`--dataset`). |
41 | | -NPAQ offers the following options: |
| 74 | +- Quantify Fairness: `quant-fair constraints_fname`. To quantify fairness you |
| 75 | + need to specify the path to the constraints file. To reproduce the results in |
| 76 | + the paper, you need to select the right dataset `--dataset uci_adult` and the |
| 77 | + corresponding constraints file from the provided [fairness constraints in the |
| 78 | + benchmarks](https://teobaluta.github.io/npaq). You can specify to just encode |
| 79 | + the property to a CNF formula without quantifying by adding the |
| 80 | + `--just-encode` flag. |
| 81 | +Example query: |
42 | 82 |
|
43 | | -- `encode`(to just encode the BNN), `quant-fair`, `quant-robust` and `quant-canary` for trojan attack |
| 83 | +`python npaq bnn --arch 1blk_100 --dataset uci_adult --resize 1,66 quant-fair uci_adult-marital.txt` |
| 84 | + |
| 85 | +- Quantify Robustness: `quant-robust perturb`. To quantify robustness, specify |
| 86 | + the perturbation size as a L1-distance, i.e., the number of bits different in |
| 87 | + the adversarial example. You can specify to just encode the property to a CNF |
| 88 | + formula without quantifying by adding the `--just-encode` flag. |
| 89 | +Example query: |
44 | 90 |
|
45 | 91 | `python npaq bnn --arch 1blk_100 --dataset mnist --resize 10,10 quant-robust 2` |
46 | 92 |
|
47 | | -The encode option assumes there is a trained model in `models/mnist/` in the format of a `.pt` file (PyTorch model). For example, for a BNN with architecture of 3 internal blocks with 200 neurons and an output block with 100 neuron-input trained over an input of 28x28 (the default MNIST input) the model_name is bnn_784_3blks_200_100. |
| 93 | +- Trojan Attack Success: `quant-canary`. |
48 | 94 |
|
49 | | -I added support to specify the BNN model in a JSON config file. Instead of adding classes to the existing nncrusher/models/bnn.py for every architecture, we can use configs in JSON format. Tested training option only. Command is python nncrusher bnn-mnist --config example_cfg/bnn_1blk.json train. |
50 | | -JSON Schema: |
51 | 95 |
|
52 | | -``` |
53 | | -bnn_schema = { |
54 | | - "type" : "object", |
55 | | - "properties" : { |
56 | | - "model_type" : {"type": "string"}, |
57 | | - "name" : {"type": "string"}, |
58 | | - "blocks" : {"type": "array", |
59 | | - "items": { |
60 | | - "type" : "object", |
61 | | - "properties": { |
62 | | - "in_dim": {"type":"integer"}, |
63 | | - "out_dim": {"type": "integer"}, |
64 | | - "dropout": {"type": "boolean", "default": "false" } |
65 | | - }, |
66 | | - "required": ["in_dim", "out_dim"] |
67 | | - }, |
68 | | - }, |
69 | | - } |
70 | | -} |
71 | | -``` |
| 96 | +## Models and BNN Training |
| 97 | + |
| 98 | +We provide the trained models used in the paper as `.pt` files in at our |
| 99 | +[project page](). Just copy them in the `models/mnist` folder and specify the |
| 100 | +architecture with the `--arch` option |
| 101 | + |
| 102 | +We used the PyTorch implementation of the binarized neural networks available at |
| 103 | +[BinaryNet.pytorch](https://github.com/itayhubara/BinaryNet.pytorch), hence |
| 104 | +there might be differences in the API between current PyTorch versions and the |
| 105 | +older versions `torch==1.0.1.post2` and `torchvision==0.2.2.post3`. To use GPU |
| 106 | +you should make sure you have the right version for cuda and cuDNN (these should |
| 107 | +ship with the pytorch installation). If there are any issues with running on |
| 108 | +GPU, you may use the `--no-cuda` flag to disable GPU. |
| 109 | + |
| 110 | +You can train your own BNNs using NPAQ. For example, you may write the following |
| 111 | +command to train a BNN on the MNIST dataset: |
| 112 | + |
| 113 | +`python npaq bnn --dataset mnist train --no-cuda` |
| 114 | + |
| 115 | +See training help menu with `python npaq bnn train --help`. |
| 116 | + |
| 117 | + |
| 118 | +## How to Cite |
| 119 | + |
| 120 | +If you use NPAQ, please cite our work. |
| 121 | + |
| 122 | +The benchmarks used in our evaluation can be found [here](). More info on the |
| 123 | +project page, [NPAQ](https://teobaluta.github.io/npaq). |
0 commit comments