habeebp098
commented
3 weeks ago The latest version of the code is also encountering the same error for the network and VNNLIB file mentioned above.
alpha-beta-CROWN/complete_verifier$ python abcrown.py --config exp_configs/tutorial_examples/pytorch_model_with_one_vnnlib.yaml --device cpu
Configurations:
general:
device: cpu
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")'
buffer_has_batchdim: false
save_output: false
output_file: out.pkl
return_optimized_model: false
model:
name: null
path: null
onnx_path: net1.onnx
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
with_jacobian: false
data:
start: 0
end: 10000
select_instance: null
num_outputs: 10
mean: 0.0
std: 1.0
pkl_path: null
dataset: null
data_filter_path: null
data_idx_file: null
specification:
type: lp
robustness_type: verified-acc
norm: .inf
epsilon: null
epsilon_min: 0.0
vnnlib_path: prop_y0.vnnlb
vnnlib_path_prefix: ''
rhs_offset: null
solver:
batch_size: 64
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
optimize_disjuncts_separately: false
crown:
batch_size: 1000000000
max_crown_size: 1000000000
relu_option: adaptive
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
disable_optimization: []
invprop:
apply_output_constraints_to: []
tighten_input_bounds: false
best_of_oc_and_no_oc: false
directly_optimize: []
oc_lr: 0.1
share_gammas: false
beta-crown:
lr_alpha: 0.01
lr_beta: 0.05
lr_decay: 0.98
optimizer: adam
iteration: 50
beta: true
beta_warmup: true
enable_opt_interm_bounds: false
all_node_split_LP: false
forward:
refine: false
dynamic: false
max_dim: 10000
reset_threshold: 1.0
multi_class:
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
skip_unsafe: false
bab:
initial_max_domains: 1
max_domains: .inf
decision_thresh: 0
timeout: 360
timeout_scale: 1
max_iterations: -1
override_timeout: null
get_upper_bound: false
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: min
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
nonlinear_split:
method: shortcut
branching_point_method: uniform
num_branches: 2
filter: false
filter_beta: false
filter_batch_size: 10000
filter_iterations: 25
use_min: false
loose_tanh_threshold: null
dynamic_bbps: false
dynamic_options: [uniform, three_left, three_right]
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_sum: false
bf_backup_thresh: -1
bf_rhs_offset: 0
bf_iters: 1000000000.0
bf_batch_size: 100000
bf_zero_crossing_score: false
touch_zero_score: 0
ibp_enhancement: false
catch_assertion: false
compare_with_old_bounds: false
update_rhs_with_attack: false
sb_coeff_thresh: 0.001
sort_index: null
sort_descending: true
show_progress: false
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_batch_size: 100000000
pgd_early_stop: true
pgd_lr_decay: 0.99
pgd_alpha: auto
pgd_alpha_scale: false
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: 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
print_verbose_decisions: false
Experiments at Thu Jun 6 04:42:56 2024 on pillar1
Internal results will be saved to out.txt.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 0, vnnlib ID: 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Using onnx net1.onnx
Using vnnlib prop_y0.vnnlb
Precompiled vnnlib file found at prop_y0.vnnlb.compiled
Loading onnx net1.onnx wih quirks {}
/home/h/anaconda3/envs/alpha-beta-crown3/lib/python3.11/site-packages/onnx2pytorch/convert/layer.py:29: 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_1708025845868/work/torch/csrc/utils/tensor_numpy.cpp:206.)
layer.weight.data = torch.from_numpy(numpy_helper.to_array(weight))
/home/h/anaconda3/envs/alpha-beta-crown3/lib/python3.11/site-packages/onnx2pytorch/convert/model.py:151: UserWarning: Using experimental implementation that allows 'batch_size > 1'.Batchnorm layers could potentially produce false outputs.
warnings.warn(
Attack parameters: initialization=uniform, steps=100, restarts=30, alpha=0.07449999451637268, initialization=uniform, GAMA=False
Model output of first 5 examples:
tensor([[-9.41845608, 11.91907406, -2.72109032]])
100%|█████████████████████████████████████████████████████████████████████████████████████████████████████| 1/1 [00:01<00:00, 1.09s/it]
Adv example prediction (first 2 examples and 2 restarts):
tensor([[[-7.09657097, 9.00977802, -2.11059594]]])
PGD attack margin (first 2 examles and 10 specs):
tensor([[[16.10634995, 4.98597527]]])
number of violation: 0
Attack finished in 1.0931 seconds.
PGD attack failed
/home/h/anaconda3/envs/alpha-beta-crown3/lib/python3.11/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) in [2, 3, 4, 5] and self.quirks.get("fix_batch_size") is True:
/home/h/anaconda3/envs/alpha-beta-crown3/lib/python3.11/site-packages/onnx2pytorch/operations/reshape.py:54: TracerWarning: torch.tensor results are registered as constants in the trace. You can safely ignore this warning if you use this function to create tensors out of constant variables that would be the same every time you call this function. In any other case, this might cause the trace to be incorrect.
if (torch.prod(torch.tensor(input.shape)) != torch.prod(shape) and len(input.size()) == len(shape) + 1
/home/h/anaconda3/envs/alpha-beta-crown3/lib/python3.11/site-packages/onnx2pytorch/operations/reshape.py:54: TracerWarning: Using len to get tensor shape might cause the trace to be incorrect. Recommended usage would be tensor.shape[0]. Passing a tensor of different shape might lead to errors or silently give incorrect results.
if (torch.prod(torch.tensor(input.shape)) != torch.prod(shape) and len(input.size()) == len(shape) + 1
/home/h/anaconda3/envs/alpha-beta-crown3/lib/python3.11/site-packages/onnx2pytorch/operations/reshape.py:58: 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)]
/home/h/project2/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/leaf.py:192: UserWarning: The "has_batchdim" option for BoundBuffers is deprecated. It may be removed from the next release.
warnings.warn('The "has_batchdim" option for BoundBuffers is deprecated.'
Model: BoundedModule(
(/0): BoundInput(name=/0, inputs=[], perturbed=True)
(/shape): BoundBuffers(name=/shape, inputs=[], perturbed=False)
(/12): BoundParams(name=/12, inputs=[], perturbed=False)
(/13): BoundParams(name=/13, inputs=[], perturbed=False)
(/14): BoundParams(name=/14, inputs=[], perturbed=False)
(/15): BoundParams(name=/15, inputs=[], perturbed=False)
(/16): BoundParams(name=/16, inputs=[], perturbed=False)
(/17): BoundParams(name=/17, inputs=[], perturbed=False)
(/18): BoundParams(name=/18, inputs=[], perturbed=False)
(/19): BoundParams(name=/19, inputs=[], perturbed=False)
(/20): BoundParams(name=/20, inputs=[], perturbed=False)
(/21): BoundParams(name=/21, inputs=[], perturbed=False)
(/input): BoundTranspose(name=/input, inputs=[/0], perturbed=True)
(/input.3): BoundConv(name=/input.3, inputs=[/input, /12, /13], perturbed=True)
(/24): BoundRelu(name=/24, inputs=[/input.3], perturbed=True)
(/input.7): BoundMaxPool(name=/input.7, inputs=[/24], perturbed=True)
(/input.11): BoundConv(name=/input.11, inputs=[/input.7, /14, /15], perturbed=True)
(/27): BoundRelu(name=/27, inputs=[/input.11], perturbed=True)
(/input.15): BoundMaxPool(name=/input.15, inputs=[/27], perturbed=True)
(/input.19): BoundConv(name=/input.19, inputs=[/input.15, /16, /17], perturbed=True)
(/30): BoundRelu(name=/30, inputs=[/input.19], perturbed=True)
(/31): BoundMaxPool(name=/31, inputs=[/30], perturbed=True)
(/32): BoundTranspose(name=/32, inputs=[/31], perturbed=True)
(/33): BoundConstant(name=/33, inputs=[], perturbed=False)
(/34): BoundSplit(name=/34, inputs=[/shape, /33], perturbed=False)
(/35): BoundSplit(name=/35, inputs=[/shape, /33], perturbed=False)
(/36): BoundConstant(name=/36, value=tensor([0]))
(/37): BoundSqueeze(name=/37, inputs=[/34, /36], perturbed=False)
(/38): BoundConstant(name=/38, value=tensor([0]))
(/39): BoundSqueeze(name=/39, inputs=[/35, /38], perturbed=False)
(/40): BoundConstant(name=/40, value=tensor([0]))
(/41): BoundUnsqueeze(name=/41, inputs=[/37, /40], perturbed=False)
(/42): BoundConstant(name=/42, value=tensor([0]))
(/43): BoundUnsqueeze(name=/43, inputs=[/39, /42], perturbed=False)
(/44): BoundConcat(name=/44, inputs=[/41, /43], perturbed=False)
(/45): BoundReshape(name=/45, inputs=[/32, /44], perturbed=True)
(/input.23): BoundLinear(name=/input.23, inputs=[/45, /18, /19], perturbed=True)
(/47): BoundRelu(name=/47, inputs=[/input.23], perturbed=True)
(/48): BoundLinear(name=/48, inputs=[/47, /20, /21], perturbed=True)
)
Original output: tensor([[-9.41845608, 11.91907501, -2.72108960]])
Split layers:
BoundConv(name=/input.3, inputs=[/input, /12, /13], perturbed=True): [(BoundRelu(name=/24, inputs=[/input.3], perturbed=True), 0)]
BoundConv(name=/input.11, inputs=[/input.7, /14, /15], perturbed=True): [(BoundRelu(name=/27, inputs=[/input.11], perturbed=True), 0)]
BoundConv(name=/input.19, inputs=[/input.15, /16, /17], perturbed=True): [(BoundRelu(name=/30, inputs=[/input.19], perturbed=True), 0)]
BoundLinear(name=/input.23, inputs=[/45, /18, /19], perturbed=True): [(BoundRelu(name=/47, inputs=[/input.23], perturbed=True), 0)]
Nonlinear functions:
BoundRelu(name=/24, inputs=[/input.3], perturbed=True)
BoundMaxPool(name=/input.7, inputs=[/24], perturbed=True)
BoundRelu(name=/27, inputs=[/input.11], perturbed=True)
BoundMaxPool(name=/input.15, inputs=[/27], perturbed=True)
BoundRelu(name=/30, inputs=[/input.19], perturbed=True)
BoundMaxPool(name=/31, inputs=[/30], perturbed=True)
BoundRelu(name=/47, inputs=[/input.23], perturbed=True)
Traceback (most recent call last):
File "/home/h/project2/alpha-beta-CROWN/complete_verifier/abcrown.py", line 706, in <module>
abcrown.main()
File "/home/h/project2/alpha-beta-CROWN/complete_verifier/abcrown.py", line 638, in main
incomplete_verification_output = self.incomplete_verifier(
^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/h/project2/alpha-beta-CROWN/complete_verifier/abcrown.py", line 159, in incomplete_verifier
global_lb, ret = model.build(
^^^^^^^^^^^^
File "/home/h/project2/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 454, in build
lb, ub, aux_reference_bounds = self.net.init_alpha(
^^^^^^^^^^^^^^^^^^^^
File "/home/h/project2/alpha-beta-CROWN/complete_verifier/auto_LiRPA/optimized_bounds.py", line 845, in init_alpha
l, u = self.compute_bounds(
^^^^^^^^^^^^^^^^^^^^
File "/home/h/project2/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1316, in compute_bounds
return self._compute_bounds_main(C=C,
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/h/project2/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1414, in _compute_bounds_main
self.check_prior_bounds(final)
File "/home/h/project2/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 879, in check_prior_bounds
self.check_prior_bounds(n)
File "/home/h/project2/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 879, in check_prior_bounds
self.check_prior_bounds(n)
File "/home/h/project2/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 879, in check_prior_bounds
self.check_prior_bounds(n)
[Previous line repeated 9 more times]
File "/home/h/project2/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 897, in check_prior_bounds
self.compute_intermediate_bounds(
File "/home/h/project2/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 981, in compute_intermediate_bounds
node.lower, node.upper = self.backward_general(
^^^^^^^^^^^^^^^^^^^^^^
File "/home/h/project2/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 337, in backward_general
A, lower_b, upper_b = l.bound_backward(
^^^^^^^^^^^^^^^^^
File "/home/h/project2/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/reshape.py", line 288, in bound_backward
return [(_bound_oneside(last_lA), _bound_oneside(last_uA))], 0, 0
^^^^^^^^^^^^^^^^^^^^^^^
File "/home/h/project2/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/reshape.py", line 286, in _bound_oneside
return last_A.permute(self.perm_inv_inc_one)
^^^^^^^^^^^^^^
AttributeError: 'Patches' object has no attribute 'permute'
I have been experimenting with the alpha-beta-crown tool and encountered the following error while running it for some input data.
alpha-beta-crown) h@pillar1:~/project3/project3_2$ python /home/h/project2/alpha-beta-CROWN-main/complete_verifier/abcrown.py --onnx_path net.onnx --vnnlib_path prop_y0.vnnlb --device cpu --results_file 'abc_out_y0.txt' --no_incomplete Configurations:
general: device: cpu 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: false csv_name: null results_file: abc_out_y0.txt root_path: '' model: name: null path: null onnx_path: net.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: .inf epsilon: null vnnlib_path: prop_y0.vnnlb vnnlib_path_prefix: '' solver: batch_size: 64 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: 50 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: 360 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: 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 Thu Mar 14 13:23:25 2024 on pillar1 Internal results will be saved to abc_out_y0.txt.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 0, vnnlib ID: 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Using onnx net.onnx Using vnnlib prop_y0.vnnlb Precompiled vnnlib file found at prop_y0.vnnlb.compiled Loading onnx net.onnx wih quirks {} /home/h/anaconda3/envs/alpha-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)) /home/h/anaconda3/envs/alpha-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'." /home/h/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" Attack parameters: initialization=uniform, steps=100, restarts=30, alpha=0.07362499833106995, initialization=uniform, GAMA=False Model output of first 5 examples: tensor([[-5.98954344, 2.28598309, 3.65411043]]) Adv example prediction (first 2 examples and 2 restarts): tensor([[[-2.10495210, -0.81939900, 3.52598715]]]) PGD attack margin (first 2 examles and 10 specs): tensor([[[1.28555310, 5.63093948]]]) number of violation: 0 Attack finished in 1.2851 seconds. PGD attack failed Total VNNLIB file length: 1, max property batch size: 1, total number of batches: 1
Properties batch 0, size 1 Remaining timeout: 358.6844446659088
Instance 0 first 10 spec matrices: [[[-1. 1. 0.]
[-1. 0. 1.]]] thresholds: [0. 0.] ###### /home/h/anaconda3/envs/alpha-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) /home/h/anaconda3/envs/alpha-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)] Model prediction is: tensor([-5.98954344, 2.28598332, 3.65411091]) Traceback (most recent call last): File "/home/h/project2/alpha-beta-CROWN-main/complete_verifier/abcrown.py", line 650, in
main()
File "/home/h/project2/alpha-beta-CROWN-main/complete_verifier/abcrown.py", line 573, in main
refined_betas=refined_betas, attack_images=all_adv_candidates, attack_margins=attack_margins)
File "/home/h/project2/alpha-beta-CROWN-main/complete_verifier/abcrown.py", line 404, in complete_verifier
rhs=rhs, timeout=timeout, attack_images=this_spec_attack_images)
File "/home/h/project2/alpha-beta-CROWN-main/complete_verifier/abcrown.py", line 209, in bab
timeout=timeout, refined_betas=refined_betas, rhs=rhs)
File "/home/h/project2/alpha-beta-CROWN-main/complete_verifier/batch_branch_and_bound.py", line 399, in relu_bab_parallel
domain, x, stop_criterion_func=stop_criterion(decision_thresh))
File "/home/h/project2/alpha-beta-CROWN-main/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/h/project2/alpha-beta-CROWN-main/complete_verifier/auto_LiRPA/optimized_bounds.py", line 1023, in init_slope
intermediate_layer_bounds=intermediate_layer_bounds)
File "/home/h/project2/alpha-beta-CROWN-main/complete_verifier/auto_LiRPA/bound_general.py", line 1321, in compute_bounds
self.check_prior_bounds(final)
File "/home/h/project2/alpha-beta-CROWN-main/complete_verifier/auto_LiRPA/bound_general.py", line 849, in check_prior_bounds
self.check_prior_bounds(n)
File "/home/h/project2/alpha-beta-CROWN-main/complete_verifier/auto_LiRPA/bound_general.py", line 849, in check_prior_bounds
self.check_prior_bounds(n)
File "/home/h/project2/alpha-beta-CROWN-main/complete_verifier/auto_LiRPA/bound_general.py", line 849, in check_prior_bounds
self.check_prior_bounds(n)
[Previous line repeated 9 more times]
File "/home/h/project2/alpha-beta-CROWN-main/complete_verifier/auto_LiRPA/bound_general.py", line 857, in check_prior_bounds
node.inputs[i], prior_checked=True)
File "/home/h/project2/alpha-beta-CROWN-main/complete_verifier/auto_LiRPA/bound_general.py", line 959, in compute_intermediate_bounds
unstable_size=unstable_size)
File "/home/h/project2/alpha-beta-CROWN-main/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/h/project2/alpha-beta-CROWN-main/complete_verifier/auto_LiRPA/operators/shape.py", line 507, in bound_backward
return [(_bound_oneside(last_lA), _bound_oneside(last_uA))], 0, 0
File "/home/h/project2/alpha-beta-CROWN-main/complete_verifier/auto_LiRPA/operators/shape.py", line 505, in _bound_oneside
return last_A.permute(self.perm_inv_inc_one)
AttributeError: 'Patches' object has no attribute 'permute'
Strangely, the tool works perfectly for some other inputs. I have attached both the neural network and VNNLB files.
net.txt prop_y0.txt