problems with GE and LE on one variable
yizhake opened this issue · 1 comments
Hi,
Background:
I want to use Marabou to verify a variant of neural network: a network whose biases are intervals instead of scalars (I have lower and upper bound per bias).
I encode a query such that each neuron is encoded with 2 equations: GE and LE, which means that the neuron is bigger/smaller than the relevant weighted sum of previous layer's neurons + the lower/upper bound on the bias, respectively).
Marabou fails while processing the attached query with the following error:
Assertion violation! File src/engine/ReluConstraint.cpp, line 974
I've carefully checked the query file and think it is valid.
The query and the log of marabou files are attached.
Please help me understand the problem.
Thank you very much!
It seems the issue is due to the fact that the NetworkLevelReasoner is not fully constructed, which a heuristic in the DeepSoI module depends on. I posed a fix (#829) here.
On the other hand, if you run the current master branch with: ../build/Marabou --input-query q_cora.ipq --soi-init-strategy=current-assignment
Marabou also terminates correctly.