Error running vnncomp22/vggnet16.yaml

[mhmd97z]

Hi,

I tried to run exp_configs/vnncomp22/vggnet16.yaml without any changes, but I got the following NotImplementedError.

I'd appreciate it if you could look into this.

Traceback (most recent call last):
  File "abcrown.py", line 656, in <module>
    main()
  File "abcrown.py", line 579, in main
    refined_betas=refined_betas, attack_images=all_adv_candidates, attack_margins=attack_margins)
  File "abcrown.py", line 410, in complete_verifier
    rhs=rhs, timeout=timeout, attack_images=this_spec_attack_images)
  File "abcrown.py", line 200, in bab
    rhs=rhs, timeout=timeout, branching_method=arguments.Config["bab"]["branching"]["method"])
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/batch_branch_and_bound_input_split.py", line 164, in input_bab_parallel
    bounding_method=bounding_method,
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 1141, in build_the_model
    x=(x,), C=self.c, method=bounding_method, cutter=self.cutter, bound_upper=False)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 1319, in compute_bounds
    self.check_prior_bounds(final)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 847, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 847, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 847, in check_prior_bounds
    self.check_prior_bounds(n)
  [Previous line repeated 29 more times]
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 855, in check_prior_bounds
    node.inputs[i], prior_checked=True)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/bound_general.py", line 883, in compute_intermediate_bounds
    node=node, concretize=True)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/forward_bound.py", line 16, in forward_general
    return self.forward_general_dynamic(C, node, concretize, offset)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/forward_bound.py", line 156, in forward_general_dynamic
    linear_inp = self.forward_general_dynamic(node=l_pre, offset=offset)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/forward_bound.py", line 168, in forward_general_dynamic
    *inp, max_dim=max_dim, offset=offset)
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/base.py", line 228, in bound_dynamic_forward
    raise NotImplementedError(f'bound_dynamic_forward is not implemented for {self}.')
NotImplementedError: bound_dynamic_forward is not implemented for BoundMaxPool(name="/input.8").

[shizhouxing]

@mhmd97z MaxPool is not supported. You'll need to convert the model to a ReLU network by:
https://github.com/Verified-Intelligence/alpha-beta-CROWN/blob/main/vnncomp_scripts/prepare_instance.sh#L42

[huanzhang12]

To be clear, MaxPool is supported for CROWN (backward mode bound propagation) and its variants. However it is not implemented in the forward propagation mode for this model.

[mhmd97z]

Got it. Thanks