# Towards Efficient Formal Verification of Spiking Neural Network

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 21 of its 36 references that are in the map.
- First posted on arXiv 20 Aug 2024.

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

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Universal adversarial perturbations](https://mlsanity.com/paper/1610.08401/) (2016)
- [Threat of Adversarial Attacks on Deep Learning in Computer Vision: A Survey](https://mlsanity.com/paper/1801.00553/) (2018)
- [On the Number of Linear Regions of Deep Neural Networks](https://mlsanity.com/paper/1402.1869/) (2014)
- [Training Spiking Neural Networks Using Lessons From Deep Learning](https://mlsanity.com/paper/2109.12894/) (2021)
- [Spiking-YOLO: Spiking Neural Network for Energy-Efficient Object Detection](https://mlsanity.com/paper/1903.06530/) (2019)
- [From Words to Watts: Benchmarking the Energy Costs of Large Language Model Inference](https://mlsanity.com/paper/2310.03003/) (2023)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Multi-digit Number Recognition from Street View Imagery using Deep Convolutional Neural Networks](https://mlsanity.com/paper/1312.6082/) (2013)
- [Supervised learning based on temporal coding in spiking neural networks](https://mlsanity.com/paper/1606.08165/) (2016)
- [Towards deep learning with segregated dendrites](https://mlsanity.com/paper/1610.00161/) (2016)
- [Introduction to Neural Network Verification](https://mlsanity.com/paper/2109.10317/) (2021)
- [Temporal-Coded Deep Spiking Neural Network with Easy Training and Robust Performance](https://mlsanity.com/paper/1909.10837/) (2019)
- [Toward Robust Spiking Neural Network Against Adversarial Perturbation](https://mlsanity.com/paper/2205.01625/) (2022)
- [Adversarially Robust Spiking Neural Networks Through Conversion](https://mlsanity.com/paper/2311.09266/) (2023)
- [Spiking Neural Networks modelled as Timed Automata with parameter learning](https://mlsanity.com/paper/1808.01893/) (2018)
- [Timing-Based Backpropagation in Spiking Neural Networks Without Single-Spike Restrictions](https://mlsanity.com/paper/2211.16113/) (2022)
- [Robust and Efficient Adversarial Defense in SNNs via Image Purification and Joint Detection](https://mlsanity.com/paper/2404.17092/) (2024)

## Abstract (arXiv)

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.