Wrong verification result for local robustness of MNIST network
Aaron99B opened this issue · 0 comments
Dears,
I want to use Marbou to verify a feed forward MNIST network. I have the problem, that Marabou is giving me wrong answers for my queries. I am trying to check the robustness of the network for different epsilon values, but Marabou always gives me the result UNSAT. I include a vnnlib property file I use and the network I use in the onnx format.
I also tried my setup of for other networks, and for some it seems to work and gives the right results. However for the network I send you in the .zip file it doesn't, while other verifiers like AbCrown can use the network. Do you now if Marabou has a problem reading the network? If there is a problem with my network it would be great to get an error message from the verifier and not just the UNSAT result.
I built Marabou on a linux machine and use it like this in my python code:
options = Marabou.createOptions(timeoutInSeconds=self.timeout, verbosity=0)
network = Marabou.read_onnx(network_path)
exitCode, vars, stats = network.solve(options=options, verbose=False, propertyFilename=str(vnnlib_property_path))
Kindly