extract marabou adversarial query after converting from onnx to MarabouNetwork fails

[yizhake]

The following code

1. loads onnx network and converts it to MarabouNetwork,
2. adds input and output constraints of an adversarial property, and
3. tries to extract a query into a variable ipq.

The last step fails with the error message below. The input onnx network can be downloaded from yizhak_net2.onnx.gz, (should be unzipped before running the code).

Code:

import tempfile
import numpy as np
import onnxruntime as ort
from maraboupy import Marabou, MarabouCore

def read_onnx_by_marabou(onnx_model: onnx.ModelProto):
    """load marabou network from onnx"""
    tmp_onnx_file = tempfile.NamedTemporaryFile(mode='wb')
    onnx.save(onnx_model, tmp_onnx_file.name)
    network = Marabou.read_onnx(tmp_onnx_file.name)
    tmp_onnx_file.close()
    return network

def add_robustness_input_region(network, x, epsilon):
    """add input constraints"""
    # Set the input bounds to be an delta ball (in l1-norm ) around a data point
    input_vars = network.inputVars[0].flatten()
    assert len(input_vars) == len(x)
    for i in range(len(x)):
        network.setLowerBound(input_vars[i], x[i] - epsilon)
        network.setUpperBound(input_vars[i], x[i] + epsilon)

def add_classification_output_condition(network, y, delta):
    """add output constraints (single runner or disjunction)"""
    # y as the winner index
    output_vars = network.outputVars[0][0]
    winner_var = output_vars[y]
    runners_vars = output_vars[:y].tolist() + output_vars[y+1:].tolist()
    disjunction = []
    for var in runners_vars:
        eq = MarabouCore.Equation(MarabouCore.Equation.GE)
        eq.addAddend(1, var)
        eq.addAddend(-1, winner_var)
        eq.setScalar(delta)
        disjunction.append([eq])
    network.addDisjunctionConstraint(disjunction)

def run_model(input_data):
    input_data = input_data.astype(np.float32).reshape(1,-1)
    input_name = session.get_inputs()[0].name
    output_name = session.get_outputs()[0].name
    result = session.run([output_name], {input_name: input_data})
    return result[0]

onnx_path = "yizhak_net2.onnx"
onet = onnx.load(onnx_path)
mnet = read_onnx_by_marabou(onet)
session = ort.InferenceSession(onnx_path)
x = np.array(list([0.1]*784))
y = run_model(x).argmax()
EPSILON = 0.0005  # full network: SAT, partial network: UNSAT
DELTA = 0.0001
add_robustness_input_region(mnet, x, epsilon=EPSILON)
add_classification_output_condition(mnet, y, delta=DELTA)
# ipq = mnet.getMarabouQuery()  # older version
ipq = mnet.getInputQuery()  # latest version

Error:

Traceback (most recent call last):
  File "verify/with_marabou.py", line 96, in <module>
    ipq = mnet.getInputQuery()
  File "Marabou2/maraboupy/parsers/InputQueryBuilder.py", line 333, in getInputQuery
    eq = MarabouCore.Equation(e.EquationType)
TypeError: __init__(): incompatible constructor arguments. The following argument types are supported:
    1. maraboupy.MarabouCore.Equation()
    6. maraboupy.MarabouCore.Equation(arg0: maraboupy.MarabouCore.Equation.EquationType)
Invoked with: <class 'maraboupy.MarabouCore.Equation.EquationType'>

[yizhake]

The solution is based on another issue: Replace the following line: eq = MarabouCore.Equation(MarabouCore.Equation.GE) # older version with: eq = MarabouUtils.Equation(MarabouCore.Equation.GE) # latest version

Thank you @wu-haoze for the help!