Open rdesmartin opened 2 months ago
Hi there, I suspect this is because the default numerical error tolerance is too loose for this network. If you built Marabou from the source, could you try setting some of the numerical error tolerance values to smaller values and recompile?
Set the following to 1e-9 https://github.com/NeuralNetworkVerification/Marabou/blob/3c8e1054ff10d4371525ff1e7e15f18430a2b6d2/src/configuration/GlobalConfiguration.cpp#L81 Set the following to 1e-7 https://github.com/NeuralNetworkVerification/Marabou/blob/3c8e1054ff10d4371525ff1e7e15f18430a2b6d2/src/configuration/GlobalConfiguration.cpp#L93
Hi,
I am working on proof checking for Marabou proofs, and I wanted to raise a case where Marabou concludes that a query is UNSAT (during preprocessing), but running PGD adversarial attack seem to generate satisfying assignments.
The results come from experiments by my colleague Marco Casadio running Marabou as a Vehicle back-end; each Marabou property corresponds to classification robustness within a hyper-rectangle around a correctly classified input from the training data. Here is the network (in ONNX format), the Vehicle-generated Marabou properties and the satisfying assignments (serialised in CSV from numpy, each line is an input point): pgd_ce.zip.
Here is an example query that I ran and the output; Marabou concludes UNSAT at pre-processing so no proof is generated:
Output:
Let me know if you need more info; the full code for the PGD attack can be found here.