NPAQ: Quantitative Verification for Neural Nets

NPAQ (Neural Property Approximate Quantifier) is a quantitative verification
tool that can quantify robustness, fairness and trojan attack success for
binarized neural networks (BNNs). This work is by Teodora Baluta, Shiqi Shen,
Shweta Shinde, Kuldeep S. Meel and Prateek Saxena, as published in CCS
2019. NPAQ relies on
approximate model counting and uses the latest version of
ApproxMCv3.

How to Build

To build on Linux you need the following:

• Python 2.7
• (currently z3 requirement but will this dependency will be eliminated when we
  cleanup more of the code)
• ApproxMC

First, compile the encoder:

cd mlp2cnf; make

Next, install the other requirements in a virtualenv (here, npaq):

mkvirtualenv npaq
pip install -r requirements.txt
./setup.sh

Unless you want NPAQ to only encode your problem to a CNF formula and not do any
quantification (for whatever reason) you will not need approxmc. Otherwise,
please follow the setup instructions for ApproxMC
here and make sure
approxmc is in your path.

Usage Example

It is always a good idea to check the options with python npaq --help from the
project’s root directory but we will go over the options below.

Selecting the Architecture, Dataset and Input Size

• Architecture: You can specify the number of blocks and neurons per
  block either as a JSON file (see [1]) or you can select from the predefined
  ones: {1blk_100, 2blk_100_50}
  See npaq/models/bnn.py for the definitions and project page for details on the BNN models in
  the benchmark.

• Dataset: By default, the dataset is MNIST (--dataset mnist), you can select UCI Adult dataset
  using the option --dataset uci_adult.

• Input size: The input size is a pair width,height where (--resize) and the
  dataset (--dataset).

Quantifying Properties

• Encoding to CNF formulas: encode. This just encodes the BNN to a CNF
  formula. 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 file name should be
  in the following format bnn_784_3blks_200_100.pt.
  Example query:

python npaq bnn --arch 1blk_100 --dataset uci_adult --resize 10,10 encode

• Quantify Fairness: quant-fair constraints_fname. To quantify fairness you
  need to specify the path to the constraints file. To reproduce the results in
  the paper, you need to select the right dataset --dataset uci_adult and the
  corresponding constraints file from the provided fairness constraints in the
  benchmarks. You can specify to just encode
  the property to a CNF formula without quantifying by adding the
  --just-encode flag.
  Example query:

python npaq bnn --arch 1blk_100 --dataset uci_adult --resize 1,66 quant-fair uci_adult-marital.txt

• Quantify Robustness: quant-robust perturb. To quantify robustness, specify
  the perturbation size as a L1-distance, i.e., the number of bits different in
  the adversarial example. You can specify to just encode the property to a CNF
  formula without quantifying by adding the --just-encode flag.
  Example query:

python npaq bnn --arch 1blk_100 --dataset mnist --resize 10,10 quant-robust 2

The query above is taking an image from mnist at random. You may specify a concrete input as
following:

python npaq bnn --encoder card --arch 1blk_100 --dataset mnist --resize 10,10 quant-robust 2 --concrete_ip concrete_inputs --num_samples 1

• Trojan Attack Success: The trojan attack success property reduces to quantifying how many inputs
  with specific input constraints (the trigger constraints found under trojan_imgs folder) are
  labeled as the attack’s target label. We encode the trojan sucess for all labels and all epochs
  for a specific architecture as follows:

python npaq bnn --encoder card --arch 1blk_100 --dataset mnist --resize 10,10 quant-label --w_trojan trojan-success --just-encode

Models and BNN Training

We provide the trained models used in the paper as .pt files in at our
project page. Just copy them in the models/mnist folder and specify the
architecture with the --arch option

We used the PyTorch implementation of the binarized neural networks available at
BinaryNet.pytorch, hence
there might be differences in the API between current PyTorch versions and the
older versions torch==1.0.1.post2 and torchvision==0.2.2.post3. To use GPU
you should make sure you have the right version for cuda and cuDNN (these should
ship with the pytorch installation). If there are any issues with running on
GPU, you may use the --no-cuda flag to disable GPU.

You can train your own BNNs using NPAQ. For example, you may write the following
command to train a BNN on the MNIST dataset:

python npaq bnn --dataset mnist train --no-cuda

See training help menu with python npaq bnn train --help.

How to Cite

If you use NPAQ, please cite our work.

The benchmarks used in our evaluation can be found here. More info on the
project page, NPAQ.

Checkout our subsequent work on this in PROVERO.