search

Verified-Intelligence / auto_LiRPA

auto_LiRPA: An Automatic Linear Relaxation based Perturbation Analysis Library for Neural Networks and General Computational Graphs
https://arxiv.org/pdf/2002.12920
Other
269 stars 67 forks source link
adversarial-defense adversarial-examples adversarial-machine-learning certified-defense-models crown-bound ibp-bounds robustness robustness-verification

readme

auto_LiRPA: Automatic Linear Relaxation based Perturbation Analysis for Neural Networks

Documentation Status Open In Colab Video Introduction BSD license

What's New?

Introduction

auto_LiRPA is a library for automatically deriving and computing bounds with linear relaxation based perturbation analysis (LiRPA) (e.g. CROWN and DeepPoly) for neural networks, which is a useful tool for formal robustness verification. We generalize existing LiRPA algorithms for feed-forward neural networks to a graph algorithm on general computational graphs, defined by PyTorch. Additionally, our implementation is also automatically differentiable, allowing optimizing network parameters to shape the bounds into certain specifications (e.g., certified defense). You can find a video ▶️ introduction here.

Our library supports the following algorithms:

Our library allows automatic bound derivation and computation for general computational graphs, in a similar manner that gradients are obtained in modern deep learning frameworks -- users only define the computation in a forward pass, and auto_LiRPA traverses through the computational graph and derives bounds for any nodes on the graph. With auto_LiRPA we free users from deriving and implementing LiPRA for most common tasks, and they can simply apply LiPRA as a tool for their own applications. This is especially useful for users who are not experts of LiRPA and cannot derive these bounds manually (LiRPA is significantly more complicated than backpropagation).

Technical Background in 1 Minute

Deep learning frameworks such as PyTorch represent neural networks (NN) as a computational graph, where each mathematical operation is a node and edges define the flow of computation:

Normally, the inputs of a computation graph (which defines a NN) are data and model weights, and PyTorch goes through the graph and produces model prediction (a bunch of numbers):

Our auto_LiRPA library conducts perturbation analysis on a computational graph, where the input data and model weights are defined within some user-defined ranges. We get guaranteed output ranges (bounds):

Installation

Python 3.7+ and PyTorch 1.11+ are required. It is highly recommended to have a pre-installed PyTorch that matches your system and our version requirement. See PyTorch Get Started. Then you can install auto_LiRPA via:

git clone https://github.com/Verified-Intelligence/auto_LiRPA
cd auto_LiRPA
pip install .

If you intend to modify this library, use pip install -e . instead.

Optionally, you may build and install native CUDA modules (CUDA toolkit required):

python auto_LiRPA/cuda_utils.py install

Quick Start

First define your computation as a nn.Module and wrap it using auto_LiRPA.BoundedModule(). Then, you can call the compute_bounds function to obtain certified lower and upper bounds under input perturbations:

from auto_LiRPA import BoundedModule, BoundedTensor, PerturbationLpNorm

# Define computation as a nn.Module.
class MyModel(nn.Module):
    def forward(self, x):
        # Define your computation here.

model = MyModel()
my_input = load_a_batch_of_data()
# Wrap the model with auto_LiRPA.
model = BoundedModule(model, my_input)
# Define perturbation. Here we add Linf perturbation to input data.
ptb = PerturbationLpNorm(norm=np.inf, eps=0.1)
# Make the input a BoundedTensor with the pre-defined perturbation.
my_input = BoundedTensor(my_input, ptb)
# Regular forward propagation using BoundedTensor works as usual.
prediction = model(my_input)
# Compute LiRPA bounds using the backward mode bound propagation (CROWN).
lb, ub = model.compute_bounds(x=(my_input,), method="backward")

Checkout examples/vision/simple_verification.py for a complete but very basic example.

We also provide a Google Colab Demo including an example of computing verification bounds for a 18-layer ResNet model on CIFAR-10 dataset. Once the ResNet model is defined as usual in Pytorch, obtaining provable output bounds is as easy as obtaining gradients through autodiff. Bounds are efficiently computed on GPUs.

More Working Examples

We provide a wide range of examples of using auto_LiRPA:

auto_LiRPA has also been used in the following works:

Full Documentations

For more documentations, please refer to:

Publications

Please kindly cite our papers if you use the auto_LiRPA library. Full BibTeX entries can be found here.

The general LiRPA based bound propagation algorithm was originally proposed in our paper:

The auto_LiRPA library is further extended to allow optimized bound (α-CROWN), split constraints (β-CROWN) general constraints (GCP-CROWN), and higher-order computational graphs:

Certified robust training using auto_LiRPA is improved to allow much shorter warmup and faster training:

Branch and bound for non-ReLU and general activation functions:

Tightening of bounds and preimage computation using the INVPROP algorithm:

Developers and Copyright

Team lead:

Current developers:

Past developers:

We thank the commits and pull requests from community contributors.

Our library is released under the BSD 3-Clause license.