return all input-output pairs that satisfy the given range

[chenyi10]

filename = "./data/models/model_epoch_999"

OPT = Marabou.createOptions(timeoutInSeconds=10,verbosity=0)

inputNames = ['Placeholder'] outputName = ['Identity'] network = Marabou.read_tf(filename=filename, modelType='savedModel_v2')

inputVars = network.inputVars[0][0] outputVars = network.outputVars[0][0]

for i in range(8): for j in range(10): network.setLowerBound(inputVars[i][j],-100) network.setUpperBound(inputVars[i][j],100)

for k in range(8): network.setLowerBound(outputVars[k][0], -100) network.setUpperBound(outputVars[k][0], 100)

exitCode, vals, stats = network.solve(filename="",options=OPT)

How to make it return all input-output pairs that satisfy the given range?

[wu-haoze]

Hi @chenyi10 , in general there can be an infinite number of satisfying assignments. One way to create different satisfying assignments is by partitioning your input region into sub-regions and call Marabou on each one of them.

[chenyi10]

Thanks!Is the one-dimensional convolutional network not supported for validation? @wu-haoze

[wu-haoze]

Yeah, we haven't supported it yet (https://github.com/NeuralNetworkVerification/Marabou/issues/723).

[chenyi10]

if i want to Verify the one-dimensional convolutional network，Do you hava some ideas @wu-haoze

[wu-haoze]

if i want to Verify the one-dimensional convolutional network，Do you hava some ideas @wu-haoze

I think other than us actually implementing the parsing of 1-d convolution, there won't be an easy solution. I don't have a guaranteed timeline for this though. One possible alternative route is to somehow convert the convolutional network to a fully connected one. This might be possible using the ONNX package. I'm not aware whether there is a tool that automatically does this.

[chenyi10]

I converted the convolutional network to a fully connected one,but I couldnot use marabou to verify it ,some operations such as "shape gatherv2 Prod pack" havenot been implemented. Thanks for your help!@wu-haoze

[wu-haoze]

@chenyi10 is your network in the onnx format? If so, perhaps it’s worth trying onnxsim to get rid of some constant operators: https://github.com/daquexian/onnx-simplifier

If it still didn’t work, feel free to share the network with me (haozewu@stanford.edu) and I can try to add the missing operators post simplication.