'NoneType' object has no attribute 'ndim' when verifiying nonlinear network

[jannickstrobel]

Bug Description

I am trying to verify a small network containing multiple nonlinearities. While the initial CROWN bound calculation works, there is an error in the first BaB round:

Exception has occurred: AttributeError
'NoneType' object has no attribute 'ndim'
  File "/home/strobel/alpha-beta-CROWN/complete_verifier/heuristics/nonlinear/bbps.py", line 485, in _fast_backward_propagation
    if bound.ndim < 3:

System configuration:

• OS: Ubuntu 24.04.2
• Python version: Python 3.11.9
• Pytorch Version: PyTorch2.3.1
• 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

Screenshots

The error occurs in file bbps.py in the "_fast_backward_propagation" method. When the name of the current node is not in "lAs", bound is None in Line 485.

Full program run output: output.txt
Config file: config.txt

[shizhouxing]

Could you share your model definition?

…

On Mar 13, 2025, at 3:24 PM, Huan Zhang ***@***.***> wrote: Assigned #91 <#91> to @shizhouxing <https://github.com/shizhouxing>. — Reply to this email directly, view it on GitHub <#91 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACUBAREC4LFZFQ5AZU2UXIT2UHLPXAVCNFSM6AAAAABY3UDS46VHI2DSMVQWIX3LMV45UABCJFZXG5LFIV3GK3TUJZXXI2LGNFRWC5DJN5XDWMJWG42DQMZSGQ2DCNA>. You are receiving this because you were assigned.

[jannickstrobel]

Hello,

my model definition looks like this:

class Network(nn.Module):
    def __init__(self, input_dim, hidden_neurons, output_size):
        super().__init__()
        self.prepare = False
        self.input_dim = input_dim
        self.input_size = np.prod(input_dim)
        self.output_size = output_size

        # Input Layer
        layers = [nn.Linear(self.input_size, hidden_neurons[0]), nn.ReLU()]

        # Hidden Layer
        for i in range(1, len(hidden_neurons)):
            layers.append(nn.Linear(hidden_neurons[i - 1], hidden_neurons[i]))
            layers.append(nn.ReLU())

        # Output Layer
        layers.append(nn.Linear(hidden_neurons[-1], self.output_size))

        # Combined Model
        self.network = nn.Sequential(*layers)
        self.loss_fn = nn.CrossEntropyLoss() 
        self.optimizer = torch.optim.SGD(self.parameters(), lr=0.01, momentum=0.9)

        self.cl = 2
        self.ri = load_and_transform_image(f"abc/ri/{self.cl:05}.png", self.input_dim)

    def forward(self, x):

        def metric_mse(input1, input2):
            input1 = input1.to(device='cuda')
            input2 = input2.to(device='cuda')

            diff = torch.sub(input1, input2)
            squared_diff = torch.square(diff)
            mse = torch.mean(squared_diff, dim=1, keepdim=True)

            return mse
        
        if self.prepare:
            output = self.network(x)
        else:         
            eps = torch.tensor([[1e-9]]).to(device='cuda')   
            cl = torch.tensor([self.cl]).to(device='cuda')
            ri = self.ri.unsqueeze(0)

            metric_val = metric_mse(x, ri)
            pred       = self.network(x).to(device='cuda')
            max_out, _ = torch.max(pred, dim=1, keepdim=True)

            cl_pred = torch.add(pred.index_select(1, cl), eps)
            class_wrong = torch.sub(max_out, cl_pred)           # >= 0 if class is wrong eps is causing the error!
            metric_corr = metric_val - 0.99                     # >= 0 if metric is correct  
            
            conc = torch.cat((class_wrong, metric_corr), dim=1)
            output, _ = torch.min(conc, dim=1, keepdim=True)
            #output = torch.cat((class_wrong, metric_corr), dim=1)

        return output

my config looks like this:

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.
  sparse_alpha: false
  sparse_interm: false
  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-refine  # 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: false  # Enable/Disable initial alpha-CROWN incomplete verification (disable this can save GPU memory).

model:
  name: Customized("abc_model.py", "Network", input_dim=(3,3,3), hidden_neurons=[3, 3], output_size=3)
  path: abc/abc_model.pth
  input_shape: [ -1, 27 ] #[ -1, 3, 10, 10 ] 

specification:
  vnnlib_path: abc/property_vec.vnnlib

solver:
  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".
  batch_size: 32
  auto_enlarge_batch_size: true

bab:
  decision_thresh: 0
  pruning_in_iteration: true
  sort_domain_interval: 1
  timeout: 360000
  branching:
    method: nonlinear
    candidates: 3
    reduceop: max
    #branching_input_and_activation: true
    nonlinear_split:
      num_branches: 2
      method: shortcut
      filter: true

debug:
  view_model: false

attack:
  pgd_order: skip