Failed Marabou Queries throwing Unknown 'error' instead of 'sat'/'unsat'

[paulsushmita]

Hi,

I was trying to call the Marabou solver in my code to explain NNs. It returns sat/unsat values for a smaller bound of input queries. However, it threw an error value at a later stage where the bounds were increased a bit for the many of input queries.

1. The error reads:

   Engine: Unknown error!
   Input query has been saved as failedMarabouQuery.ipq. Please attach the input query when you open the issue on GitHub.

   Can you please help me understand the reason of it throwing an error (attached the failed query file)? failedMarabouQuery.ipq.zip

2. I am trying to use Marabou non-incrementally as it has the limitation as of now. Will it be possible to generate an explanation or is there any scalability restriction that I must take care of which can resolve this?

[wu-haoze]

Hi @paulsushmita , thanks for your interests in the tool.

When I run ./build/Marabou --input-query failedMarabouQuery.ipq with the latest master branch, I got UNSAT.

Could you answer the following questions so that I can better diagnose the issue:

1. Did you set any flags when running Marabou?
2. Does the issue only happen when you use Marabou incrementally?
3. Did you try the latest master branch?
4. If the issue persisted, could you call network.saveQuery(filename="test.ipq") right before where you called network.solve() and share the test.ipq with me?

I think using Marabou non-incrementally is fine for the network size that you send.

[paulsushmita]

Hi @wu-haoze, thanks for your reply.

To answer your questions:

1. I have not set any flags when running Marabou.
2. I am currently using Marabou non-incrementally. 2a. But I would love to use Marabou incrementally. Can you please share the correct method to do that? (I tried incrementally but I was getting ERROR value and thus, landed to non-incremental calls.)
3. I have checked with the latest code too, and it is still the same.
4. Sure, I have saved the queries (that calls Marabou solver non-incrementally) in test.ipq.zip.

Additionally,

5. After seeing your reply that the failedMarabouQuery.ipq returns you unsat, I made an additional call to the Marabou solver after an ERROR, with the same queries (assuming it would return ERROR). To my surprise, it returned an unsat.
   I will update with comments on further findings.

Thanks.

[paulsushmita]

Update to 5. When I receive an ERROR, I reuse the queries to call the solver non-incrementally again (100 times) and get the following values for each iteration:

unsat
unsat
unsat
ERROR
unsat
ERROR
ERROR
unsat
unsat
ERROR
.
.
.

So, it is not hard to reproduce it as well. I was assuming it can be reproduced when the solver is called multiple times.

6. For what conditions does the solver throw us an ERROR?

[wu-haoze]

@paulsushmita thanks for the update, I’ll take a look at the new query file you sent ASAP. And just to be clear, you called Marabou 100 times on the same query, and it non-deterministically returns ERROR? That would be very surprising.

The solver can return error for different reasons, but generally it should be derterministic.

[paulsushmita]

@wu-haoze yes, that is what I am trying to do.

[At each iteration below, Marabou is called non-incrementally (deleted, loaded with network file and populated with input queries again).] I have all the input values fixed initially (added to a fixed pixel set. I free each pixel (add it to a free pixel set, remove from the fixed pixel set) to an epsilon ball area at each iteration (while other pixels take values according to the set they are in) and check its robustness. If it is robust (unsat), it returns and continues for the next pixel; else remove it from the free set and add it to the fixed pixel set until all pixels are iterated.

I added an else if part above, when an ERROR is encountered, I call the Marabou solver again and it returns non-deterministic solutions (unsat and ERROR).

Let me know if you want me to attach the code file just to be sure the use of Marabou is in the correct manner.

Thanks.

[paulsushmita]

Hi @wu-haoze. Did you get a chance to look into the issue?

[wu-haoze]

Hi @paulsushmita , I’ll get back to you in a day.

[wu-haoze]

@paulsushmita , I'm able to reproduce the error on my end. The crashes stem from the implementation of the Max constraint. I think it will take some additional time for me to pose a fix, but there are two solutions for now:

1. Change your network to not use Max pool.
2. Build Marabou with Gurobi (I obtained UNSAT running the default configuration of Marabou).

When Gurobi is built, I would further try setting the option options = Marabou.createOptions(verbosity = 0, solveWithMILP=True, numWorkers=[# of available processors]) network.solve(options = options) to see if this improves runtime efficiency.

You're probably already using the Marabou.createOptions method? See https://github.com/NeuralNetworkVerification/Marabou/blob/master/maraboupy/examples/2_ONNXExample.py for an example.

[paulsushmita]

Thanks for the suggestions @wu-haoze. I have modified my network and not using Max pool currently. It works fine now without throwing ERROR. Also, thanks for the suggestion of using options (I was using Marabou.solve(verbose=False) previously and that did not really work).

Leaving this issue open for you to close:

The crashes stem from the implementation of the Max constraint.