September 2022 release

Co-Authored-By: Kaidi Xu <[email protected]> Co-Authored-By: Huan Zhang <[email protected]> Co-Authored-By: Yihan Wang <[email protected]> Co-Authored-By: Shiqi Wang <[email protected]> Co-Authored-By: Linyi Li <[email protected]> Co-Authored-By: Kathryn (Jinqi) Chen <[email protected]> Co-Authored-By: Zhuolin Yang <[email protected]>
Verified-Intelligence · Sep 15, 2022 · f3e5f31 · f3e5f31
1 parent 02f6266
commit f3e5f31
Show file tree

Hide file tree

Showing 87 changed files with 9,625 additions and 4,289 deletions.
diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
diff --git a/.gitignore b/.gitignore
@@ -4,5 +4,16 @@ __pycache__
 *.egg-info
 dist
 *.swp
+*.swo
 *.log
-.trace_graph
+.trace_graph
+Verified_ret*.npy
+Verified-acc*.npy
+vnn-comp_*.npz
+*.tar.gz
+verifier_log_*
+*.pth
+*.pt
+.idea
+*.so
+release
diff --git a/.travis.yml b/.travis.yml
@@ -3,8 +3,10 @@ python:
   - "3.8"
 install:
   - pip install --editable .
-  - cd examples 
+  - cd examples
   - pip install -r requirements.txt
+  - pip install git+https://github.com/KaidiXu/onnx2pytorch.git
+  - pip install onnxruntime
   - cd ..
   - sudo fallocate -l 16G /swapfile
   - sudo chmod 600 /swapfile
@@ -14,4 +16,5 @@ install:
 script:
   - cd tests
   - python utils/download_models.py
-  - pytest 
+  - pytest
+  - cd ..
diff --git a/README.md b/README.md
@@ -13,16 +13,17 @@
 
 ## What's New?
 
