verivital / nnv

Neural Network Verification Software Tool
http://www.verivital.com
108 stars 48 forks source link

Issue in ImageStar estimateRanges #237

Closed m-usama-z closed 2 weeks ago

m-usama-z commented 1 month ago

Hi. The update to the estimateRanges function in ImageStar.m in f06303b introduced the following lines:

                x1 = obj.V(:,:,:,1) + tensorprod(obj.V(:,:,:,2:end), obj.pred_lb, 4, 1);
                x2 = obj.V(:,:,:,1) + tensorprod(obj.V(:,:,:,2:end), obj.pred_ub, 4, 1);
                image_lb = min(x1,x2);
                image_ub = max(x1,x2);

instead of the previous code that utilizes the estimateRange function. The previous code, in estimateRange, obtains:

    1. Lower bound by multiplying 
             - lower bounds of predicate variables with positive elements of V, and
             - upper bounds of predicate variables with negative elements of V.

    2. Upper bound by multiplying
             - lower bounds of predicate variables with negative elements of V, and
             - upper bounds of predicate variables with positive elements of V.

In doing so, the worst-case bounds are obtained, which would have been the true bounds if not for the constraints other than the upper and lower bounds. But the new code above seems to be doing something different. Can anyone kindly clarify if I'm mistaken and how the new code is working? From my understanding, the estimateRanges function is supposed to provide over-approximate bounds, but not under-approximate bounds; does that not make the above code wrong? Thank you very much for any guidance.

m-usama-z commented 1 month ago

On another note, there seems to be a redundant function named estimageRange in ImageStar.m.

m-usama-z commented 1 month ago

Coming back to the original issue, thank you for the use of the tensorprod function still. With that, the aforementioned "correct logic" (in my opinion) is implemented as follows:

                gens = obj.V(:,:,:,2:end);
                pos_gens = gens;
                pos_gens(gens < 0) = 0;
                neg_gens = gens;
                neg_gens(gens > 0) = 0;
                image_lb = obj.V(:,:,:,1) + tensorprod(pos_gens, obj.pred_lb, 4, 1) + tensorprod(neg_gens, obj.pred_ub, 4, 1);
                image_ub = obj.V(:,:,:,1) + tensorprod(pos_gens, obj.pred_ub, 4, 1) + tensorprod(neg_gens, obj.pred_lb, 4, 1);
mldiego commented 3 weeks ago

Can you provide an example where the original function fails to estimate the overapproximate ranges?

From my understanding, and the few tests I ran, they are computing the same lower and upper bounds.

m-usama-z commented 3 weeks ago

Sorry about my last comment (that I've deleted), I was mistaken today instead of before 😅. Anyways, to answer your question, this simple example should do the trick:

clear
V(1,1,1,1) = 0;
V(1,1,1,2) = -1;
V(1,1,1,3) = 1;
C = [0 0];
d = 0;
ub = [1; 1];
lb = -ub;

I = ImageStar(V, C, d, lb, ub);

[lb1, ub1] = I.estimateRanges_old;
I.im_lb = [];
I.im_ub = [];
[lb2, ub2] = I.estimateRanges_maybe_wrong;

disp([lb1, ub1])
disp([lb2, ub2])
disp(norm([lb1, ub1] - [lb2, ub2], 'fro'))

with the code before your change, or the code I supplied in the comment above, being in the estimateRanges_old function and your code being in the estimateRanges_maybe_wrong function. You should see the output:

    -2     2

     0     0

    2.8284

where [-2, 2] are the correct bounds, and [0, 0] are the wrong bounds. Please let me know if I'm mistaken in any way. Thank you again.

mldiego commented 2 weeks ago

Thank you for providing the example, I have fixed this error in #240