Questions in the paper

[ytsao]

Hi,

I'm interested about the forward-backward abstract interpretation method in the paper, Scalable Verification of GNN-Based Job Schedulers.
While I met some problems in the example that provided in the paper, I found there is typo and unclear numbers in the Figure 2.

1. In the blue area, should the lower bound for x8 be -0.0045?
2. I was testing this simple network by CROWN which is using the same abstract method as DeepPoly, yet I have different bounds for x10 & x11. Here is the intervals I have for these two neurons, x10 \in [-2.050, 0.3450], x11 \in [1.73, 4.33]. It seems I have same lower bound for x10 and upper bound for x11. I'm not sure which one is correct.
3. I'm using the updated bounds for x10 and x11 to start backward analysis, by using Gurobi to solve the provided optimization problem to compute the new upper bound for x9. While I got the resulting upper bound should be -0.4775, it is even lower than its old lower bound, so by the termination logic, it should be terminated in x8 and x9 layer not x4s' layer. Could you please explain how do you have a new upper bound (-0.275) to me?

Those are the problems and questions I have so far, If I understood incorrectly please correct me, thanks!

Best regards,
Yi-Nung