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".
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_from_vnnlib.py.
Further details, including how to produce a .json configuration file (see ./bab_configs/) for the OVAL framework will be soon added to the repository
The code was implemented assuming to be run under python3.6.
We assume the user's Python environment is based on Anaconda.
Installation steps (see also vnncomp_scripts/install_tool.sh):
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.6
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