Issue with `network.solve()` method in Marabou

[Vafali]

Dear Marabou Developers,

I am currently using the Marabou library for a project and I have encountered an issue with the network.solve() method. When I call this method, it raises a ValueError with the message "The truth value of an array with more than one element is ambiguous. Use a.any() or a.all()".

By the way I have trained a model using (Proximal policy optimization ) PPO. My model expects two separate inputs (lidar and state), input dimension is 340.

Here is a simplified version of my code:

# Load the network
network = Marabou.read_onnx(network_file)

# Define the input variables
input_vars = network.inputVars[0][0].tolist()

# Set bounds for all input variables
for i in range(len(input_vars)):
    network.setUpperBound(input_vars[i], 1.0)
    network.setLowerBound(input_vars[i], -1.0)

# Define collision threshold (meters)
collision_threshold = 0.2

# Get output variable numbers
output_vars = network.outputVars[0]

# Safety property formulation using output variable numbers
safety_property = []
for var in output_vars:
    equation = MarabouUtils.Equation(MarabouUtils.MarabouCore.Equation.LE)
    equation.addAddend(1, var)
    equation.setScalar(-collision_threshold)
    safety_property.append(equation)

# Add the safety property to the verification problem
for eq in safety_property:
    network.addEquation(eq)

# Run the verification
try:
    vals = network.solve()
except ValueError:
    print("Error: The solve method returned an ambiguous array.")
    vals = None

I have checked the definition of my network and the safety property, and they seem to be correct. I am not sure why the solve method is returning an ambiguous array instead of a dictionary mapping variable numbers to their values in the solution, or an empty dictionary if no solution exists.

I would appreciate any guidance or suggestions you might have to help me resolve this issue.

Thank you for your time and assistance.

Best regards,

[wu-haoze]

Hi @Vafali , this error usually occurs when the variables in "equation.addAddend(1, var)" and/or "network.setLowerBound(input_vars[i], -1.0)" are arrays instead of scalars.

I would suggest printing the "var" in "equation.addAddend(1, var)" and see if it is not a scalar. If it is not, most likely, you need to have "output_vars = network.outputVars[0][0]"

[Vafali]

Dear @wu-haoze, I have printed them. I tried a lot of things but i am not able to solve this. I would appreciate your prompt attention to this matter.

Output variables are indeed scalars, as they should be.

Instructions for updating: non-resource variables are not supported in the long term Length of input_vars: 340 Output variables: [4436 4437 4438 4439] Current output variable: 4436 Current output variable: 4437 Current output variable: 4438 Current output variable: 4439

[wu-haoze]

I see. Could you share the network and the script that you’re using so I can reproduce the issue on my end?

在 2024年4月19日，08:23，VAFALI SOLTANMURADOV @.***> 写道：



Dear @wu-haozehttps://github.com/wu-haoze, I have printed them. I tried a lot of things but i am not able to solve this. I would appreciate your prompt attention to this matter.

Output variables are indeed scalars, as they should be.

Instructions for updating: non-resource variables are not supported in the long term Length of input_vars: 340 Output variables: [4436 4437 4438 4439] Current output variable: 4436 Current output variable: 4437 Current output variable: 4438 Current output variable: 4439

— Reply to this email directly, view it on GitHubhttps://github.com/NeuralNetworkVerification/Marabou/issues/802#issuecomment-2066803297, or unsubscribehttps://github.com/notifications/unsubscribe-auth/ACRZF25CM6Y66NE4QJ5BZNDY6EZILAVCNFSM6AAAAABGPIKUF6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDANRWHAYDGMRZG4. You are receiving this because you were mentioned.Message ID: @.***>

[Vafali]

I can send you them via email if you want. It seems GitHub doesn't support onnx and pth file type. If this is your email I can send you now. haozewu@stanford.edu

[wu-haoze]

Sure that would work.

在 2024年4月19日，08:36，VAFALI SOLTANMURADOV @.***> 写道：



I can send you them via email if you want. It seems GitHub doesn't support onnx and pth file type. If this is your email I can send you now. @.**@.>

