Giter VIP home page Giter VIP logo

verified-intelligence / alpha-beta-crown Goto Github PK

View Code? Open in Web Editor NEW
214.0 14.0 50.0 72.08 MB

alpha-beta-CROWN: An Efficient, Scalable and GPU Accelerated Neural Network Verifier (winner of VNN-COMP 2021, 2022, and 2023)

License: Other

Python 97.51% Shell 0.94% C++ 1.52% Makefile 0.02%
robustness robustness-verification neural-networks adversarial-examples adversarial-robustness neural-network-verification

alpha-beta-crown's Introduction

α,β-CROWN (alpha-beta-CROWN): A Fast and Scalable Neural Network Verifier with Efficient Bound Propagation

α,β-CROWN (alpha-beta-CROWN) is a neural network verifier based on an efficient linear bound propagation framework and branch and bound. It can be accelerated efficiently on GPUs and can scale to relatively large convolutional networks (e.g., millions of parameters). It also supports a wide range of neural network architectures (e.g., CNN, ResNet, and various activation functions), thanks to the versatile auto_LiRPA library developed by us. α,β-CROWN can provide provable robustness guarantees against adversarial attacks and can also verify other general properties of neural networks.

α,β-CROWN is the winning verifier in VNN-COMP 2021, VNN-COMP 2022, and VNN-COMP 2023 (International Verification of Neural Networks Competition) with the highest total score, outperforming many other neural network verifiers on a wide range of benchmarks over 2 years. Details of competition results can be found in VNN-COMP 2021 slides, report, VNN-COMP 2022 report, VNN-COMP 2023 slides and report.

α,β-CROWN combines our efforts in neural network verification in a series of papers building up the bound propagation framework during the past five years. See the Publications section below.

Supported Features

Our verifier consists of the following core algorithms:

  • β-CROWN (Wang et al. 2021): complete verification with CROWN (Zhang et al. 2018) and branch and bound for ReLU.
  • GenBaB (Shi et al. 2024): Branch and bound for general nonlinear functions.
  • α-CROWN (Xu et al., 2021): incomplete verification with optimized CROWN bound.
  • GCP-CROWN (Zhang et al. 2022): CROWN-like bound propagation with general cutting plane constraints.
  • BaB-Attack (Zhang et al. 2022): Branch and bound based adversarial attack for tackling hard instances.
  • MIP (Tjeng et al., 2017): mixed integer programming (slow but can be useful on small models).
  • INVPROP (Kotha et al. 2023): tightens bounds with constraints on model outputs, and computes provable preimages for neural networks.

Based on auto_LiRPA (Xu et al., 2020) for general computational graphs, we support these neural network architectures:

  • Layers: fully connected (FC), convolutional (CNN), pooling (average pool and max pool), transposed convolution
  • Activation functions or nonlinear functions: ReLU, sigmoid, tanh, arctan, sin, cos, tan, gelu, pow, multiplication and self-attention
  • Residual connections, Transformers, LSTMs, and other irregular graphs

We support the following verification specifications:

  • Lp norm perturbation (p=1,2,infinity, as often used in robustness verification)
  • VNNLIB format input (at most two layers of AND/OR clause, as used in VNN-COMP 2021 and 2022)
  • Any linear specifications on neural network output (which can be added as a linear layer)

We provide many example configurations in complete_verifier/exp_configs directory to start with:

  • MNIST: MLP and CNN models
  • CIFAR-10, CIFAR-100, TinyImageNet: CNN and ResNet models
  • ACASXu, NN4sys and other low input-dimension models

See the Guide on Algorithm Selection to find the most suitable example to get started.

Installation and Setup

α,β-CROWN is tested on Python 3.7+ and PyTorch 1.11. It can be installed easily into a conda environment. If you don't have conda, you can install miniconda.

Clone our verifier including the auto_LiRPA submodule:

git clone --recursive https://github.com/Verified-Intelligence/alpha-beta-CROWN.git

Setup the conda environment:

# Remove the old environment, if necessary.
conda deactivate; conda env remove --name alpha-beta-crown
# install all dependents into the alpha-beta-crown environment
conda env create -f complete_verifier/environment.yaml --name alpha-beta-crown
# activate the environment
conda activate alpha-beta-crown

If you use the α-CROWN and/or β-CROWN verifiers (which covers the most use cases), a Gurobi license is not needed. If you want to use MIP based verification algorithms (feasible only for small MLP models), you need to install a Gurobi license with the grbgetkey command. If you don't have access to a license, by default the above installation procedure includes a free and restricted license, which is actually sufficient for many relatively small NNs. If you use the GCP-CROWN verifier, an installation of IBM CPlex solver is required. Instructions to install the CPlex solver can be found in the VNN-COMP benchmark instructions or the GCP-CROWN instructions.

If you prefer to install packages manually rather than using a prepared conda environment, you can refer to this installation script.

If you want to run α,β-CROWN verifier on the VNN-COMP benchmarks (e.g., to make a comparison to a new verifier), you can follow this guide.

Instructions

We provide a unified front-end for the verifier, abcrown.py. All parameters for the verifier are defined in a yaml config file. For example, to run robustness verification on a CIFAR-10 ResNet network, you just run:

conda activate alpha-beta-crown  # activate the conda environment
cd complete_verifier
python abcrown.py --config exp_configs/tutorial_examples/cifar_resnet_2b.yaml

You can find explanations for the most useful parameters in this example config file. For detailed usage and tutorial examples, please see the Usage Documentation. We also provide a large range of examples in the complete_verifier/exp_configs folder.

Publications

If you use our verifier in your work, please kindly cite our papers:

α,β-CROWN combines our existing efforts on neural network verification:

  • CROWN (Zhang et al. NeurIPS 2018) is a very efficient bound propagation based verification algorithm. CROWN propagates a linear inequality backwards through the network and utilizes linear bounds to relax activation functions.

  • The "convex relaxation barrier" (Salman et al., NeurIPS 2019) paper concludes that optimizing the ReLU relaxation allows CROWN (referred to as a "greedy" primal space solver) to achieve the same solution as linear programming (LP) based verifiers.

  • LiRPA (Xu et al., NeurIPS 2020) is a generalization of CROWN on general computational graphs and we also provide an efficient GPU implementation, the auto_LiRPA library.

  • α-CROWN (sometimes referred to as optimized CROWN or optimized LiRPA) is used in the Fast-and-Complete verifier (Xu et al., ICLR 2021), which jointly optimizes intermediate layer bounds and final layer bounds in CROWN via variable α. α-CROWN typically has greater power than LP since LP cannot cheaply tighten intermediate layer bounds.

  • β-CROWN (Wang et al., NeurIPS 2021) incorporates ReLU split constraints in branch and bound (BaB) into the CROWN bound propagation procedure via an additional optimizable parameter β. The combination of efficient and GPU accelerated bound propagation with branch and bound produces a powerful and scalable neural network verifier.

  • BaB-Attack (Zhang et al., ICML 2022) is a strong falsifier (adversarial attack) based on branch and bound, which can find adversarial examples for hard instances where gradient or input-space-search based methods cannot succeed.

  • GCP-CROWN (Zhang et al., NeurIPS 2022) enables the use of general cutting planes methods for neural network verification in a GPU-accelerated and very efficient bound propagation framework. Cutting planes can significantly strengthen bound tightness.

  • GenBaB (Shi et al., WFVML 2023) enables branch-and-bound based verification for non-ReLU and general nonlinear functions, achieving significant improvements on verifying neural networks with non-ReLU activation functions such as Transformer and LSTM networks, and models that consist of neural networks and additional nonlinear operations such as ML for AC Optimal Power Flow.

  • INVPROP (Kotha et al., NeurIPS 2023) handles constraints on the outputs of neural networks which enables tight and provable bounds on the preimage of a neural network. We demonstrated several applications, including OOD detection, backward reachability analysis for NN-controlled systems, and tightening bounds for robustness verification.

We provide bibtex entries below:

@article{zhang2018efficient,
  title={Efficient Neural Network Robustness Certification with General Activation Functions},
  author={Zhang, Huan and Weng, Tsui-Wei and Chen, Pin-Yu and Hsieh, Cho-Jui and Daniel, Luca},
  journal={Advances in Neural Information Processing Systems},
  volume={31},
  pages={4939--4948},
  year={2018},
  url={https://arxiv.org/pdf/1811.00866.pdf}
}

@article{xu2020automatic,
  title={Automatic perturbation analysis for scalable certified robustness and beyond},
  author={Xu, Kaidi and Shi, Zhouxing and Zhang, Huan and Wang, Yihan and Chang, Kai-Wei and Huang, Minlie and Kailkhura, Bhavya and Lin, Xue and Hsieh, Cho-Jui},
  journal={Advances in Neural Information Processing Systems},
  volume={33},
  year={2020}
}

@article{salman2019convex,
  title={A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks},
  author={Salman, Hadi and Yang, Greg and Zhang, Huan and Hsieh, Cho-Jui and Zhang, Pengchuan},
  journal={Advances in Neural Information Processing Systems},
  volume={32},
  pages={9835--9846},
  year={2019}
}

@inproceedings{xu2021fast,
    title={{Fast and Complete}: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers},
    author={Kaidi Xu and Huan Zhang and Shiqi Wang and Yihan Wang and Suman Jana and Xue Lin and Cho-Jui Hsieh},
    booktitle={International Conference on Learning Representations},
    year={2021},
    url={https://openreview.net/forum?id=nVZtXBI6LNn}
}

@article{wang2021beta,
  title={{Beta-CROWN}: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification},
  author={Wang, Shiqi and Zhang, Huan and Xu, Kaidi and Lin, Xue and Jana, Suman and Hsieh, Cho-Jui and Kolter, J Zico},
  journal={Advances in Neural Information Processing Systems},
  volume={34},
  year={2021}
}

@InProceedings{zhang22babattack,
  title = 	 {A Branch and Bound Framework for Stronger Adversarial Attacks of {R}e{LU} Networks},
  author =       {Zhang, Huan and Wang, Shiqi and Xu, Kaidi and Wang, Yihan and Jana, Suman and Hsieh, Cho-Jui and Kolter, Zico},
  booktitle = 	 {Proceedings of the 39th International Conference on Machine Learning},
  volume = 	 {162},
  pages = 	 {26591--26604},
  year = 	 {2022},
}

@article{zhang2022general,
  title={General Cutting Planes for Bound-Propagation-Based Neural Network Verification},
  author={Zhang, Huan and Wang, Shiqi and Xu, Kaidi and Li, Linyi and Li, Bo and Jana, Suman and Hsieh, Cho-Jui and Kolter, J Zico},
  journal={Advances in Neural Information Processing Systems},
  year={2022}
}

@article{shi2023generalnonlinear,
  title={Formal Verification for Neural Networks with General Nonlinearities via Branch-and-Bound},
  author={Shi, Zhouxing and Jin, Qirui and Kolter, J Zico and Jana, Suman and Hsieh, Cho-Jui and Zhang, Huan},
  journal={2nd Workshop on Formal Verification of Machine Learning (WFVML 2023)},
  year={2023}
}

@inproceedings{kotha2023provably,
 author = {Kotha, Suhas and Brix, Christopher and Kolter, J. Zico and Dvijotham, Krishnamurthy and Zhang, Huan},
 booktitle = {Advances in Neural Information Processing Systems},
 editor = {A. Oh and T. Neumann and A. Globerson and K. Saenko and M. Hardt and S. Levine},
 pages = {80270--80290},
 publisher = {Curran Associates, Inc.},
 title = {Provably Bounding Neural Network Preimages},
 url = {https://proceedings.neurips.cc/paper_files/paper/2023/file/fe061ec0ae03c5cf5b5323a2b9121bfd-Paper-Conference.pdf},
 volume = {36},
 year = {2023}
}

Developers and Copyright

The α,β-CROWN verifier is developed by a team from CMU, UCLA, Drexel University, Columbia University and UIUC:

Team lead:

Current developers:

Past developers:

The team acknowledges the financial and advisory support from Prof. Zico Kolter ([email protected]), Prof. Cho-Jui Hsieh ([email protected]), Prof. Suman Jana ([email protected]), Prof. Bo Li ([email protected]), and Prof. Xue Lin ([email protected]).

Our library is released under the BSD 3-Clause license. A copy of the license is included here.

alpha-beta-crown's People

Contributors

foreverzyh avatar huanzhang12 avatar kamdoumloich avatar shizhouxing avatar tcwangshiqi-columbia avatar yihanwang617 avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

alpha-beta-crown's Issues

Query of theorem of handling residual networks with ADD layer

Dear,

I am very impressed when reading your papers regarding the theorems where you solve the constrained problems with efficient algorithms that run on GPU.
In the theorem proofs, I notice that the original constrained problem includes constraints x(i) = W(i)x(i-1)+b(i), which only captures fully-connected/convolutional/... layers's behavior.
But for an Add layer in residual networks in ONNX model, its function is like x(i) = x(i-1)+x(i-k). I fail to see how this theorem extends to residual networks, but I did observe residual networks in your experiments.
So I wonder if there is a theorem behind handling the residual networks? And is this theorem (if any) just a customization of your existing theorem?
Thank you in advance for your clarification!

Error running vnncomp22/vggnet16.yaml

Hi,

I tried to run exp_configs/vnncomp22/vggnet16.yaml without any changes, but I got the following NotImplementedError.

I'd appreciate it if you could look into this.

Traceback (most recent call last):
  File "abcrown.py", line 656, in <module>
    main()
  File "abcrown.py", line 579, in main
    refined_betas=refined_betas, attack_images=all_adv_candidates, attack_margins=attack_margins)
  File "abcrown.py", line 410, in complete_verifier
    rhs=rhs, timeout=timeout, attack_images=this_spec_attack_images)
  File "abcrown.py", line 200, in bab
    rhs=rhs, timeout=timeout, branching_method=arguments.Config["bab"]["branching"]["method"])
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/batch_branch_and_bound_input_split.py", line 164, in input_bab_parallel
    bounding_method=bounding_method,
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1141, in build_the_model
    x=(x,), C=self.c, method=bounding_method, cutter=self.cutter, bound_upper=False)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1319, in compute_bounds
    self.check_prior_bounds(final)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 847, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 847, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 847, in check_prior_bounds
    self.check_prior_bounds(n)
  [Previous line repeated 29 more times]
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 855, in check_prior_bounds
    node.inputs[i], prior_checked=True)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 883, in compute_intermediate_bounds
    node=node, concretize=True)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/forward_bound.py", line 16, in forward_general
    return self.forward_general_dynamic(C, node, concretize, offset)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/forward_bound.py", line 156, in forward_general_dynamic
    linear_inp = self.forward_general_dynamic(node=l_pre, offset=offset)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/forward_bound.py", line 168, in forward_general_dynamic
    *inp, max_dim=max_dim, offset=offset)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/base.py", line 228, in bound_dynamic_forward
    raise NotImplementedError(f'bound_dynamic_forward is not implemented for {self}.')
NotImplementedError: bound_dynamic_forward is not implemented for BoundMaxPool(name="/input.8").

Can I compute the upper bound using incomplete verifier?

I am new to this tool. When I am running the example, I notice that the incomplete verifier will compute the upper bound and lower bound at each ReLU layer. At each ReLU layer, I see the ub and lb value, but at the last, the ub value will become infinity. Although I know this tool only focuses on the lower bound to verify whether the specification is satisfied or not, is it feasible to use this tool to compute the upper bound?

environment.yaml file for Mac OS

Hello and fantastic work on developing your tool!

I am just beginning to try it out, and want to try running it on a Mac OS computer. I have the impression that your environment.yaml file is for linux rather than Mac OS. I am wondering if you happen to already have an environment.yml file that works for Mac OS. (If not and I reach one that works, I will be happy to share it.)

MIP Verification error

Describe the bug
I tried to use MIP to check my properties, but I am experimenting some problems. I first tried MIP using the example provided in the documentation in the MIP section. I pulled the vnncomp2022_benchmarks repository, executed the Tiny MNIST fully connected networks configuration, and it worked successfully! However, when I adapted this previous configuration file to work with my properties, I get an assertion error. After debugging, I tried setting the sparse_alpha: false to bypass that assertion error, and it worked, but I got a Gurobi length miss-match error.

To Reproduce
I created a small zip file containing a minimum example to reproduce the bug. This zip file contains a yaml configuration, a vnnlib property, a model, error logs (with and without the sparse_alpha set to false), and the instructions for reproducing the problem. The zip file can be found at https://drive.google.com/file/d/1bUXpezrTdKAhfxj2im8oQcqM2JzV9v3I/view?usp=share_link

System configuration:

  • OS: Ubuntu 20.04.3 LTS (Focal Fossa)
  • Conda version: conda 4.13.0
  • Python version: Python 3.7.13
  • Pytorch version: Pytorch 1.11.0
  • Hardware: CPU Intel(R) Xeon(R) Silver 4216 CPU @ 2.10GHz
  • Have you tried to reproduce the problem in a cleanly created conda/virtualenv environment using official installation instructions and the latest code on the main branch?: [No] I am using code from commit 1c29191 , but I do not think that the newer changes fix the problem since none of the changes modify the code where the problem is happening.

Error when changing last layer's weight

Hi, I figured CROWN does not support having the ReLU function as last year (it throws some error), so I thought I could add an identity Linear layer after ReLU as follows:

class MyModel(nn.ModuleList):
        def __init__(self, device=torch.device("cpu")):
            super(MyModel, self).__init__()        
            self.to(device)
            
            self.af = nn.ReLU()
            self.lin1 = nn.Linear(19, 32)
            self.lin2 = nn.Linear(32, 32)
            self.out = nn.Linear(32, 15)

            self.c2d_1 = torch.nn.Conv1d(1, 24, 15)
            self.c2d_2 = torch.nn.Conv1d(24, 12, 1)
            self.c2d_3 = torch.nn.Conv1d(12, 6, 1)
            self.c2d_4 = torch.nn.Conv1d(6, 3, 1)
            self.c2d_5 = torch.nn.Conv1d(3, 1, 1)

            self.eye = torch.nn.Linear(1, 1)
            self.eye.weight = torch.nn.Parameter(torch.ones_like(self.eye.weight))
            self.eye.bias = torch.nn.Parameter(torch.tensor([0.], requires_grad=True))       

       def forward(self, obs):
            obs = self.af(self.lin1(obs))
            obs = self.af(self.lin2(obs))
            logits = self.out(obs)
            after_conv1 = self.af(self.c2d_1(logits))
            after_conv2 = self.af(self.c2d_2(after_conv1))
            after_conv3 = self.af(self.c2d_3(after_conv2))
            after_conv4 = self.af(self.c2d_4(after_conv3))
            after_conv5 = self.af(self.c2d_5(after_conv4))
            return self.eye(after_conv5)[0]

Nonetheless, it gives me the following error:

