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

Reciprocal AssertionError #78

Open jannickstrobel opened 1 month ago

jannickstrobel commented 1 month ago

Hello together, I am trying to add nonlinear calculations to the ouput of a network, inlcuding a division.

I am using torch.reciprocal for this, by definition, the denominator is >0. Nevertheless, alpha-beta-crown reports an assertion error in BoundReciprocal:

  File "/home/*/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/activation_base.py", line 285, in bound_backward
    self.bound_relax(x, init=True, dim_opt=start_shape)
  File "/home/*/alpha-beta-CROWN/complete_verifier/auto_LiRPA/operators/convex_concave.py", line 131, in bound_relax
    assert x.lower.min() > 0
           ^^^^^^^^^^^^^^^^^
AssertionError

I added a Relu function to clamp the denominator to >0 but this did not resolve the error. These are the lines causing my error:

_C3 = 0.00000144
denominator = torch.add(torch.relu(torch.sub(denominator, _C3)), _C3)            
recip_denom = torch.reciprocal(denominator)

Full output: https://pastebin.com/Bb9WiwFU

System configuration:

Thank you very much for your help already!