Something went wrong in query compilation: CannotEliminateNot

[BenCoke12]

Error raised for the superclass robustness script.

Specification: https://github.com/BenCoke12/FashionVerification/blob/main/vclspecs/fashionSuperclassRobustness.vcl Network: https://github.com/BenCoke12/FashionVerification/blob/main/onnxnetworks/fashion1l32n.onnx Image dataset: https://github.com/BenCoke12/FashionVerification/blob/main/idxdata/individuals/Image104.idx Label dataset: https://github.com/BenCoke12/FashionVerification/blob/main/idxdata/individuals/Label104.idx Epsilon: 0.05

Command: vehicle verify --specification vclspecs/fashionSuperclassRobustness.vcl --network classifier:onnxnetworks/fashion1l32n.onnx --parameter epsilon:0.05 --dataset trainingImages:idxdata/individuals/Im age104.idx --dataset trainingLabels:idxdata/individuals/Label104.idx --verifier Marabou --verifierLocation ../Marabou/bu ild/Marabou

Error:

Something went wrong in query compilation: CannotEliminateNot[ not ((or (not ((and ((forallIndex 28) (lambda (i : Index .( 28)) (((forall {pi (j : Index .( 28)) Bool} ) {{forallIndex 28 }}) (lambda (j : Index .( 28)) ((and (((((<= {Rat} ) {Rat} ) {{leqRat }}) ((((- {Rat} ) {Rat} ) {{negRat }}) epsilon)) ((((! {Rat} ) .{ 28} ) ((((! {(Vector Rat) .( 28)} ) .{ 28} ) 𝓲2) 𝓲1)) 𝓲0))) (((((<= {Rat} ) {Rat} ) {{leqRat }}) ((((! {Rat} ) .{ 28} ) ((((! {(Vector Rat) .( 28)} ) .{ 28} ) 𝓲2) 𝓲 1)) 𝓲0)) epsilon))))))) ((forallI ndex 28) (lambda (i : Index .( 28)) (((forall {pi (j : Index .( 28)) Bool} ) {{forallIndex 28 }}) (lambda (j : Index .( 28)) ((and (((((<= {Rat} ) {Rat} ) {{leqRat }}) ((((fromNat {Rat} ) {{fromNatToRat }}) 0) .{{() }})) ((((! {Rat} ) .{ 28} ) ((((! {(Vector Rat) .( 28)} ) .{ 28} ) 𝓲 2) 𝓲1)) 𝓲0))) (((((<= {Rat} ) {Rat} ) {{leqRat }}) ((((! {Rat} ) .{ 28} ) ((((! {(Vector Rat) .( 28)} ) .{ 28} ) 𝓲2) 𝓲1)) 𝓲0)) (((( fromNat {Rat} ) {{fromNatToRat }}) 1) .{{() }})))))))))) ((or ((or ((and ((or False) (((foldList (lambda (x : Bool) (lambda (y : Bool) ((or 𝓲 1) 𝓲0)))) False) ((mapList (lambd a (class : Index .( 10)) (((((== {Index .( 10)} ) {Index .( 10)} ) {{(equalsIndex {10} ) {10} }}) 𝓲2) 𝓲0 ))) (((:: {Index .( 10)} ) 2) (((:: {Index .( 10)} ) 3) (((:: {Index .( 10)} ) 4) (((:: {Index .( 10)} ) 6) (nil {Index .( 10)} ))))))))) ((forallIndex 10) (lambda (j : Index .( 10)) ((=> (((((!= {Index .( 10)} ) {Index .( 10)} ) {{(notEqualsIndex {10} ) {10} }}) 𝓲0) 𝓲1)) (((((> {Rat} ) {Rat} ) {{gtRat }}) ((((! {Rat} ) .{ 10} ) (classifier 𝓲2)) 𝓲 1)) ((((! {Rat} ) .{ 10} ) (classifier 𝓲2)) 𝓲0))))) )) (((foldList (lambda (x : Bool) (lambda (y : Bool) ((or 𝓲 1) 𝓲0)))) False) ((mapList (lambda (class : Index .( 10)) ((and ((inSuperclass 𝓲2) 𝓲1)) ((advis es 𝓲 3) 𝓲0)))) ((( :: {Index .( 10)} ) 2) (((:: {Index .( 10)} ) 3) (((:: {Index .( 10)} ) 4) (((:: {Index .( 10)} ) 6) (nil {Index .( 10)} ))))))))) (((foldList (lambda (x : Bool) (lambda (y : Bool) ((or 𝓲1) 𝓲0)))) False) ((mapList (lambda (su per : List (Index .( 10))) ((((((existsIn {Index .( 10)} ) {List} ) {{foldList }}) {{mapList }}) (lambda (class : Index .( 10)) ((and ((inSuperclass 𝓲2) 𝓲1)) ((advises 𝓲3) 𝓲0)))) 𝓲0))) (((:: {List (Index .( 10))} ) (( (:: {Index .( 10)} ) 5) (((:: {Index .( 10)} ) 7) (((:: {Index .( 10)} ) 9) (nil {Index .( 10)} ))))) (((:: {List (Index .( 10))} ) (((:: {Index .( 10)} ) 1) (nil {Index .( 10)} ))) (((:: {List (Index .( 10))} ) (((:: {Index .( 10)} ) 8) (nil {Index .( 10)} ))) (nil {List (Index .( 10))} )))))))) ]

[MatthewDaggitt]

Thanks. Any chance you could have a go at minimising it? Which version of Vehicle are you running?