Error Zonotope/evaluation neuralNetworkOld

[phK3]

Concrete evaluation of neuralNetworkOld and overapproximate evaluation with zonotopes gives wrong results.

The execution of the following code:

net = neuralnetwork2cora('./networks/CAS/ACASXU_experimental_v2a_1_8.nnet');
[in_spec, out_spec] = vnnlib2cora('./vnncomp2022_benchmarks/benchmarks/acasxu/vnnlib/prop_3.vnnlib');
z = zonotope(in_spec{1});
interval(net.evaluate(z))

produced the output

ans =

  [0.0000, 0.0000]
  [0.0000, 0.0000]
  [0.0000, 0.0000]
  [0.0000, 0.0000]
  [0.0000, 0.0000]

The concrete evaluation also results in

>> net.evaluate(in_spec{1}.inf)

ans =

     0
     0
     0
     0
     0

However, evaluating the same .nnet network in a different program or loading the corresponding .onnx network in CORA results in the output of

>> acas = neuralNetwork.readONNXNetwork('./vnncomp2022_benchmarks/benchmarks/acasxu/onnx/ACASXU_run2a_1_8_batch_2000.onnx', true, 'BSSC', 'BC');
>> acas.evaluate(in_spec{1}.inf)

ans =

  5×1 single column vector

   -0.0203
   -0.0191
   -0.0191
   -0.0180
   -0.0180

The .nnet networks are available in this repo, while the .onnx networks and .vnnlib specifications are available in this repo.

[toladnertum]

Dear @phK3,

Thank you very much for addressing this issue.

As far as I am aware, the NNET format is ambiguous with respect to the final activation layer. The format only implicitly adds ReLU as activation functions, thus, it is unclear if there should be an activation layer after the last linear layer.

CORA adds a ReLU activation after each linear layer, which results in the described zero vector as an output vector. We prefer the ONNX format due to this ambiguity.

Hope that helps!

---

Note: CORA gets a big update regarding the verification of neural networks with the next major release, which eliminates the neuralNetworkOld class.

[toladnertum]

Closing this issue as CORA v2024 is now released.