Traceback (most recent call last):
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 612, in <module>
    abcrown.main()
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 591, in main
    verified_status = self.complete_verifier(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 416, in complete_verifier
    l, nodes, ret = self.bab(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 241, in bab
    result = general_bab(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/bab.py", line 340, in general_bab
    global_lb = act_split_round(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/bab.py", line 165, in act_split_round
    split_domain(net, domains, d, batch, impl_params=impl_params,
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/bab.py", line 70, in split_domain
    branching_heuristic.get_branching_decisions(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/torch/autograd/grad_mode.py", line 27, in decorate_context
    return func(*args, **kwargs)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/heuristics/kfsb.py", line 143, in get_branching_decisions
    k_ret_lbs = self.net.update_bounds(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 303, in update_bounds
    lb, _, = self.net.compute_bounds(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1206, in compute_bounds
    return self._compute_bounds_main(C=C,
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1311, in _compute_bounds_main
    ret = self.backward_general(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/backward_bound.py", line 324, in backward_general
    lb, ub = concretize(self, batch_size, output_dim, lb, ub,
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/backward_bound.py", line 671, in concretize
    lA = roots[i].lA.reshape(output_dim, batch_size, -1).transpose(0, 1) if bound_lower else None
RuntimeError: shape '[1, 4, -1]' is invalid for input of size 1

P.S: the error is gone when I remove this line of parameter setting:

self.eye.weight = torch.nn.Parameter(torch.ones_like(self.eye.weight))

Support for Softmax

Hi,
I could not find any Softmax function in the provided demos. I wanted to confirm with you whether Softmax is supported or not.
Thanks!

Use norms other then linf

I want to use ab-crown to verify neural networks with localrobustness property with the l-1 and l-2 norms. When I do this I get "Only Linf-norm attack is supported, the pgd_order will be changed to skip"

To Reproduce
Please provide us with the following to receive timely help:

  1. python alpha-beta-CROWN/complete_verifier/abcrown.py --config "./config_ffnnRELU__Point_6_500.onnx_image_1.yaml"

  2. Model files, especially when the bug is only triggered on specific models.
    norm_bug.zip

*/miniconda3/envs/alpba-beta-crown/lib/python3.7/site-packages/onnx2pytorch/convert/layer.py:30: UserWarning: The given NumPy array is not writable, and PyTorch does not support non-writable tensors. This means writing to this tensor will result in undefined behavior. You may want to copy the array to protect its data or make it writable before converting it to a tensor. This type of warning will be suppressed for the rest of this program. (Triggered internally at /opt/conda/conda-bld/pytorch_1646755953518/work/torch/csrc/utils/tensor_numpy.cpp:178.)
layer.weight.data = torch.from_numpy(numpy_helper.to_array(weight))
*/miniconda3/envs/alpba-beta-crown/lib/python3.7/site-packages/onnx2pytorch/convert/model.py:154: UserWarning: Using experimental implementation that allows 'batch_size > 1'.Batchnorm layers could potentially produce false outputs.
"Using experimental implementation that allows 'batch_size > 1'."
*/miniconda3/envs/alpba-beta-crown/lib/python3.7/site-packages/onnx2pytorch/operations/reshape.py:36: TracerWarning: Converting a tensor to a Python boolean might cause the trace to be incorrect. We can't record the data flow of Python values, so this value will be treated as a constant in the future. This means that the trace might not generalize to other inputs!
if (shape[0] == 1 and (len(shape) == 4 or len(shape) == 2)

*/miniconda3/envs/alpba-beta-crown/lib/python3.7/site-packages/onnx2pytorch/operations/reshape.py:55: TracerWarning: Iterating over a tensor might cause the trace to be incorrect. Passing a tensor of different shape won't change the number of iterations executed (and might lead to errors or silently give incorrect results).
shape = [x if x != 0 else input.size(i) for i, x in enumerate(shape)]
Configurations:

general:
device: cuda
seed: 100
conv_mode: patches
deterministic: false
double_fp: false
loss_reduction_func: sum
record_bounds: false
sparse_alpha: true
save_adv_example: false
precompile_jit: false
complete_verifier: bab
enable_incomplete_verification: true
csv_name: null
results_file: out.txt
root_path: ''
model:
name: null
path: null
onnx_path: ./ffnnRELU__Point_6_500.onnx
onnx_path_prefix: ''
cache_onnx_conversion: false
onnx_quirks: null
input_shape: null
onnx_loader: default_onnx_and_vnnlib_loader
onnx_optimization_flags: none
data:
start: 0
end: 10000
select_instance: null
num_outputs: 10
mean: 0.0
std: 1.0
pkl_path: null
dataset: CIFAR
data_filter_path: null
data_idx_file: null
specification:
type: lp
robustness_type: verified-acc
norm: 2
epsilon: null
vnnlib_path: ./mnist_train_property_1_eps_0.127.vnnlib
vnnlib_path_prefix: ''
solver:
batch_size: 4096
min_batch_size_ratio: 0.1
use_float64_in_last_iteration: false
early_stop_patience: 10
start_save_best: 0.5
bound_prop_method: alpha-crown
prune_after_crown: false
crown:
batch_size: 1000000000
max_crown_size: 1000000000
alpha-crown:
alpha: true
lr_alpha: 0.1
iteration: 100
share_slopes: false
no_joint_opt: false
lr_decay: 0.98
full_conv_alpha: true
beta-crown:
lr_alpha: 0.01
lr_beta: 0.03
lr_decay: 0.98
optimizer: adam
iteration: 20
beta: true
beta_warmup: true
enable_opt_interm_bounds: false
all_node_split_LP: false
forward:
refine: false
dynamic: false
max_dim: 10000
multi_class:
multi_class_method: allclass_domain
label_batch_size: 32
skip_with_refined_bound: true
mip:
parallel_solvers: 8
solver_threads: 4
refine_neuron_timeout: 15
refine_neuron_time_percentage: 0.8
early_stop: true
adv_warmup: true
mip_solver: gurobi
bab:
initial_max_domains: 1
max_domains: .inf
decision_thresh: 0
timeout: 1200
timeout_scale: 1
override_timeout: null
get_upper_bound: false
dfs_percent: 0.0
pruning_in_iteration: true
pruning_in_iteration_ratio: 0.2
sort_targets: false
batched_domain_list: true
optimized_intermediate_layers: ''
interm_transfer: true
cut:
enabled: false
bab_cut: false
lp_cut: false
method: null
lr: 0.01
lr_decay: 1.0
iteration: 100
bab_iteration: -1
early_stop_patience: -1
lr_beta: 0.02
number_cuts: 50
topk_cuts_in_filter: 100
batch_size_primal: 100
max_num: 1000000000
patches_cut: false
cplex_cuts: false
cplex_cuts_wait: 0
cplex_cuts_revpickup: true
cut_reference_bounds: true
fix_intermediate_bounds: false
branching:
method: kfsb
candidates: 5
reduceop: max
sb_coeff_thresh: 0.001
input_split:
enable: false
enhanced_bound_prop_method: alpha-crown
enhanced_branching_method: naive
enhanced_bound_patience: 100000000.0
attack_patience: 100000000.0
adv_check: 0
sort_domain_interval: -1
attack:
enabled: false
beam_candidates: 8
beam_depth: 7
max_dive_fix_ratio: 0.8
min_local_free_ratio: 0.2
mip_start_iteration: 5
mip_timeout: 30.0
adv_pool_threshold: null
refined_mip_attacker: false
refined_batch_size: null
attack:
pgd_order: before
pgd_steps: 100
pgd_restarts: 30
pgd_early_stop: true
pgd_lr_decay: 0.99
pgd_alpha: auto
pgd_loss_mode: null
enable_mip_attack: false
cex_path: ./test_cex.txt
attack_mode: PGD
gama_lambda: 10.0
gama_decay: 0.9
check_clean: false
input_split:
pgd_steps: 100
pgd_restarts: 30
pgd_alpha: auto
input_split_enhanced:
pgd_steps: 200
pgd_restarts: 5000000
pgd_alpha: auto
input_split_check_adv:
pgd_steps: 5
pgd_restarts: 5
pgd_alpha: auto
debug:
lp_test: null

Experiments at Mon Aug 28 12:52:53 2023 on ethnode33
Only Linf-norm attack is supported, the pgd_order will be changed to skip
Internal results will be saved to out.txt.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 0, vnnlib ID: 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Using onnx ./ffnnRELU__Point_6_500.onnx
Using vnnlib ./mnist_train_property_1_eps_0.127.vnnlib
Precompiled vnnlib file found at ./mnist_train_property_1_eps_0.127.vnnlib.compiled
Loading onnx ./ffnnRELU__Point_6_500.onnx wih quirks {}
Model prediction is: tensor([[ 10.79480839, -32.92673492, -10.14999199, -17.28115654, -19.48822784,
-11.00737000, -5.19352055, -12.42144966, -11.82566643, -15.57086086]],
device='cuda:0')
Traceback (most recent call last):
File "alpha-beta-CROWN/complete_verifier/abcrown.py", line 647, in
main()
File "alpha-beta-CROWN/complete_verifier/abcrown.py", line 535, in main
incomplete_verifier(model_ori, x, data_ub=data_max, data_lb=data_min, vnnlib=vnnlib)
File "alpha-beta-CROWN/complete_verifier/abcrown.py", line 69, in incomplete_verifier
domain, x, data_lb, data_ub, vnnlib, stop_criterion_func=stop_criterion_min(arguments.Config["bab"]["decision_thresh"]))
File "./alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1069, in build_the_model
(self.x,), share_slopes=share_slopes, c=self.c, bound_upper=False)
File "/home/bosmanaw/verona/VERONA/alpha-beta-CROWN/complete_verifier/auto_LiRPA/optimized_bounds.py", line 1023, in init_slope
intermediate_layer_bounds=intermediate_layer_bounds)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1321, in compute_bounds
self.check_prior_bounds(final)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 849, in check_prior_bounds
self.check_prior_bounds(n)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 849, in check_prior_bounds
self.check_prior_bounds(n)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 849, in check_prior_bounds
self.check_prior_bounds(n)
[Previous line repeated 8 more times]
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 857, in check_prior_bounds
node.inputs[i], prior_checked=True)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 935, in compute_intermediate_bounds
node=node, delete_bounds_after_use=True)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/interval_bound.py", line 31, in IBP_general
n, delete_bounds_after_use=delete_bounds_after_use)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/interval_bound.py", line 31, in IBP_general
n, delete_bounds_after_use=delete_bounds_after_use)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/interval_bound.py", line 31, in IBP_general
n, delete_bounds_after_use=delete_bounds_after_use)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/interval_bound.py", line 42, in IBP_general
node.interval = node.interval_propagate(*inp)
File "./alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/convolution.py", line 283, in interval_propagate
deviation = torch.mul(weight, weight).sum((1, 2, 3)).sqrt() * eps
TypeError: unsupported operand type(s) for *: 'Tensor' and 'NoneType'

  1. It's just having all files in a central location and run the command line commands I gave.

Without the above information, you might not be able to receive timely help from us.

System configuration:

  • OS:

  • Python version:

  • Pytorch Version:

  • Have you tried to reproduce the problem in a cleanly created conda/virtualenv environment using official installation instructions and the latest code on the main branch?: YES

AssertionError when running my model

error:
in "patches.py" line 380, in inplace_unfold
assert len(kernel_size) == 2 and len(padding) == 4 and len(stride) == 2

I just add my model in model_defs.py, but it will report the error above.
My model contains Conv2d, BatchNorm2d, ReLU, MaxPool2d and Dropout. Besides, my dataset's shape is (6000, 1, 1024, 2).

What are the possible reasons for such an error? Will the difference between the two dimensions of the dataset have an effect on the comparison?

Sequence of Conv1d Error

Thanks for adding the support for conv1d in the new release.

I get the following error when I have a sequence of two conv1d in my network architecture:

class MyModel(nn.ModuleList):
        def __init__(self, device=torch.device("cpu")):
            super(MyModel, self).__init__()        
            self.to(device)
            self.af = nn.ReLU()
            self.lin1 = nn.Linear(19, 15)
            self.c1d_1 = torch.nn.Conv1d(1, 24, 15)
            self.c1d_2 = torch.nn.Conv1d(24, 1, 1)
       
       def forward(self, obs):
            lin1 = self.af(self.lin1(obs))
            after_conv1 = self.af(self.c1d_1(lin1.unsqueeze(dim=0)))
            after_conv2 = self.af(self.c1d_2(after_conv1))
            return after_conv2[0]

The error:

Traceback (most recent call last):
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 612, in <module>
    abcrown.main()
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 591, in main
    verified_status = self.complete_verifier(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 416, in complete_verifier
    l, nodes, ret = self.bab(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 241, in bab
    result = general_bab(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/bab.py", line 246, in general_bab
    global_lb, ret = net.build(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 455, in build
    lb, ub, aux_reference_bounds = self.net.init_alpha(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/optimized_bounds.py", line 766, in init_alpha
    l, u = self.compute_bounds(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1206, in compute_bounds
    return self._compute_bounds_main(C=C,
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1303, in _compute_bounds_main
    self.check_prior_bounds(final)
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
    self.check_prior_bounds(n)
  [Previous line repeated 3 more times]
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 804, in check_prior_bounds
    self.compute_intermediate_bounds(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 910, in compute_intermediate_bounds
    node.lower, node.upper = self.backward_general(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/backward_bound.py", line 337, in backward_general
    lb = lb.view(batch_size, *output_shape) if bound_lower else None
RuntimeError: view size is not compatible with input tensor's size and stride (at least one dimension spans across two contiguous subspaces). Use .reshape(...) instead.

I tried the solutions I found online (replacing view by reshape AND adding contiguous() before view()), but it throws another error:

Traceback (most recent call last):
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 612, in <module>
    abcrown.main()
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 591, in main
    verified_status = self.complete_verifier(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 416, in complete_verifier
    l, nodes, ret = self.bab(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 241, in bab
    result = general_bab(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/bab.py", line 246, in general_bab
    global_lb, ret = net.build(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 455, in build
    lb, ub, aux_reference_bounds = self.net.init_alpha(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/optimized_bounds.py", line 766, in init_alpha
    l, u = self.compute_bounds(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1206, in compute_bounds
    return self._compute_bounds_main(C=C,
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1303, in _compute_bounds_main
    self.check_prior_bounds(final)
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 804, in check_prior_bounds
    self.compute_intermediate_bounds(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 915, in compute_intermediate_bounds
    self.restore_sparse_bounds(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/backward_bound.py", line 584, in restore_sparse_bounds
    lower[:, unstable_idx] = new_lower.view(batch_size, -1)
RuntimeError: shape mismatch: value tensor of shape [1331] cannot be broadcast to indexing result of shape [1, 11]

UnsatisfiableError when creating conda environment using environment.yml

When creating conda environment using environment.yml, I am getting the following error:

Collecting package metadata (repodata.json): done
Solving environment: |
Found conflicts! Looking for incompatible packages.
failed

UnsatisfiableError: The following specifications were found to be incompatible with each other:

Package icu conflicts for:
fontconfig==2.13.1=h6c09931_0 -> libxml2[version='>=2.9.10,<2.10.0a0'] -> icu[version='>=58.2,<59.0a0']
matplotlib==3.5.1=py37h06a4308_1 -> pyqt -> qt=5.9 -> icu[version='>=58.2,<59.0a0']
gst-plugins-base==1.14.0=h8213a91_2 -> gstreamer[version='>=1.14.0,<2.0a0'] -> gettext -> libxml2[version='>=2.9.10,<2.10.0a0'] -> icu[version='>=58.2,<59.0a0']
keras==2.4.3=hd3eb1b0_0 -> tensorflow -> tensorflow-base==2.5.0=mkl_py37h35b2a3d_0 -> icu[version='>=68.1,<69.0a0']
scikit-image==0.19.2=py37h51133e4_0 -> networkx[version='>=2.2'] -> matplotlib[version='>=3.3'] -> matplotlib-base[version='>=3.5.1,<3.5.2.0a0'] -> icu[version='>=58.2,<59.0a0']
icu==58.2=he6710b0_3
pyqt==5.9.2=py37h05f1152_2 -> qt=5.9 -> icu[version='>=58.2,<59.0a0']
qt==5.9.7=h5867ecd_1 -> icu[version='>=58.2,<59.0a0']
libxml2==2.9.14=h74e7548_0 -> icu[version='>=58.2,<59.0a0']
keras-base==2.4.3=pyhd3eb1b0_0 -> tensorflow[version='>=2.2'] -> tensorflow-base==2.5.0=mkl_py37h35b2a3d_0 -> icu[version='>=68.1,<69.0a0']

How to deal with it? Thank you!

NotImplementedError when analysing on onnx network

Hi,

I tried to use your tool to analyze mnist_relu_6_100.onnx from ERAN system (https://files.sri.inf.ethz.ch/eran/nets/onnx/mnist/mnist_relu_6_100.onnx).
I used command python abcrown.py --config exp_configs/mnist_6_100.yaml
The yaml is as follows:

general:
  complete_verifier: bab-refine
model:
  name: mnist_6_100
  path: models/eran/mnist_relu_6_100.onnx
data:
  dataset: MNIST_ERAN_UN
  std: [1.0]
  mean: [0.0]
specification:
  epsilon: 0.025
attack:
  pgd_order: after
solver:
  batch_size: 1024
  beta-crown:
    iteration: 20
  mip:
    parallel_solvers: 16
    refine_neuron_time_percentage: 0.8
bab:
  timeout: 1000
  branching:
    reduceop: max

It returned me:

Traceback (most recent call last):
  File "abcrown.py", line 650, in <module>
    main()
  File "abcrown.py", line 553, in main
    verified_status, init_global_lb, lower_bounds, upper_bounds, refined_betas = mip(saved_bounds=saved_bounds)
  File "abcrown.py", line 145, in mip
    score=score, stop_criterion_func=stop_criterion_min(1e-4))
  File "/home/yuyi/alpha-beta-CROWN/complete_verifier/lp_mip_solver.py", line 1968, in build_the_model_mip_refine
    raise NotImplementedError
NotImplementedError

Could you please advise me why would this happen?

Thanks and regards,
Yuyi

Config parameter on time-out

Hi,

I tried to run MNIST_ERAN dataset with network mnist_convSmallRELU__Point.
And I tried to increase the execution time with the hope that it would return more conclusive images.
I update the config as follows:
bab: timeout: 2000 branching: reduceop: max
But the program still terminates very quickly, with average execution time 3.06 seconds for each image.
I wonder why the verification process still terminates early with 2000 seconds timeout?
Thanks for your help!

Best regards,
Veronica

Unknown results for ReLU networks in ERAN benchmark

Hi,

I followed your instructions online to run robustness verification on ERAN benchmark, eg:
python robustness_verifier.py --config exp_configs/mnist_conv_small.yaml
but change the epsilon from 0.12 to 0.11.
I also used the same parameter configuration in mnist_6_100.yaml to run on ERAN mnist_3_100 and mnist_5_100.
Since alpha-beta-CROWN should be a complete tool for ReLU-activated networks, I am confused that there are still some images with inconclusive results.
May I ask why this is the case? And how may I run it with complete behavior?
Thank you so much for your help!

RuntimeError when verify CNN model with Tanh activation function

Hello, I notice that alpha-beta-crown is available for Sigmoid, Tanh activation functions. I use this code to verify model from ERAN. The CNN model with Sigmoid activation function has run smoothly, while for CNN model with Tanh activation function

Traceback (most recent call last):
  File "abcrown.py", line 650, in <module>
    main()
  File "abcrown.py", line 538, in main
    incomplete_verifier(model_ori, x, data_ub=data_max, data_lb=data_min, vnnlib=vnnlib)
  File "abcrown.py", line 72, in incomplete_verifier
    domain, x, data_lb, data_ub, vnnlib, stop_criterion_func=stop_criterion_min(arguments.Config["bab"]["decision_thresh"]))
  File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1122, in build_the_model
    bound_upper=False, aux_reference_bounds=aux_reference_bounds, cutter=self.cutter)
  File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1170, in compute_bounds
    cutter=cutter, decision_thresh=decision_thresh)
  File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/optimized_bounds.py", line 592, in get_optimized_bounds
    update_mask=preserve_mask)
  File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1321, in compute_bounds
    self.check_prior_bounds(final)
  File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 849, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 857, in check_prior_bounds
    node.inputs[i], prior_checked=True)
  File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 959, in compute_intermediate_bounds
    unstable_size=unstable_size)
  File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 154, in backward_general
    l.lA, l.uA, *l.inputs, start_shape=start_shape, start_node=node)
  File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/activation.py", line 258, in bound_backward
    lA, lbias = _bound_oneside(last_lA, sign=-1)
  File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/activation.py", line 255, in _bound_oneside
    A_prod, _bias = multiply_by_A_signs(last_A, w_pos, w_neg, b_pos, b_neg)
  File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/clampmult.py", line 122, in multiply_by_A_signs
    return ClampedMultiplication.apply(A, d_pos, d_neg, b_pos, b_neg, False)
  File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/clampmult.py", line 101, in forward
    return ClampedMultiplication.clamp_mutiply_forward(A, d_pos, d_neg, b_pos, b_neg, patches_mode)
RuntimeError: The following operation failed in the TorchScript interpreter.
Traceback of TorchScript (most recent call last):
  File "/home/XueZhiYi/academic/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/clampmult.py", line 42, in clamp_mutiply_forward
        A_pos = A.clamp(min=0)
        A_neg = A.clamp(max=0)
        A_new = d_pos * A_pos + d_neg * A_neg
                ~~~~~~~~~~~~~ <--- HERE
        bias_pos = bias_neg = torch.tensor(0.)
        if b_pos is not None:
RuntimeError: The size of tensor a (1000) must match the size of tensor b (304) at non-singleton dimension 0

The command to run is:

python abcrown.py --onnx_path onnx/mnist/convMedGTANH__Point.onnx  --dataset MNIST --epsilon 0.02 --device cpu --complete_verifier skip --no_full_conv_alpha --end 100

I have fixed the code like Sigmoid in backward_bound.py:

if (sparse_intermediate_bounds and isinstance(node, (BoundRelu, BoundSigmoid))
                and nj.name != final_node_name and not share_slopes):

to

if (sparse_intermediate_bounds and isinstance(node, (BoundRelu, BoundSigmoid, BoundTanh))
                and nj.name != final_node_name and not share_slopes):

How to deal with it? Thank you!

alpha-beta-crown always returns timeout even for a very simple model

Hi everyone,

We are currently trying to get a workflow involving neural network verification for networks that involve convolutional layers to run. Unfortunately, we are having little luck so far, because when skipping PGD-Attack, alpha-beta-crown always returns timeout. The result remained the same for "bab" and for "GCP-CROWN".

We defined a simple test case to allow the reproduction of our problem. Please can you tell us why we get "timeout" every time even for such a simple case? We Attached an example Jupyter notebook for learning and writing an ONNX-file, the resulting the ONNX file, the vnnlib-property file, theyaml-configuration file, and an image of the output we get.

The command we use to run alpha-beta-crown is as follow:

python abcrown.py --config personal_config/onnx_with_one_vnnlib.yaml --timeout 100

example_cnn.zip

RuntimeError: CUDA error: device-side assert triggered

Describe the bug
When I use alpha-beta-crown for evaluation, an cuda error shows, here is the log
"
Traceback (most recent call last):
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/abcrown.py", line 612, in
abcrown.main()
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/abcrown.py", line 591, in main
verified_status = self.complete_verifier(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/abcrown.py", line 416, in complete_verifier
l, nodes, ret = self.bab(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/abcrown.py", line 235, in bab
result = input_bab_parallel(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/input_split/batch_branch_and_bound.py", line 182, in input_bab_parallel
global_lb, ret = net.build(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 455, in build
lb, ub, aux_reference_bounds = self.net.init_alpha(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/optimized_bounds.py", line 766, in init_alpha
l, u = self.compute_bounds(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1206, in compute_bounds
return self._compute_bounds_main(C=C,
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1303, in _compute_bounds_main
self.check_prior_bounds(final)
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
self.check_prior_bounds(n)
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
self.check_prior_bounds(n)
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
self.check_prior_bounds(n)
[Previous line repeated 1 more time]
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 804, in check_prior_bounds
self.compute_intermediate_bounds(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 910, in compute_intermediate_bounds
node.lower, node.upper = self.backward_general(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 256, in backward_general
A, lower_b, upper_b = l.bound_backward(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/nonlinear.py", line 512, in bound_backward
As, lbias, ubias = super().bound_backward(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/activation_base.py", line 248, in bound_backward
As, lbias, ubias = super().bound_backward(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/activation_base.py", line 66, in bound_backward
self.bound_relax(x, init=True)
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/nonlinear.py", line 231, in bound_relax
self.bound_relax_impl_sigmoid(lb, ub, self.act_func, self.d_act_func)
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/nonlinear.py", line 174, in bound_relax_impl_sigmoid
self.add_linear_relaxation(
File "/scratch/shuyilin/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/activation_base.py", line 46, in add_linear_relaxation
w_out[..., mask] = (k[..., mask].to(w_out) if isinstance(k, Tensor)
RuntimeError: CUDA error: device-side assert triggered
CUDA kernel errors might be asynchronously reported at some other API call,so the stacktrace below might be incorrect.
For debugging consider passing CUDA_LAUNCH_BLOCKING=1.
"
I have several onnx files for one model (the only difference of them is the weights and bias). But some onnx files meet this problem and some not.

To Reproduce

  • Unzip the reproduce.zip.
  • In /reproduce, run python xxx/abcrown.py --config --config pensieve_parallel_big_3_2_0_0_error.yaml will reproduce the error
  • In /reproduce, run python xxx/abcrown.py --config --config pensieve_parallel_big_3_2_0_0.yaml will evaluate successfully

System configuration:

  • Ubuntu 11.4.0-1ubuntu1~22.04
  • Python 3.9
  • alpha-beta-crown: 23 Octorber release

Thanks in advance for any ideas and suggestions.

reproduce.zip

Query on the way your system handles vgg-16 network

Hi,

I wonder how do you handle vgg16 networks in your system.
And I noticed from prepare_instance.sh that you would call up dnnv to convert the maxpooling layer to relu.
So may I double-check that when your system verifies on vgg16, it verified on the converted network?
Thank you so much for your reply!

Best regards,
Yuyi

alpha-beta-crown behavior

Hi,

I tried the following simple network to make sure I correctly understood alpha-beta-CROWN behavior.
Untitled Diagram drawio

Case 1:
(assert (or
(and (>= X_0 -1.0) (<= X_0 1.0) (>= X_1 0.5) (<= X_1 0.5) (<= Y_0 -0.6))
))
The true interval of y_0 is [-0.5, 0.5]. alpha-beta-CROWN returned safe.

Case 2:
(assert (or
(and (>= X_0 -1.0) (<= X_0 1.0) (>= X_1 0.5) (<= X_1 0.5) (>= Y_0 0.0))
))
The true interval of y_0 is [-0.5, 0.5]. alpha-beta-CROWN returned unknown.

The result of case 1 is as I expected, but I expected the result of case 2 to be unsafe as alpha-beta-crown is sound and complete. Please correct me if I am wrong but when two possible cases of the only Relu node are investigated and the corresponding bounds are calculated, I think we can give a definite response with regard to the violation or satisfaction of the defined property.

Here are the yaml config yaml.txt and the model model.txt in case you need them.

Query on the back propagation algorithm in the original crown

I have read the paper《Efficient neural network robustness certification with general activation functions》(proposed CROWN),I have a question:
Why should back propagate to the first layer to calculate Global bounds by Λ(0) and Ω(0)?will the Global bounds obtained this way be more accurate?

auto_LiRPA runtime error for self-built onnx network

Hi,

I tried to run abcrown on the network built by myself.
A special thing about my network is that it is like "residual linear", where I have a "
Add" node but its inputs are two "Gemm" nodes (unlike residual block which is two Conv nodes as inputs of "Add")
The input of the network is [1, 1, 28, 28] , and I set the input shape in .yaml as well.

model:
   input_shape: [1, 1, 28, 28] 

But during execution, it gave me:

  File "alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 857, in check_prior_bounds
    node.inputs[i], prior_checked=True)
  File "alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 946, in compute_intermediate_bounds
    ref_intermediate_lb, ref_intermediate_ub)
  File "alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 346, in get_sparse_C
    num_channel = node.output_shape[-3]
IndexError: tuple index out of range

I thought auto-LiRPA can handle any DAG? I am not sure what leads to the problem.
Could you please kindly give me some advice?

Thanks and regards,
Yuyi

Unable to run BAB attack with any given configuration files

Describe the bug
Running with any configuration file in exp_configs/bab_attack/ fails with error

To Reproduce
Please provide us with the following to receive timely help:

  1. Clone official repository
  2. Set up conda env
  3. Run conda activate alpha-beta-crown
  4. Run python abcrown.py --config exp_configs/bab_attack/cifar_cnn_a_adv.yaml

Just running the official reposity with the given configuration file is failing for bab attack.
Output:

/home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/pkg_resources/__init__.py:121: DeprecationWarning: pkg_resources is deprecated as an API
  warnings.warn("pkg_resources is deprecated as an API", DeprecationWarning)
/home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/pkg_resources/__init__.py:2870: DeprecationWarning: Deprecated call to `pkg_resources.declare_namespace('google')`.
Implementing implicit namespace packages (as specified in PEP 420) is preferred to `pkg_resources.declare_namespace`. See https://setuptools.pypa.io/en/latest/references/keywords.html#keyword-namespace-packages
  declare_namespace(pkg)
/home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/torchvision/io/image.py:13: UserWarning: Failed to load image Python extension: /home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/torchvision/image.so: undefined symbol: _ZNK3c1010TensorImpl36is_contiguous_nondefault_policy_implENS_12MemoryFormatE
  warn(f"Failed to load image Python extension: {e}")
Configurations:

general:
  device: cuda
  seed: 100
  conv_mode: patches
  deterministic: false
  double_fp: false
  loss_reduction_func: sum
  sparse_alpha: true
  sparse_interm: true
  save_adv_example: false
  eval_adv_example: false
  show_adv_example: false
  precompile_jit: false
  complete_verifier: bab
  enable_incomplete_verification: true
  csv_name: null
  results_file: out.txt
  root_path: ''
  deterministic_opt: false
  graph_optimizer: 'Customized("custom_graph_optimizer", "default_optimizer")'
  no_batchdim_buffers: false
  save_output: false
  output_file: out.pkl
model:
  name: cnn_4layer_adv
  path: models/sdp/cifar_cnn_a_adv.model
  onnx_path: null
  onnx_path_prefix: ''
  cache_onnx_conversion: false
  debug_onnx: false
  onnx_quirks: null
  input_shape: null
  onnx_loader: default_onnx_and_vnnlib_loader
  onnx_optimization_flags: none
  onnx_vnnlib_joint_optimization_flags: none
  check_optmized: false
  flatten_final_output: false
  optimize_graph: null
data:
  start: 537
  end: 538
  select_instance: null
  num_outputs: 10
  mean: [0.4914, 0.4824, 0.4467]
  std: [0.2471, 0.2435, 0.2616]
  pkl_path: null
  dataset: CIFAR
  data_filter_path: null
  data_idx_file: null
specification:
  type: lp
  robustness_type: verified-acc
  norm: .inf
  epsilon: 0.00784313725
  epsilon_min: 0.0
  vnnlib_path: null
  vnnlib_path_prefix: ''
  rhs_offset: null
solver:
  batch_size: 8192
  auto_enlarge_batch_size: false
  min_batch_size_ratio: 0.1
  use_float64_in_last_iteration: false
  early_stop_patience: 10
  start_save_best: 0.5
  bound_prop_method: alpha-crown
  init_bound_prop_method: same
  prune_after_crown: false
  crown:
    batch_size: 1000000000
    max_crown_size: 1000000000
  alpha-crown:
    alpha: true
    lr_alpha: 0.1
    iteration: 100
    share_alphas: false
    lr_decay: 0.98
    full_conv_alpha: true
    max_coeff_mul: .inf
    matmul_share_alphas: false
    apply_output_constraints_to: []
    disable_optimization: []
  beta-crown:
    lr_alpha: 0.01
    lr_beta: 0.05
    lr_decay: 0.999
    optimizer: adam
    iteration: 100
    beta: true
    beta_warmup: true
    enable_opt_interm_bounds: false
    all_node_split_LP: false
  forward:
    refine: false
    dynamic: false
    max_dim: 10000
  multi_class:
    label_batch_size: 32
    skip_with_refined_bound: true
  mip:
    parallel_solvers: 8
    solver_threads: 1
    refine_neuron_timeout: 15
    refine_neuron_time_percentage: 0.8
    early_stop: true
    adv_warmup: true
    mip_solver: gurobi
    skip_unsafe: false
bab:
  initial_max_domains: 1
  max_domains: 5000000
  decision_thresh: 0
  timeout: 1800
  timeout_scale: 1
  override_timeout: null
  get_upper_bound: true
  dfs_percent: 0.0
  pruning_in_iteration: true
  pruning_in_iteration_ratio: 0.2
  sort_targets: false
  batched_domain_list: true
  optimized_interm: ''
  interm_transfer: true
  recompute_interm: false
  sort_domain_interval: -1
  vanilla_crown: false
  cut:
    enabled: false
    implication: false
    bab_cut: false
    lp_cut: false
    method: null
    lr: 0.01
    lr_decay: 1.0
    iteration: 100
    bab_iteration: -1
    early_stop_patience: -1
    lr_beta: 0.02
    number_cuts: 50
    topk_cuts_in_filter: 1000
    batch_size_primal: 100
    max_num: 1000000000
    patches_cut: false
    cplex_cuts: false
    cplex_cuts_wait: 0
    cplex_cuts_revpickup: true
    cut_reference_bounds: true
    fix_intermediate_bounds: false
  branching:
    method: kfsb
    candidates: 3
    reduceop: max
    enable_intermediate_bound_opt: false
    branching_input_and_activation: false
    branching_input_and_activation_order: [input, relu]
    branching_input_iterations: 30
    branching_relu_iterations: 50
    sb_coeff_thresh: 0.001
    nonlinear_split:
      method: shortcut
      branching_point_method: uniform
      num_branches: 2
      branching_point_refinement: false
      filter: false
      filter_beta: false
      filter_batch_size: 10000
      filter_iterations: 25
      shortlist_size: 500
      loose_tanh_threshold: null
    new_input_split:
      enable: false
      batch_size: 2
      rounds: 1
      init_alpha_batch_size: 8192
      full_alpha: false
    input_split:
      enable: false
      enhanced_bound_prop_method: alpha-crown
      enhanced_branching_method: naive
      enhanced_bound_patience: 100000000.0
      attack_patience: 100000000.0
      adv_check: 0
      split_partitions: 2
      sb_margin_weight: 1.0
      sb_primary_spec: null
      sb_primary_spec_iter: 1
      sb_sum: false
      bf_backup_thresh: -1
      bf_rhs_offset: 0
      bf_zero_crossing_score: false
      ibp_enhancement: false
      catch_assertion: false
      compare_with_old_bounds: false
      update_rhs_with_attack: false
  attack:
    enabled: true
    beam_candidates: 128
    beam_depth: 6
    max_dive_fix_ratio: 0.5
    min_local_free_ratio: 0.5
    mip_start_iteration: 2
    mip_timeout: 360
    adv_pool_threshold: null
    refined_mip_attacker: true
    refined_batch_size: null
attack:
  pgd_order: before
  pgd_steps: 100
  pgd_restarts: 100
  pgd_batch_size: 100000000
  pgd_early_stop: true
  pgd_lr_decay: 0.99
  pgd_alpha: auto
  pgd_loss_mode: null
  enable_mip_attack: false
  adv_saver: default_adv_saver
  early_stop_condition: default_early_stop_condition
  adv_example_finalizer: default_adv_example_finalizer
  pgd_loss: default_pgd_loss
  cex_path: ./test_cex.txt
  attack_mode: diverse_pgd
  attack_tolerance: 0.0
  attack_func: attack_with_general_specs
  gama_lambda: 10.0
  gama_decay: 0.9
  check_clean: false
  input_split:
    pgd_steps: 100
    pgd_restarts: 30
    pgd_alpha: auto
  input_split_enhanced:
    pgd_steps: 200
    pgd_restarts: 500000
    pgd_alpha: auto
  input_split_check_adv:
    pgd_steps: 5
    pgd_restarts: 5
    pgd_alpha: auto
    max_num_domains: 10
debug:
  view_model: false
  lp_test: null
  rescale_vnnlib_ptb: null
  test_optimized_bounds: false
  test_optimized_bounds_after_n_iterations: 0

Experiments at Tue Feb 20 22:08:43 2024 on potato
Sequential(
  (0): Conv2d(3, 16, kernel_size=(4, 4), stride=(2, 2), padding=(1, 1))
  (1): ReLU()
  (2): Conv2d(16, 32, kernel_size=(4, 4), stride=(2, 2), padding=(1, 1))
  (3): ReLU()
  (4): Flatten(start_dim=1, end_dim=-1)
  (5): Linear(in_features=2048, out_features=100, bias=True)
  (6): ReLU()
  (7): Linear(in_features=100, out_features=10, bias=True)
)
Parameters:
  0.weight: shape torch.Size([16, 3, 4, 4])
  0.bias: shape torch.Size([16])
  2.weight: shape torch.Size([32, 16, 4, 4])
  2.bias: shape torch.Size([32])
  5.weight: shape torch.Size([100, 2048])
  5.bias: shape torch.Size([100])
  7.weight: shape torch.Size([10, 100])
  7.bias: shape torch.Size([10])
Trying generic MNIST/CIFAR data loader.
Files already downloaded and verified
Internal results will be saved to out.txt.

 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 0, vnnlib ID: 537 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Attack parameters: initialization=uniform, steps=100, restarts=100, alpha=0.008052505552768707, initialization=uniform, GAMA=False
Model output of first 5 examples:
 tensor([[ -7.39000368, -13.28085136,  -4.82924271,  -7.23044920,  -5.35508966,
          -8.15784931,  -6.39428473,  -8.74342728, -11.18965244, -12.32971764]],
       device='cuda:0')
100%|████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████| 1/1 [00:00<00:00,  2.07it/s]
Adv example prediction (first 2 examples and 2 restarts):
 tensor([[[ -6.71217108, -12.28457832,  -4.12656498,  -6.24762297,  -4.17495298,
           -7.11022472,  -5.33284330,  -7.67359495, -10.33115959, -11.30035210],
         [ -6.71217108, -12.28457832,  -4.12656498,  -6.24762297,  -4.17495298,
           -7.11022472,  -5.33284330,  -7.67359495, -10.33115959, -11.30035210]]],
       device='cuda:0')
PGD attack margin (first 2 examles and 10 specs):
 tensor([[[2.58560610, 8.15801334, 2.12105799, 0.04838800, 2.98365974,
          1.20627832, 3.54702997, 6.20459461, 7.17378712]]], device='cuda:0')
number of violation:  0
Attack finished in 1.0545 seconds.
PGD attack failed
/home/yusuf/Desktop/abc_fresh/complete_verifier/auto_LiRPA/parse_graph.py:154: FutureWarning: 'torch.onnx.symbolic_helper._set_opset_version' is deprecated in version 1.13 and will be removed in version 1.14. Please remove its usage and avoid setting internal variables directly.
  _set_opset_version(12)
Model: BoundedModule(
  (/input.1): BoundInput(name=/input.1, inputs=[], perturbed=True)
  (/1): BoundParams(name=/1, inputs=[], perturbed=False)
  (/2): BoundParams(name=/2, inputs=[], perturbed=False)
  (/3): BoundParams(name=/3, inputs=[], perturbed=False)
  (/4): BoundParams(name=/4, inputs=[], perturbed=False)
  (/5): BoundParams(name=/5, inputs=[], perturbed=False)
  (/6): BoundParams(name=/6, inputs=[], perturbed=False)
  (/7): BoundParams(name=/7, inputs=[], perturbed=False)
  (/8): BoundParams(name=/8, inputs=[], perturbed=False)
  (/input): BoundConv(name=/input, inputs=[/input.1, /1, /2], perturbed=True)
  (/input.4): BoundRelu(name=/input.4, inputs=[/input], perturbed=True)
  (/input.8): BoundConv(name=/input.8, inputs=[/input.4, /3, /4], perturbed=True)
  (/12): BoundRelu(name=/12, inputs=[/input.8], perturbed=True)
  (/13): BoundFlatten(name=/13, inputs=[/12], perturbed=True)
  (/input.12): BoundLinear(name=/input.12, inputs=[/13, /5, /6], perturbed=True)
  (/15): BoundRelu(name=/15, inputs=[/input.12], perturbed=True)
  (/16): BoundLinear(name=/16, inputs=[/15, /7, /8], perturbed=True)
)
Original output: tensor([[ -7.39000368, -13.28085136,  -4.82924271,  -7.23044920,  -5.35508966,
          -8.15784931,  -6.39428473,  -8.74342632, -11.18965340, -12.32971668]],
       device='cuda:0')
Split layers:
  BoundConv(name=/input, inputs=[/input.1, /1, /2], perturbed=True): [(BoundRelu(name=/input.4, inputs=[/input], perturbed=True), 0)]
  BoundConv(name=/input.8, inputs=[/input.4, /3, /4], perturbed=True): [(BoundRelu(name=/12, inputs=[/input.8], perturbed=True), 0)]
  BoundLinear(name=/input.12, inputs=[/13, /5, /6], perturbed=True): [(BoundRelu(name=/15, inputs=[/input.12], perturbed=True), 0)]
Nonlinear functions:
   BoundRelu(name=/input.4, inputs=[/input], perturbed=True)
   BoundRelu(name=/12, inputs=[/input.8], perturbed=True)
   BoundRelu(name=/15, inputs=[/input.12], perturbed=True)
layer /input.4 using sparse-features alpha with shape [686]; unstable size 686; total size 4096 ([1, 16, 16, 16])
layer /input.4 start_node /input.8 using sparse-spec alpha [2, 458, 1, 686] with unstable size 457 total_size 2048 output_shape (32, 8, 8)
layer /input.4 start_node /input.12 using sparse-spec alpha [2, 25, 1, 686] with unstable size 24 total_size 100 output_shape torch.Size([100])
layer /input.4 start_node /16 using full alpha [2, 9, 1, 686] with unstable size None total_size 9 output_shape 9
layer /12 using sparse-features alpha with shape [457]; unstable size 457; total size 2048 ([1, 32, 8, 8])
layer /12 start_node /input.12 using sparse-spec alpha [2, 25, 1, 457] with unstable size 24 total_size 100 output_shape torch.Size([100])
layer /12 start_node /16 using full alpha [2, 9, 1, 457] with unstable size None total_size 9 output_shape 9
layer /15 using sparse-features alpha with shape [24]; unstable size 24; total size 100 ([1, 100])
layer /15 start_node /16 using full alpha [2, 9, 1, 24] with unstable size None total_size 9 output_shape 9
Optimizable variables initialized.
initial CROWN bounds: tensor([[ 0.77253890,  5.35441875,  0.88030529, -0.71995872,  1.51813030,
         -0.45570922,  1.82640553,  3.47526670,  4.63339520]], device='cuda:0') None
best_l after optimization: 18.567962646484375
alpha/beta optimization time: 2.470933437347412
initial alpha-crown bounds: tensor([[ 0.91563702,  5.49638367,  1.00899839, -0.58640003,  1.65252423,
         -0.34389973,  2.01817369,  3.65779972,  4.74874640]], device='cuda:0')
Worst class: (+ rhs) -0.586400032043457
Total VNNLIB file length: 9, max property batch size: 1, total number of batches: 9
lA shape: [torch.Size([9, 1, 16, 16, 16]), torch.Size([9, 1, 32, 8, 8]), torch.Size([9, 1, 100])]

Properties batch 0, size 1
Remaining timeout: 1795.2805857658386
##### Instance 0 first 10 spec matrices: 
tensor([[[ 0.,  0.,  1.,  0., -1.,  0.,  0.,  0.,  0.,  0.]]])
thresholds: tensor([0.], device='cuda:0') ######
Remaining spec index tensor([0], device='cuda:0') with bounds tensor([[-0.58640003]], device='cuda:0') need to verify.
Model prediction is: tensor([ -7.39000368, -13.28085136,  -4.82924271,  -7.23044920,  -5.35508966,
         -8.15784931,  -6.39428473,  -8.74342632, -11.18965340, -12.32971668],
       device='cuda:0')
build_with_refined_bounds batch [1/1]
setting alpha for layer /input.4 start_node /16 with alignment adjustment
setting alpha for layer /12 start_node /16 with alignment adjustment
setting alpha for layer /15 start_node /16 with alignment adjustment
all alpha initialized
true A is required, we do a full backward CROWN pass to obtain it
(alpha-)CROWN with fixed intermediate bounds: tensor([[-0.58639872]], device='cuda:0') tensor([[1.64917374]], device='cuda:0')
Intermediate layers: /input,/input.8,/input.12,/16
Keeping alphas for these layers: ['/16']
Keeping alphas for these layers: ['/16']
Traceback (most recent call last):
  File "/home/yusuf/Desktop/abc_fresh/complete_verifier/abcrown.py", line 612, in <module>
    abcrown.main()
  File "/home/yusuf/Desktop/abc_fresh/complete_verifier/abcrown.py", line 591, in main
    verified_status = self.complete_verifier(
  File "/home/yusuf/Desktop/abc_fresh/complete_verifier/abcrown.py", line 398, in complete_verifier
    l, nodes, ret = self.bab(
  File "/home/yusuf/Desktop/abc_fresh/complete_verifier/abcrown.py", line 241, in bab
    result = general_bab(
  File "/home/yusuf/Desktop/abc_fresh/complete_verifier/bab.py", line 302, in general_bab
    domains = DomainClass(
  File "/home/yusuf/Desktop/abc_fresh/complete_verifier/attack/domains.py", line 206, in __init__
    candidate_domains = [to_cpu(ReLUDomain(
  File "/home/yusuf/Desktop/abc_fresh/complete_verifier/attack/domains.py", line 206, in <listcomp>
    candidate_domains = [to_cpu(ReLUDomain(
  File "/home/yusuf/Desktop/abc_fresh/complete_verifier/attack/domains.py", line 94, in to_cpu
    self.lA = [lA.to(device='cpu', non_blocking=True) for lA in self.lA]
  File "/home/yusuf/Desktop/abc_fresh/complete_verifier/attack/domains.py", line 94, in <listcomp>
    self.lA = [lA.to(device='cpu', non_blocking=True) for lA in self.lA]
AttributeError: 'str' object has no attribute 'to'

System configuration:

  • OS: Ubuntu 23.04
  • Python version: Python 3.9.17
  • Pytorch Version: 1.13.1+cu117
  • Hardware: intel 13900h, rtx 4070
  • Have you tried to reproduce the problem in a cleanly created conda/virtualenv environment using official installation instructions and the latest code on the main branch?: Yes

need help with Regression model and batch-normalization

Hi,

I would like to kindly ask for help with the following two items:

  1. I have trained a feed forward DNN regression model in pytorch with say 12 input neurons and 50 output neurons. I have used dropout and batch-normalization layers in between also. The structure is given below. I was wondering if the alpha-beta-CROWN module can handle such a model. If so do I need to make any changes regarding the BN layers or everything will be taken care of automatically.

dropout_rate = 0.2
number_of_neurons = 30

model = nn.Sequential(
nn.Linear(x_train.shape[1], number_of_neurons),
nn.ReLU(),
nn.BatchNorm1d(number_of_neurons),
nn.Dropout(dropout_rate),
nn.Linear(number_of_neurons, number_of_neurons),
nn.ReLU(),
nn.BatchNorm1d(number_of_neurons),
nn.Dropout(dropout_rate),
nn.Linear(number_of_neurons, y_train.shape[1])
).cuda()

  1. My main concern is with the data preparation. Currently I have one .npy file with 2k rows and 12 columns for input (X) and 2k rows and 50 columns for output (Y). I have 2k test samples. looking at the sample data given for example in mnist_eran folder, y_eran.npy only has one column which makes sense for classification problems. I am wondering what should I do to my dataset specifically for the output to make it compatible with the alpha-beta-CROWN module. Also what other changes should I make in the config.YAML file to make the analysis compatible for regression analysis.

Thank you in advance for your help!

Bound backward error of BoundMaxPool layer

I trained several adv trained models based on the origin github repo of Madry and Trades, even with the defination in alpha-beta-CROWN/complete_verifier/model_defs.py.
When I use robustness_verifier.py to validate these models, an same error raised for all of them.

The error caused by the code assert type(last_lA) == torch.Tensor or type(last_uA) == torch.Tensor in auto_LiRPA/operators/convolution.py -> class BoundMaxPool -> function bound_backward.

When I check the type of last_lA, I found it is patches not tensor, so cannot pass the assert check.

I then checked the demos in exp_configs, I want to use a model and config provided by you to reproduce the error but I found unfortunately that it seems no model contains the MaxPool layer. If you need me to provide a model for reproducing this problem, I will be happy to do so.

AssertionError Due to Certain Data

Dear alpha-beta-CROWN Team,

I would like to extend my gratitude for your excellent work.

Your sample code works perfectly when we run it.

However, I'm writing to report an issue that I encountered
while attempting to run your sample code with a custom model using the following command:

python abcrown.py --config exp_configs/mnist_S.yaml

To provide some context, I added a custom model definition in model_defs.py, which looks as follows:

def conv_S():
    model = nn.Sequential(
        nn.Conv2d(1, 16, 4, stride=2, padding=1),
        nn.ReLU(),
        nn.MaxPool2d(2),
        nn.Conv2d(16, 32, 4, stride=2, padding=1),
        nn.ReLU(),
        nn.MaxPool2d(2),
        Flatten(),
        nn.Linear(32, 24),
        nn.ReLU(),
        nn.Linear(24, 10)
    )
    return model

At this point, the code executes perfectly in idx 0 to 12 but has a result in idx 13,
it encounters the following issue:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 13, vnnlib ID: 13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Attack parameters: initialization=uniform, steps=100, restarts=100, alpha=0.025000005960464478, initialization=uniform, GAMA=False
Model output of first 5 examples:
 tensor([[ 9.34262276, -7.84992790,  1.48994040, -5.32939434, -1.97707677,
          0.06667299,  0.49797791, -3.03078222,  2.04741216, -0.75792819]],
       device='cuda:0')
Adv example prediction (first 2 examples and 2 restarts):
 tensor([[[ 6.48601294, -7.30414724,  0.62207073, -3.60429788, -2.02184796,
          -0.06410425, -1.29587710, -2.43488121,  4.11566591,  1.92593360],
         [ 6.48601294, -7.30414724,  0.62207073, -3.60429788, -2.02184796,
          -0.06410425, -1.29587710, -2.43488121,  4.11566591,  1.92593360]]],
       device='cuda:0')
PGD attack margin (first 2 examles and 10 specs):
 tensor([[[13.79016018,  5.86394215, 10.09031105,  8.50786114,  6.55011702,
           7.78188992,  8.92089462,  2.37034702,  4.56007957]]],
       device='cuda:0')
number of violation:  0
Attack finished in 0.3795 seconds.
PGD attack failed
/home/user/anaconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/nn/functional.py:749: UserWarning: Note that order of the arguments: ceil_mode and return_indices will changeto match the args list in nn.MaxPool2d in a future release.
  warnings.warn("Note that order of the arguments: ceil_mode and return_indices will change"
Model prediction is: tensor([[ 9.34262276, -7.84992790,  1.48994040, -5.32939434, -1.97707677,
          0.06667299,  0.49797791, -3.03078222,  2.04741216, -0.75792819]],
       device='cuda:0')
layer /10 using sparse-features alpha with shape [1178]; unstable size 1178; total size 3136 (torch.Size([1, 16, 14, 14]))
layer /10 start_node /input.8 using sparse-spec alpha with unstable size 166 total_size 288 output_shape (32, 3, 3)
layer /10 start_node /input.12 using sparse-spec alpha with unstable size 21 total_size 24 output_shape torch.Size([24])
layer /10 start_node /25 using full alpha with unstable size None total_size 9 output_shape 9
Traceback (most recent call last):
  File "abcrown.py", line 647, in <module>
    main()
  File "abcrown.py", line 535, in main
    incomplete_verifier(model_ori, x, data_ub=data_max, data_lb=data_min, vnnlib=vnnlib)
  File "abcrown.py", line 69, in incomplete_verifier
    domain, x, data_lb, data_ub, vnnlib, stop_criterion_func=stop_criterion_min(arguments.Config["bab"]["decision_thresh"]))
  File "/home/user/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1069, in build_the_model
    (self.x,), share_slopes=share_slopes, c=self.c, bound_upper=False)
  File "/home/user/alpha-beta-CROWN/complete_verifier/auto_LiRPA/optimized_bounds.py", line 1050, in init_slope
    final_node_name=final_node_name)
  File "/home/user/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 760, in get_alpha_crown_start_nodes
    assert not sparse_intermediate_bounds or use_sparse_conv is False  # Double check our assumption holds. If this fails, then we created wrong shapes for alpha.
AssertionError

It would be greatly appreciated if you could provide guidance or support to help me overcome this problem.

For your convenience, I have prepared our materials, including mnist_S.yaml, ConvS-custom.pth and model_defs.py, with

wget -O materials.rar https://www.dropbox.com/scl/fi/pnn7ob5focdhr6r3kr843/materials.rar?rlkey=9vp37h1gkxrhf8t2gf8fthqsg&dl=1
unrar x marerials.rar

Thank you in advance for your assistance.

System configuration:

  • OS: Ubuntu 18.04.6 LTS
  • Python version: Python 3.7.13
  • Pytorch Version: PyTorch 1.11.0
  • Hardware: NVIDIA GeForce GTX 1080 Ti
  • Have you tried to reproduce the problem in a cleanly created conda/virtualenv environment using official installation instructions and the latest code on the main branch?: Yes

Input linear constraint

It seems that input linear constraint (e.g., x_1 > x_2) is not supported. I got the following error message.

File "alpha-beta-CROWN/complete_verifier/read_vnnlib.py", line 80, in update_rv_tuple
f"input constraints must be box ({op} {first} {second})"
AssertionError: input constraints must be box

Is there a plan to support input linear constraint in the near future?

GCP-CROWN‘s SDP example error

Describe the bug
Hi, when I reproduced the results for SDP models with GCP-CROWN, an error occurred.

To Reproduce
run 'python abcrown.py --config exp_configs/GCP-CROWN/mnist_cnn_a_adv.yaml'

Traceback (most recent call last):
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/abcrown.py", line 609, in
abcrown.main()
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/abcrown.py", line 588, in main
verified_status = self.complete_verifier(
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/abcrown.py", line 399, in complete_verifier
l, nodes, ret = self.bab(
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/abcrown.py", line 242, in bab
result = general_bab(
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/bab.py", line 269, in general_bab
net.set_cuts(model_incomplete.A_saved, x, ret['lower_bounds'], ret['upper_bounds'])
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/cut_verification.py", line 269, in set_cuts
cuts = add_input_cuts(self, A, number_cuts=number_cuts, device=self.net.device)
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/site-packages/torch/autograd/grad_mode.py", line 27, in decorate_context
return func(*args, **kwargs)
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/implied_cuts.py", line 237, in add_input_cuts
assert last_A.matmul(center) - last_A.abs().matmul(diff) + last_b < 0
AssertionError
mip solver model built in 0.6189 seconds.
lower bounds for all target labels: [1.9055490493774414, 0.5247936248779297, -2.302560329437256, -1.420586109161377, -0.5922765731811523, -0.33838844299316406, -1.5372157096862793, 1.1211633682250977, 0.47852492332458496]
Starting MIP solver for these labels: [2, 3, 4, 5, 6]
start creating model mps for candidates: ['lay/16_2', 'lay/16_3', 'lay/16_4', 'lay/16_5', 'lay/16_6']
parallel save mip model to /home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/CPLEX_cuts/cplexmip_lay-16_starttime=1708308422_idx=1_spec=2_30843038.mps
parallel save mip model to /home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/CPLEX_cuts/cplexmip_lay-16_starttime=1708308422_idx=1_spec=3_30843038.mps
parallel save mip model to /home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/CPLEX_cuts/cplexmip_lay-16_starttime=1708308422_idx=1_spec=4_30843038.mps
parallel save mip model to /home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/CPLEX_cuts/cplexmip_lay-16_starttime=1708308422_idx=1_spec=5_30843038.mps
parallel save mip model to /home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/CPLEX_cuts/cplexmip_lay-16_starttime=1708308422_idx=1_spec=6_30843038.mps
parallel mps save finish
/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/lp_mip_solver.py:1146: ResourceWarning: unclosed file <_io.TextIOWrapper name='/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/cuts/CPLEX_cuts/cplexmip_lay-16_starttime=1708308422_idx=1_spec=2_30843038.log' mode='w' encoding='ANSI_X3.4-1968'>
proc, logfile = run_get_cuts_subprocess(model_filename_stamped)
ResourceWarning: Enable tracemalloc to get the object allocation traceback
Process Process-2:
Traceback (most recent call last):
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/multiprocessing/managers.py", line 802, in _callmethod
conn = self._tls.connection
AttributeError: 'ForkAwareLocal' object has no attribute 'connection'

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/multiprocessing/process.py", line 315, in _bootstrap
self.run()
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/multiprocessing/process.py", line 108, in run
self._target(*self._args, **self._kwargs)
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/site-packages/torch/autograd/grad_mode.py", line 27, in decorate_context
return func(*args, **kwargs)
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/lp_mip_solver.py", line 1042, in construct_mip_with_model
build_the_model_mip(model, labels_to_verify=None, save_mps=save_mps, process_dict=process_dict, x=x, intermediate_bounds=intermediate_bounds)
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/lp_mip_solver.py", line 1152, in build_the_model_mip
raise e
File "/home/ictt/Documents/qj/VNN/alpha-beta-CROWN/complete_verifier/lp_mip_solver.py", line 1147, in build_the_model_mip
processes[pidx] = {'pid': proc.pid, '_logfile': logfile, '_fname_stamped': model_filename_stamped, 'c': model_c_row}
File "", line 2, in setitem
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/multiprocessing/managers.py", line 806, in _callmethod
self._connect()
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/multiprocessing/managers.py", line 793, in _connect
conn = self._Client(self._token.address, authkey=self._authkey)
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/multiprocessing/connection.py", line 502, in Client
c = SocketClient(address)
File "/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/multiprocessing/connection.py", line 630, in SocketClient
s.connect(address)
FileNotFoundError: [Errno 2] No such file or directory
/home/ictt/miniconda3/envs/alpha-beta-crown2/lib/python3.9/subprocess.py:1052: ResourceWarning: subprocess 4172529 is still running
_warn("subprocess %s is still running" % self.pid,
ResourceWarning: Enable tracemalloc to get the object allocation traceback

System configuration:
NVIDIA TITAN RTX 24G.
environment_pyt111.yaml

How to solve the problem?

Import error

Import error at the end of alpha-beta-crown tutorial

Low precision bug for batch-norm models

When I verify a CROWN-ibp pre-trained model using alpha-beta-CROWN, it consistenly shows Result: image x prediction is incorrect, skipped. As a result the overall verified acc. is very low depsite CROWN-verified acc. is relatively normal.

I guess that's batch-norm support problem, because in the printed log I see two new warnings:

/home/zhangheng/anaconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/nn/functional.py:2113: TracerWarning: Converting a tensor to a Python boolean might cause the trace to be incorrect. We can't record the data flow of Python values, so this value will be treated as a constant in the future. This means that the trace might not generalize to other inputs!

  if size_prods == 1:

/home/zhangheng/anaconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/onnx/symbolic_helper.py:680: UserWarning: ONNX export mode is set to inference mode, but operator batch_norm is set to training  mode. The model will be exported in inference, as specified by the export mode.

  training_mode + ", as specified by the export mode.")

I tried some scripts without batchnorm included in exp_configs folder, there are no these two warnings.

Here are the log file, please have a look, thank you!

CROWN-ibp-model-verify.txt

Documentation info and "save_adv_example" only saving last example

A little bit more of basic information explaining the settings would be useful:

  • Explain what are the "unkown", "safe-incomplete" answers you get for some inputs.
  • Also, give an explanation of the different settings for the "robustness_type" setting with links to the papers where they are introduced.

Also,
it seems that the setting "save_adv_example" is only saving the last counterexample found by the solver in the file "test_cex.txt". It would be more useful to have the option to save at least one counterexample for each unsafe input instance.

Compatibility problems pytorch and onnx2pytorch

Hello,
I am having some incompatibility issues at the moment with the alpha-beta-CROWN tool running the experiments for the VNNCOMP21 competition.

I have created a conda environment with python 3.8 and I have installed the packages manually using the installation script provided. The command to install onnx2pytorch from Github did not work: git+git://github.com/Sarimuko/onnx2pytorch@8879f72c41ba960ff6495ae754d885eac2ebf656#egg=onnx2pytorch

So, I installed the pip package available for onnx2python (last version is 0.4.1). This package showed to have some incompatibilities with the pytorch version 1.8.2 (the last available at the pytorch-lts channel). Then I replaced this version by the pytorch version 1.11 for CUDA from the pytorch channel in Anaconda. Like this, the code worked but it still fails in some of the predefined benchmarks of the competition due to some of the torch modules that seem to be incompatible in some way with the code.

My questions are:

Is there a pip package version for onnx2pytorch that matches (or being similar) the one of git+git://github.com/Sarimuko/onnx2pytorch@8879f72c41ba960ff6495ae754d885eac2ebf656#egg=onnx2pytorch?

Do you know what is the latest version of pytorch compatible with the alpha-beta-CROWN code?

I have attached the images with the command introduced to run the code, the errors obtained and the pytorch, onnx, CUDA, onnx2pytorch versions installed.

Thank you in advance.

ErrorAlphaBeta

command_alphabeta

pytorchconda
onnx

Cuda Requirement?

While I am aware that AB Crown only works with Ubuntu, I am wondering if a NVIDIA GPU is a requirement. I believe this may be possible to enable while using a VM, although my attempts have not been successful. Any guidance on that would be wonderful, but in the meantime I am wondering if there is any way to utilize the tool without the CUDA?

Here is my output when running the command: python abcrown.py --config exp_configs/mnist_6_100.yaml

I receive the same output on my VM which runs Kubuntu 23.04, which I attempted to install CUDA on.


/Users/lizsotomayor/miniconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/onnx/mapping.py:27: DeprecationWarning: `np.object` is a deprecated alias for the builtin `object`. To silence this warning, use `object` by itself. Doing this will not modify any behavior and is safe. 
Deprecated in NumPy 1.20; for more details and guidance: https://numpy.org/devdocs/release/1.20.0-notes.html#deprecations
  int(TensorProto.STRING): np.dtype(np.object)
Configurations:

general:
  device: cuda
  seed: 100
  conv_mode: patches
  deterministic: false
  double_fp: false
  loss_reduction_func: sum
  record_bounds: false
  sparse_alpha: true
  save_adv_example: false
  precompile_jit: false
  complete_verifier: bab-refine
  enable_incomplete_verification: true
  csv_name: null
  results_file: out.txt
  root_path: ''
model:
  name: mnist_6_100
  path: models/eran/mnist_6_100_nat.pth
  onnx_path: null
  onnx_path_prefix: ''
  cache_onnx_conversion: false
  onnx_quirks: null
  input_shape: null
  onnx_loader: default_onnx_and_vnnlib_loader
  onnx_optimization_flags: none
data:
  start: 0
  end: 10000
  select_instance: null
  num_outputs: 10
  mean: [0.0]
  std: [1.0]
  pkl_path: null
  dataset: MNIST_ERAN_UN
  data_filter_path: null
  data_idx_file: null
specification:
  type: lp
  robustness_type: verified-acc
  norm: .inf
  epsilon: 0.026
  vnnlib_path: null
  vnnlib_path_prefix: ''
solver:
  batch_size: 1024
  min_batch_size_ratio: 0.1
  use_float64_in_last_iteration: false
  early_stop_patience: 10
  start_save_best: 0.5
  bound_prop_method: alpha-crown
  prune_after_crown: false
  crown:
    batch_size: 1000000000
    max_crown_size: 1000000000
  alpha-crown:
    alpha: true
    lr_alpha: 0.1
    iteration: 100
    share_slopes: false
    no_joint_opt: false
    lr_decay: 0.98
    full_conv_alpha: true
  beta-crown:
    lr_alpha: 0.01
    lr_beta: 0.05
    lr_decay: 0.98
    optimizer: adam
    iteration: 20
    beta: true
    beta_warmup: true
    enable_opt_interm_bounds: false
    all_node_split_LP: false
  forward:
    refine: false
    dynamic: false
    max_dim: 10000
  multi_class:
    multi_class_method: allclass_domain
    label_batch_size: 32
    skip_with_refined_bound: true
  mip:
    parallel_solvers: 16
    solver_threads: 1
    refine_neuron_timeout: 15
    refine_neuron_time_percentage: 0.8
    early_stop: true
    adv_warmup: true
    mip_solver: gurobi
bab:
  initial_max_domains: 1
  max_domains: .inf
  decision_thresh: 0
  timeout: 300
  timeout_scale: 1
  override_timeout: null
  get_upper_bound: false
  dfs_percent: 0.0
  pruning_in_iteration: true
  pruning_in_iteration_ratio: 0.2
  sort_targets: false
  batched_domain_list: true
  optimized_intermediate_layers: ''
  interm_transfer: true
  cut:
    enabled: false
    bab_cut: false
    lp_cut: false
    method: null
    lr: 0.01
    lr_decay: 1.0
    iteration: 100
    bab_iteration: -1
    early_stop_patience: -1
    lr_beta: 0.02
    number_cuts: 50
    topk_cuts_in_filter: 100
    batch_size_primal: 100
    max_num: 1000000000
    patches_cut: false
    cplex_cuts: false
    cplex_cuts_wait: 0
    cplex_cuts_revpickup: true
    cut_reference_bounds: true
    fix_intermediate_bounds: false
  branching:
    method: kfsb
    candidates: 3
    reduceop: max
    sb_coeff_thresh: 0.001
    input_split:
      enable: false
      enhanced_bound_prop_method: alpha-crown
      enhanced_branching_method: naive
      enhanced_bound_patience: 100000000.0
      attack_patience: 100000000.0
      adv_check: 0
      sort_domain_interval: -1
  attack:
    enabled: false
    beam_candidates: 8
    beam_depth: 7
    max_dive_fix_ratio: 0.8
    min_local_free_ratio: 0.2
    mip_start_iteration: 5
    mip_timeout: 30.0
    adv_pool_threshold: null
    refined_mip_attacker: false
    refined_batch_size: null
attack:
  pgd_order: after
  pgd_steps: 100
  pgd_restarts: 30
  pgd_early_stop: true
  pgd_lr_decay: 0.99
  pgd_alpha: auto
  pgd_loss_mode: null
  enable_mip_attack: false
  cex_path: ./test_cex.txt
  attack_mode: PGD
  gama_lambda: 10.0
  gama_decay: 0.9
  check_clean: false
  input_split:
    pgd_steps: 100
    pgd_restarts: 30
    pgd_alpha: auto
  input_split_enhanced:
    pgd_steps: 200
    pgd_restarts: 5000000
    pgd_alpha: auto
  input_split_check_adv:
    pgd_steps: 5
    pgd_restarts: 5
    pgd_alpha: auto
debug:
  lp_test: null

Experiments at Wed Sep 20 01:30:43 2023 on Lizs-Air-3.lan
Sequential(
  (0): Flatten()
  (1): Linear(in_features=784, out_features=100, bias=True)
  (2): ReLU()
  (3): Linear(in_features=100, out_features=100, bias=True)
  (4): ReLU()
  (5): Linear(in_features=100, out_features=100, bias=True)
  (6): ReLU()
  (7): Linear(in_features=100, out_features=100, bias=True)
  (8): ReLU()
  (9): Linear(in_features=100, out_features=100, bias=True)
  (10): ReLU()
  (11): Linear(in_features=100, out_features=10, bias=True)
)
/Users/lizsotomayor/alpha-beta-CROWN-main/complete_verifier/utils.py:623: UserWarning: To copy construct from a tensor, it is recommended to use sourceTensor.clone().detach() or sourceTensor.clone().detach().requires_grad_(True), rather than torch.tensor(sourceTensor).
  eps_temp = torch.tensor(eps_temp).reshape(1, -1, 1, 1)
############################
Sampled data loaded. No normalization used!
Shape: torch.Size([1000, 1, 28, 28]) torch.Size([1000]) torch.Size([1000])
X range: tensor(1.) tensor(0.) tensor(0.12226457)
Note runnerup label is empty here!
############################
Internal results will be saved to Verified_ret_[mnist_6_100]_start=0_end=10000_iter=20_b=1024_timeout=300_branching=kfsb-max-3_lra-init=0.1_lra=0.01_lrb=0.05_PGD=after_cplex_cuts=False_multiclass=allclass_domain.npy.

 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 0, vnnlib ID: 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Traceback (most recent call last):
  File "abcrown.py", line 647, in <module>
    main()
  File "abcrown.py", line 512, in main
    model_ori = model_ori.to(device)
  File "/Users/lizsotomayor/miniconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/nn/modules/module.py", line 989, in to
    return self._apply(convert)
  File "/Users/lizsotomayor/miniconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/nn/modules/module.py", line 641, in _apply
    module._apply(fn)
  File "/Users/lizsotomayor/miniconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/nn/modules/module.py", line 664, in _apply
    param_applied = fn(param)
  File "/Users/lizsotomayor/miniconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/nn/modules/module.py", line 987, in convert
    return t.to(device, dtype if t.is_floating_point() or t.is_complex() else None, non_blocking)
  File "/Users/lizsotomayor/miniconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/torch/cuda/__init__.py", line 221, in _lazy_init
    raise AssertionError("Torch not compiled with CUDA enabled")
AssertionError: Torch not compiled with CUDA enabled

About the output when running on a ResNet18 pretrained model

Hi, thanks for your great work in this field. I was trying to use the abcrown.py file with a ResNet18 adversarially pretrained model (from the Fast Adversarial Training repo). But I'm seeing intermediate outputs like

Result: unknown in 121.7578 seconds

Is this concerning or should I let it run completely before checking the results? Because it is taking quite some time (reached 800 out of 1000 samples on CIFAR10 in ~20 hours). Also, I had to change the config file to use

  crown:
    batch_size: 8
    max_crown_size: 8

because the default batch size and max crown size were 10^8 which caused an out-of-memory error even on a 24GB GPU. Does that seem reasonable or will there be a problem with the evaluation (like not being comparable to the reported results in your papers)?

ResolvePackageNotFound

When I try to execute the below command:
conda env create -f complete_verifier/environment.yml

I face this issue:
Collecting package metadata (repodata.json): done
Solving environment: failed

ResolvePackageNotFound:

  • xz==5.2.5=h7b6447c_0
  • x264==1!157.20191217=h7b6447c_0
  • mkl-service==2.3.0=py37he8ac12f_0
  • lcms2==2.12=h3be6417_0
  • _openmp_mutex==4.5=1_gnu
  • pluggy==0.13.1=py37h06a4308_0
  • giflib==5.2.1=h7b6447c_0
  • pytest==6.2.4=py37h06a4308_2
  • readline==8.1=h27cfd23_0
  • bottleneck==1.3.2=py37heb32a55_1
  • jpeg==9b=h024ee3a_2
  • libidn2==2.3.2=h7f8727e_0
  • numpy==1.19.2=py37h54aff64_0
  • ca-certificates==2021.10.26=h06a4308_2
  • ffmpeg==4.2.2=h20bf706_0
  • bzip2==1.0.8=h7b6447c_0
  • libprotobuf==3.17.2=h4ff587b_1
  • lame==3.100=h7b6447c_0
  • libwebp-base==1.2.0=h27cfd23_0
  • certifi==2021.10.8=py37h06a4308_0
  • lz4-c==1.9.3=h295c915_1
  • gnutls==3.6.15=he1e5248_0
  • sqlite==3.36.0=hc218d9a_0
  • libopus==1.3.1=h7b6447c_0
  • intel-openmp==2021.4.0=h06a4308_3561
  • openh264==2.1.0=hd408876_0
  • cudatoolkit==11.1.74=h6bb024c_0
  • nettle==3.7.3=hbbd107a_1
  • setuptools==58.0.4=py37h06a4308_0
  • gmp==6.2.1=h2531618_2
  • protobuf==3.17.2=py37h295c915_0
  • libunistring==0.9.10=h27cfd23_0
  • importlib-metadata==4.8.1=py37h06a4308_0
  • libuv==1.40.0=h7b6447c_0
  • pyyaml==6.0=py37h7f8727e_1
  • tk==8.6.11=h1ccaba5_0
  • freetype==2.11.0=h70c0345_0
  • ninja==1.10.2=hff7bd54_1
  • zlib==1.2.11=h7b6447c_3
  • libstdcxx-ng==9.3.0=hd4cf53a_17
  • libgomp==9.3.0=h5101ec6_17
  • ncurses==6.3=heee7806_1
  • zstd==1.4.9=haebb681_0
  • pip==21.0.1=py37h06a4308_0
  • pytorch==1.8.2=py3.7_cuda11.1_cudnn8.0.5_0
  • libffi==3.3=he6710b0_2
  • python==3.7.11=h12debd9_0
  • openssl==1.1.1l=h7f8727e_0
  • ld_impl_linux-64==2.35.1=h7274673_9
  • libgcc-ng==9.3.0=h5101ec6_17
  • pillow==8.4.0=py37h5aabda8_0
  • mkl_random==1.1.0=py37hd6b4f25_0
  • yaml==0.2.5=h7b6447c_0
  • libpng==1.6.37=hbc83047_0
  • libtiff==4.2.0=h85742a9_0
  • mkl_fft==1.3.0=py37h54f3939_0
  • pandas==1.3.4=py37h8c16a72_0
  • libtasn1==4.16.0=h27cfd23_0
  • libwebp==1.2.0=h89dd481_0
  • numpy-base==1.19.2=py37hfa32c7d_0
  • libvpx==1.7.0=h439df22_0
  • numexpr==2.7.3=py37hb2eb853_0

For your information, I am working on Windows OS.

custome model error

Hi there,
I tried to verify a customized model using alpha-beta-crown, but I got an error I could not figure out how to fix. I'd appreciate it if you could have a look at it.

yaml file:

general:
  enable_incomplete_verification: False
  loss_reduction_func: max
  conv_mode: matrix
model:
  name: cmars
  input_shape: 19
specification:
  vnnlib_path: cmars/vnnlib/large_1/N8/h32/basic.vnnlib
attack:
  pgd_order: skip
solver:
  batch_size: 500000  
  bound_prop_method: forward+backward
  beta-crown:
    iteration: 10  
bab:
  initial_max_domains: 100
  branching:
    method: naive  # Split on input space.
    input_split:
      enable: True
      adv_check: .inf

The model is defined in model_defs.py:

def cmars() -> nn.Sequential:
    return nn.Sequential(
            nn.Linear(19, 32),
            nn.ReLU(),
            nn.Linear(32, 32),
            nn.ReLU(),
            nn.Linear(32, 140),
            nn.ReLU(),
            nn.Linear(140, 1),
    )

basic.vnnlib

(declare-const X_0 Real)
(declare-const X_1 Real)
(declare-const X_2 Real)
(declare-const X_3 Real)
(declare-const X_4 Real)
(declare-const X_5 Real)
(declare-const X_6 Real)
(declare-const X_7 Real)
(declare-const X_8 Real)
(declare-const X_9 Real)
(declare-const X_10 Real)
(declare-const X_11 Real)
(declare-const X_12 Real)
(declare-const X_13 Real)
(declare-const X_14 Real)
(declare-const X_15 Real)
(declare-const X_16 Real)
(declare-const X_17 Real)
(declare-const X_18 Real)

(declare-const Y_0 Real)

(assert (or 
	(and (<= X_0 0.11281310021877289) (>= X_0 0.08347102999687195) (<= X_1 -0.04856841638684273) (>= X_1 -0.07791049033403397) (<= X_2 -0.004555195104330778) (>= X_2 -0.033897269517183304) (<= X_3 0.06879998743534088) (>= X_3 0.03945791721343994) (<= X_4 0.1568262130022049) (>= X_4 0.12748414278030396) (<= X_5 0.2448524385690689) (>= X_5 0.21551036834716797) (<= X_6 0.2595234811306) (>= X_6 0.23018139600753784) (<= X_7 0.33287864923477173) (>= X_7 0.303536593914032) (<= X_8 0.42090487480163574) (>= X_8 0.391562819480896) (<= X_9 0.42090487480163574) (>= X_9 0.391562819480896) (<= X_10 0.391562819480896) (>= X_10 0.36222073435783386) (<= X_11 0.47958904504776) (>= X_11 0.4502469599246979) (<= X_12 0.6262993812561035) (>= X_12 0.5969573259353638) (<= X_13 0.6996545791625977) (>= X_13 0.6703125238418579) (<= X_14 0.7143256068229675) (>= X_14 0.6849835515022278) (<= X_15 0.6262993812561035) (>= X_15 0.5969573259353638) (<= X_16 0.5529442429542542) (>= X_16 0.5236021280288696) (<= X_17 0.4502469599246979) (>= X_17 0.42090487480163574) (<= X_18 0.4942600727081299) (>= X_18 0.46491798758506775) (>= Y_0 0))
))

The error:

Traceback (most recent call last):
  File "abcrown.py", line 661, in <module>
    main()
  File "abcrown.py", line 584, in main
    refined_betas=refined_betas, attack_images=all_adv_candidates, attack_margins=attack_margins)
  File "abcrown.py", line 410, in complete_verifier
    rhs=rhs, timeout=timeout, attack_images=this_spec_attack_images)
  File "abcrown.py", line 200, in bab
    rhs=rhs, timeout=timeout, branching_method=arguments.Config["bab"]["branching"]["method"])
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/batch_branch_and_bound_input_split.py", line 164, in input_bab_parallel
    bounding_method=bounding_method,
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1141, in build_the_model
    x=(x,), C=self.c, method=bounding_method, cutter=self.cutter, bound_upper=False)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1319, in compute_bounds
    self.check_prior_bounds(final)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 847, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 847, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 847, in check_prior_bounds
    self.check_prior_bounds(n)
  [Previous line repeated 6 more times]
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 855, in check_prior_bounds
    node.inputs[i], prior_checked=True)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 883, in compute_intermediate_bounds
    node=node, concretize=True)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/forward_bound.py", line 32, in forward_general
    self.forward_general(node=l_pre, offset=offset)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/forward_bound.py", line 40, in forward_general
    linear = node.linear = node.bound_forward(self.dim_in, *inp)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/linear.py", line 651, in bound_forward
    y.upper.transpose(-1, -2) if y.upper is not None else None
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/linear.py", line 509, in bound_forward
    lw, lb, uw, ub = BoundLinear.bound_forward_mul(x.lw, x_lb, x.uw, x_ub, w)
RuntimeError: The following operation failed in the TorchScript interpreter.
Traceback of TorchScript (most recent call last):
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/linear.py", line 457, in bound_forward_mul
    def bound_forward_mul(x_lw: Tensor, x_lb: Tensor, x_uw: Tensor, x_ub: Tensor, w: Tensor):
        w_pos, w_neg = w.clamp(min=0), w.clamp(max=0)
        lw = x_lw.matmul(w_pos) + x_uw.matmul(w_neg)
             ~~~~~~~~~~~ <--- HERE
        uw = x_uw.matmul(w_pos) + x_lw.matmul(w_neg)
        lb = x_lb.matmul(w_pos) + x_ub.matmul(w_neg)
RuntimeError: mat1 and mat2 shapes cannot be multiplied (19x1 and 19x32)

Randomness of visited subdomains

Hi,

I just noticed that when running on the same network and the same property, the visited subdomains could be different.

all nodes are split!!
9651 domains visited
Result: timeout
Time: 111.90976047515869
all nodes are split!!
9777 domains visited
Result: timeout
Time: 112.87935328483582
all nodes are split!!
9790 domains visited
Result: timeout
Time: 114.08122301101685

For example, I presented the printouts of 3 executions given the same config (I set the attack as skip, and the bab timeout as 360)
Even though all nodes are split, I wonder why different numbers of domains were visited for different execution.
What leads to this randomness of domains?
I would be grateful if you could share some insights.

Thanks and regards,
Yuyi

Help not displayed.

Describe the bug
Calling the main script to display help by

python abcrown.py --help

fails with

ValueError: unsupported format character ')' (0x29) at index 17

To Reproduce
Just use above command on current main.

System configuration:

  • OS: Ubuntu 20.04
  • Python version: 3.9
  • Pytorch Version: 1.12
  • Hardware: irrelevant
  • Have you tried to reproduce the problem in a cleanly created conda/virtualenv environment using official installation instructions and the latest code on the main branch?: Yes. Same error occurs.

Fix
The error seems to come from the use of "%" in a help message: l.291 in arguments.py

        self.add_argument('--mip_refine_timeout', type=float, default=0.8,
                          help='Percentage (x100%) of time used for improving all intermediate layer bounds using mip. Default to be 0.8*timeout.',
                          hierarchy=h + ["refine_neuron_time_percentage"])

Doubling % fixes the error (https://stackoverflow.com/questions/20480018/valueerror-unsupported-format-character)

CUDA out of memory

Hi, I am using alpha-beta-CROWN to certify a model, called CNN7, on CIFAR10 dataset. However, I met "CUDA out of memory error":

torch.cuda.OutOfMemoryError: CUDA out of memory. Tried to allocate 10.11 GiB (GPU 0; 23.65 GiB total capacity; 8.18 GiB already allocated; 8.91 GiB free; 13.24 GiB reserved in total by PyTorch) If reserved memory is >> allocated memory try setting max_split_size_mb to avoid fragmentation.  See documentation for Memory Management and PYTORCH_CUDA_ALLOC_CONF

As shown above, the memory of my GPU card is 24GB.

The structure of CNN7 is as follows:

Sequential(
  (0): Conv2d(3, 64, kernel_size=(3, 3), stride=(1, 1), padding=(1, 1))
  (1): ReLU()
  (2): Conv2d(64, 64, kernel_size=(3, 3), stride=(1, 1), padding=(1, 1))
  (3): ReLU()
  (4): Conv2d(64, 128, kernel_size=(3, 3), stride=(2, 2), padding=(1, 1))
  (5): ReLU()
  (6): Conv2d(128, 128, kernel_size=(3, 3), stride=(1, 1), padding=(1, 1))
  (7): ReLU()
  (8): Conv2d(128, 128, kernel_size=(3, 3), stride=(1, 1), padding=(1, 1))
  (9): ReLU()
  (10): Flatten(start_dim=1, end_dim=-1)
  (11): Linear(in_features=32768, out_features=512, bias=True)
  (12): ReLU()
  (13): Linear(in_features=512, out_features=10, bias=True)
)

I am considering if CNN7 model is too big to be certified by alpha-beta-CROWN.

So is there any way for me to certify CNN7 using alpha-beta-CROWN (without a GPU card with larger memory)?

Binary out.txt file

Describe the bug
The adverse example is output in a binary file out.txt. Is there a way to read it?

Additional context
This is not really a bug, but a usability issue.

Assertion error when bab-get_upper_bound argument is true

Hi,

When I tried to evaluate both the lower and upper bound of a NN by calling the bab() method in /complete_verifier/bab_verification_general.py, it has an assertion error in the compute_bounds() method in auto_LiRPA/bound_general.py.

It seems that we cannot have return_A == True when calling compute_bounds() since method == crown-optimized (was set here). However, it seems that in this build_the_model_with_refined_bounds() method, return_A is set to True if we want to get_upper_bound.

Thanks for helping.

Zhilu

PackagesNotFoundError when Creating Conda Environment for alpha-beta-CROWN

Dear alpha-beta-CROWN Team,

I hope this message finds you well. I've been working on running your latest version of Alpha-Beta-CROWN, but I've encountered a PackagesNotFoundError while executing the following command:

conda create -f complete_verifier/environment.yaml --name alpha-beta-crown

The following command will also show the same error:

conda create -f complete_verifier/environment_2022.yaml --name alpha-beta-crown
conda create -f complete_verifier/environment_pyt111.yaml --name alpha-beta-crown
conda create -f complete_verifier/environment_pyt200.yaml --name alpha-beta-crown
conda create -f complete_verifier/environment_pyt201.yaml --name alpha-beta-crown

The error message I received is as follows:

Collecting package metadata (current_repodata.json): done
Solving environment: failed with repodata from current_repodata.json, will retry with next repodata source.
Collecting package metadata (repodata.json): done
Solving environment: failed

PackagesNotFoundError: The following packages are not available from current channels:

  - complete_verifier/environment.yaml

Current channels:

  - https://repo.anaconda.com/pkgs/main/linux-64
  - https://repo.anaconda.com/pkgs/main/noarch
  - https://repo.anaconda.com/pkgs/r/linux-64
  - https://repo.anaconda.com/pkgs/r/noarch
  - https://conda.anaconda.org/conda-forge/linux-64
  - https://conda.anaconda.org/conda-forge/noarch

To search for alternate channels that may provide the conda package you're
looking for, navigate to

    https://anaconda.org

and use the search bar at the top of the page.

I would greatly appreciate your guidance and support to help me overcome this issue.

Thank you in advance for your help.

System configuration:

  • OS: 18.04.6 LTS
  • Have you tried to reproduce the problem in a cleanly created conda/virtualenv environment using official installation instructions and the latest code on the main branch?: Yes

AssertionError when run conv model with sigmoid function

Hello, I use your example file at 'exp_configs/cifar_conv_small_sigmoid.yaml' to run abcrown.py, then I got an assertion error:

File "/home/xue/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 760, in get_alpha_crown_start_nodes
assert not sparse_intermediate_bounds or use_sparse_conv is False # Double check our assumption holds. If this fails, then we created wrong shapes for alpha.
AssertionError

I wonder how to handle this?
Thank you.

RuntimeError onnx network when verifying, while network works at inference

Describe the bug
When verifying an onnx network with latest version of ab-crown we get an ONNXRuntime error, that does not exist when running inference with the model.
This is regarding a squeeze layer.
We have tried using the recommended version of onnx and onnxruntime, as well as the most recent versions available.

To Reproduce

  1. A minimum example is attached in "music_bugreport.zip
    music_bugreport.zip

  2. provided in zip

  3. complete output in txt file in zip.

  4. reproduce the problem by activating your environment and then running python alpha-beta-CROWN/complete_verifier/abcrown.py --config "vgg16.onnx/config_vgg16.onnx_image_instance0.npy.yaml"

Without the above information, you might not be able to receive timely help from us.

music_bugreport.zip

System configuration:

  • Python version: 3.1.13

Screenshots
If applicable, add screenshots to help explain your problem.

Additional context
Add any other context about the problem here.

Index error when running self-defined pytorch model

Hi,

I am running abcrown on a self-defined pytorch model, where I replaced the model_ori as the following model, where all L_i are nn.Linear layers.:

class SVDNetBig(nn.Module):
    def __init__(self, L1, L2, L3, L4, L5, L6, L7):
        super(SVDNetBig, self).__init__()
        self.flatten = nn.Flatten()
        self.L1 = L1
        self.L1R = nn.ReLU(inplace = True)
        self.L2 = L2
        self.L2R = nn.ReLU(inplace = True)
        self.L3 = L3
        self.L3R = nn.ReLU(inplace = True)
        self.L4 = L4
        self.L4R = nn.ReLU(inplace = True)
        self.L5 = L5
        self.L5R = nn.ReLU(inplace = True)
        self.L6 = L6
        self.L6R = nn.ReLU(inplace = True)
        self.L7 = L7

    def forward(self, x):
        out = torch.sub(x, torch.tensor([[[[0.1307000070810318]]]], device = x.device))
        out = torch.div(out, torch.tensor([[[[0.30810001492500305]]]], device = x.device))
        out = self.flatten(out)
        out = self.L1(out)
        out = self.L1R(out)
        out = self.L2(out)
        out = self.L2R(out)
        out = self.L3(out)
        out = self.L3R(out)
        out = self.L4(out)
        out = self.L4R(out)
        out = self.L5(out)
        out = self.L5R(out)
        out = self.L6(out)
        out = self.L6R(out)
        out = self.L7(out)
        return out

The generated BoundedModule is defined as follows:

BoundedModule(
  (/0): BoundInput(name="/0")
  (/1): BoundParams(name="/1")
  (/2): BoundParams(name="/2")
  (/3): BoundParams(name="/3")
  (/4): BoundParams(name="/4")
  (/5): BoundParams(name="/5")
  (/6): BoundParams(name="/6")
  (/7): BoundParams(name="/7")
  (/8): BoundParams(name="/8")
  (/9): BoundParams(name="/9")
  (/10): BoundParams(name="/10")
  (/11): BoundParams(name="/11")
  (/12): BoundParams(name="/12")
  (/13): BoundParams(name="/13")
  (/14): BoundParams(name="/14")
  (/15): BoundConstant(name="/15")
  (/16): BoundSub(name="/16")
  (/17): BoundConstant(name="/17")
  (/18): BoundDiv(name="/18")
  (/19): BoundFlatten(name="/19")
  (/input): BoundLinear(name="/input")
  (/21): BoundRelu(name="/21")
  (/input.3): BoundLinear(name="/input.3")
  (/23): BoundRelu(name="/23")
  (/input.7): BoundLinear(name="/input.7")
  (/25): BoundRelu(name="/25")
  (/input.11): BoundLinear(name="/input.11")
  (/27): BoundRelu(name="/27")
  (/input.15): BoundLinear(name="/input.15")
  (/29): BoundRelu(name="/29")
  (/input.19): BoundLinear(name="/input.19")
  (/31): BoundRelu(name="/31")
  (/32): BoundLinear(name="/32")
)

However, calling model.build_the_model() gives me IndexError:

  File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 156, in backward_general
    A, lower_b, upper_b = l.bound_backward(l.lA, l.uA, *l.inputs)
  File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/bivariate.py", line 562, in bound_backward
    uA_y = _bound_oneside(last_uA, y, sign=-1)
  File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/bivariate.py", line 550, in _bound_oneside
    return self.broadcast_backward(sign * last_A, w)
  File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/base.py", line 282, in broadcast_backward
    if shape[i] == 1 and A.shape[i + 1] != 1 and i != batch_dim:
IndexError: tuple index out of range
  File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 156, in backward_general
    A, lower_b, upper_b = l.bound_backward(l.lA, l.uA, *l.inputs)
  File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/bivariate.py", line 562, in bound_backward
    uA_y = _bound_oneside(last_uA, y, sign=-1)
  File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/bivariate.py", line 550, in _bound_oneside
    return self.broadcast_backward(sign * last_A, w)
  File "/home/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/base.py", line 282, in broadcast_backward
    if shape[i] == 1 and A.shape[i + 1] != 1 and i != batch_dim:
IndexError: tuple index out of range

Any insights on how to solve the issue? Thank you so much for your reply!

unsqueeze+conv2d error

Hi, I am trying to simulate the conv1d operation using unsqueeze+conv2d (as conv1d is not already supported), but I get this error that I cannot fix. When I remove the convolutional layer, I do not get the error, so the error should have something to do with conv2d. I'd appreciate your help.

The error:

Model prediction is: tensor([0.17936328], device='cuda:0')
initial forward+backward bounds (first 10): tensor([-0.18187992], device='cuda:0')
Traceback (most recent call last):
  File "abcrown.py", line 666, in <module>
    main()
  File "abcrown.py", line 589, in main
    refined_betas=refined_betas, attack_images=all_adv_candidates, attack_margins=attack_margins)
  File "abcrown.py", line 410, in complete_verifier
    rhs=rhs, timeout=timeout, attack_images=this_spec_attack_images)
  File "abcrown.py", line 200, in bab
    rhs=rhs, timeout=timeout, branching_method=arguments.Config["bab"]["branching"]["method"])
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/batch_branch_and_bound_input_split.py", line 297, in input_bab_parallel
    stop_func=stop_func,
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/batch_branch_and_bound_input_split.py", line 71, in batch_verification_input_split
    stop_criterion_func=stop_func(thresholds),
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1518, in get_lower_bound_naive
    bound_upper=False, return_A=True, needed_A_dict=needed_A_dict)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1328, in compute_bounds
    unstable_idx=alpha_idx, update_mask=update_mask)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 221, in backward_general
    lb = lb.view(batch_size, *output_shape) if bound_lower else None
RuntimeError: shape '[8192, 1]' is invalid for input of size 67108864

The model:

class MyModel(nn.ModuleList):
        def __init__(self, device=torch.device("cpu")):
            super(MyModel, self).__init__()        
            self.to(device)

            self.af = nn.ReLU()
            self.lin1 = nn.Linear(19, 32)
            self.lin2 = nn.Linear(32, 32)
            self.lin3 = nn.Linear(32, 15)

            self.conv2d = nn.Conv2d(
                in_channels=1, out_channels=1, kernel_size=(1, 15)
            )

        def forward(self, obs):
            lin1 = self.af(self.lin1(obs))
            lin2 = self.af(self.lin2(lin1))
            lin3 = self.lin3(lin2).unsqueeze(0).unsqueeze(0)
            conved = self.conv2d(lin3)

            return conved[0][0]

YAML file:

general:
  enable_incomplete_verification: False
  loss_reduction_func: max
  conv_mode: matrix
model:
  name: cmars
  input_shape: [1, 19]
specification:
  vnnlib_path: /home/mzi/sys-rl-verif/verif-slicing/cmars/vnnlib/large_1/N8/h32/basic-a1.vnnlib
attack:
  pgd_order: skip
solver:
  bound_prop_method: forward+backward
bab:
  method: sb
  input_split:
    enable: True
    adv_check: .inf
VNNLib property is as that in my previous question.

basic.vnnlib

(declare-const X_0 Real)
(declare-const X_1 Real)
(declare-const X_2 Real)
(declare-const X_3 Real)
(declare-const X_4 Real)
(declare-const X_5 Real)
(declare-const X_6 Real)
(declare-const X_7 Real)
(declare-const X_8 Real)
(declare-const X_9 Real)
(declare-const X_10 Real)
(declare-const X_11 Real)
(declare-const X_12 Real)
(declare-const X_13 Real)
(declare-const X_14 Real)
(declare-const X_15 Real)
(declare-const X_16 Real)
(declare-const X_17 Real)
(declare-const X_18 Real)

(declare-const Y_0 Real)

(assert (or 
	(and (<= X_0 0.11281310021877289) (>= X_0 0.08347102999687195) (<= X_1 -0.04856841638684273) (>= X_1 -0.07791049033403397) (<= X_2 -0.004555195104330778) (>= X_2 -0.033897269517183304) (<= X_3 0.06879998743534088) (>= X_3 0.03945791721343994) (<= X_4 0.1568262130022049) (>= X_4 0.12748414278030396) (<= X_5 0.2448524385690689) (>= X_5 0.21551036834716797) (<= X_6 0.2595234811306) (>= X_6 0.23018139600753784) (<= X_7 0.33287864923477173) (>= X_7 0.303536593914032) (<= X_8 0.42090487480163574) (>= X_8 0.391562819480896) (<= X_9 0.42090487480163574) (>= X_9 0.391562819480896) (<= X_10 0.391562819480896) (>= X_10 0.36222073435783386) (<= X_11 0.47958904504776) (>= X_11 0.4502469599246979) (<= X_12 0.6262993812561035) (>= X_12 0.5969573259353638) (<= X_13 0.6996545791625977) (>= X_13 0.6703125238418579) (<= X_14 0.7143256068229675) (>= X_14 0.6849835515022278) (<= X_15 0.6262993812561035) (>= X_15 0.5969573259353638) (<= X_16 0.5529442429542542) (>= X_16 0.5236021280288696) (<= X_17 0.4502469599246979) (>= X_17 0.42090487480163574) (<= X_18 0.4942600727081299) (>= X_18 0.46491798758506775) (>= Y_0 0))
))

assert not sparse_intermediate_bounds or use_sparse_conv is False

Firstly, thank you for your amazing work and for sharing it with us.

I try to use your framework to run robustness tests on a very simple convnet for classification task. The implementation is as following:

import pickle

def load_pickled_data(file, columns):
    """
    Loads pickled training and test data.
    
    Parameters
    ----------
    file    : 
              Name of the pickle file.
    columns : list of strings
              List of columns in pickled data we're interested in.

    Returns
    -------
    A tuple of datasets for given columns.    
    """

    with open(file, mode='rb') as f:
        dataset = pickle.load(f)
    return tuple(map(lambda c: dataset[c], columns))

import torch
import numpy as np
from typing import Tuple

class TSRDataset(torch.utils.data.Dataset):
    
    def __init__(self, pickled_X: np.array, pickled_y: np.array, transform=None) -> None:
        
        super(TSRDataset).__init__()
        self.X_ = pickled_X
        self.y_ = pickled_y
#     # 4. Make function to load images
#     def load_image(self, index: int) -> Image.Image:
#         "Opens an image via a path and returns it."
#         image_path = self.paths[index]
#         return Image.open(image_path) 
    
    def __len__(self) -> int:
        "Returns the total number of samples."
        return len(self.X_)
    
    # Overwrite the __getitem__() method (required for subclasses of torch.utils.data.Dataset)
    def __getitem__(self, index: int) -> Tuple[torch.Tensor, int]:
        "Returns one sample of data, data and label (X, y)."
        img = self.X_[index]
        class_idx = self.y_[index]
        
        return img, class_idx # return data, label (X, y)

import torch.nn as nn

class CNN(nn.Module):
    def __init__(self, params):
        super(CNN, self).__init__()
    
        self.conv1 = nn.Conv2d(in_channels=1, out_channels=params.conv1_d, kernel_size=params.conv1_k, stride=1, padding=self.get_pad(params.conv1_k, 1))
        self.conv2 = nn.Conv2d(in_channels=params.conv1_d, out_channels=params.conv2_d, kernel_size=params.conv2_k, stride=1, padding=self.get_pad(params.conv2_k, 1))
        self.conv3 = nn.Conv2d(in_channels=params.conv2_d, out_channels=params.conv3_d, kernel_size=params.conv3_k, stride=1, padding=self.get_pad(params.conv3_k, 1))
        self.fc4 = nn.Linear(in_features=3584, out_features=params.fc4_size)
        self.out = nn.Linear(in_features=params.fc4_size, out_features=params.num_classes)
        self.params = params
    
    def get_pad(self, ksize, stride):
    
        in_height = in_width = 32
        stride_height = stride_width = stride
        strides = [stride_height, stride_width]
        filter_height = filter_width = ksize                 

        if (in_height % strides[0] == 0):
            pad_along_height = max(filter_height - stride_height, 0)
        else:
            pad_along_height = max(filter_height - (in_height % stride_height), 0)
        if (in_width % strides[1] == 0):
            pad_along_width = max(filter_width - stride_width, 0)
        else:
            pad_along_width = max(filter_width - (in_width % stride_width), 0)

        pad_top = pad_along_height // 2
        pad_bottom = pad_along_height - pad_top
        pad_left = pad_along_width // 2
        pad_right = pad_along_width - pad_left
        
        return [pad_left, pad_right]
    
    def forward(self, x, is_training=True):
        # Convolutions
        x = self.conv1(x)
        x = nn.functional.relu(x)
        x = nn.functional.max_pool2d(x, kernel_size=2, stride=2, padding=self.get_pad(2,2))
#         x = nn.functional.dropout(x, p=self.params.conv1_p, training=is_training)
        x1 = x.clone()
        x = self.conv2(x)
        x = nn.functional.relu(x)
        x = nn.functional.max_pool2d(x, kernel_size=2, stride=2, padding=self.get_pad(2,2))
#         x = nn.functional.dropout(x, p=self.params.conv2_p, training=is_training)
        x2 = x.clone()
        x = self.conv3(x)
        x = nn.functional.relu(x)
        x = nn.functional.max_pool2d(x, kernel_size=2, stride=2, padding=self.get_pad(2,2))
#         x = nn.functional.dropout(x, p=self.params.conv3_p, training=is_training)
        x3 = x.clone()

        # Fully connected
        x1 = nn.functional.max_pool2d(x1, kernel_size=4, stride=4, padding=self.get_pad(4,4))
        x1 = torch.flatten(x1, 1, -1)
        x2 = nn.functional.max_pool2d(x2, kernel_size=2, stride=2, padding=self.get_pad(2,2))
        x2 = torch.flatten(x2, 1, -1)
        x3 = torch.flatten(x3, 1, -1)
        x = torch.cat((x1, x2, x3), dim=-1)
        x = self.fc4(x)
        x = nn.functional.relu(x)
#         x = nn.functional.dropout(x, p=self.params.fc4_p, training=is_training)
        x = self.out(x)
        return x
 
 
def get_model():
    from collections import namedtuple

    Parameters = namedtuple('Parameters', [
            # Data parameters
            'num_classes', 'image_size', 
            # Training parameters
            'batch_size', 'max_epochs', 'log_epoch', 'print_epoch',
            # Optimisations
            'learning_rate_decay', 'learning_rate',
            'l2_reg_enabled', 'l2_lambda', 
            'early_stopping_enabled', 'early_stopping_patience', 
            'resume_training', 
            # Layers architecture
            'conv1_k', 'conv1_d', 'conv1_p', 
            'conv2_k', 'conv2_d', 'conv2_p', 
            'conv3_k', 'conv3_d', 'conv3_p', 
            'fc4_size', 'fc4_p'
        ])

    parameters = Parameters(
        # Data parameters
        num_classes = 43,
        image_size = (32, 32),
        # Training parameters
        batch_size = 256,
        max_epochs = 30,
        log_epoch = 1,
        print_epoch = 1,
        # Optimisations
        learning_rate_decay = True,
        learning_rate = 0.001,
        l2_reg_enabled = False,
        l2_lambda = 0.0001,
        early_stopping_enabled = True,
        early_stopping_patience = 25,
        resume_training = False,
        # Layers architecture
        conv1_k = 5, conv1_d = 32, conv1_p = 0.9,
        conv2_k = 5, conv2_d = 64, conv2_p = 0.8,
        conv3_k = 5, conv3_d = 128, conv3_p = 0.7,
        fc4_size = 1024, fc4_p = 0.5
    )
     
    return CNN(parameters)
        
    
def tsr_data(eps):
    """Example dataloader. For MNIST and CIFAR you can actually use existing ones in utils.py."""
    assert eps is not None
    data_path = '/kaggle/input/reqnew/train_extended_preprocessed.p'
    X_test, y_test = load_pickled_data(data_path, columns = ['features', 'labels'])
    # You can access the mean and std stored in config file.
    mean = torch.tensor(np.mean(X_test, axis=(0,1,2)))
    std = torch.tensor(np.std(X_test, axis=(0,1,2)))
#     normalize = transforms.Normalize(mean=mean, std=std)
    test_data = TSRDataset(X_test, y_test, transform=None)
    # Load entire dataset.
    testloader = torch.utils.data.DataLoader(test_data,\
            batch_size=10000, shuffle=False, num_workers=0)
    X, labels = next(iter(testloader))
    
    # Set data_max and data_min to be None if no clip. For CIFAR-10 we clip to [0,1].
    data_max = torch.reshape((1. - mean) / std, (1, -1, 1, 1))
    data_min = torch.reshape((0. - mean) / std, (1, -1, 1, 1))
    if eps is None:
        raise ValueError('You must specify an epsilon')
    # Rescale epsilon.
    ret_eps = torch.reshape(eps / std, (1, -1, 1, 1))
    return torch.tensor(X).permute((0,3,1,2)), torch.argmax(torch.tensor(labels), dim=-1), data_max, data_min, ret_eps

My loaded data is actually an np array of shape [N, H, W, C] where C is 1 since it is in grayscale. The labels are classes that range from 0 to 42.

When I run alpha-beta-CROWN with the attached configuration, I got the following output:


/kaggle/working
Configurations:

general:
  device: cuda
  seed: 100
  conv_mode: patches
  deterministic: false
  double_fp: false
  loss_reduction_func: sum
  record_bounds: false
  sparse_alpha: true
  save_adv_example: false
  precompile_jit: false
  complete_verifier: bab
  enable_incomplete_verification: true
  csv_name: null
  results_file: out.txt
  root_path: ''
model:
  name: 'Customized("custom_model_data", "get_model")'
  path: /kaggle/working/model_torch.pt
  onnx_path: null
  onnx_path_prefix: ''
  cache_onnx_conversion: false
  onnx_quirks: null
  input_shape: null
  onnx_loader: default_onnx_and_vnnlib_loader
  onnx_optimization_flags: none
data:
  start: 0
  end: 10
  select_instance: null
  num_outputs: 43
  mean: 0.0
  std: 1.0
  pkl_path: null
  dataset: 'Customized("custom_model_data", "tsr_data")'
  data_filter_path: null
  data_idx_file: null
specification:
  type: lp
  robustness_type: verified-acc
  norm: .inf
  epsilon: 0.00784313725
  vnnlib_path: null
  vnnlib_path_prefix: ''
solver:
  batch_size: 256
  min_batch_size_ratio: 0.1
  use_float64_in_last_iteration: false
  early_stop_patience: 10
  start_save_best: 0.5
  bound_prop_method: alpha-crown
  prune_after_crown: false
  crown:
    batch_size: 1000000000
    max_crown_size: 1000000000
  alpha-crown:
    alpha: true
    lr_alpha: 0.1
    iteration: 100
    share_slopes: false
    no_joint_opt: false
    lr_decay: 0.98
    full_conv_alpha: true
  beta-crown:
    lr_alpha: 0.01
    lr_beta: 0.05
    lr_decay: 0.98
    optimizer: adam
    iteration: 20
    beta: true
    beta_warmup: true
    enable_opt_interm_bounds: false
    all_node_split_LP: false
  forward:
    refine: false
    dynamic: false
    max_dim: 10000
  multi_class:
    multi_class_method: allclass_domain
    label_batch_size: 32
    skip_with_refined_bound: true
  mip:
    parallel_solvers: null
    solver_threads: 1
    refine_neuron_timeout: 15
    refine_neuron_time_percentage: 0.8
    early_stop: true
    adv_warmup: true
    mip_solver: gurobi
bab:
  initial_max_domains: 1
  max_domains: .inf
  decision_thresh: 0
  timeout: 300
  timeout_scale: 1
  override_timeout: null
  get_upper_bound: false
  dfs_percent: 0.0
  pruning_in_iteration: true
  pruning_in_iteration_ratio: 0.2
  sort_targets: false
  batched_domain_list: true
  optimized_intermediate_layers: ''
  interm_transfer: true
  cut:
    enabled: false
    bab_cut: false
    lp_cut: false
    method: null
    lr: 0.01
    lr_decay: 1.0
    iteration: 100
    bab_iteration: -1
    early_stop_patience: -1
    lr_beta: 0.02
    number_cuts: 50
    topk_cuts_in_filter: 100
    batch_size_primal: 100
    max_num: 1000000000
    patches_cut: false
    cplex_cuts: false
    cplex_cuts_wait: 0
    cplex_cuts_revpickup: true
    cut_reference_bounds: true
    fix_intermediate_bounds: false
  branching:
    method: kfsb
    candidates: 3
    reduceop: min
    sb_coeff_thresh: 0.001
    input_split:
      enable: false
      enhanced_bound_prop_method: alpha-crown
      enhanced_branching_method: naive
      enhanced_bound_patience: 100000000.0
      attack_patience: 100000000.0
      adv_check: 0
      sort_domain_interval: -1
  attack:
    enabled: false
    beam_candidates: 8
    beam_depth: 7
    max_dive_fix_ratio: 0.8
    min_local_free_ratio: 0.2
    mip_start_iteration: 5
    mip_timeout: 30.0
    adv_pool_threshold: null
    refined_mip_attacker: false
    refined_batch_size: null
attack:
  pgd_order: before
  pgd_steps: 100
  pgd_restarts: 100
  pgd_early_stop: true
  pgd_lr_decay: 0.99
  pgd_alpha: auto
  pgd_loss_mode: null
  enable_mip_attack: false
  cex_path: ./test_cex.txt
  attack_mode: PGD
  gama_lambda: 10.0
  gama_decay: 0.9
  check_clean: false
  input_split:
    pgd_steps: 100
    pgd_restarts: 30
    pgd_alpha: auto
  input_split_enhanced:
    pgd_steps: 200
    pgd_restarts: 5000000
    pgd_alpha: auto
  input_split_check_adv:
    pgd_steps: 5
    pgd_restarts: 5
    pgd_alpha: auto
debug:
  lp_test: null

Experiments at Fri May  5 09:26:50 2023 on b2ccc2a2c33d
CNN(
  (conv1): Conv2d(1, 32, kernel_size=(5, 5), stride=(1, 1), padding=(2, 2))
  (conv2): Conv2d(32, 64, kernel_size=(5, 5), stride=(1, 1), padding=(2, 2))
  (conv3): Conv2d(64, 128, kernel_size=(5, 5), stride=(1, 1), padding=(2, 2))
  (fc4): Linear(in_features=3584, out_features=1024, bias=True)
  (out): Linear(in_features=1024, out_features=43, bias=True)
)
/kaggle/working/alpha-beta-CROWN/complete_verifier/custom_model_data.py:211: UserWarning: To copy construct from a tensor, it is recommended to use sourceTensor.clone().detach() or sourceTensor.clone().detach().requires_grad_(True), rather than torch.tensor(sourceTensor).
  return torch.tensor(X).permute((0,3,1,2)), torch.argmax(torch.tensor(labels), dim=-1), data_max, data_min, ret_eps
Internal results will be saved to Verified_ret_[Customized_model]_start=0_end=10_iter=20_b=256_timeout=300_branching=kfsb-min-3_lra-init=0.1_lra=0.01_lrb=0.05_PGD=before_cplex_cuts=False_multiclass=allclass_domain.npy.

 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 0, vnnlib ID: 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Attack parameters: initialization=uniform, steps=100, restarts=100, alpha=0.007461458444595337, initialization=uniform, GAMA=False
Model output of first 5 examples:
 tensor([[-26.63533783,  -5.86781883,  -4.54763603, -21.69909477, -20.81317139,
          -0.61611140, -16.72828102, -13.13037777, -18.94099617, -26.45909882,
          -4.61056852, -12.54259109,  -0.75518376, -16.09009552,  -2.99634385,
         -11.60897160, -17.43187332,  -9.52975750, -18.21758842, -29.91522217,
         -33.70221329, -23.20652962, -18.36230087, -25.41592407, -33.91773987,
         -21.16673660, -17.64099312, -39.80070496, -35.47123337, -31.05479431,
         -22.17935181, -18.36315536, -43.14264679, -13.38010883,  12.96510029,
         -20.21791458,  -4.28863621,  -6.38604784,  41.21236038,  -6.59563351,
           4.28117037, -27.70765305,  -9.50008297]], device='cuda:0')
Adv example prediction (first 2 examples and 2 restarts):
 tensor([[[-26.52582550,  -3.93510056,  -6.41698170, -20.35298538, -20.99528694,
           -6.70625925, -16.09720039, -15.72246552, -17.80824852, -23.99833107,
          -11.98600864, -10.19097519,   2.43953228,  -9.03533268,  -2.28550172,
           -9.02405930, -19.05975914,  -7.56664610, -19.64624596, -25.21205711,
          -34.47130585, -25.68278313, -19.72745895, -25.75965881, -34.31901932,
          -21.08712769, -16.40643311, -36.51839066, -30.18853760, -27.88558769,
          -23.38009453, -19.63435936, -35.52644348, -10.87827301,  20.88450241,
           -9.49922180,  -2.24221802,   1.64629138,  29.64516830,  -7.80061817,
            5.89254475, -24.37758255, -11.45957851],
         [-26.52582741,  -3.93510199,  -6.41698503, -20.35298538, -20.99528885,
           -6.70626211, -16.09720039, -15.72246647, -17.80824661, -23.99833107,
          -11.98601246, -10.19097233,   2.43953443,  -9.03533077,  -2.28550124,
           -9.02405930, -19.05976105,  -7.56664419, -19.64624596, -25.21205330,
          -34.47130585, -25.68278503, -19.72745895, -25.75965881, -34.31901550,
          -21.08712578, -16.40643501, -36.51838684, -30.18853188, -27.88558388,
          -23.38009453, -19.63436317, -35.52643967, -10.87827301,  20.88450432,
           -9.49921989,  -2.24221563,   1.64629233,  29.64516640,  -7.80062008,
            5.89254475, -24.37757874, -11.45957756]]], device='cuda:0')
PGD attack margin (first 2 examles and 10 specs):
 tensor([[[56.17099380, 33.58026886, 36.06214905, 49.99815369, 50.64045715,
          36.35142899, 45.74237061, 45.36763382, 47.45341492, 53.64349747]]],
       device='cuda:0')
number of violation:  0
Attack finished in 16.8530 seconds.
PGD attack failed
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/parse_graph.py:147: FutureWarning: 'torch.onnx.symbolic_helper._set_opset_version' is deprecated in version 1.13 and will be removed in version 1.14. Please remove its usage and avoid setting internal variables directly.
  _set_opset_version(12)
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/parse_graph.py:45: FutureWarning: 'torch.onnx._patch_torch._node_getitem' is deprecated in version 1.13 and will be removed in version 1.14. Please Internally use '_node_get' in symbolic_helper instead..
  attrs = {k: n[k] for k in n.attributeNames()}
Model prediction is: tensor([[-26.63533783,  -5.86781883,  -4.54763603, -21.69909477, -20.81317139,
          -0.61611140, -16.72828102, -13.13037777, -18.94099617, -26.45909882,
          -4.61056852, -12.54259109,  -0.75518376, -16.09009552,  -2.99634385,
         -11.60897160, -17.43187332,  -9.52975750, -18.21758842, -29.91522217,
         -33.70221329, -23.20652962, -18.36230087, -25.41592407, -33.91773987,
         -21.16673660, -17.64099312, -39.80070496, -35.47123337, -31.05479431,
         -22.17935181, -18.36315536, -43.14264679, -13.38010883,  12.96510029,
         -20.21791458,  -4.28863621,  -6.38604784,  41.21236038,  -6.59563351,
           4.28117037, -27.70765305,  -9.50008297]], device='cuda:0')
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/bound_general.py:946: UserWarning: Creating an identity matrix with size 8192x8192 for node BoundMaxPool(name="/input"). This may indicate poor performance for bound computation. If you see this message on a small network please submit a bug report.
  ref_intermediate_lb, ref_intermediate_ub)
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/bound_general.py:946: UserWarning: Creating an identity matrix with size 4096x4096 for node BoundMaxPool(name="/input.4"). This may indicate poor performance for bound computation. If you see this message on a small network please submit a bug report.
  ref_intermediate_lb, ref_intermediate_ub)
layer /12 using sparse-features alpha with shape [11222]; unstable size 11222; total size 32768 (torch.Size([1, 32, 32, 32]))
layer /12 start_node /input using full alpha with unstable size None total_size 8192 output_shape torch.Size([32, 16, 16])
layer /12 start_node /x.3 using full alpha with unstable size 64 total_size 64 output_shape 64
layer /12 start_node /input.4 using full alpha with unstable size None total_size 4096 output_shape torch.Size([64, 8, 8])
layer /12 start_node /x.7 using full alpha with unstable size 128 total_size 128 output_shape 128
layer /12 start_node /x.11 using full alpha with unstable size 1024 total_size 1024 output_shape torch.Size([1024])
layer /12 start_node /28 using full alpha with unstable size None total_size 42 output_shape 42
Traceback (most recent call last):
  File "/kaggle/working/alpha-beta-CROWN/complete_verifier/abcrown.py", line 647, in <module>
    main()
  File "/kaggle/working/alpha-beta-CROWN/complete_verifier/abcrown.py", line 535, in main
    incomplete_verifier(model_ori, x, data_ub=data_max, data_lb=data_min, vnnlib=vnnlib)
  File "/kaggle/working/alpha-beta-CROWN/complete_verifier/abcrown.py", line 69, in incomplete_verifier
    domain, x, data_lb, data_ub, vnnlib, stop_criterion_func=stop_criterion_min(arguments.Config["bab"]["decision_thresh"]))
  File "/kaggle/working/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1069, in build_the_model
    (self.x,), share_slopes=share_slopes, c=self.c, bound_upper=False)
  File "/kaggle/working/alpha-beta-CROWN/auto_LiRPA/optimized_bounds.py", line 1050, in init_slope
    final_node_name=final_node_name)
  File "/kaggle/working/alpha-beta-CROWN/auto_LiRPA/backward_bound.py", line 760, in get_alpha_crown_start_nodes
    assert not sparse_intermediate_bounds or use_sparse_conv is False  # Double check our assumption holds. If this fails, then we created wrong shapes for alpha.
AssertionError

To solve this issue, I tried to change full_conv_alpha, conv_mode, or share_alpha parameters but I got another error with those:

/kaggle/working
/opt/conda/lib/python3.7/site-packages/onnx/mapping.py:27: DeprecationWarning: `np.object` is a deprecated alias for the builtin `object`. To silence this warning, use `object` by itself. Doing this will not modify any behavior and is safe. 
Deprecated in NumPy 1.20; for more details and guidance: https://numpy.org/devdocs/release/1.20.0-notes.html#deprecations
  int(TensorProto.STRING): np.dtype(np.object)
Configurations:

general:
  device: cuda
  seed: 100
  conv_mode: matrix
  deterministic: false
  double_fp: false
  loss_reduction_func: sum
  record_bounds: false
  sparse_alpha: false
  save_adv_example: false
  precompile_jit: false
  complete_verifier: bab
  enable_incomplete_verification: true
  csv_name: null
  results_file: out.txt
  root_path: ''
model:
  name: 'Customized("custom_model_data", "get_model")'
  path: /kaggle/working/model_torch.pt
  onnx_path: null
  onnx_path_prefix: ''
  cache_onnx_conversion: false
  onnx_quirks: null
  input_shape: null
  onnx_loader: default_onnx_and_vnnlib_loader
  onnx_optimization_flags: none
data:
  start: 0
  end: 10
  select_instance: null
  num_outputs: 43
  mean: 0.0
  std: 1.0
  pkl_path: null
  dataset: 'Customized("custom_model_data", "tsr_data")'
  data_filter_path: null
  data_idx_file: null
specification:
  type: lp
  robustness_type: verified-acc
  norm: .inf
  epsilon: 0.00784313725
  vnnlib_path: null
  vnnlib_path_prefix: ''
solver:
  batch_size: 256
  min_batch_size_ratio: 0.1
  use_float64_in_last_iteration: false
  early_stop_patience: 10
  start_save_best: 0.5
  bound_prop_method: alpha-crown
  prune_after_crown: false
  crown:
    batch_size: 1000000000
    max_crown_size: 1000000000
  alpha-crown:
    alpha: true
    lr_alpha: 0.1
    iteration: 100
    share_slopes: false
    no_joint_opt: false
    lr_decay: 0.98
    full_conv_alpha: false
  beta-crown:
    lr_alpha: 0.01
    lr_beta: 0.05
    lr_decay: 0.98
    optimizer: adam
    iteration: 20
    beta: true
    beta_warmup: true
    enable_opt_interm_bounds: false
    all_node_split_LP: false
  forward:
    refine: false
    dynamic: false
    max_dim: 10000
  multi_class:
    multi_class_method: allclass_domain
    label_batch_size: 32
    skip_with_refined_bound: true
  mip:
    parallel_solvers: null
    solver_threads: 1
    refine_neuron_timeout: 15
    refine_neuron_time_percentage: 0.8
    early_stop: true
    adv_warmup: true
    mip_solver: gurobi
bab:
  initial_max_domains: 1
  max_domains: .inf
  decision_thresh: 0
  timeout: 300
  timeout_scale: 1
  override_timeout: null
  get_upper_bound: false
  dfs_percent: 0.0
  pruning_in_iteration: true
  pruning_in_iteration_ratio: 0.2
  sort_targets: false
  batched_domain_list: true
  optimized_intermediate_layers: ''
  interm_transfer: true
  cut:
    enabled: false
    bab_cut: false
    lp_cut: false
    method: null
    lr: 0.01
    lr_decay: 1.0
    iteration: 100
    bab_iteration: -1
    early_stop_patience: -1
    lr_beta: 0.02
    number_cuts: 50
    topk_cuts_in_filter: 100
    batch_size_primal: 100
    max_num: 1000000000
    patches_cut: false
    cplex_cuts: false
    cplex_cuts_wait: 0
    cplex_cuts_revpickup: true
    cut_reference_bounds: true
    fix_intermediate_bounds: false
  branching:
    method: kfsb
    candidates: 3
    reduceop: min
    sb_coeff_thresh: 0.001
    input_split:
      enable: false
      enhanced_bound_prop_method: alpha-crown
      enhanced_branching_method: naive
      enhanced_bound_patience: 100000000.0
      attack_patience: 100000000.0
      adv_check: 0
      sort_domain_interval: -1
  attack:
    enabled: false
    beam_candidates: 8
    beam_depth: 7
    max_dive_fix_ratio: 0.8
    min_local_free_ratio: 0.2
    mip_start_iteration: 5
    mip_timeout: 30.0
    adv_pool_threshold: null
    refined_mip_attacker: false
    refined_batch_size: null
attack:
  pgd_order: before
  pgd_steps: 100
  pgd_restarts: 100
  pgd_early_stop: true
  pgd_lr_decay: 0.99
  pgd_alpha: auto
  pgd_loss_mode: null
  enable_mip_attack: false
  cex_path: ./test_cex.txt
  attack_mode: PGD
  gama_lambda: 10.0
  gama_decay: 0.9
  check_clean: false
  input_split:
    pgd_steps: 100
    pgd_restarts: 30
    pgd_alpha: auto
  input_split_enhanced:
    pgd_steps: 200
    pgd_restarts: 5000000
    pgd_alpha: auto
  input_split_check_adv:
    pgd_steps: 5
    pgd_restarts: 5
    pgd_alpha: auto
debug:
  lp_test: null

Experiments at Mon May  1 17:49:40 2023 on d2707ae0421e
CNN(
  (conv1): Conv2d(1, 32, kernel_size=(5, 5), stride=(1, 1), padding=(2, 2))
  (conv2): Conv2d(32, 64, kernel_size=(5, 5), stride=(1, 1), padding=(2, 2))
  (conv3): Conv2d(64, 128, kernel_size=(5, 5), stride=(1, 1), padding=(2, 2))
  (fc4): Linear(in_features=3584, out_features=1024, bias=True)
  (out): Linear(in_features=1024, out_features=43, bias=True)
)
/kaggle/working/alpha-beta-CROWN/complete_verifier/custom_model_data.py:211: UserWarning: To copy construct from a tensor, it is recommended to use sourceTensor.clone().detach() or sourceTensor.clone().detach().requires_grad_(True), rather than torch.tensor(sourceTensor).
  return torch.tensor(X).permute((0,3,1,2)), torch.argmax(torch.tensor(labels), dim=-1), data_max, data_min, ret_eps
Internal results will be saved to Verified_ret_[Customized_model]_start=0_end=10_iter=20_b=256_timeout=300_branching=kfsb-min-3_lra-init=0.1_lra=0.01_lrb=0.05_PGD=before_cplex_cuts=False_multiclass=allclass_domain.npy.

 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 0, vnnlib ID: 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Attack parameters: initialization=uniform, steps=100, restarts=100, alpha=0.007461458444595337, initialization=uniform, GAMA=False
Model output of first 5 examples:
 tensor([[-26.63533783,  -5.86781883,  -4.54763603, -21.69909477, -20.81317139,
          -0.61611140, -16.72828102, -13.13037777, -18.94099617, -26.45909882,
          -4.61056852, -12.54259109,  -0.75518376, -16.09009552,  -2.99634385,
         -11.60897160, -17.43187332,  -9.52975750, -18.21758842, -29.91522217,
         -33.70221329, -23.20652962, -18.36230087, -25.41592407, -33.91773987,
         -21.16673660, -17.64099312, -39.80070496, -35.47123337, -31.05479431,
         -22.17935181, -18.36315536, -43.14264679, -13.38010883,  12.96510029,
         -20.21791458,  -4.28863621,  -6.38604784,  41.21236038,  -6.59563351,
           4.28117037, -27.70765305,  -9.50008297]], device='cuda:0')
Adv example prediction (first 2 examples and 2 restarts):
 tensor([[[-26.52582550,  -3.93510056,  -6.41698170, -20.35298538, -20.99528694,
           -6.70625925, -16.09720039, -15.72246552, -17.80824852, -23.99833107,
          -11.98600864, -10.19097519,   2.43953228,  -9.03533268,  -2.28550172,
           -9.02405930, -19.05975914,  -7.56664610, -19.64624596, -25.21205711,
          -34.47130585, -25.68278313, -19.72745895, -25.75965881, -34.31901932,
          -21.08712769, -16.40643311, -36.51839066, -30.18853760, -27.88558769,
          -23.38009453, -19.63435936, -35.52644348, -10.87827301,  20.88450241,
           -9.49922180,  -2.24221802,   1.64629138,  29.64516830,  -7.80061817,
            5.89254475, -24.37758255, -11.45957851],
         [-26.52582741,  -3.93510199,  -6.41698503, -20.35298538, -20.99528885,
           -6.70626211, -16.09720039, -15.72246647, -17.80824661, -23.99833107,
          -11.98601246, -10.19097233,   2.43953443,  -9.03533077,  -2.28550124,
           -9.02405930, -19.05976105,  -7.56664419, -19.64624596, -25.21205330,
          -34.47130585, -25.68278503, -19.72745895, -25.75965881, -34.31901550,
          -21.08712578, -16.40643501, -36.51838684, -30.18853188, -27.88558388,
          -23.38009453, -19.63436317, -35.52643967, -10.87827301,  20.88450432,
           -9.49921989,  -2.24221563,   1.64629233,  29.64516640,  -7.80062008,
            5.89254475, -24.37757874, -11.45957756]]], device='cuda:0')
PGD attack margin (first 2 examles and 10 specs):
 tensor([[[56.17099380, 33.58026886, 36.06214905, 49.99815369, 50.64045715,
          36.35142899, 45.74237061, 45.36763382, 47.45341492, 53.64349747]]],
       device='cuda:0')
number of violation:  0
Attack finished in 13.5393 seconds.
PGD attack failed
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/parse_graph.py:147: FutureWarning: 'torch.onnx.symbolic_helper._set_opset_version' is deprecated in version 1.13 and will be removed in version 1.14. Please remove its usage and avoid setting internal variables directly.
  _set_opset_version(12)
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/parse_graph.py:45: FutureWarning: 'torch.onnx._patch_torch._node_getitem' is deprecated in version 1.13 and will be removed in version 1.14. Please Internally use '_node_get' in symbolic_helper instead..
  attrs = {k: n[k] for k in n.attributeNames()}
Model prediction is: tensor([[-26.63533783,  -5.86781883,  -4.54763603, -21.69909477, -20.81317139,
          -0.61611140, -16.72828102, -13.13037777, -18.94099617, -26.45909882,
          -4.61056852, -12.54259109,  -0.75518376, -16.09009552,  -2.99634385,
         -11.60897160, -17.43187332,  -9.52975750, -18.21758842, -29.91522217,
         -33.70221329, -23.20652962, -18.36230087, -25.41592407, -33.91773987,
         -21.16673660, -17.64099312, -39.80070496, -35.47123337, -31.05479431,
         -22.17935181, -18.36315536, -43.14264679, -13.38010883,  12.96510029,
         -20.21791458,  -4.28863621,  -6.38604784,  41.21236038,  -6.59563351,
           4.28117037, -27.70765305,  -9.50008297]], device='cuda:0')
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/bound_general.py:946: UserWarning: Creating an identity matrix with size 8192x8192 for node BoundMaxPool(name="/input"). This may indicate poor performance for bound computation. If you see this message on a small network please submit a bug report.
  ref_intermediate_lb, ref_intermediate_ub)
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/bound_general.py:946: UserWarning: Creating an identity matrix with size 16384x16384 for node BoundConv(name="/x.3"). This may indicate poor performance for bound computation. If you see this message on a small network please submit a bug report.
  ref_intermediate_lb, ref_intermediate_ub)
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/bound_general.py:946: UserWarning: Creating an identity matrix with size 4096x4096 for node BoundMaxPool(name="/input.4"). This may indicate poor performance for bound computation. If you see this message on a small network please submit a bug report.
  ref_intermediate_lb, ref_intermediate_ub)
/kaggle/working/alpha-beta-CROWN/auto_LiRPA/bound_general.py:946: UserWarning: Creating an identity matrix with size 8192x8192 for node BoundConv(name="/x.7"). This may indicate poor performance for bound computation. If you see this message on a small network please submit a bug report.
  ref_intermediate_lb, ref_intermediate_ub)
layer /12 start_node /input using full alpha with unstable size None total_size 8192 output_shape torch.Size([32, 16, 16])
layer /12 start_node /x.3 using full alpha with unstable size None total_size 16384 output_shape torch.Size([64, 16, 16])
layer /12 start_node /input.4 using full alpha with unstable size None total_size 4096 output_shape torch.Size([64, 8, 8])
layer /12 start_node /x.7 using full alpha with unstable size None total_size 8192 output_shape torch.Size([128, 8, 8])
layer /12 start_node /x.11 using full alpha with unstable size 1024 total_size 1024 output_shape torch.Size([1024])
layer /12 start_node /28 using full alpha with unstable size None total_size 42 output_shape 42
Traceback (most recent call last):
  File "/kaggle/working/alpha-beta-CROWN/complete_verifier/abcrown.py", line 647, in <module>
    main()
  File "/kaggle/working/alpha-beta-CROWN/complete_verifier/abcrown.py", line 535, in main
    incomplete_verifier(model_ori, x, data_ub=data_max, data_lb=data_min, vnnlib=vnnlib)
  File "/kaggle/working/alpha-beta-CROWN/complete_verifier/abcrown.py", line 69, in incomplete_verifier
    domain, x, data_lb, data_ub, vnnlib, stop_criterion_func=stop_criterion_min(arguments.Config["bab"]["decision_thresh"]))
  File "/kaggle/working/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1069, in build_the_model
    (self.x,), share_slopes=share_slopes, c=self.c, bound_upper=False)
  File "/kaggle/working/alpha-beta-CROWN/auto_LiRPA/optimized_bounds.py", line 1054, in init_slope
    node.init_opt_parameters(start_nodes)
  File "/kaggle/working/alpha-beta-CROWN/auto_LiRPA/operators/pooling.py", line 54, in init_opt_parameters
    dtype=torch.float, device=ref.device, requires_grad=True)
TypeError: empty(): argument 'size' must be tuple of SymInts, but found element of type torch.Size at pos 2

I could not solve the problem and I guess the second one is not the way to go. I am in need of your help.
Sorry for the long text. Thanks in advance

env.txt

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.