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

• URL: http://arxiv.org/abs/2606.20674v1
• Date: Fri, 12 Jun 2026 15:02:04 GMT
• Title: A Formal Tool for Verification of Probabilistic Spiking Neural Networks Based on Quotient Abstractions
• Abstract summary: Spiking Neural Networks (SNNs) model biological neural dynamics more faithfully than classical artificial networks.<n>Model verification faces a fundamental barrier: the state space explosion problem.<n>This paper introduces a weight-discretized quotient model abstraction that maps continuous synaptic weights to a compact integer range.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Spiking Neural Networks (SNNs) model biological neural dynamics more faithfully than classical artificial networks, but their stochastic, event-driven computation -- rooted in ion-channel noise and unreliable synaptic vesicle release -- demands probabilistic models for which deterministic abstractions are mathematically inadequate. Formal verification of such models via probabilistic model checking faces a fundamental barrier: the state space explosion problem, where the Discrete-Time Markov Chain (DTMC) encoding grows exponentially with the number of neurons. General-purpose quotient model abstractions [1] can in principle mitigate this growth by partitioning membrane potentials into equivalence classes, but a naïve application to SNNs discards synaptic weight information, limiting the properties that can be verified. This paper introduces a weight-discretized quotient model abstraction that maps continuous synaptic weights to a compact integer range while preserving the relative contribution of each synapse, and presents CogSpike, a unified workbench that integrates SNN design, simulation, and PRISM-based formal verification within a single isomorphic tool chain. The discretization is accompanied by formal correctness guarantees: a two-sided fidelity theorem confines any firing disagreement to a bounded gray zone around threshold, and an Asymptotic Silence theorem gives the exact limit guarantee that unforced neurons fall permanently silent. A topology-dependent scaling analysis shows that the state space reduction compounds exponentially -- approximately $17\times$ per neuron for discretization parameter $W = 3$ -- enabling verification of networks that are otherwise intractable, as confirmed empirically across seven canonical topologies.

Related papers

• Interval and fuzzy physics-augmented neural networks (iPANN and fPANN) for uncertainty quantification and propagation in constitutive modeling [0.7607244757956827]
  We propose interval and fuzzy physics-augmented neural networks (iPANNs and fPANNs) for uncertainty-aware hyperelastic modeling.<n>iPANNs learn lower, mean, and upper free energy density branches whose stresses, by automatic differentiation, ultimately noisy stress observations.<n>We evaluate the framework on synthetic data with heteroscedastic noise, varying random realizations, shifted means, and varying noise magnitudes.
  arXiv  Detail & Related papers  (2026-07-22T16:26:59Z)
• Emergent Manifold Separability during Reasoning in Large Language Models [46.78826734548872]
  Chain-of-Thought prompting significantly improves reasoning in Large Language Models.<n>We quantify the linear separability of latent representations without the confounding factors of probe training.
  arXiv  Detail & Related papers  (2026-02-23T20:36:17Z)
• Dense Neural Networks are not Universal Approximators [53.27010448621372]
  We show that dense neural networks do not possess universality of arbitrary continuous functions.<n>We consider ReLU neural networks subject to natural constraints on weights and input and output dimensions.
  arXiv  Detail & Related papers  (2026-02-07T16:52:38Z)
• A Complement to Neural Networks for Anisotropic Inelasticity at Finite Strains [0.0]
  We propose a complement to modeling that augments neural networks with material principles to capture anisotropy and inelasticity at finite strains.<n>Key element is a dual potential that governs dissipation, consistently incorporates anisotropy, and-unlike conventional formulations convex-satisfies the dissipation inequality without requiring convexity.
  arXiv  Detail & Related papers  (2025-10-05T13:01:05Z)
• Overcoming Dimensional Factorization Limits in Discrete Diffusion Models through Quantum Joint Distribution Learning [79.65014491424151]
  We propose a quantum Discrete Denoising Diffusion Probabilistic Model (QD3PM)<n>It enables joint probability learning through diffusion and denoising in exponentially large Hilbert spaces.<n>This paper establishes a new theoretical paradigm in generative models by leveraging the quantum advantage in joint distribution learning.
  arXiv  Detail & Related papers  (2025-05-08T11:48:21Z)
• Can KAN CANs? Input-convex Kolmogorov-Arnold Networks (KANs) as hyperelastic constitutive artificial neural networks (CANs) [0.0]
  We present a new type of model for learning the laws of.<n>trainable material behavior.<n>The resulting models are both compact hyper-trainible interpretable.<n>relationships analytical compressionity.<n>We show that ICKANs accurately capture stress-s models across diverse diverse strain states.
  arXiv  Detail & Related papers  (2025-03-07T17:42:24Z)
• Learning local discrete features in explainable-by-design convolutional neural networks [0.0]
  We introduce an explainable-by-design convolutional neural network (CNN) based on the lateral inhibition mechanism. The model consists of the predictor, that is a high-accuracy CNN with residual or dense skip connections. By collecting observations and directly calculating probabilities, we can explain causal relationships between motifs of adjacent levels.
  arXiv  Detail & Related papers  (2024-10-31T18:39:41Z)
• Consistency of Neural Causal Partial Identification [17.503562318576414]
  Recent progress in Causal Models showcased how identification and partial identification of causal effects can be automatically carried out via neural generative models.<n>We prove consistency of partial identification via NCMs in a general setting with both continuous and categorical variables.<n>Results highlight the impact of the design of the underlying neural network architecture in terms of depth and connectivity.
  arXiv  Detail & Related papers  (2024-05-24T16:12:39Z)
• On the Trade-off Between Efficiency and Precision of Neural Abstraction [62.046646433536104]
  Neural abstractions have been recently introduced as formal approximations of complex, nonlinear dynamical models. We employ formal inductive synthesis procedures to generate neural abstractions that result in dynamical models with these semantics.
  arXiv  Detail & Related papers  (2023-07-28T13:22:32Z)
• Gibbs-Duhem-Informed Neural Networks for Binary Activity Coefficient Prediction [45.84205238554709]
  We propose Gibbs-Duhem-informed neural networks for the prediction of binary activity coefficients at varying compositions. We include the Gibbs-Duhem equation explicitly in the loss function for training neural networks.
  arXiv  Detail & Related papers  (2023-05-31T07:36:45Z)
• Neural Abstractions [72.42530499990028]
  We present a novel method for the safety verification of nonlinear dynamical models that uses neural networks to represent abstractions of their dynamics. We demonstrate that our approach performs comparably to the mature tool Flow* on existing benchmark nonlinear models.
  arXiv  Detail & Related papers  (2023-01-27T12:38:09Z)
• Modeling Implicit Bias with Fuzzy Cognitive Maps [0.0]
  This paper presents a Fuzzy Cognitive Map model to quantify implicit bias in structured datasets. We introduce a new reasoning mechanism equipped with a normalization-like transfer function that prevents neurons from saturating.
  arXiv  Detail & Related papers  (2021-12-23T17:04:12Z)
• The Causal Neural Connection: Expressiveness, Learnability, and Inference [125.57815987218756]
  An object called structural causal model (SCM) represents a collection of mechanisms and sources of random variation of the system under investigation. In this paper, we show that the causal hierarchy theorem (Thm. 1, Bareinboim et al., 2020) still holds for neural models. We introduce a special type of SCM called a neural causal model (NCM), and formalize a new type of inductive bias to encode structural constraints necessary for performing causal inferences.
  arXiv  Detail & Related papers  (2021-07-02T01:55:18Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.