verivital / nnv

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

Empty Sets in output of MaxPooling2DLayer #234

Closed m-usama-z closed 3 weeks ago

m-usama-z commented 1 month ago

Hi. It appears that, perhaps due to numerical imprecisions, it is possible for the MaxPooling2DLayer to output some empty ImageStars in the exact mode (some output sets are fine, some are empty). They were detected when gurobi resulted in infeasiblity while attempting to get lower and upper bounds in a subsequent MaxPooling2DLayer. It seems appropriate to check sets for emptiness after reachability analysis of this layer and avoid storing the empty sets. Interestingly, glpk still considered the infeasible problem of obtaining bounds feasible and solved it, so this issue actually went undetected until gurobi was used :)

m-usama-z commented 1 month ago

Actually, it seems that the problem is resolved by using gurobi instead of linprog and passing lp_solver in the following line in the function reach_star_exact in MaxPooling2DLayer.m:

images = obj.stepSplitMultipleInputs(images, pad_image, split_pos(i, :, :), max_index{split_pos(i, 1), split_pos(i, 2), split_pos(i, 3)}, [], lp_solver);

Currently, lp_solver is not being passed here. With this change, there seems to be no need to check for empty sets.

m-usama-z commented 1 month ago

Although, there can still be some issues (potentially somewhere else than MaxPooling2DLayer) which were resolved when I set gurobi's tolerances to the minimum possible, as follows:

        params.OptimalityTol = 1e-09;
        params.FeasibilityTol = 1e-09;
mldiego commented 3 weeks ago

Thanks for catching this one as well! The commit 6e0ff3549899722e76ee0d5be370d85ea82ee975 has fixed this issue.