An SMT Toolbox for Adversarial Robustness Evaluation for Spiking Neural Networks
摘要
Spiking Neural Networks (SNN) are gaining wide prominence in recent times, due to their promise of comparable learning capability as classical neural networks, with an additional benefit of low power consumption that makes them ideally suited for low resource environments. SNNs are slowly making inroads into diverse application domains including safety-critical systems, wherein, the requirement of adherence to correctness specifications is of paramount importance. Of equal importance is the issue of robustness against adversarial perturbations, which has been an element of recent concern for classical neural networks. This work presents a tool for adversarial robustness evaluation of spiking neural networks leveraging the use of Satisfiability Modulo Theory (SMT) solvers. Given an SNN, an input on which the SNN is known to behave correctly, and a value of the maximum amount \(\varDelta \) of allowed perturbation, our framework can come up with a guarantee that the given SNN is either robust against any such \(\varDelta \) -perturbation of the known input or provide a counterexample input for which the SNN falters. Our tool first encodes the SNN as a collection of symbolic SMT constraints using the Linear Arithmetic (LRA) fragment and then carries out adversarial robustness analysis using the popular SMT solver Z3. We present case studies of our framework on the MNIST dataset.