matosjr/nnequiv

Fork of nnenum for equivalence checking

NNEquiv

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.

Getting started

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] are ONNX networks
• [input space] is an input space defined in examples/equiv/properties.py
• [property] is either top or the epsilon value to be proven (e.g. 0.05)
• [strategy] is the refinement strategy (no refinement: DONT)

Experimental Evaluation

If you are looking for further information on the experimental evaluation of this tool, you might be interested in this repository

Citation

If you use this work in your research please:

• Cite the work by Stanley Bak et al. on which we base our implementation
• Cite our work which extends the Geometric Path Enumeration Algorithm to multiple networks