Wrong verification result for local robustness of MNIST network

[Aaron99B]

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))

Archiv.zip

Kindly