Input linear constraint about alpha-beta-crown HOT 4 OPEN

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

from alpha-beta-crown.

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.

from alpha-beta-crown.

@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.

from alpha-beta-crown.

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

from alpha-beta-crown.