Probabilistic Modeling of Spiking Neural Networks with Contract-Based Verification

TL;DR

This paper introduces a probabilistic modeling framework for Spiking Neural Networks (SNNs) that supports formal verification and simulation, addressing the challenge of ensuring global reaction requirements in stochastic timing scenarios.

Contribution

It provides a simple, parametric model framework for elementary neural bundles and their connections, enabling formal verification and simulation of SNNs.

Findings

Model framework translates into existing model-checkers and simulators.

Supports expressing neural bundles and connections with latency and probability.

Facilitates formal verification of SNNs with stochastic timing.

Abstract

Spiking Neural Networks (SNN) are models for "realistic" neuronal computation, which makes them somehow different in scope from "ordinary" deep-learning models widely used in AI platforms nowadays. SNNs focus on timed latency (and possibly probability) of neuronal reactive activation/response, more than numerical computation of filters. So, an SNN model must provide modeling constructs for elementary neural bundles and then for synaptic connections to assemble them into compound data flow network patterns. These elements are to be parametric patterns, with latency and probability values instantiated on particular instances (while supposedly constant "at runtime"). Designers could also use different values to represent "tired" neurons, or ones impaired by external drugs, for instance. One important challenge in such modeling is to study how compound models could meet global reaction requirements (in stochastic timing challenges), provided similar provisions on individual neural bundles. A temporal language of logic to express such assume/guarantee contracts is thus needed. This may lead to formal verification on medium-sized models and testing observations on large ones. In the current article, we make preliminary progress at providing a simple model framework to express both elementary SNN neural bundles and their connecting constructs, which translates readily into both a model-checker and a simulator (both already existing and robust) to conduct experiments.