Unknown results for ReLU networks in ERAN benchmark

[JacksonZyy]

Hi,

I followed your instructions online to run robustness verification on ERAN benchmark, eg:
python robustness_verifier.py --config exp_configs/mnist_conv_small.yaml
but change the epsilon from 0.12 to 0.11.
I also used the same parameter configuration in mnist_6_100.yaml to run on ERAN mnist_3_100 and mnist_5_100.
Since alpha-beta-CROWN should be a complete tool for ReLU-activated networks, I am confused that there are still some images with inconclusive results.
May I ask why this is the case? And how may I run it with complete behavior?
Thank you so much for your help!

[huanzhang12]

Thank you for reaching out!
It is very normal that some images have "unknown" verification results. alpha-beta-CROWN is complete in the sense that given an infinite time it will produce an answer. However, NN verification is theoretically an NP-complete problem, and there are hard instances that cannot be solved quickly. All the complete verifiers so far just try to solve as many as possible given a specific timeout limit. You can try to increase the timeout, however, on most networks, we won't expect it to solve completely within a few minutes timeout.

[JacksonZyy]

Thanks for your explanation!