AssertionError: for each property in OR, only one clause supported so far

[idan0610]

Running the attached network saved in ONNX format, with the given property encoded inside the attached vnnlib file, while skipping the pgd attack, results in the following error:

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: true
  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: ./NAPS_ONNX/cls0_id45_cls1_id86.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: ./NAPS_VNNLIB/cls0_id45_cls1_id86.vnnlib
  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: 43500
  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: skip
  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: NAPS_ADVS_ALPHA_CROWN/cls0_id45_cls1_id86.cex
  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 Mon Dec 23 11:54:02 2024 on Idan
Internal results will be saved to out.txt.

 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% idx: 0, vnnlib ID: 0 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Using onnx ./NAPS_ONNX/cls0_id45_cls1_id86.onnx
Using vnnlib ./NAPS_VNNLIB/cls0_id45_cls1_id86.vnnlib
.compiled file md5: d7fc38e5b66d5313dd3d8b70e9aba779 does not match the current vnnlib md5: 5b195a9ccd15daca46053072720a32a7. Regenerating...
5 inputs and 25 outputs in vnnlib
Loading onnx ./NAPS_ONNX/cls0_id45_cls1_id86.onnx with quirks {}
/home/idan0610/miniconda3/envs/alpha-beta-crown/lib/python3.11/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_1708025845868/work/torch/csrc/utils/tensor_numpy.cpp:206.)
  weight = torch.from_numpy(numpy_helper.to_array(params[0]))
/home/idan0610/miniconda3/envs/alpha-beta-crown/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(

**************************
Model might not be converted correctly. Please check onnx conversion carefully.
Output by pytorch: [[0.54926336 0.5443503  0.54828876 0.53256744 0.5463338  0.
  0.         0.         0.8619423  2.0155995  0.         0.
  0.         0.         0.         6.3346176  0.         0.
  0.         1.800857   1.6441518  0.         0.         0.
  0.        ]]
Output by onnx: [[  0.5492632    0.54435027   0.5482887    0.53256744   0.5463335
   -8.425573   -34.01707    -22.37343      0.8619389    2.0155973
  -29.097502    -5.0950704   -5.708405    -0.5234605  -43.24539
    6.3346148   -2.3508124   -6.2296753   -0.233619     1.8008599
    1.6441505  -13.230407   -87.856415   -22.436367    -9.063261  ]]
Max error: tensor(87.85641479)
**************************

Traceback (most recent call last):
  File "/home/idan0610/Marabou_dev/cdcl/alpha-beta-CROWN/complete_verifier/abcrown.py", line 706, in <module>
    abcrown.main()
  File "/home/idan0610/Marabou_dev/cdcl/alpha-beta-CROWN/complete_verifier/abcrown.py", line 638, in main
    incomplete_verification_output = self.incomplete_verifier(
                                     ^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/idan0610/Marabou_dev/cdcl/alpha-beta-CROWN/complete_verifier/abcrown.py", line 85, in incomplete_verifier
    assert all([len(_[0]) == 1 for _ in specs]), \
AssertionError: for each property in OR, only one clause supported so far

This is the output I get when running on both CPU and CUDA.

To Reproduce
python3 abcrown.py --config cls0_id45_cls1_id86.yaml

System configuration:

OS: Tried on both Debian 12.6 and WSL2 with Ubuntu 20.04

Python version: 3.11

Pytorch Version: 2.5.1+cu124

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

Thanks in advance for your help on this issue

cls0_id45_cls1_id86.zip

[AvrahamRaviv]

Same here
My solution was to divide the verification process into separate queries.