— Reply to this email directly, view it on GitHubhttps://github.com/NeuralNetworkVerification/Marabou/issues/802#issuecomment-2066824339, or unsubscribehttps://github.com/notifications/unsubscribe-auth/ACRZF26LOZ7DV6JHBL4PJO3Y6E2XZAVCNFSM6AAAAABGPIKUF6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDANRWHAZDIMZTHE. You are receiving this because you were mentioned.Message ID: @.***>

[wu-haoze]

Hi @Vafali , I ran the following script:

from maraboupy import Marabou
from maraboupy import MarabouCore
from maraboupy import MarabouUtils
import os

# Load the network
network = Marabou.read_onnx("trial2.onnx")

# Define the input variables
input_vars = network.inputVars[0][0].tolist()

# Set bounds for all input variables
for i in range(len(input_vars)):
    network.setUpperBound(input_vars[i], 1.0)
    network.setLowerBound(input_vars[i], -1.0)

# Define collision threshold (meters)
collision_threshold = 0.2

# Get output variable numbers
output_vars = network.outputVars[0]
print(output_vars)
# Safety property formulation using output variable numbers
safety_property = []
for var in output_vars:
    equation = MarabouUtils.Equation(MarabouUtils.MarabouCore.Equation.LE)
    print(var)
    equation.addAddend(1, var)
    equation.setScalar(-collision_threshold)
    safety_property.append(equation)

# Add the safety property to the verification problem
for eq in safety_property:
    network.addEquation(eq)

vals = network.solve()

and got the following error:

[[4436 4437 4438 4439]] [4436 4437 4438 4439] Traceback (most recent call last): File "/home/haozewu/Projects/Marabou_dev/Marabou/test.py", line 36, in vals = network.solve() File "/home/haozewu/Projects/Marabou_dev/Marabou/maraboupy/MarabouNetwork.py", line 70, in solve ipq = self.getInputQuery() File "/home/haozewu/Projects/Marabou_dev/Marabou/maraboupy/parsers/InputQueryBuilder.py", line 279, in getInputQuery assert v < self.numVars ValueError: The truth value of an array with more than one element is ambiguous. Use a.any() or a.all()

Same thing with "trial1.onnx".

The output of the second print statement suggests that, as I suspected earlier, the input to the addAddend method was not a scalar. When I change: output_vars = network.outputVars[0] to output_vars = network.outputVars[0][0] It's able to start solving.

Please let me know whether the fix works on your end.

[Vafali]

Dear @wu-haoze ,I've already tried the method you suggested previously, but unfortunately, I'm still encountering the same issue. Below, I've pasted the output from my Terminal for your reference: The output I'm seeing is from the Marabou solver, and the "UNKNOWN" at the end indicates that the solver was unable to determine whether the safety property I specified can be violated or not. Please correct me if I'm wrong. In my opinion the reasons could be:

1. There is a bug or limitation in the solver.
2. The safety property is indeed neither probably true or false given the constrains of network.
3. The problem is too complex for the solver to handle within its resource limits (time, memory, etc.)

By the way, I am getting same issues with Robustness Analysis. You can see it the code I have sent you.

Branching heuristics set to PseudoImpact

Engine::solve: Initial statistics

