search

Verified-Intelligence / alpha-beta-CROWN

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

MIP Verification error #26

Closed Felipetoledo4815 closed 11 months ago

Felipetoledo4815 commented 1 year ago

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

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

System configuration:

huanzhang12 commented 1 year ago

@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?

Felipetoledo4815 commented 1 year ago

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

KaidiXu commented 1 year ago

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

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!