search

eth-sri / eran

ETH Robustness Analyzer for Deep Neural Networks
Apache License 2.0
320 stars 103 forks source link

Unable to get a "Verified Unsafe" verdict on any image on running deeppoly #64

Closed debtanu97 closed 3 years ago

debtanu97 commented 3 years ago

Sir,

I am trying to use DeepPoly to certify robustness of the Deep NN models already present on the repo : mnist_relu_3_50.tf and all the other .tf files based on the mnist_test.csv dataset present. But I am always getting the verditc of either "Verified" or "Failed" and never a "Verified Unsafe" verdict. Could you point out to a dataset and a corresponding model which which give a "Verified Unsafe" verdict. I want to use the tool to certify some of my own NN models against some specifications, and hence am trying to familiarize myself with the tool. Could you please help me out by pointing out to a "Verified Unsafe" example?

Thank You

GgnDpSngh commented 3 years ago

Hi there,

Thanks for your interest in using ERAN. Currently, we do not support counterexamples when running the analysis with only the DeepPoly domain. In order to obtain counterexamples on this network, you can add the option "--complete True" or run with "refinepoly" domain. Let me know if it works.

Cheers, Gagandeep Singh

debtanu97 commented 3 years ago

Hi Sir,

Thanks for the reply I did try to use the options suggested by you, but the tool showed the following error : "gurobipy.GurobiError: No Gurobi license found (user deeppoly, host deeppoly, hostid 3a1cbe7e, cores 1)". Although I did install Gurobi in my system using the instructions mentioned in the Readme file, there is some license issue. Can you suggest a fix for this?

Thank You

GgnDpSngh commented 3 years ago

Hi there,

You would need to acquire a license from Gurobi, e.g., here: https://www.gurobi.com/academia/academic-program-and-licenses/

Cheers, Gagandeep Singh

debtanu97 commented 3 years ago

Hi Sir,

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