11:20:11 Statistics update: --- Time Statistics --- Total time elapsed: 1710 milli (00:00:01) Main loop: 0 milli (00:00:00) Preprocessing time: 1559 milli (00:00:01) Unknown: 151 milli (00:00:00) Breakdown for main loop: [0.00%] Simplex steps: 0 milli [0.00%] Explicit-basis bound tightening: 0 milli [0.00%] Constraint-matrix bound tightening: 0 milli [0.00%] Degradation checking: 0 milli [0.00%] Precision restoration: 0 milli [0.00%] Statistics handling: 0 milli [0.00%] Constraint-fixing steps: 0 milli [0.00%] Valid case splits: 0 milli. Average per split: 0.00 milli [0.00%] Applying stored bound-tightening: 0 milli [0.00%] SMT core: 0 milli [0.00%] Symbolic Bound Tightening: 150 milli [0.00%] SoI-based local search: 0 milli [0.00%] SoI-based local search: 0 milli [0.00%] Unaccounted for: 0 milli --- Preprocessor Statistics --- Number of preprocessor bound-tightening loop iterations: 3 Number of eliminated variables: 2053 Number of constraints removed due to variable elimination: 0 Number of equations removed due to variable elimination: 0 --- Engine Statistics --- Number of main loop iterations: 1 0 iterations were simplex steps. Total time: 0 milli. Average: 0.00 milli. 0 iterations were constraint-fixing steps. Total time: 0 milli. Average: 0.00 milli Number of active piecewise-linear constraints: 0 / 0 Constraints disabled by valid splits: 0. By SMT-originated splits: 0 Last reported degradation: 0.0000000000. Max degradation so far: 0.0000000000. Restorations so far: 0 Number of simplex pivots we attempted to skip because of instability: 0. Unstable pivots performed anyway: 0 --- Tableau Statistics --- Total number of pivots performed: 0 Real pivots: 0. Degenerate: 0 (0.00%) Degenerate pivots by request (e.g., to fix a PL constraint): 0 (0.00%) Average time per pivot: 0.00 milli Total number of fake pivots performed: 0 Total number of rows added: 0. Number of merged columns: 0 Current tableau dimensions: M = 4100, N = 10593 --- SMT Core Statistics --- Total depth is 0. Total visited states: 1. Number of splits: 0. Number of pops: 0 Max stack depth: 0 --- Bound Tightening Statistics --- Number of tightened bounds: 0. Number of rows examined by row tightener: 0. Consequent tightenings: 0 Number of explicit basis matrices examined by row tightener: 0. Consequent tightenings: 0 Number of bound tightening rounds on the entire constraint matrix: 0. Consequent tightenings: 0 Number of bound notifications sent to PL constraints: 0. Tightenings proposed: 0 --- Basis Factorization statistics --- Number of basis refactorizations: 2 --- Projected Steepest Edge Statistics --- Number of iterations: 0. Number of resets to reference space: 1. Avg. iterations per reset: 0 --- SBT --- Number of tightened bounds: 2052 --- SoI-based local search --- Number of proposed phase pattern update: 0. Number of accepted update: 0 [0.00%] Total time (% of local search time) updating SoI phase pattern : 0 milli [0.00%] Total time obtaining current assignment: 0 milli [0.00%] Total time getting SoI phase pattern : 0 milli [0.00%] --- Context dependent statistics --- Number of pushes / pops: 0 / 0 [0.00%] Pre-Push hook: 0 milli [0.00%] Push : 0 milli [0.00%] Post-Pop hook: 0 milli [0.00%] Pop : 0 milli [0.00%] Total context-switching time: 0 milli --- Proof Certificate --- Number of certified leaves: 0 Number of leaves to delegate: 0

---

Before declaring sat, recomputing...

Engine::solve: at leaf node but solving inconclusive

