Input linear constraint

[cong-liu-2000]

It seems that input linear constraint (e.g., x_1 > x_2) is not supported. I got the following error message.

File "alpha-beta-CROWN/complete_verifier/read_vnnlib.py", line 80, in update_rv_tuple
f"input constraints must be box ({op} {first} {second})"
AssertionError: input constraints must be box

Is there a plan to support input linear constraint in the near future?

[huanzhang12]

Thank you for reaching out to us! Currently, it is not supported. If you have a good use case for this, we can consider adding this feature in the near future. Can you provide a bit more details on the application case? Feel free to send me an email and we can find some time to chat.

Thanks,
Huan

[cong-liu-2000]

We want to check if a NN function is monotonic. The idea is to concat two side-by-side copies of the NN, and check if x(i) > x'(i) => y(i) > y'(i) while other x(j)= x'(j), j != i.

[huanzhang12]

@cong-liu-2000 Thanks for providing the details! In this case, you can use the technique based on Jacobian to provide verification on monotonicity. You can check out the description in section 5.3 in this paper (Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagation, NeurIPS 2022): https://arxiv.org/pdf/2210.07394.pdf

The current version of the autoLiRPA library does support Jacobian bounds and monotonicity analysis, and you can use this file as an example. https://github.com/Verified-Intelligence/auto_LiRPA/blob/master/examples/vision/jacobian.py

In addition, we will release the next version of autoLiRPA very soon and it will include a better API for Jacobian analysis.

[cong-liu-2000]

What you refer to seems to check "local" monotonicity. But I am interested in "global" monotonicity.