Use norms other then linf

AWbosman commented 1 year ago

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:

python alpha-beta-CROWN/complete_verifier/abcrown.py --config "./config_ffnnRELU__Point_6_500.onnx_image_1.yaml"
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 ./ffnnRELUPoint_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 ./ffnnRELUPoint_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'

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

huanzhang12 commented 1 year ago

Thanks for reporting the problem to us. Currently, the support of other norms is still incomplete and it works only for simple cases. I will take a look at your example to see how to fix it.

fabiobrau commented 10 months ago

Hi everyone,

any update about l2 norm? I tried the following configuration

# This is an example configuration file that contains most useful parameter settings.
model:
  name: resnet2b  # This model is defined in model_defs.py. Add your own model definitions there.
  path: models/cifar10_resnet/resnet2b.pth  # Path to PyTorch checkpoint.
data:
  dataset: CIFAR  # Dataset name. This is just the standard CIFAR-10 test set defined in the "load_verification_dataset()" function in utils.py
  #mean: [0.4914, 0.4822, 0.4465]  # Mean for normalization.
  #std: [0.2471, 0.2435, 0.2616]  # Std for normalization.
  start: 0  # First example to verify in dataset.
  end: 100  # Last example to verify in dataset. We verify 100 examples in this test.
specification:
  norm: 2 
  epsilon: 0.1411764705882353  # epsilon=36./255.
attack:  # Currently attack is only implemented for Linf norm.
  pgd_order: skip
solver:
  batch_size: 2048  # Number of subdomains to compute in parallel in bound solver. Decrease if you run out of memory.
  alpha-crown:
    iteration: 100   # Number of iterations for alpha-CROWN optimization. Alpha-CROWN is used to compute all intermediate layer bounds before branch and bound starts.
    lr_alpha: 0.1    # Learning rate for alpha in alpha-CROWN. The default (0.1) is typically ok.
  beta-crown:
    lr_alpha: 0.01  # Learning rate for optimizing the alpha parameters, the default (0.01) is typically ok, but you can try to tune this parameter to get better lower bound.
    lr_beta: 0.05  # Learning rate for optimizing the beta parameters, the default (0.05) is typically ok, but you can try to tune this parameter to get better lower bound.
    iteration: 20  # Number of iterations for beta-CROWN optimization. 20 is often sufficient, 50 or 100 can also be used.
bab:
  timeout: 120  # Timeout threshold for branch and bound. Increase for verifying more points.
  branching:  # Parameters for branching heuristics.
    reduceop: min  # Reduction function for the branching heuristic scores, min or max. Using max can be better on some models.
    method: kfsb  # babsr is fast but less accurate; fsb is slow but most accurate; kfsb is usually a balance.
    candidates: 3  # Number of candidates to consider in fsb and kfsb. More leads to slower but better branching. 3 is typically good enough.

however running the abcrown.py script with the configuration above, I am getting the following error

