Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Efficient Formal Verification of Spiking Neural Network

Baekryun Seong, Jieung Kim, Sang-Ki Ko

TL;DR

This work targets the robustness verification of spiking neural networks (SNNs) in the context of energy-efficient AI. It introduces temporal encoding to reformulate SNNs as SMT-friendly constraints, and provides a theoretical analysis showing exponential reduction in the adversarial perturbation space compared to rate encoding, especially when the time horizon is large. To address remaining solver scalability, it proposes a Direct Counterexample Search (DCS) method that bypasses SMT bottlenecks while delivering equivalent robustness insights, and validates these approaches with MNIST and Fashion-MNIST experiments. The results demonstrate practical verification improvements and pave the way for safer deployment of SNNs in safety-critical settings, with future work focusing on larger architectures, convolutional SNNs, and GPU-accelerated verification.

Abstract

Recently, AI research has primarily focused on large language models (LLMs), and increasing accuracy often involves scaling up and consuming more power. The power consumption of AI has become a significant societal issue; in this context, spiking neural networks (SNNs) offer a promising solution. SNNs operate event-driven, like the human brain, and compress information temporally. These characteristics allow SNNs to significantly reduce power consumption compared to perceptron-based artificial neural networks (ANNs), highlighting them as a next-generation neural network technology. However, societal concerns regarding AI go beyond power consumption, with the reliability of AI models being a global issue. For instance, adversarial attacks on AI models are a well-studied problem in the context of traditional neural networks. Despite their importance, the stability and property verification of SNNs remains in the early stages of research. Most SNN verification methods are time-consuming and barely scalable, making practical applications challenging. In this paper, we introduce temporal encoding to achieve practical performance in verifying the adversarial robustness of SNNs. We conduct a theoretical analysis of this approach and demonstrate its success in verifying SNNs at previously unmanageable scales. Our contribution advances SNN verification to a practical level, facilitating the safer application of SNNs.

Towards Efficient Formal Verification of Spiking Neural Network

TL;DR

This work targets the robustness verification of spiking neural networks (SNNs) in the context of energy-efficient AI. It introduces temporal encoding to reformulate SNNs as SMT-friendly constraints, and provides a theoretical analysis showing exponential reduction in the adversarial perturbation space compared to rate encoding, especially when the time horizon is large. To address remaining solver scalability, it proposes a Direct Counterexample Search (DCS) method that bypasses SMT bottlenecks while delivering equivalent robustness insights, and validates these approaches with MNIST and Fashion-MNIST experiments. The results demonstrate practical verification improvements and pave the way for safer deployment of SNNs in safety-critical settings, with future work focusing on larger architectures, convolutional SNNs, and GPU-accelerated verification.

Abstract

Recently, AI research has primarily focused on large language models (LLMs), and increasing accuracy often involves scaling up and consuming more power. The power consumption of AI has become a significant societal issue; in this context, spiking neural networks (SNNs) offer a promising solution. SNNs operate event-driven, like the human brain, and compress information temporally. These characteristics allow SNNs to significantly reduce power consumption compared to perceptron-based artificial neural networks (ANNs), highlighting them as a next-generation neural network technology. However, societal concerns regarding AI go beyond power consumption, with the reliability of AI models being a global issue. For instance, adversarial attacks on AI models are a well-studied problem in the context of traditional neural networks. Despite their importance, the stability and property verification of SNNs remains in the early stages of research. Most SNN verification methods are time-consuming and barely scalable, making practical applications challenging. In this paper, we introduce temporal encoding to achieve practical performance in verifying the adversarial robustness of SNNs. We conduct a theoretical analysis of this approach and demonstrate its success in verifying SNNs at previously unmanageable scales. Our contribution advances SNN verification to a practical level, facilitating the safer application of SNNs.
Paper Structure (27 sections, 2 theorems, 14 equations, 5 figures, 4 tables, 1 algorithm)

This paper contains 27 sections, 2 theorems, 14 equations, 5 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Formal Verification of Neural Networks
  4. Mathematical Modeling of SNNs
  5. Information Encoding in SNNs
  6. Adversarial Robustness in SNNs
  7. Preliminaries
  8. Spiking Neural Networks
  9. Variable definitions
  10. Spiking neurons
  11. Spike encoding
  12. Adversarial Attack
  13. Spike train perturbation
  14. Perturbation space
  15. Methodology
  16. ...and 12 more sections

Key Result

Lemma 1

Let $\Delta=\alpha TN$, where $0\le \alpha\le1$. The perturbation space ratio of rate encoding to temporal encoding is $O((T^{\alpha T}/(1+2\alpha T))^{N})$.

Figures (5)

  • Figure 1: The mechanism of SNN. The Spike train of the previous layer, which consists of 0 and 1, is multiplied with weights and integrated together. The integrated value is added to potential, which decays with time.
  • Figure 2: Two ways to encode inputs in SNNs.
  • Figure 3: MNIST Examples of the original input image (left) and the image with temporal perturbation (right) where $\Delta=4$.
  • Figure 4: Verification runtime with different numbers of time steps (left) and different numbers of hidden neurons (right) at MNIST and FashionMNIST dataset. In FashionMNIST, at 6 time steps, two instances timed out for $>$ 80,000 seconds.
  • Figure 5: DCS Verification runtime with different numbers of time steps (left) and different numbers of hidden neurons (right) at MNIST dataset, with different $\Delta$s.

Theorems & Definitions (5)

  • Definition 1: $\Delta$-Perturbation Space
  • Lemma 1
  • proof
  • Theorem 1
  • proof