MIP Verification error about alpha-beta-crown HOT 3 CLOSED

@Felipetoledo4815 Thanks for reporting the issue to us! Could you provide a full error traceback and paste it here? It will be very helpful for us to confirm we can reproduce the same bug.

@KaidiXu could you help with this issue?

from alpha-beta-crown.

Sure, both error logs (with and without the sparse_alpha set to false) are inside the zip file mentioned above. However here is the full error traceback without using the sparse_alpha=false:

/home/felipe/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)
/home/felipe/miniconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/onnx2pytorch/convert/operations.py:154: 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.)
weight = torch.from_numpy(numpy_helper.to_array(params[0]))
/home/felipe/miniconda3/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'."
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: true
precompile_jit: false
complete_verifier: mip
enable_incomplete_verification: true
csv_name: null
results_file: ./out_35_d20_MIP.txt
root_path: ''
model:
name: null
path: null
onnx_path: ./model_35_d20.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_35_d20.vnnlib
vnnlib_path_prefix: ''
solver:
batch_size: 500
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: 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: 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 Fri Mar 17 10:14:54 2023 on lab-server
Internal results will be saved to ./out_35_d20_MIP.txt.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 0, vnnlib ID: 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Using onnx ./model_35_d20.onnx
Using vnnlib ./prop_35_d20.vnnlib
50 inputs and 2 outputs in vnnlib
Loading onnx ./model_35_d20.onnx wih quirks {}
Attack parameters: initialization=uniform, steps=100, restarts=30, alpha=1.2497498989105225, initialization=uniform, GAMA=False
Model output of first 5 examples:
tensor([[-1.49143803, 1.02468622]])
Adv example prediction (first 2 examples and 2 restarts):
tensor([[[-0.78454685, 0.44151267]]])
PGD attack margin (first 2 examles and 10 specs):
tensor([[[1.22605956]]])
number of violation: 0
Attack finished in 0.1926 seconds.
PGD attack failed
Model prediction is: tensor([[-1.49143803, 1.02468622]])
layer /14 using sparse-features alpha with shape [208]; unstable size 208; total size 318 (torch.Size([1, 318]))
layer /14 start_node /16 using sparse-spec alpha with unstable size 61 total_size 102 output_shape torch.Size([102])
layer /14 start_node /19 using full alpha with unstable size None total_size 1 output_shape 1
Optimizable variables initialized.
initial CROWN bounds: tensor([[-283521.18750000]]) None
Traceback (most recent call last):
File "/Data/alpha-beta-CROWN/complete_verifier/abcrown.py", line 650, in
main()
File "/Data/alpha-beta-CROWN/complete_verifier/abcrown.py", line 538, in main
incomplete_verifier(model_ori, x, data_ub=data_max, data_lb=data_min, vnnlib=vnnlib)
File "/Data/alpha-beta-CROWN/complete_verifier/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/felipe/Data/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/felipe/Data/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1170, in compute_bounds
cutter=cutter, decision_thresh=decision_thresh)
File "/home/felipe/Data/alpha-beta-CROWN/complete_verifier/auto_LiRPA/optimized_bounds.py", line 592, in get_optimized_bounds
update_mask=preserve_mask)
File "/home/felipe/Data/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1321, in compute_bounds
self.check_prior_bounds(final)
File "/home/felipe/Data/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 849, in check_prior_bounds
self.check_prior_bounds(n)
File "/home/felipe/Data/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 857, in check_prior_bounds
node.inputs[i], prior_checked=True)
File "/home/felipe/Data/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 959, in compute_intermediate_bounds
unstable_size=unstable_size)
File "/home/felipe/Data/alpha-beta-CROWN/complete_verifier/auto_LiRPA/backward_bound.py", line 146, in backward_general
beta_for_intermediate_layers=self.intermediate_constr is not None)
File "/home/felipe/Data/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/activation.py", line 672, in bound_backward
self._backward_relaxation(last_lA, last_uA, x, start_node, unstable_idx)
File "/home/felipe/Data/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/activation.py", line 598, in _backward_relaxation
assert self.alpha_lookup_idx[start_node.name] is None
AssertionError

And here is the full error traceback when setting sparse_alpha=false:

Configurations:

