Verified-Intelligence / alpha-beta-CROWN

alpha-beta-CROWN: An Efficient, Scalable and GPU Accelerated Neural Network Verifier (winner of VNN-COMP 2021, 2022, 2023, and 2024)
Other
243 stars 60 forks source link

assert not sparse_intermediate_bounds or use_sparse_conv is False #28

Closed yusiyoh closed 11 months ago

yusiyoh commented 1 year ago

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

yusiyoh commented 1 year ago

Would be great to have an opinion on this..

Thanks again

shizhouxing commented 1 year ago

Hi @yusiyoh , this issue should have been fixed in our internal development version which will be released soon.