# On Neural Network Equivalence Checking using SMT Solvers

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

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Builds on 19 of its 42 references that are in the map.
- First posted on arXiv 22 Mar 2022.

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

- [Distilling the Knowledge in a Neural Network](https://mlsanity.com/paper/1503.02531/) (2015)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [From Softmax to Sparsemax: A Sparse Model of Attention and Multi-Label Classification](https://mlsanity.com/paper/1602.02068/) (2016)
- [A Survey of Model Compression and Acceleration for Deep Neural Networks](https://mlsanity.com/paper/1710.09282/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Regularization for Deep Learning: A Taxonomy](https://mlsanity.com/paper/1710.10686/) (2017)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [Introduction to Neural Network Verification](https://mlsanity.com/paper/2109.10317/) (2021)
- [An Overview of Neural Network Compression](https://mlsanity.com/paper/2006.03669/) (2020)
- [An SMT-Based Approach for Verifying Binarized Neural Networks](https://mlsanity.com/paper/2011.02948/) (2020)
- [A Survey on Deep Neural Network Compression: Challenges, Overview, and Solutions](https://mlsanity.com/paper/2010.03954/) (2020)
- [DeepAbstract: Neural Network Abstraction for Accelerating Verification](https://mlsanity.com/paper/2006.13735/) (2020)
- [ReluDiff: Differential Verification of Deep Neural Networks](https://mlsanity.com/paper/2001.03662/) (2020)
- [Automated Verification of Neural Networks: Advances, Challenges and Perspectives](https://mlsanity.com/paper/1805.09938/) (2018)
- [Geometric Path Enumeration for Equivalence Verification of Neural Networks](https://mlsanity.com/paper/2112.06582/) (2021)
- [A Symbolic Neural Network Representation and its Application to Understanding, Verifying, and Patching Networks](https://mlsanity.com/paper/1908.06223/) (2019)

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

- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [FairQuant: Certifying and Quantifying Fairness of Deep Neural Networks](https://mlsanity.com/paper/2409.03220/) (2024)
- [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)
- [Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems](https://mlsanity.com/paper/2312.10842/) (2023)
- [A Digital Twin prototype for traffic sign recognition of a learning-enabled autonomous vehicle](https://mlsanity.com/paper/2402.09097/) (2024)
- [Formal Local Implication Between Two Neural Networks](https://mlsanity.com/paper/2409.16726/) (2024)
- [Verifying Computational Graphs in Production-Grade Distributed Machine Learning Frameworks](https://mlsanity.com/paper/2509.10694/) (2025)
- [Influence-Guided Concolic Testing of Transformer Robustness](https://mlsanity.com/paper/2509.23806/) (2025)
- [Mission-Level Runtime Assurance for LLM-Assisted ISR Swarms over a Verification-Aware Fabric](https://mlsanity.com/paper/2607.23532/) (2026)

## Abstract (arXiv)

Two pretrained neural networks are deemed equivalent if they yield similar outputs for the same inputs. Equivalence checking of neural networks is of great importance, due to its utility in replacing learning-enabled components with equivalent ones, when there is need to fulfill additional requirements or to address security threats, as is the case for example when using knowledge distillation, adversarial training etc. SMT solvers can potentially provide solutions to the problem of neural network equivalence checking that will be sound and complete, but as it is expected any such solution is associated with significant limitations with respect to the size of neural networks to be checked. This work presents a first SMT-based encoding of the equivalence checking problem, explores its utility and limitations and proposes avenues for future research and improvements towards more scalable and practically applicable solutions. We present experimental results that shed light to the aforementioned issues, for diverse types of neural network models (classifiers and regression networks) and equivalence criteria, towards a general and application-independent equivalence checking approach.