general:
device: cpu
seed: 100
conv_mode: patches
deterministic: false
double_fp: false
loss_reduction_func: sum
record_bounds: false
sparse_alpha: false
save_adv_example: true
precompile_jit: false
complete_verifier: mip
enable_incomplete_verification: true
csv_name: null
results_file: ./out_35_d20_MIP.txt
root_path: ''
model:
name: null
path: null
onnx_path: ./model_35_d20.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_35_d20.vnnlib
vnnlib_path_prefix: ''
solver:
batch_size: 500
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: 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: 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 Fri Mar 17 10:29:32 2023 on lab-server
Internal results will be saved to ./out_35_d20_MIP.txt.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 0, vnnlib ID: 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Using onnx ./model_35_d20.onnx
Using vnnlib ./prop_35_d20.vnnlib
Precompiled vnnlib file found at ./prop_35_d20.vnnlib.compiled
Loading onnx ./model_35_d20.onnx wih quirks {}
Attack parameters: initialization=uniform, steps=100, restarts=30, alpha=1.2497498989105225, initialization=uniform, GAMA=False
Model output of first 5 examples:
tensor([[-1.49143803, 1.02468622]])
Adv example prediction (first 2 examples and 2 restarts):
tensor([[[-0.78454685, 0.44151267]]])
PGD attack margin (first 2 examles and 10 specs):
tensor([[[1.22605956]]])
number of violation: 0
Attack finished in 0.1901 seconds.
PGD attack failed
Model prediction is: tensor([[-1.49143803, 1.02468622]])
layer /14 start_node /16 using full alpha with unstable size 61 total_size 102 output_shape torch.Size([102])
layer /14 start_node /19 using full alpha with unstable size None total_size 1 output_shape 1
Optimizable variables initialized.
initial CROWN bounds: tensor([[-283521.18750000]]) None
Early stop at 43th iter due to 10 iterations no improvement!
best_l after optimization: -233565.984375 with beta sum per layer: []
alpha/beta optimization time: 0.29564619064331055
initial alpha-CROWN bounds: tensor([[-233565.98437500]])
Worst class: (+ rhs) -233565.984375
Set parameter Username
Academic license - for non-commercial use only - expires 2023-08-24
/home/felipe/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)
/home/felipe/miniconda3/envs/alpha-beta-crown/lib/python3.7/site-packages/onnx2pytorch/convert/operations.py:154: 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.)
weight = torch.from_numpy(numpy_helper.to_array(params[0]))
/home/felipe/miniconda3/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'."
mip_multi_proc: 8, mip_threads: 4, total threads used: 32
Traceback (most recent call last):
File "/Data/alpha-beta-CROWN/complete_verifier/abcrown.py", line 650, in
main()
File "/Data/alpha-beta-CROWN/complete_verifier/abcrown.py", line 553, in main
verified_status, init_global_lb, lower_bounds, upper_bounds, refined_betas = mip(saved_bounds=saved_bounds)
File "/Data/alpha-beta-CROWN/complete_verifier/abcrown.py", line 111, in mip
mip_global_lb, mip_global_ub, mip_status, mip_adv = lirpa_model.build_the_model_mip(labels_to_verify=labels_to_verify, save_adv=True)
File "/home/felipe/Data/alpha-beta-CROWN/complete_verifier/lp_mip_solver.py", line 771, in build_the_model_mip
mip_threads=mip_threads, model_type="mip", x=x, intermediate_bounds=intermediate_bounds)
File "/home/felipe/Data/alpha-beta-CROWN/complete_verifier/lp_mip_solver.py", line 547, in build_solver_model
x=x, C=m.c, intermediate_layer_bounds=intermediate_bounds, final_node_name=m.net.final_name, model_type=model_type, solver_pkg=m.net.solver_pkg)
File "/home/felipe/Data/alpha-beta-CROWN/complete_verifier/auto_LiRPA/solver_module.py", line 61, in build_solver_module
self._build_solver_general(node=final, C=C, model_type=model_type, solver_pkg=solver_pkg)
File "/home/felipe/Data/alpha-beta-CROWN/complete_verifier/auto_LiRPA/solver_module.py", line 70, in _build_solver_general
self._build_solver_general(n, C=C, model_type=model_type, solver_pkg=solver_pkg)
File "/home/felipe/Data/alpha-beta-CROWN/complete_verifier/auto_LiRPA/solver_module.py", line 70, in _build_solver_general
self._build_solver_general(n, C=C, model_type=model_type, solver_pkg=solver_pkg)
File "/home/felipe/Data/alpha-beta-CROWN/complete_verifier/auto_LiRPA/solver_module.py", line 82, in _build_solver_general
model_type=model_type, solver_pkg=solver_pkg)
File "/home/felipe/Data/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/linear.py", line 599, in build_solver
lin_expr += grb.LinExpr(coeffs, v[0])
File "src/gurobipy/linexpr.pxi", line 71, in gurobipy.LinExpr.init
gurobipy.GurobiError: Linear expression arguments of different length

from alpha-beta-crown.

Hi @Felipetoledo4815, it looks like the model you provided has three consecutive linear layers (three nodes after the ReLU):

Is there any specific reason that you have this design?
Our codebase may not be general enough for this case, could you please try to merge them into one linear layer with a matrix size = 318*2 and a bias term?
If there is still an issue, please let me know!

from alpha-beta-crown.