Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix incorrect variable indices in maraboupy MarabouNetwork.varMap #440

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

Reginhar
Copy link

@Reginhar Reginhar commented Mar 3, 2021

When playing around with maraboupy, I wanted to add some constraints on the values of the hidden nodes, but I noticed that the variable indices listed in varMap were incorrect. For the purpose of this test, I am using a simple network (linked below) with four inputs, one ReLU hidden layer with three nodes, and two outputs. Here is the old situation:

>>> from maraboupy import Marabou

>>> marabou_network = Marabou.read_onnx("my-nn.onnx")
>>> print(marabou_network.inputVars)
[array([[0, 1, 2, 3]])]
>>> print(marabou_network.outputVars)
[[4 5]]
>>> print(marabou_network.varMap)
{'input.1': array([[0, 1, 2, 3]]), '5': array([[4, 5, 6]]), '6': array([[7, 8, 9]]), '7': array([[4, 5]])}

As you can see, the indices 4 and 5 are used twice, which is wrong. This is a problem when I want to specify constraints on the hidden nodes, because varMap does not contain the correct variable indices. I investigated what caused this error.

In maraboupy/MarabouNetworkONNX.py and maraboupy/MarabouNetworkTF.py, the ONNX and TensorFlow models are loaded and variables and equations are generated from them. The generated variables are put into self.varMap, which is a dictionary that maps the names of the ONNX and TF nodes to their associated variables. After parsing the model, the variables are rearranged such that the lowest variable indices are occupied by the model's input variables, followed by the output variables, followed by the variables of the hidden layers.

Reassigning the variable indices means that they have to be updated everywhere, including in the generated equations and in varMap. As you can see in the output, the indices 4 and 5 have been reassigned to be the output variables in varMap, but the other variables have not been reassigned: node '5' still uses indices 4 and 5 as well, and the other variables have not been incremented.

This PR fixes this issue.

New result:

>>> print(marabou_network.inputVars)
[array([[0, 1, 2, 3]])]
>>> print(marabou_network.outputVars)
[[4 5]]
>>> print(marabou_network.varMap)
{'input.1': array([[0, 1, 2, 3]]), '5': array([[6, 7, 8]]), '6': array([[ 9, 10, 11]]), '7': array([[4, 5]])}

The ONNX file I used is inside this ZIP file (GitHub does not allow onnx files here): my-nn.zip

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant