AssertionError on act.inputs

[jannickstrobel]

Describe the bug I am trying to verify a specification based on a metric by joining the original network and the metric into a new network.

The BnB part of the verification returns an AssertionError

assert len(act.inputs) == 1
           ^^^^^^^^^^^^^^^^^^^^
AssertionError

To Reproduce .yaml file:

general:
  device: cuda  # Select device to run verifier, cpu or cuda (GPU).
  conv_mode: patches  # Convolution mode during bound propagation: "patches" mode (default) is very efficient, but may not support all architecture; "matrix" mode is slow but supports all architectures.
  save_adv_example: false  # Save returned adversarial example in file.
  eval_adv_example: false  # Whether to validate the saved adversarial example.
  show_adv_example: true  # Print the adversarial example.
  complete_verifier: bab  # Complete verification verifier. "bab": branch and bound with beta-CROWN or GCP-CROWN; "mip": mixed integer programming (MIP) formulation; "bab-refine": branch and bound with intermediate layer bounds computed by MIP; "Customized": customized verifier, need to specially def by user.
  enable_incomplete_verification: true  # Enable/Disable initial alpha-CROWN incomplete verification (disable this can save GPU memory).
  results_file: out.txt  # Path to results file.
  save_output: false  # Save output for test.
  output_file: out.pkl  # Path to the output file.
  return_optimized_model: false  # Return the model with optimized bounds after incomplete verification is done.
model:
  name: Customized("custom_net", "Network")
  path: alpha-beta-CROWN/complete_verifier/models/custom_net/custom_net.pth
  input_shape: [ 1, 300 ] #[ -1, 3, 10, 10 ] 
specification:
  vnnlib_path: alpha-beta-CROWN/complete_verifier/exp_configs/custom/custom_net.vnnlib
solver:
  batch_size: 2048  # Batch size in bound solver (number of parallel splits).
  bound_prop_method: alpha-crown  # Bound propagation method used for incomplete verification and input split based branch and bound.
  init_bound_prop_method: same  # Bound propagation method used for the initial bound in input split based branch and bound. If "same" is specified, then it will use the same method as "bound_prop_method".
bab:
  branching:
    method: kfsb  # Branching heuristic. babsr is fast but less accurate; fsb is slow but most accurate; kfsb is usually a balance; kfsb-intercept-only is faster but may lead to worse branching; sb is fast smart branching which relies on the A matrix.
    candidates: 4  # Number of candidates to consider when using fsb or kfsb. More candidates lead to slower but better branching.
    reduceop: min  # Reduction operation to compute branching scores from two sides of a branch (min or max). max can work better on some models.
    input_split:
      enable: false  # Branch on input domain rather than unstable neurons.
      show_progress: true  # Show progress during input split.

The specification asserts that the input for every input variable is in range (-1, 1) and the output is <= 0

(assert (<= X_0 1))
(assert (>= X_0 -1))
(assert (<= X_1 1))
(assert (>= X_1 -1))
...

(assert (<= Y_0 0))

Network:

...
self.sequential = nn.Sequential(
            nn.Linear(input_size, relu_layer_size),
            nn.ReLU(),
            nn.Linear(relu_layer_size, relu_layer_size),
            nn.ReLU(),
            nn.Linear(relu_layer_size, 43)
        )

...

def forward(self, input): 
        def metric_mse(input1, input2):
            input1 = input1.to(device='cuda')
            input2 = input2.to(device='cuda')
            temp = (input1 - input2) ** 2
            mse = torch.mean(temp, dim=tuple(range(1, input1.dim())), keepdim=True)
            similarity = 1 - mse
            return similarity

        def join(input):
            metric_val  = metric_mse(input, self.reference)
            pred        = self.sequential(input).to(device='cuda')
            diff        = pred[0, self.cl] - pred
            min_val     = torch.min(diff, dim=1, keepdim=True)[0]
            met_val     = self.threshold - metric_val
            concat      = torch.cat((min_val, met_val), dim=1)
            output      = torch.max(concat, dim=1, keepdim=True)[0]
            return output

System configuration:

• OS: Ubuntu 20.04.
• Python version: 3.11.8
• Pytorch Version: 2.2.1
• Have you tried to reproduce the problem in a cleanly created conda environment using official installation instructions and the latest code on the main branch?: Yes

Full error trace:

Traceback (most recent call last):
  File "/home/js/alpha-beta-CROWN/complete_verifier/abcrown.py", line 706, in <module>
    abcrown.main()
  File "/home/js/alpha-beta-CROWN/complete_verifier/abcrown.py", line 684, in main
    verified_status = self.complete_verifier(
                      ^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/js/alpha-beta-CROWN/complete_verifier/abcrown.py", line 481, in complete_verifier
    l, nodes, ret = self.bab(
                    ^^^^^^^^^
  File "/home/js/alpha-beta-CROWN/complete_verifier/abcrown.py", line 294, in bab
    result = general_bab(
             ^^^^^^^^^^^^
  File "/home/js/alpha-beta-CROWN/complete_verifier/bab.py", line 308, in general_bab
    global_lb = act_split_round(
                ^^^^^^^^^^^^^^^^
  File "/home/js/alpha-beta-CROWN/complete_verifier/bab.py", line 164, in act_split_round
    split_domain(net, domains, d, batch, impl_params=impl_params,
  File "/home/js/alpha-beta-CROWN/complete_verifier/bab.py", line 65, in split_domain
    branching_heuristic.get_branching_decisions(
  File "/home/js/miniconda3/envs/alpha-beta-crown/lib/python3.11/site-packages/torch/utils/_contextlib.py", line 115, in decorate_context
    return func(*args, **kwargs)
           ^^^^^^^^^^^^^^^^^^^^^
  File "/home/js/alpha-beta-CROWN/complete_verifier/heuristics/kfsb.py", line 64, in get_branching_decisions
    score, intercept_tb = self.babsr_score(
                          ^^^^^^^^^^^^^^^^^
  File "/home/js/alpha-beta-CROWN/complete_verifier/heuristics/babsr.py", line 121, in babsr_score
    b_temp = get_preact_params(layer)
             ^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/js/alpha-beta-CROWN/complete_verifier/heuristics/utils.py", line 30, in get_preact_params
    assert len(act.inputs) == 1
           ^^^^^^^^^^^^^^^^^^^^
AssertionError

Content of act.inputs at the error breakpoint:

[shizhouxing]

Hi @jannickstrobel ,

Since your model contains some nonlinearities (square function) other than ReLU, you'll need to use the BBPS heuristic proposed in this paper instead of kFSB which is only for ReLU models. An example is ML4ACOPF.

[jannickstrobel]

Thank you very much for the quick help, with your comment I was able to fix the error!