-- Our neural network verification tool [α,β-CROWN](https://github.com/huanzhang12/alpha-beta-CROWN.git) ([alpha-beta-CROWN](https://github.com/huanzhang12/alpha-beta-CROWN.git)) **won** [VNN-COMP 2021](https://sites.google.com/view/vnn2021) **with the highest total score**, outperforming 11 SOTA verifiers. α,β-CROWN uses the `auto_LiRPA` library as its core bound computation library.
-- Support for [custom operators](https://auto-lirpa.readthedocs.io/en/latest/custom_op.html). (01/02/2022) 
+- Our neural network verification tool [α,β-CROWN](https://github.com/huanzhang12/alpha-beta-CROWN.git) ([alpha-beta-CROWN](https://github.com/huanzhang12/alpha-beta-CROWN.git)) (using `auto_LiRPA` as its core library) **won** [VNN-COMP 2022](https://sites.google.com/view/vnn2022). Our library supports the large CIFAR100, TinyImageNet and ImageNet models in VNN-COMP 2022. (09/2022)
+- Implementation of **general cutting planes** ([GCP-CROWN](https://arxiv.org/pdf/2208.05740.pdf)), support of more activation functions and improved performance and scalability. (09/2022)
+- Our neural network verification tool [α,β-CROWN](https://github.com/huanzhang12/alpha-beta-CROWN.git) ([alpha-beta-CROWN](https://github.com/huanzhang12/alpha-beta-CROWN.git)) **won** [VNN-COMP 2021](https://sites.google.com/view/vnn2021) **with the highest total score**, outperforming 11 SOTA verifiers. α,β-CROWN uses the `auto_LiRPA` library as its core bound computation library. (09/2021)
 - [Optimized CROWN/LiRPA](https://arxiv.org/pdf/2011.13824.pdf) bound (α-CROWN) for ReLU, **sigmoid**, **tanh**, and **maxpool** activation functions, which can significantly outperform regular CROWN bounds. See [simple_verification.py](examples/vision/simple_verification.py#L59) for an example. (07/31/2021)
 - Handle split constraints for ReLU neurons ([β-CROWN](https://arxiv.org/pdf/2103.06624.pdf)) for complete verifiers. (07/31/2021)
-- A memory efficient GPU implementation of backward (CROWN) bounds for 
+- A memory efficient GPU implementation of backward (CROWN) bounds for
 convolutional layers. (10/31/2020)
 - Certified defense models for downscaled ImageNet, TinyImageNet, CIFAR-10, LSTM/Transformer. (08/20/2020)
 - Adding support to **complex vision models** including DenseNet, ResNeXt and WideResNet. (06/30/2020)
-- **Loss fusion**, a technique that reduces training cost of tight LiRPA bounds 
-(e.g. CROWN-IBP) to the same asympototic complexity of IBP, making LiRPA based certified 
+- **Loss fusion**, a technique that reduces training cost of tight LiRPA bounds
+(e.g. CROWN-IBP) to the same asympototic complexity of IBP, making LiRPA based certified
 defense scalable to large datasets (e.g., TinyImageNet, downscaled ImageNet). (06/30/2020)
 - **Multi-GPU** support to scale LiRPA based training to large models and datasets. (06/30/2020)
 - Initial release. (02/28/2020)
@@ -46,6 +47,7 @@ Our library supports the following algorithms:
 * Backward mode LiRPA bound propagation ([CROWN](https://arxiv.org/pdf/1811.00866.pdf)/[DeepPoly](https://files.sri.inf.ethz.ch/website/papers/DeepPoly.pdf))
 * Backward mode LiRPA bound propagation with optimized bounds ([α-CROWN](https://arxiv.org/pdf/2011.13824.pdf))
 * Backward mode LiRPA bound propagation with split constraints ([β-CROWN](https://arxiv.org/pdf/2103.06624.pdf))
+* Generalized backward mode LiRPA bound propagation with general cutting plane constraints ([GCP-CROWN](https://arxiv.org/pdf/2208.05740.pdf))
 * Forward mode LiRPA bound propagation ([Xu et al., 2020](https://arxiv.org/pdf/2002.12920))
 * Forward mode LiRPA bound propagation with optimized bounds (similar to [α-CROWN](https://arxiv.org/pdf/2011.13824.pdf))
 * Interval bound propagation ([IBP](https://arxiv.org/pdf/1810.12715.pdf))
@@ -89,9 +91,11 @@ user-defined ranges.  We get guaranteed output ranges (bounds):
 
 ## Installation
 
-Python 3.7+ is required. Pytorch 1.8 (LTS) is recommended, although a newer
-version might also work. It is highly recommended to have a pre-installed PyTorch
-that matches your system and our version requirement. See [PyTorch Get Started](https://pytorch.org/get-started). 
+Python 3.7+ and PyTorch 1.8+ are required.
+PyTorch 1.11 is recommended, although other recent versions might also work.
+It is highly recommended to have a pre-installed PyTorch
+that matches your system and our version requirement.
+See [PyTorch Get Started](https://pytorch.org/get-started).
 Then you can install `auto_LiRPA` via:
 
 ```bash
@@ -102,6 +106,11 @@ python setup.py install
 
 If you intend to modify this library, use `python setup.py develop` instead.
 
+Optionally, you may build and install native CUDA modules (CUDA toolkit required):
+```bash
+python auto_LiRPA/cuda_utils.py install
+```
+
 ## Quick Start
 
 First define your computation as a `nn.Module` and wrap it using
@@ -127,7 +136,7 @@ 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="CROWN")
+lb, ub = model.compute_bounds(x=(my_input,), method="backward")
 ```
 
 Checkout
@@ -142,7 +151,7 @@ obtaining gradients through autodiff. Bounds are efficiently computed on GPUs.
 
 ## More Working Examples
 
-We provide [a wide range of examples](doc/src/examples.md) of using `auto_LiRPA`: 
+We provide [a wide range of examples](doc/src/examples.md) of using `auto_LiRPA`:
 
 * [Basic Bound Computation and **Robustness Verification** of Neural Networks](doc/src/examples.md#basic-bound-computation-and-robustness-verification-of-neural-networks)
 * [Basic **Certified Adversarial Defense** Training](doc/src/examples.md#basic-certified-adversarial-defense-training)
@@ -151,6 +160,10 @@ We provide [a wide range of examples](doc/src/examples.md) of using `auto_LiRPA`
 * [Certifiably Robust Language Classifier using **Transformers**](doc/src/examples.md#certifiably-robust-language-classifier-with-transformer-and-lstm)
 * [Certified Robustness against **Model Weight Perturbations**](doc/src/examples.md#certified-robustness-against-model-weight-perturbations-and-certified-defense)
 
+`auto_LiRPA` has also be used in the following works:
+* [**α,β-CROWN for complete neural network verification**](https://github.com/huanzhang12/alpha-beta-CROWN)
+* [**Fast certified robust training**](https://github.com/shizhouxing/Fast-Certified-Robust-Training)
+
 ## Full Documentations
 
 For more documentations, please refer to:
@@ -166,33 +179,48 @@ Please kindly cite our papers if you use the `auto_LiRPA` library. Full [BibTeX
 
 The general LiRPA based bound propagation algorithm was originally proposed in our paper:
 
-* [Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond](https://arxiv.org/pdf/2002.12920).  
-NeurIPS 2020  
+* [Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond](https://arxiv.org/pdf/2002.12920).
+NeurIPS 2020
 Kaidi Xu\*, Zhouxing Shi\*, Huan Zhang\*, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, Cho-Jui Hsieh (\* Equal contribution)
 
-The `auto_LiRPA` library is further extended to allow optimized bound (α-CROWN) and split constraints (β-CROWN):
+The `auto_LiRPA` library is further extended to allow optimized bound (α-CROWN), split constraints (β-CROWN) and general constraints (GCP-CROWN):
 
-* [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://arxiv.org/pdf/2011.13824.pdf).  
-ICLR 2021  
-Kaidi Xu\*, Huan Zhang\*, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin and Cho-Jui Hsieh (\* Equal contribution)
+* [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://arxiv.org/pdf/2011.13824.pdf).
+ICLR 2021.
+Kaidi Xu\*, Huan Zhang\*, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin and Cho-Jui Hsieh (\* Equal contribution).
 
-* [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification](https://arxiv.org/pdf/2103.06624.pdf).  
-NeurIPS 2021  
-Shiqi Wang\*, Huan Zhang\*, Kaidi Xu\*, Suman Jana, Xue Lin, Cho-Jui Hsieh and Zico Kolter (\* Equal contribution)
+* [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification](https://arxiv.org/pdf/2103.06624.pdf).
+NeurIPS 2021.
+Shiqi Wang\*, Huan Zhang\*, Kaidi Xu\*, Suman Jana, Xue Lin, Cho-Jui Hsieh and Zico Kolter (\* Equal contribution).
 
+* [GCP-CROWN: General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://arxiv.org/abs/2208.05740).
+Huan Zhang\*, Shiqi Wang\*, Kaidi Xu\*, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh and Zico Kolter (\* Equal contribution).
+
+Certified robust training using `auto_LiRPA` is improved to allow much shorter warmup and faster training:
+* [Fast Certified Robust Training with Short Warmup](https://arxiv.org/pdf/2103.17268.pdf).
+NeurIPS 2021.
+Zhouxing Shi\*, Yihan Wang\*, Huan Zhang, Jinfeng Yi and Cho-Jui Hsieh (\* Equal contribution).
 
 ## Developers and Copyright
 
 | [Kaidi Xu](https://kaidixu.com/) | [Zhouxing Shi](https://shizhouxing.github.io/) | [Huan Zhang](https://huan-zhang.com/) | [Yihan Wang](https://yihanwang617.github.io/) | [Shiqi Wang](https://www.cs.columbia.edu/~tcwangshiqi/) |
 |:--:|:--:| :--:| :--:| :--:|
 | <img src="https://kaidixu.files.wordpress.com/2020/07/profile2-1.jpg" width="125" /> | <img src="https://shizhouxing.github.io/photo.jpg" width="115" /> | <img src="https://huan-zhang.appspot.com/images/Huan_Zhang_photo.jpg" width="125" /> | <img src="https://upload.wikimedia.org/wikipedia/commons/8/89/Portrait_Placeholder.png" width="125" height="125" /> | <img src="https://www.cs.columbia.edu/~tcwangshiqi/images/shiqiwang.jpg" width="125" /> |
 
-* Kaidi Xu ([email protected]): main developer
-* Zhouxing Shi ([email protected]): main developer
-* Huan Zhang ([email protected]): team lead
-* Yihan Wang ([email protected])
-* Shiqi Wang ([email protected]): contact for beta-CROWN
+Team lead:
+* Huan Zhang ([email protected]), CMU
+
+Main developers:
+* Zhouxing Shi ([email protected]), UCLA
+* Kaidi Xu ([email protected]), Drexel University
+
+Contributors:
+* Yihan Wang ([email protected]), UCLA
+* Shiqi Wang ([email protected]), Columbia University
+* Linyi Li ([email protected]), UIUC
+* Jinqi (Kathryn) Chen ([email protected]), CMU
+* Zhuolin Yang ([email protected]), UIUC
 
-We thank [commits](https://github.com/KaidiXu/auto_LiRPA/commits) and [pull requests](https://github.com/KaidiXu/auto_LiRPA/pulls) from community contributors.
+We thank the[commits](https://github.com/KaidiXu/auto_LiRPA/commits) and [pull requests](https://github.com/KaidiXu/auto_LiRPA/pulls) from community contributors.
 
 Our library is released under the BSD 3-Clause license.
diff --git a/auto_LiRPA/__init__.py b/auto_LiRPA/__init__.py
@@ -1,7 +1,8 @@
-from .bound_general import BoundedModule, BoundDataParallel
+from .bound_general import BoundedModule
+from .bound_multi_gpu import BoundDataParallel
 from .bounded_tensor import BoundedTensor, BoundedParameter
 from .perturbations import PerturbationLpNorm, PerturbationSynonym
 from .wrapper import CrossEntropyWrapper, CrossEntropyWrapperMultiInput
 from .bound_op_map import register_custom_op, unregister_custom_op
 
-__version__ = '0.2'
+__version__ = '0.3'