mnmueller
commented
3 years ago Hello @debtanu97,
Per default, ERAN only tries to verify a property and not falsify it. "Failed" simply means that the property could not be proven (with the chosen evaluation mode).
To reduce runtime, we might terminate an optimization process before a feasible solution is found if a failure to certify can already be shown, this will lead to a "Failed" output, despite a continued search maybe generating a counterexample. Further, even if a feasible solution to the optimization problem is found that violates the safety property, the corresponding example might not actually violate the safety property (due to the relaxations introduced).
To actively search for counterexamples, please set --complete True. Note that this will increase runtime substantially.
Cheers, Mark
debtanu97
Hi Sir, (In Reference to Issue #64 )
Sorry for commenting on a closed issue. I was able to acquire a gurobi license and using the refinepoly domain. But most of the images for the mnist_relu_3_100.tf network, started giving a "Failed" verdict with an epsilon value 0.1.
But going by your paper on "An Abstract domain for Certifying Neural Networks", shouldn't it be the fact that an image for which we want to satisfy a property with large epsilon values(lets say 0.5) should be marked unsafe? Since, in the worst case we end up changing all pixel values by 0.5 and the resulting image might not look like the original image at all and the NN would not classify this as being the original image hence not satisfying our property.
Could you clarify what a "Failed" verdict means? - In the Readme file it is meantioned that when deeppoly/refinepoly cannot give Verify Safe or Unsafe. Does it mean that, on increasing the timeout limit we can actually get a safe/unsafe verdict?
Thank You