Simplex Verify

This repository contains code for Simplex Verify.

Neural Network bounds

The repository provides code for algorithms to compute output bounds for ReLU-based neural networks (and, more generally, piecewise-linear networks, which can be transformed into equivalent ReLUs). The main files are in the plnn/simplex_solver folder.

• Baseline_LinearizedNetwork in plnn/simplex_solver/baseline_gurobi_linear_approximation.py represents the PLANET relaxation of the network in Gurobi and uses the commercial solver to compute the model's output bounds.
• DP_LinearizedNetwork in plnn/simplex_solver/disjunctive_gurobi.py represents the proposed Simplex Relaxation relaxation of the network in Gurobi and uses the commercial solver to compute the model's output bounds.
• Baseline_SimplexLP in plnn/simplex_solver/baseline_solver.py implements the Opt-Lirpa Planet baseline in PyTorch, based on the Planet relaxation.
• SimplexLP in plnn/simplex_solver/solver.py implements the Simplex Verify algorithm presented in the paper, a fast lirpa style algorithm for our proposed relaxation.
• plnn/simplex_solver/baseline_cut_anderson_optimization.py is the file corresponding to the Active Sets

These classes offer two main interfaces (see, for instance tools/bounding_tools/simplex_cifar_bound_comparison.py for detailed usage, including algorithm parametrization):

• Given some pre-computed intermediate bounds, compute the bounds on the neural network output: call build_model_using_intermediate_net, then compute_lower_bound.
• Compute bounds for activations of all network layers, one after the other (each layer's computation will use the bounds computed for the previous one): define_linear_approximation.

Repository structure

• ./plnn/ contains the code for the various algorithms.
• ./tools/ contains code to interface the bounds computation classes.
• ./scripts/ is a set of python scripts that, via ./tools, run the paper's experiments.
• ./data/advertorch/ contains the trained neural network employed for both the complete and incomplete verification experiments.

Running the code

Dependencies

The code was implemented assuming to be run under python3.6. We have a dependency on:

• The Gurobi solver to solve the LP arising from the Network linear approximation. Gurobi can be obtained from here and academic licenses are available from here.
• Pytorch to represent the Neural networks and to use as a Tensor library.

Installation

We assume the user's Python environment is based on Anaconda.

cd simplex_verify

#Create a conda environment
conda create -n simplex-verify python=3.6
conda activate simplex-verify

# Install gurobipy 
conda config --add channels http://conda.anaconda.org/gurobi
pip install .
#might need
#conda install gurobi

# Install pytorch to this virtualenv
# (or check updated install instructions at http://pytorch.org)
# modify the cuda version to your version
conda install pytorch torchvision cudatoolkit=10.2 -c pytorch 

# Install the code of this repository
python setup.py install

# Install mmbt dependencies (required for multi-modal experiments)
pip install torch torchvision sklearn pytorch-pretrained-bert numpy tqdm matplotlib

# Install advertorch dependencies (required for adversarial training and pgd bounds)
cd advertorch
python setup.py install
cd ..

Execution

Finally, all l₁ robustness verification experiments can be replicated by running

python scripts/run_simplex_incomplete.py