On Neural Network Equivalence Checking using SMT Solvers
This addresses the need for sound and complete equivalence checking in applications like knowledge distillation and adversarial training, but it is incremental due to scalability limitations.
The paper tackled the problem of checking equivalence between two pretrained neural networks using SMT solvers, presenting a first encoding and experimental results on diverse models and criteria to explore its utility and limitations.
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.