This repository contains PyTorch code for state-of-the-art GPU-accelerated neural network verification based on Branch and Bound (BaB), developed by the OVAL research group at the University of Oxford. See the "publications" section below for references.
Complete neural network verification can be cast as a non-convex global minimization problem, which can be solved via BaB. BaB operates by computing lower and upper bounds to the global minimum, which can be iteratively tightened by dividing the feasible domain into subproblems. Lower bounds can be obtained by solving a convex relaxation of the network via an incomplete verifier. Upper bounds are obtained via falsification algorithms (heuristics, such as adversarial attacks for adversarial robustness properties). The branching strategy, the algorithm employed to create the subproblems, strongly influences the tightness of the lower bounds.
The OVAL framework currently includes the following incomplete verifiers for piecewise-linear networks:
- IBP (Gowal et al. 2018) (
Propagationinplnn/proxlp_solver/propagation.py). - Propagation-based algorithms: CROWN (Zhang et al. 2018), Fast-Lin (Wong and Kolter 2018)
(
Propagationinplnn/proxlp_solver/propagation.py).
- Dual solvers for the convex hull of element-wise activations, based on Lagrangian Decomposition (Bunel et al. 2020b) (
SaddleLPinplnn/proxlp_solver/solver.py). - Gurobi solver for the Planet (Ehlers 2017) relaxation (
LinearizedNetworkinplnn/network_linear_approximation.py). - Beta-CROWN (Wang et al. 2021), a state-of-the-art solver for the Planet relaxation (
Propagationinplnn/proxlp_solver/propagation.py). - DeepVerify (Dvijotham et al. 2018) (
DJRelaxationLPinplnn/proxlp_solver/dj_relaxation.py).
- Active Set (De Palma et al. 2021c), and Saddle Point (De Palma et al. 2021a), state-of-the-art fast dual solvers for the tighter linear relaxation by
Anderson et al. (2020) (
ExpLPinplnn/explp_solver/solver.py). - Gurobi cutting-plane solver for the relaxation by Anderson et al. (2020)
(
AndersonLinearizedNetworkinplnn/anderson_linear_approximation.py).
These incomplete verifiers can be employed both to compute bounds on the networks' intermediate activations (intermediate bounds), or lower bounds on the network's output. Two main interfaces are available:
- Given some pre-computed intermediate bounds, compute the bounds on the neural network output:
call
build_model_using_bounds, thencompute_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.
Incomplete verifiers of different bounding tightness and cost can be combined by relying on stratification (section 6.3 of De Palma et al. (2021a)).
Subdomains are created by splitting the input domain or by splitting piecewise-linear activations into their linear components. The following two branching
strategies are available (plnn/branch_and_bound/branching_scores.py):
- The inexpensive input splitting heuristic from "BaB" in Bunel et al. (2020a).
- The SR activation splitting heuristic from from "BaBSR" in Bunel et al. (2020a).
- FSB (De Palma et al. 2021b): a state-of-the-art activation splitting strategy combining SR with inexpensive strong branching to significantly reduce verification times.
Upper bounding is performed using a generalization of the MI-FGSM attack (Dong et al. 2017) to general property falsification (MI_FGSM_Attack_CAN in adv_exp/mi_fgsm_attack_canonical_form.py).
The OVAL framework was developed as part of the following publications:
- "A Unified View of Piecewise Linear Neural Network Verification";
- "Branch and Bound for Piecewise Linear Neural Network Verification";
- "Lagrangian Decomposition for Neural Network Verification";
- "Scaling the Convex Barrier with Active Sets";
- "Scaling the Convex Barrier with Sparse Dual Algorithms";
- "Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition".
If you use our code in your research, please cite the papers associated to the employed algorithms, along with (Bunel et al. 2020a) and (De Palma et al. 2021b) for the BaB framework.
Additionally, learning-based algorithms for branching and upper bounding (not included in the framework) were presented in:
- "Neural Network Branching for Neural Network Verification";
- "Generating Adversarial Examples with Graph Neural Networks".
Code to aid towards the replication of the findings described in "Scaling the Convex Barrier with Sparse Dual Algorithms" is provided in folder scripts_jmlr.
Note, however, that these were based on an earlier version of the codebase.
The repository provides two main functionalities: incomplete verification (bounding) and complete verification (branch and bound). We now detail how to run the OVAL framework in each of the two cases.
File ./tools/local_robustness_from_onnx.py provides a script to verify that an .onnx network is robust to perturbations
in l_inf norm to its input points (local robustness verification).
The comments in the file indicate which blocks should be modified to perform verification of different input-output
specifications (which will need to be represented in canonical form, see section 2.1 of De Palma et al. (2021b)),
and detail its input interface.
Note that an .onnx input is not necessary: the user can alternatively specify a piecewise-linear network by directly
passing a list of layers to the bab_from_json function, as long as the network is in canonical form.
The configuration/parameters of OVAL BaB are passed via a .json configuration file (see those in ./bab_configs/).
As an example, execute the following command:
python tools/local_robustness_from_onnx.py --network_filename ./models/onnx/cifar_base_kw.onnx
Some details on how to produce a .json configuration file (see ./bab_configs/) for the OVAL framework can be found at json_instructions.md.
All the bounding algorithms contained in the repository share a common interface (see "Incomplete Verifiers" above).
File ./tools/bounds_from_onnx.py provides a guide to the interface and usage of the bounding (incomplete verification) algorithms.
The guide supports bounding computations for a loaded .onnx network, or for small randomly sampled networks.
As for the complete verification use-case, the user can modify the code to pass a piecewise-linear network as a list of PyTorch layers.
In addition, the file contains an example on how to directly run branch and bound without resorting to .json
configuration files. In this case, a small timeout is set to compute tighter bounds on the first output neuron of the loaded network.
As an example, execute the following command:
python tools/bounds_from_onnx.py --network_filename ./models/onnx/cifar_base_kw.onnx
Scripts to run the code within the context of VNNCOMP2021 are contained in ./vnncomp_scripts/.
Verification on a property expressed in the vnnlib format
(ONNX network for the network + .vnnlib file for the property) --or on a list of properties in a .csv file--
can be executed by running ./tools/bab_tools/bab_from_vnnlib.py (check the code for details).
In addition, code to run the framework on the OVAL and COLT datasets from VNNCOMP 2020
(see section 8.1 of De Palma et al. (2021b)) is contained in ./tools/bab_tools/bab_runner.py.
The network to be verified/bounded (either via .onnx parsing or directly from a list of torch layers) must have the following form,
where optional layers are enclosed in brackets:
input -> [additions/positive-multiplications/reshapings/flattenings] ->
linear (nn.Linear or nn.Conv2d) -> [additions/multiplications/reshapings/flattenings] -> ReLU() ->
[reshapings/flattenings] -> linear -> [additions/multiplications/reshapings/flattenings] -> ReLU() ->
[reshapings/flattenings] -> [linear] -> [additions/multiplications/reshapings/flattenings]
The code was implemented assuming to be run under python3.7.
We assume the user's Python environment is based on Anaconda.
git clone --recursive https://github.com/oval-group/oval-bab.git
cd oval-bab
# Create a conda environment
conda create -y -n oval python=3.7
conda activate oval
# Install pytorch to this virtualenv
# (or check updated install instructions at http://pytorch.org)
conda install -y pytorch torchvision cudatoolkit -c pytorch
# Install the code of this repository
pip install .In order to run the Gurobi-based solvers (outperformed by dual algorithms on networks with more than 1k neurons), a Gurobi license and installation is required.
Gurobi can be obtained from here and academic licenses are available from here. Note that to run the code for VNN-COMP '21, an installation of Gurobi is not needed.
# Install gurobipy
conda config --add channels http://conda.anaconda.org/gurobi
pip install .
# might need
# conda install gurobi