NNEquiv is a neural network equivalence verification tool based on the geometric path enumeration algorithm.
This implementation is based on the NNEnum tool by Stanley Bak for single neural networks.
To get started it's best to have a look at examples/equiv/test.py
which explains how equivalence properties can be verified.
You can also invoke the approach by running:
examples/equiv/test.py [first-net] [second-net] [input space] [property] [strategy]
where:
[first-net]
and[second-net]
areONNX
networks[input space]
is an input space defined inexamples/equiv/properties.py
[property]
is eithertop
or the epsilon value to be proven (e.g.0.05
)[strategy]
is the refinement strategy (no refinement:DONT
)
If you are looking for further information on the experimental evaluation of this tool, you might be interested in this repository
If you use this work in your research please: