On Neural Network Equivalence Checking using SMT Solvers

TL;DR

This paper introduces an SMT-based method for neural network equivalence checking, analyzing its capabilities and limitations across different models and criteria, aiming for more scalable solutions.

Contribution

It presents the first SMT encoding for neural network equivalence checking, exploring its utility, limitations, and proposing future research directions.

Findings

Effective for small to medium neural networks

Highlights scalability limitations of SMT-based approaches

Provides insights into equivalence criteria applicability

Abstract

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.