# Geometric Path Enumeration for Equivalence Verification of Neural Networks

arXiv: https://arxiv.org/abs/2112.06582 · HTML: https://mlsanity.com/paper/2112.06582/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 29 references that are in the map.
- First posted on arXiv 13 Dec 2021.

## Builds on (most cited first, 8 of 8)

- [Distilling the Knowledge in a Neural Network](https://mlsanity.com/paper/1503.02531/) (2015)
- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [A Survey of Model Compression and Acceleration for Deep Neural Networks](https://mlsanity.com/paper/1710.09282/) (2017)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [ReluDiff: Differential Verification of Deep Neural Networks](https://mlsanity.com/paper/2001.03662/) (2020)
- [NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation](https://mlsanity.com/paper/2009.09943/) (2020)

## Built on by (most cited first, 6 of 6)

- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [On Neural Network Equivalence Checking using SMT Solvers](https://mlsanity.com/paper/2203.11629/) (2022)
- [Optimized Symbolic Interval Propagation for Neural Network Verification](https://mlsanity.com/paper/2212.08567/) (2022)
- [Revisiting Differential Verification: Equivalence Verification with Confidence](https://mlsanity.com/paper/2410.20207/) (2024)
- [CEG4N: Counter-Example Guided Neural Network Quantization Refinement](https://mlsanity.com/paper/2207.04231/) (2022)
- [Floating-Point Neural Network Verification at the Software Level](https://mlsanity.com/paper/2510.23389/) (2025)

## Abstract (arXiv)

As neural networks (NNs) are increasingly introduced into safety-critical domains, there is a growing need to formally verify NNs before deployment. In this work we focus on the formal verification problem of NN equivalence which aims to prove that two NNs (e.g. an original and a compressed version) show equivalent behavior. Two approaches have been proposed for this problem: Mixed integer linear programming and interval propagation. While the first approach lacks scalability, the latter is only suitable for structurally similar NNs with small weight changes. The contribution of our paper has four parts. First, we show a theoretical result by proving that the epsilon-equivalence problem is coNP-complete. Secondly, we extend Tran et al.'s single NN geometric path enumeration algorithm to a setting with multiple NNs. In a third step, we implement the extended algorithm for equivalence verification and evaluate optimizations necessary for its practical use. Finally, we perform a comparative evaluation showing use-cases where our approach outperforms the previous state of the art, both, for equivalence verification as well as for counter-example finding.