A Formal Tool for Verification of Probabilistic Spiking Neural Networks Based on Quotient Abstractions

Researchers introduce CogSpike, a formal verification tool for probabilistic spiking neural networks that addresses the state space explosion problem through weight-discretized quotient abstractions. The innovation enables verification of previously intractable neural network models by reducing computational complexity exponentially while maintaining mathematical fidelity guarantees.

The paper tackles a fundamental challenge in neural network verification: proving the correctness of spiking neural networks (SNNs) that operate under probabilistic, event-driven computation mimicking biological brain dynamics. Traditional formal verification methods collapse when applied to SNNs because the underlying discrete-time Markov chains grow exponentially with neuron count, rendering large networks impossible to verify exhaustively.

The breakthrough centers on weight-discretized quotient abstractions, a technique that compresses continuous synaptic weights into compact integer ranges while preserving their relative contributions. This compression strategy avoids the critical flaw of naive abstraction approaches that discard weight information entirely. CogSpike implements this methodology within a unified tool chain integrating design, simulation, and PRISM-based formal verification.

The mathematical rigor is compelling: the authors provide formal correctness guarantees including a two-sided fidelity theorem that bounds firing disagreements to a threshold region, and an Asymptotic Silence theorem guaranteeing permanent neuron silence under specific conditions. Empirical results demonstrate exponential state space reduction—approximately 17-fold per neuron with discretization parameter W=3—making previously intractable networks verifiable.

This advancement matters significantly for neuromorphic computing and AI safety communities. As SNNs gain adoption in edge computing and biological-inspired AI systems, the ability to formally verify their behavior becomes critical for safety-critical applications. The tool bridges the gap between theoretical neuroscience simulation and practical hardware deployment verification, enabling developers to prove network properties rather than relying on empirical testing alone.

• →Weight-discretized quotient abstractions reduce SNN state spaces exponentially while preserving synaptic weight information needed for property verification.
• →CogSpike provides formal correctness guarantees including a fidelity theorem bounding firing disagreements and an Asymptotic Silence theorem for permanent neuron behavior.
• →Approximately 17× state space reduction per neuron enables verification of networks previously too complex for formal analysis.
• →The unified tool chain integrates SNN design, simulation, and PRISM-based verification within a single isomorphic platform.
• →Formal verification of probabilistic SNNs addresses critical safety requirements for neuromorphic computing deployment in safety-critical applications.