NeuralNetworkVerification/Marabou

collins_rul_cnn benchmark: Operation Dropout not implemented

hatoruday opened this issue · 2 comments

Hello,

I am attempting to use Marabou to verify the collins_rul_cnn model from the vnncomp2022 repository. While there exists a benchmark result for Marabou in the vnncomp2023_results repository, I encounter an issue when trying to load the ONNX model for the collinsCNN model.

Upon executing the following code:

Copy code
print("\nConvolutional Network about Collins Example")
filename = '../../vnncomp2023_benchmarks/benchmarks/collins_rul_cnn/onnx/NN_rul_full_window_40.onnx'
network = Marabou.read_onnx(filename)

I receive the following error indicating that the Dropout operation is not implemented:

Copy code
NotImplementedError: Operation Dropout not implemented
---------------------------------------------------------------------------
NotImplementedError                       Traceback (most recent call last)
Cell In[6], line 3
      1 print("\nConvolutional Network about Collins Example")
      2 filename = '/vnncomp2023_benchmarks/benchmarks/collins_rul_cnn/onnx/NN_rul_full_window_40.onnx'
----> 3 network = Marabou.read_onnx(filename)

File ~/.conda/envs/marabou2/lib/python3.9/site-packages/maraboupy/Marabou.py:75, in read_onnx(filename, inputNames, outputNames)
     64 def read_onnx(filename, inputNames=None, outputNames=None):
     65     """Constructs a MarabouNetworkONNX object from an ONNX file
     66 
     67     Args:
   (...)
     73         :class:`~maraboupy.MarabouNetworkONNX.MarabouNetworkONNX`
     74     """
---> 75     return MarabouNetworkONNX(filename, inputNames, outputNames)

File ~/.conda/envs/marabou2/lib/python3.9/site-packages/maraboupy/MarabouNetworkONNX.py:36, in MarabouNetworkONNX.__init__(self, filename, inputNames, outputNames)
     34 def __init__(self, filename, inputNames=None, outputNames=None):
     35     super().__init__()
---> 36     self.readONNX(filename, inputNames, outputNames)

File ~/.conda/envs/marabou2/lib/python3.9/site-packages/maraboupy/MarabouNetworkONNX.py:74, in MarabouNetworkONNX.readONNX(self, filename, inputNames, outputNames, preserveExistingConstraints)
     71     initNames = [node.name for node in self.graph.initializer]
     72     self.outputNames = [out.name for out in self.graph.output if out.name not in initNames]
...
    209     self.subEquations(node, makeEquations)
    210 else:
--> 211     raise NotImplementedError("Operation {} not implemented".format(node.op_type))

NotImplementedError: Operation Dropout not implemented

It appears that the MarabouNetworkONNX class does not have an implementation for the Dropout operation. I am curious about how the experiment results for the Collins CNN model were obtained given this limitation. Were there any specific modifications or workarounds used to bypass or handle layers with the Dropout operation in the ONNX model?

Any guidance or insights on how to proceed with verifying the Collins CNN model using Marabou would be greatly appreciated. Thank you in advance for your assistance.

Hi @hatoruday , to reproduce the competition results you need to use the competition branch https://github.com/wu-haoze/Marabou/tree/vnn-comp-23.

Dropout was implemented there, but not merged to master. I created a PR #774 which adds dropout support.

You could pull that branch or wait until that PR is merged and pull/rebuild the master. On that branch, the following script seems to work.

from maraboupy import Marabou
from maraboupy import MarabouCore

net = Marabou.read_onnx("./NN_rul_full_window_20.onnx")
q = net.getInputQuery()
MarabouCore.loadProperty(q, "./vnncomp2022/vnnlib/robustness_2perturbations_delta10_epsilon10_w20.vnnlib")                                                                                                        
options = Marabou.createOptions(numWorkers=32, solveWithMILP=True)
Marabou.solve_query(q, options=options)

I successfully pulled your branch! thank you for your assistance.