verinet failing
Opened this issue · 1 comments
Sorry, next right up...
Running VeriNet crashes with a ValueError. I tested this on develop and master. I am not sure if it produced the same error on master, but it also failed.
File ".../venv/lib/python3.9/site-packages/dnnv/__main__.py", line 113, in _main
return main(*cli.parse_args())
File ".../venv/lib/python3.9/site-packages/dnnv/__main__.py", line 74, in main
result, cex = verifier.verify(phi, **params)
File ".../venv/lib/python3.9/site-packages/dnnv/verifiers/common/base.py", line 102, in verify
return cls(phi, **kwargs).run()
File ".../venv/lib/python3.9/site-packages/dnnv/verifiers/common/base.py", line 137, in run
subproperty_result, cex = self.check(subproperty)
File ".../venv/lib/python3.9/site-packages/dnnv/verifiers/common/base.py", line 106, in check
executor_inputs = self.build_inputs(prop)
File ".../venv/lib/python3.9/site-packages/dnnv/verifiers/verinet/__init__.py", line 53, in build_inputs
output_op.b = np.vstack(
File "<__array_function__ internals>", line 5, in vstack
File ".../venv/lib/python3.9/site-packages/numpy/core/shape_base.py", line 282, in vstack
return _nx.concatenate(arrs, 0)
File "<__array_function__ internals>", line 5, in concatenate
ValueError: all the input array dimensions for the concatenation axis must match exactly, but along dimension 1, the array at index 0 has size 1 and the array at index 1 has size 4
I did:
python3 -m virtualenv venv --python python3.9
source venv/bin/activate
pip install git+https://github.com/dlshriver/dnnv.git@develop
dnnv_manage install verinet
git clone https://github.com/dlshriver/dnnv-benchmarks benchmarks
dnnv benchmarks/benchmarks/ACAS_Xu/properties/property_2.py -N "N" benchmarks/benchmarks/ACAS_Xu/onnx/N_2_1.onnx --verinet
Best regards,
David
Very interesting. I've confirmed this results in that error, but I don't have a solution yet. It still passes the test suite so it does work on some simple problems. I'll do a bit more digging tomorrow.