search

Verified-Intelligence / alpha-beta-CROWN

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

Sequence of Conv1d Error #41

Closed mhmd97z closed 1 year ago

mhmd97z commented 1 year ago

Thanks for adding the support for conv1d in the new release.

I get the following error when I have a sequence of two conv1d in my network architecture:

class MyModel(nn.ModuleList):
        def __init__(self, device=torch.device("cpu")):
            super(MyModel, self).__init__()        
            self.to(device)
            self.af = nn.ReLU()
            self.lin1 = nn.Linear(19, 15)
            self.c1d_1 = torch.nn.Conv1d(1, 24, 15)
            self.c1d_2 = torch.nn.Conv1d(24, 1, 1)

       def forward(self, obs):
            lin1 = self.af(self.lin1(obs))
            after_conv1 = self.af(self.c1d_1(lin1.unsqueeze(dim=0)))
            after_conv2 = self.af(self.c1d_2(after_conv1))
            return after_conv2[0]

The error:

Traceback (most recent call last):
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 612, in <module>
    abcrown.main()
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 591, in main
    verified_status = self.complete_verifier(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 416, in complete_verifier
    l, nodes, ret = self.bab(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 241, in bab
    result = general_bab(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/bab.py", line 246, in general_bab
    global_lb, ret = net.build(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 455, in build
    lb, ub, aux_reference_bounds = self.net.init_alpha(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/optimized_bounds.py", line 766, in init_alpha
    l, u = self.compute_bounds(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1206, in compute_bounds
    return self._compute_bounds_main(C=C,
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1303, in _compute_bounds_main
    self.check_prior_bounds(final)
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
    self.check_prior_bounds(n)
  [Previous line repeated 3 more times]
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 804, in check_prior_bounds
    self.compute_intermediate_bounds(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 910, in compute_intermediate_bounds
    node.lower, node.upper = self.backward_general(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/backward_bound.py", line 337, in backward_general
    lb = lb.view(batch_size, *output_shape) if bound_lower else None
RuntimeError: view size is not compatible with input tensor's size and stride (at least one dimension spans across two contiguous subspaces). Use .reshape(...) instead.

I tried the solutions I found online (replacing view by reshape AND adding contiguous() before view()), but it throws another error:

Traceback (most recent call last):
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 612, in <module>
    abcrown.main()
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 591, in main
    verified_status = self.complete_verifier(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 416, in complete_verifier
    l, nodes, ret = self.bab(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/abcrown.py", line 241, in bab
    result = general_bab(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/bab.py", line 246, in general_bab
    global_lb, ret = net.build(
  File "/home/mzi/sys-rl-verif/alpha-beta-CROWN/complete_verifier/beta_CROWN_solver.py", line 455, in build
    lb, ub, aux_reference_bounds = self.net.init_alpha(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/optimized_bounds.py", line 766, in init_alpha
    l, u = self.compute_bounds(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1206, in compute_bounds
    return self._compute_bounds_main(C=C,
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 1303, in _compute_bounds_main
    self.check_prior_bounds(final)
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 800, in check_prior_bounds
    self.check_prior_bounds(n)
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 804, in check_prior_bounds
    self.compute_intermediate_bounds(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/bound_general.py", line 915, in compute_intermediate_bounds
    self.restore_sparse_bounds(
  File "/home/mzi/anaconda3/envs/crown/lib/python3.9/site-packages/auto_LiRPA-0.4.0-py3.9.egg/auto_LiRPA/backward_bound.py", line 584, in restore_sparse_bounds
    lower[:, unstable_idx] = new_lower.view(batch_size, -1)
RuntimeError: shape mismatch: value tensor of shape [1331] cannot be broadcast to indexing result of shape [1, 11]
shizhouxing commented 1 year ago

Hi @mhmd97z , currently the library requires that the batch dimension is fixed. I see you have lin1.unsqueeze(dim=0) which seems to alter the batch dimension. Could you please avoid this unsqueeze by adding the batch dimension in obs before it's passed into the model?

mhmd97z commented 1 year ago

Thanks for your response. It fixed the issue.