Wrong evaluation results of NLR on specific input

[idan0610]

Hello,

I'm trying to verify the given onnx network (both input and output are of size 1) with the given vnnlib property, but I get a spurious counterexample. I use the following terminal command:

Marabou/build/Marabou dp-net_0.onnx dp-net_0.vnnlib

After some debugging, I noticed that, when I call the evaluate() method of the NLR object on a specific input, I get the wrong output. For example, if I add the following code snippet after the call to initializeNetworkLevelReasoning() in processInputQuery() in Engine.cpp:

double *inp = new double[1];
double *out = new double[1];
inp[0] = 1.5;
_networkLevelReasoner->evaluate(inp, out);
std::cout << "input: " << *inp << "; output: " << *out << std::endl;
delete[] inp;
delete[] out;

I get the following print:

input: 1.5; output: 8.37823

But running the given onnx network directly with onnxruntime:

import onnxruntime as ort

session = ort.InferenceSession("dp-net_0.onnx"))
input_name = session.get_inputs()[0].name
input_data = np.array([[1.5]], dtype=np.float32)
output_data = session.run(None, {input_name: input_data})

print(output_data[0][0,0])

Gives the output 24.654705.

My suspicion is that it is related to the C++ version of the ONNX parser. When I try to load this network in debug mode, I get:

Assertion violation! File /home/idan0610/Marabou_dev/for_elbit_new/Marabou/src/input_parsers/TensorUtils.cpp, line 43

Thanks for your help on this issue!

dp-net_0.zip

[MatthewDaggitt]

Hi @idan0610 that does indeed sound like there's at least one bug in the C++ parser. I'll try and get some time to look at next week, but in the mean time, any chance you could shrink the network to the minimal example that triggers the bug? As you've already got the debugger up and running, you should be able to work out which layer is causing it fairly easily?

[idan0610]

Here is a small version of the network, where the problem still persists

Thanks Matthew!

dp-net_0_small.zip