Assertion Error in auto_LiRPA with ViT Architecture, no support for negative values in BoundReciprocal

[GabrieleRoncolato]

I am experiencing an issue when attempting to apply auto_LiRPA to a standard Vision Transformer architecture inspired on the lucidrains implementation available at: https://github.com/lucidrains/vit-pytorch/blob/main/vit_pytorch/vit.py The following assertion error arises when computing the lower and upper bounds using the IBP+backward method: File "/home/ronco/miniconda3/envs/autolirpa/lib/python3.7/site-packages/auto_LiRPA-0.4.0-py3.7.egg/auto_LiRPA/operators/nonlinear.py", line 580, in interval_propagate assert h_L.min() > 0, 'Only positive values are supported in BoundReciprocal'

I have attempted to isolate the error by removing the attention layers and changing the activation functions (including replacing GELU with ReLU), but to no avail. The error appears to arbitrarily manifest indipendently of these changes.

To Reproduce I am using the dataset and code from the base example present in auto_LiRPA/examples/vision/simple_verification.py The following code shows my model architecture: https://pastebin.com/9y60d6hK This code shows how I'm trying to compute the output bounds using auto lirpa in IBP+backward mode: https://pastebin.com/zM5yPuCt

Error stacktrace The error stacktrace is available at: https://pastebin.com/75HhVGLi

System configuration:

• OS: Ubuntu 22.04
• Python version: 3.7.12
• Pytorch Version: 1.11.0
• Hardware: GTX 1070
• I am still encountering the problem in a clean conda environment, after running through the official installation instructions

[shizhouxing]

Hi @GabrieleRoncolato , thanks for your detailed information for the issue.

It looks like the issue might come from the layer normalization. assert h_L.min() > 0 may fail when the bounds are not tight enough and the denominator in the layer normalization is not certifiably positive. In the paper about Transformer verification (https://openreview.net/pdf?id=BJxwPJHFwS), we discussed removing the variance related terms in layer normalization to make Transformers more verification-friendly (in Section 4.1).

We will soon release a new version of the code containing ViT (a variant with a modified layer normalization) and GeLU.

[GabrieleRoncolato]

Thank you very much, I have defined a custom LayerNormalization module removing the variance and it solved the issue with the normalization layers. However, the softmax function appears to raise the same error. I have read in the paper that softmax too is processed using a BoundReciprocal node, so it must be that although the denominator is strictly positive, its lower bound is approximated as potentially zero or negative?

[shizhouxing]

it must be that although the denominator is strictly positive, its lower bound is approximated as potentially zero or negative?

Yes, I think it was the case. We have fixed the issue and the fix will be included in our next release.