Exception has occurred: RuntimeError
Expected 3D (unbatched) or 4D (batched) input to conv2d, but got input of size: [1, 1, 3, 32, 32]
  File "/home/f.brau/alpha-beta-CROWN/complete_verifier/model_defs.py", line 164, in forward
    out = self.relu(self.conv1(x))
  File "/home/f.brau/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 110, in __init__
    self.final_shape = model(
  File "/home/f.brau/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 55, in __init__
    self.net = BoundedModule(
  File "/home/f.brau/alpha-beta-CROWN/complete_verifier/abcrown.py", line 198, in bab
    self.model = LiRPANet(
  File "/home/f.brau/alpha-beta-CROWN/complete_verifier/abcrown.py", line 398, in complete_verifier
    l, nodes, ret = self.bab(
  File "/home/f.brau/alpha-beta-CROWN/complete_verifier/abcrown.py", line 591, in main
    verified_status = self.complete_verifier(
  File "/home/f.brau/alpha-beta-CROWN/complete_verifier/abcrown.py", line 614, in <module>
    abcrown.main()
RuntimeError: Expected 3D (unbatched) or 4D (batched) input to conv2d, but got input of size: [1, 1, 3, 32, 32]```

Any possible easy fix?

Thanks!

yusf1013 commented 9 months ago

@huanzhang12 could you tell us if there has been any updates on this? I am facing the exact same problem as @fabiobrau with norm = 1. Here is my configuration file GCP-CROWN/cifar_cnn_a_adv.yaml:

model:
  name: cnn_4layer_adv
  path: models/sdp/cifar_cnn_a_adv.model
data:
  dataset: CIFAR_SDP
  start: 1
  end: 5
specification:
  epsilon: 0.00784313725  # 2./255.
  norm: 1
attack:
  pgd_restarts: 50
solver:
  batch_size: 2048
  beta-crown:
    iteration: 20
bab:
  timeout: 200
  branching:
    reduceop: max
  cut:
    enabled: True
    cplex_cuts: True
    bab_cut: True
    lr_decay: 0.9

output:

mip_multi_proc: 20, mip_threads: 1, total threads used: 20
Process Process-2:
Traceback (most recent call last):
  File "/home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/multiprocessing/process.py", line 315, in _bootstrap
    self.run()
  File "/home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/multiprocessing/process.py", line 108, in run
    self._target(*self._args, **self._kwargs)
  File "/home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/torch/autograd/grad_mode.py", line 27, in decorate_context
    return func(*args, **kwargs)
  File "/home/yusuf/Desktop/alpha-beta-CROWN-main/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/yusuf/Desktop/alpha-beta-CROWN-main/complete_verifier/lp_mip_solver.py", line 1066, in build_the_model_mip
    build_solver_model(m, timeout, mip_multi_proc=mip_multi_proc,
  File "/home/yusuf/Desktop/alpha-beta-CROWN-main/complete_verifier/lp_mip_solver.py", line 638, in build_solver_model
    out_vars = m.net.build_solver_module(
  File "/home/yusuf/Desktop/alpha-beta-CROWN-main/complete_verifier/auto_LiRPA/solver_module.py", line 50, in build_solver_module
    inp_gurobi_vars = self._build_solver_input(roots[i])
  File "/home/yusuf/Desktop/alpha-beta-CROWN-main/complete_verifier/auto_LiRPA/solver_module.py", line 94, in _build_solver_input
    assert node.perturbation.norm == float("inf")
AssertionError

...
...

Remaining spec index tensor([0], device='cuda:0') with bounds tensor([[-0.96139729]], device='cuda:0') need to verify.
Traceback (most recent call last):
  File "/home/yusuf/Desktop/alpha-beta-CROWN-main/complete_verifier/abcrown.py", line 616, in <module>
    abcrown.main()
  File "/home/yusuf/Desktop/alpha-beta-CROWN-main/complete_verifier/abcrown.py", line 595, in main
    verified_status = self.complete_verifier(
  File "/home/yusuf/Desktop/alpha-beta-CROWN-main/complete_verifier/abcrown.py", line 402, in complete_verifier
    l, nodes, ret = self.bab(
  File "/home/yusuf/Desktop/alpha-beta-CROWN-main/complete_verifier/abcrown.py", line 198, in bab
    self.model = LiRPANet(
  File "/home/yusuf/Desktop/alpha-beta-CROWN-main/complete_verifier/beta_CROWN_solver.py", line 55, in __init__
    self.net = BoundedModule(
  File "/home/yusuf/Desktop/alpha-beta-CROWN-main/complete_verifier/auto_LiRPA/bound_general.py", line 110, in __init__
    self.final_shape = model(
  File "/home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/torch/nn/modules/module.py", line 1194, in _call_impl
    return forward_call(*input, **kwargs)
  File "/home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/torch/nn/modules/container.py", line 204, in forward
    input = module(input)
  File "/home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/torch/nn/modules/module.py", line 1194, in _call_impl
    return forward_call(*input, **kwargs)
  File "/home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/torch/nn/modules/conv.py", line 463, in forward
    return self._conv_forward(input, self.weight, self.bias)
  File "/home/yusuf/miniconda3/envs/alpha-beta-crown/lib/python3.9/site-packages/torch/nn/modules/conv.py", line 459, in _conv_forward
    return F.conv2d(input, weight, bias, self.stride,
RuntimeError: Expected 3D (unbatched) or 4D (batched) input to conv2d, but got input of size: [1, 1, 3, 32, 32]

Thank you.

Verified-Intelligence / alpha-beta-CROWN

Use norms other then linf #30