11:20:51 Statistics update: --- Time Statistics --- Total time elapsed: 41424 milli (00:00:41) Main loop: 39713 milli (00:00:39) Preprocessing time: 1559 milli (00:00:01) Unknown: 151 milli (00:00:00) Breakdown for main loop: [0.16%] Simplex steps: 62 milli [99.48%] Explicit-basis bound tightening: 39508 milli [0.00%] Constraint-matrix bound tightening: 0 milli [0.00%] Degradation checking: 0 milli [0.00%] Precision restoration: 0 milli [0.00%] Statistics handling: 0 milli [0.00%] Constraint-fixing steps: 0 milli [0.00%] Valid case splits: 0 milli. Average per split: 0.00 milli [0.00%] Applying stored bound-tightening: 0 milli [0.00%] SMT core: 0 milli [0.73%] Symbolic Bound Tightening: 289 milli [0.00%] SoI-based local search: 0 milli [0.00%] SoI-based local search: 0 milli [46449100146574.43%] Unaccounted for: 0 milli --- Preprocessor Statistics --- Number of preprocessor bound-tightening loop iterations: 3 Number of eliminated variables: 2053 Number of constraints removed due to variable elimination: 0 Number of equations removed due to variable elimination: 0 --- Engine Statistics --- Number of main loop iterations: 18 15 iterations were simplex steps. Total time: 62 milli. Average: 4.13 milli. 0 iterations were constraint-fixing steps. Total time: 0 milli. Average: 0.00 milli Number of active piecewise-linear constraints: 0 / 0 Constraints disabled by valid splits: 0. By SMT-originated splits: 0 Last reported degradation: 0.0000000000. Max degradation so far: 0.0000000000. Restorations so far: 0 Number of simplex pivots we attempted to skip because of instability: 0. Unstable pivots performed anyway: 0 --- Tableau Statistics --- Total number of pivots performed: 10 Real pivots: 10. Degenerate: 0 (0.00%) Degenerate pivots by request (e.g., to fix a PL constraint): 0 (0.00%) Average time per pivot: 0.10 milli Total number of fake pivots performed: 5 Total number of rows added: 0. Number of merged columns: 0 Current tableau dimensions: M = 4100, N = 10593 --- SMT Core Statistics --- Total depth is 0. Total visited states: 1. Number of splits: 0. Number of pops: 0 Max stack depth: 0 --- Bound Tightening Statistics --- Number of tightened bounds: 0. Number of rows examined by row tightener: 10. Consequent tightenings: 3 Number of explicit basis matrices examined by row tightener: 4. Consequent tightenings: 0 Number of bound tightening rounds on the entire constraint matrix: 0. Consequent tightenings: 0 Number of bound notifications sent to PL constraints: 0. Tightenings proposed: 0 --- Basis Factorization statistics --- Number of basis refactorizations: 2 --- Projected Steepest Edge Statistics --- Number of iterations: 15. Number of resets to reference space: 1. Avg. iterations per reset: 15 --- SBT --- Number of tightened bounds: 2052 --- SoI-based local search --- Number of proposed phase pattern update: 0. Number of accepted update: 0 [0.00%] Total time (% of local search time) updating SoI phase pattern : 0 milli [0.00%] Total time obtaining current assignment: 0 milli [0.00%] Total time getting SoI phase pattern : 0 milli [0.00%] --- Context dependent statistics --- Number of pushes / pops: 0 / 0 [0.00%] Pre-Push hook: 0 milli [0.00%] Push : 0 milli [0.00%] Post-Pop hook: 0 milli [0.00%] Pop : 0 milli [0.00%] Total context-switching time: 0 milli --- Proof Certificate --- Number of certified leaves: 0 Number of leaves to delegate: 0 UNKNOWN

[wu-haoze]

@Vafali this doesn't seem like the same issue as before. And UNKOWN is a possible outcome given that your network has tanh, as explained in my e-mail to you.

[Lev-Stambler]

@wu-haoze I am getting a similar UNKOWN response in a network with Softmax's. Is there some documentation or file I can look at to explain where this comes from?

[wu-haoze]

@wu-haoze I am getting a similar UNKOWN response in a network with Softmax's. Is there some documentation or file I can look at to explain where this comes from?

This is expected, as we don't have a complete procedure for deciding problems with non-piecewise-linear activations. The way we handle non-linearity is described in our recent tool paper: https://arxiv.org/abs/2401.14461

[Lev-Stambler]

@wu-haoze Okay sure and thank you for the response!

[wu-haoze]

@Lev-Stambler I should also mention that if your softmax is in the last layer and you only care about relative magnitude between outputs (like in classification), then perhaps you could pass in the network with the softmax removed or specify the outputNames to be the pre-softmax node when parsing the network like here: https://github.com/NeuralNetworkVerification/Marabou/blob/3c8e1054ff10d4371525ff1e7e15f18430a2b6d2/maraboupy/examples/2_ONNXExample.py#L37

But if the softmax is in the intermediate layers like in transformers, then we can't avoid reasoning about softmax.

[wu-haoze]

Closing due to inactivity. Feel free to re-open if needed.