oval-group/scaling-the-convex-barrier

Scaling the convex barrier for piecewise-linear neural network verification

Scaling the Convex Barrier with Active Sets

This repository contains all the code necessary to replicate the findings described in: Scaling the Convex Barrier with Active Sets. If you use it in your research, please cite:

@Article{DePalma2021,
    title={Scaling the Convex Barrier with Active Sets},
    author={De Palma, Alessandro and Behl, Harkirat Singh and Bunel, Rudy and Torr, Philip H. S. and Kumar, M. Pawan},
    journal={International Conference on Learning Representations},
    year={2021}
}

Neural Network bounds

The code for the following bounding algorithms for ReLU-based neural networks (and, more generally, piecewise-linear networks, which can be transformed into equivalent ReLUs) is provided:

• LinearizedNetwork in plnn/network_linear_approximation.py represents the PLANET relaxation of the network in Gurobi and uses the commercial solver to compute the model's output bounds.
• AndersonLinearizedNetwork in plnn/anderson_linear_approximation.py implements, in Gurobi, the linear relaxation by Anderson et al. (2020), a linear relaxation for piecewise-linear activations that is significantly tighter than the Planet relaxation. It implements the cutting plane algorithm presented by Anderson et al. both for LP relaxations and solving the complete verification MIP.
• ExpLP in plnn/explp_solver/solver.py implements the Active Set algorithm presented in the paper, a sparse dual solver for the linear relaxation by Anderson et al. (2020).
• SaddleLP in plnn/proxlp_solver/solver.py implements the dual iterative algorithms presented in "Lagrangian Decomposition for Neural Network Verification" in PyTorch, based on the Lagrangian Decomposition of the activation's convex relaxations. For ReLUs, it operates on the Planet relaxation.

These classes offer two main interfaces (see, for instance tools/bounding_tools/anderson_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_bounds, 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.

The computed neural network bounds can be employed in two different ways: alone, to perform incomplete verification; as the bounding part of branch and bound (to perform complete verification).

Branch and Bound

As part of the code release, we include BaBSR, a branch-and-bound algorithm from Branch and Bound for Piecewise Linear Neural Network Verification. Its implementation is provided in plnn/branch_and_bound/. In case dual iterative algorithms are employed for the bounding, a number of BaB sub-problems (nodes) is solved in parallel at once as a PyTorch batch.

Repository structure

• ./plnn/ contains the code for the bounding algorithms and the Branch and Bound framework.
• ./tools/ contains code to interface the bounds computation classes and the BaB framework.
• ./scripts/ is a set of python scripts that, via ./tools, run the paper's experiments.
• ./models/ contains the trained neural network employed for both the complete and incomplete verification experiments.
• verification_datasets/ contains the complete verification dataset employed in the paper, a subset of the one from Neural Network Branching for Neural Network Verification.

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 and the Integer programs for the MIP formulation. 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.

git clone --recursive https://github.com/oval-group/plnn-bab.git

cd scaling-the-convex-barrier

#Create a conda environment
conda create -n scaling-the-convex-barrier python=3.6
conda activate scaling-the-convex-barrier

# 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)
conda install pytorch torchvision cudatoolkit=9.2 -c pytorch

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

Running the experiments

The paper's experiments can be replicated as follows (adapting hardware parameters according to one's needs):

# complete verification -- In the paper, Gurobi uses 6 CPU cores
python scripts/run_anderson_bab_cifar.py --gpu_id 0 --cpus 0-5
# incomplete verification -- the paper uses 4 CPU cores
python scripts/run_anderson_incomplete.py --gpu_id 0 --cpus 0-3 --experiment all

and then plotted as:

# complete verification
python tools/bab_tools/plot_verification.py
# incomplete verification
python tools/parse_bounds.py --experiment iclr