search

NeuralNetworkVerification / Marabou

Other
264 stars 90 forks source link

exitCode "Not_DONE" #842

Open YourSaDady opened 2 months ago

YourSaDady commented 2 months ago

Hi developers! I try to solve a query using the MarabouNetworkONNX, and the exitCode that the .solve() returns is NOT_DONE. What does this result means?

The Marabou I use is just cloned, so I think there shouldn't be any issue with the version. The simple ONNX network looks like this: decoder_softmax

YourSaDady commented 1 month ago

Could the prolem be that the current Marabou doesn't support flexible input dimension while ONNX does?

YourSaDady commented 1 month ago

My query-solving options is set to Marabou.createOptions(snc=True, verbosity=0, initialSplits=2, timeoutInSeconds=1800).

I searched keyword NOT_DONE in the repository, and it seems that it only appears in DnCManager class. However, I didn't use the DnC mode.

YourSaDady commented 1 month ago

My query constraint and model constraint should be error-free: For the model constraint, I used the ONNX model to do inference and the generated result was as expected. For the query constraint, I tested a trivial case where the returned result should be SAT when the perturbation on the inputVars is small. However, as I increased the perturbation on the inputVars, the exitCode changes from SAT to UNSAT and then to NOT_DONE. I find it hard to explain this.

YourSaDady commented 1 month ago

For my case, the time_stamp dimension in the input and output of the ONNX model are flexible (different among different sample cases). However, after read_onnx(), the corresponding dimension becomes 1 for inputVars and outputVars.