A problem of "Domain notes" #1
Description
Hello,
In your README.md file of this project:
A variant of the original DeepPoly domain is implemented where the ReLU approximation is not heuristically choosing between two choices (either picking y = x or y = 0 as the new upper bound). Right now it is fixed to choosing y = 0, because there was Galois connection violation observed if this heuristic is enabled. Basically, it is observed in experiment that a smaller abstraction may unexpectedly incur larger safety distance than its containing larger abstraction.
I guess "either picking y = x or y = 0 as the new upper bound" may be "either picking y = x or y = 0 as the new lower bound".
And you said that there was Galois connection violation if the heuristic is enabled. Would you like to tell me if there is any paper or proof to support this appearance If it's not too much trouble？
Thank you！