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

Christopher Leturc; Elisabetta De Maria; Nikan Zandian Jazi

REVIEW 2 major objections 1 minor 16 references

A weight-discretized quotient abstraction reduces the DTMC state space of probabilistic SNNs by roughly 17 times per neuron while keeping firing behavior within a bounded gray zone.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.3

2026-06-27 04:39 UTC pith:BEHDGJ3Q

load-bearing objection The paper's weight-discretized quotient for SNN DTMC verification adds a fidelity theorem and asymptotic silence result with reported 17x per-neuron reduction, but the mapping's effect on transition probabilities is the part that needs the explicit error bounds shown. the 2 major comments →

arxiv 2606.20674 v1 pith:BEHDGJ3Q submitted 2026-06-12 cs.NE cs.AIcs.FL

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

Nikan Zandian Jazi , Elisabetta De Maria , Christopher Leturc This is my paper

classification cs.NE cs.AIcs.FL

keywords spiking neural networksquotient abstractionprobabilistic model checkingformal verificationstate space reductionDTMC encodingsynaptic weight discretization

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper sets out to show that continuous synaptic weights can be mapped to a compact integer range without losing the relative strength of each connection, yielding a quotient model whose DTMC encoding stays small enough for PRISM verification. Two theorems are proved: any difference in firing is confined to a narrow interval around threshold, and unforced neurons become permanently silent after finite time. The resulting reduction grows exponentially with network size. A single tool chain called CogSpike lets users design, simulate, and verify the same model without translation steps. This combination makes formal checks feasible on topologies that explode under direct encoding.

Core claim

The weight-discretized quotient model abstraction maps continuous synaptic weights to a compact integer range while preserving relative contribution; a two-sided fidelity theorem confines firing disagreement to a bounded gray zone around threshold; an Asymptotic Silence theorem guarantees unforced neurons fall permanently silent; state-space reduction compounds exponentially (approximately 17× per neuron for W=3).

What carries the argument

weight-discretized quotient model abstraction that partitions membrane potentials into equivalence classes while mapping weights to a small integer set that keeps relative synaptic strengths

Load-bearing premise

Mapping continuous weights to a small integer range while preserving relative strengths is enough to keep the fidelity and silence properties intact in the DTMC models of the networks being checked.

What would settle it

A concrete counter-example network in which the abstracted DTMC produces a firing probability that differs from the original model by more than the gray-zone bound would refute the fidelity theorem.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

Networks whose DTMC encodings are otherwise intractable become verifiable.
Unforced neurons reach permanent silence in finite time under the abstraction.
Any firing disagreement remains confined to a known interval around threshold.
State-space savings multiply with every added neuron, scaling as roughly 17× for W=3.
Design, simulation, and verification occur inside one isomorphic tool chain.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same discretization step could be reused on other stochastic neuron models whose weights dominate the state description.
Verification queries that depend only on long-run silence or threshold crossings become automatically sound once the two theorems hold.
Because the abstraction is topology-dependent, networks with dense connectivity may see larger relative savings than sparse ones.
Embedding the abstraction inside a single tool chain removes a common source of modeling mismatch between simulation and checker.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Desk Editor's Note

The paper's weight-discretized quotient for SNN DTMC verification adds a fidelity theorem and asymptotic silence result with reported 17x per-neuron reduction, but the mapping's effect on transition probabilities is the part that needs the explicit error bounds shown.

read the letter

The punchline is that this work gives a concrete way to shrink the state space for probabilistic verification of spiking networks by discretizing weights to a small integer set while claiming to keep relative synaptic strengths. They pair it with two theorems and a tool that links design to PRISM checking.

What is new is the SNN-specific version of the quotient: general ones drop the weight details, so this version maps continuous weights to integers in a way meant to preserve contributions. The two-sided fidelity theorem limits firing mismatches to a gray zone near threshold, and the silence theorem says unforced neurons eventually stay quiet. The scaling claim is topology-dependent and they back it with runs on seven canonical cases showing the exponential drop.

The tool CogSpike is a practical addition if it really lets users move from model to verified properties without switching environments. The formal guarantees are the part that could matter for safety-critical stochastic neural systems.

The soft spot is exactly the discretization step the stress-test flags. If the integer mapping distorts the effective ratios even a little, the DTMC transition probabilities shift and the gray-zone bound or silence limit may not hold as stated. The abstract describes the mapping but the full paper must supply the function and the error analysis that shows the distortion stays small enough for the theorems. Without that, the central claims rest on an unshown preservation property.

This is for people already working on probabilistic model checking of neural models or formal methods for biological computation. It deserves a serious referee because the reduction factor and the two theorems are the sort of concrete claims that need expert checking on the derivations, even if the mapping details require tightening.

Referee Report

2 major / 1 minor

Summary. The paper introduces a weight-discretized quotient model abstraction for probabilistic spiking neural networks that maps continuous synaptic weights to a compact integer range while preserving relative contributions, accompanied by a two-sided fidelity theorem confining firing disagreement to a bounded gray zone around threshold and an Asymptotic Silence theorem guaranteeing permanent silence for unforced neurons. It presents the CogSpike tool integrating SNN design, simulation, and PRISM-based verification, and reports exponential state-space reduction (approximately 17× per neuron for W=3) with empirical confirmation across seven canonical topologies.

Significance. If the discretization preserves relative contributions at the level required by the DTMC semantics and the theorems are rigorously established, the work would provide a meaningful advance in mitigating state-space explosion for formal verification of stochastic SNNs. The integrated tool chain and topology-dependent scaling analysis represent practical strengths that could enable verification of otherwise intractable networks.

major comments (2)

[Abstract] Abstract (description of weight-discretized quotient model abstraction): the claim that the integer mapping preserves relative synaptic contribution is invoked to support both the two-sided fidelity theorem and the DTMC encodings, yet no explicit mapping function, error bound on effective weight ratios, or analysis of impact on probabilistic transition probabilities is supplied; this is load-bearing because even small distortions could invalidate the gray-zone confinement.
[Abstract] Abstract (statement of the two theorems): the fidelity and Asymptotic Silence theorems are presented as formal correctness guarantees without proof sketches, derivation outlines, or error bounds tied to the free discretization parameter W, preventing assessment of whether the guarantees survive the weight mapping for the DTMC semantics.

minor comments (1)

[Abstract] The reference [1] for general-purpose quotient abstractions is cited but not expanded; adding the full bibliographic details would improve traceability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments on the abstract. We respond to each major comment below.

read point-by-point responses

Referee: [Abstract] Abstract (description of weight-discretized quotient model abstraction): the claim that the integer mapping preserves relative synaptic contribution is invoked to support both the two-sided fidelity theorem and the DTMC encodings, yet no explicit mapping function, error bound on effective weight ratios, or analysis of impact on probabilistic transition probabilities is supplied; this is load-bearing because even small distortions could invalidate the gray-zone confinement.

Authors: The abstract summarizes the contribution at a high level. The explicit mapping function, error bounds on weight ratios, and analysis of effects on transition probabilities are supplied in the full manuscript. We agree the abstract would be strengthened by briefly indicating the mapping and bound, and will revise it accordingly. revision: yes
Referee: [Abstract] Abstract (statement of the two theorems): the fidelity and Asymptotic Silence theorems are presented as formal correctness guarantees without proof sketches, derivation outlines, or error bounds tied to the free discretization parameter W, preventing assessment of whether the guarantees survive the weight mapping for the DTMC semantics.

Authors: The abstract announces the theorems without sketches, as is conventional. The full manuscript contains the proofs, derivation outlines, and W-dependent bounds. We will revise the abstract to note the dependence of the gray-zone bound on W. revision: yes

Circularity Check

0 steps flagged

No circularity detected; derivation relies on introduced abstraction and external formal guarantees

full rationale

The paper defines a weight-discretized quotient abstraction that maps continuous weights to integers while preserving relative contributions, then states two-sided fidelity and Asymptotic Silence theorems as formal correctness guarantees. These steps are presented as new contributions building on general-purpose quotient abstractions cited externally as [1]. No quoted equations, self-citations, or claims reduce the theorems or scaling analysis to fitted inputs, definitional equivalences, or load-bearing prior self-work; the chain remains self-contained with independent formal content.

Axiom & Free-Parameter Ledger

1 free parameters · 1 axioms · 0 invented entities

Abstract-only review yields minimal ledger entries; the discretization step and DTMC encoding are the main additions beyond standard probabilistic model checking.

free parameters (1)

discretization parameter W
Integer range size for synaptic weights; value W=3 used for the 17× reduction claim.

axioms (1)

domain assumption DTMC encoding of SNN dynamics is a valid probabilistic model
Invoked when stating that general quotient abstractions apply but discard weight information.

pith-pipeline@v0.9.1-grok · 5805 in / 1303 out tokens · 28444 ms · 2026-06-27T04:39:24.256725+00:00 · methodology

0 comments

read the original 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\"ive 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.

discussion (0)

Reference graph

Works this paper leans on

16 extracted references · 3 canonical work pages

[1]

MIT Press (2008)

Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)

2008
[2]

Neural Networks

Maass, W.: Networks of Spiking Neurons: The Third Generation of Neural Network Models. Neural Networks. 10, 1659–1671 (1997). 14 N. Zandian Jazi, E. De Maria, C. Leturc

1997
[3]

The Journal of Physiology

Hodgkin, A.L., Huxley, A.F.: A Quantitative Description of Membrane Current and Its Application to Conduction and Excitation in Nerve. The Journal of Physiology. 117, 500–544 (1952)

1952
[4]

IEEE Transactions on neural networks

Izhikevich, E.M.: Simple model of spiking neurons. IEEE Transactions on neural networks. 14, 1569–1572 (2003)

2003
[5]

T., Iacopi, F.: A Review of Algorithms and Hardware Implementations for Spiking Neural Networks

Nguyen, D.A., Tran, X. T., Iacopi, F.: A Review of Algorithms and Hardware Implementations for Spiking Neural Networks. Journal of Low Power Electronics and Applications. 11, 23 (2021)

2021
[7]

Cambridge University Press (2002)

Gerstner, W., Kistler, W.M.: Spiking Neuron Models: Single Neurons, Populations, Plasticity. Cambridge University Press (2002)

2002
[8]

Neural Computation

Brunel, N., Hakim, V.: Fast Global Oscillations in Networks of Integrate andFire Neurons with Low Firing Rates. Neural Computation. 11, 1621–1671 (1999)

1999
[9]

Stimberg, M., Brette, R., Goodman, D.F.M.: Brian 2, an Intuitive and Efficient Neural Simulator. eLife. 8, e47314 (2019)

2019
[10]

Frontiers in Neuroinformatics

Bekolay, T., Bergstra, J., Hunsberger, E., DeWolf, T., Stewart, T.C., Rasmussen, D., Choo, X., Voelker, A., Eliasmith, C.: Nengo: A Python Tool for Building Large Scale Functional Brain Models. Frontiers in Neuroinformatics. 7, 48 (2014)

2014
[11]

Scholarpedia

Gewaltig, M.O., Diesmann, M.: NEST (NEural Simulation Tool). Scholarpedia. 2, 1430 (2007)

2007
[12]

Frontiers in Neuroinformatics

Hazan, H., Saunders, D.J., Khan, H., Patel, D., Sanghavi, D.T., Siegelmann, H.T., Kozma, R.: BindsNET: A Machine Learning Oriented Spiking Neural Networks Library in Python. Frontiers in Neuroinformatics. 12, 89 (2018). https://doi.org/10. 3389/fninf.2018.00089

work page arXiv 2018
[13]

De Maria, E., Di Giusto, C., Laversa, L.: Spiking neural networks modelled as timed automata: with parameter learning. Nat. Comput. 19, 135–155 (2020). https://doi. org/10.1007/S11047019097279

work page doi:10.1007/s11047 2020
[14]

Frontiers of Computer Science

De Maria, E., Bahrami, A., L'Yvonnet, T., Felty, A., Gaffé, D., Ressouche, A., Grammont, F.: On the Use of Formal Methods to Model and Verify Neuronal Archetypes. Frontiers of Computer Science. 16, 163404 (2022). https://doi.org/ 10. 1007/S1170402000296

2022
[16]

Formal aspects of computing

Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal aspects of computing. 6, 512–535 (1994). Formal Verification of SNNs via Quotient Abstractions 15

1994
[17]

(Eds.), Advanced Manufacturing in Biological, Petroleum, and Nanotechnology Processing, Green Energy and Technology

Katoen, J.P., Kemna, T., Zapreev, I.S., Jansen, D.N.: Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking. In: Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007. pp. 87–101 (2007). https://doi.org/10.1007/9783540712091\_9

work page doi:10.1007/978 2007
[18]

In: Real Neurons Hidden Units: Future Directions at the Intersection of Neuroscience and Artificial Intelligence @ NeurIPS (2019)

Bellec, G., Scherr, F., Hajek, A., Salaj, D., Legenstein, R., Maass, W.: Eligibility Traces Provide a DataInspired Alternative to Backpropagation Through Time. In: Real Neurons Hidden Units: Future Directions at the Intersection of Neuroscience and Artificial Intelligence @ NeurIPS (2019)

2019

[1] [1]

MIT Press (2008)

Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)

2008

[2] [2]

Neural Networks

Maass, W.: Networks of Spiking Neurons: The Third Generation of Neural Network Models. Neural Networks. 10, 1659–1671 (1997). 14 N. Zandian Jazi, E. De Maria, C. Leturc

1997

[3] [3]

The Journal of Physiology

Hodgkin, A.L., Huxley, A.F.: A Quantitative Description of Membrane Current and Its Application to Conduction and Excitation in Nerve. The Journal of Physiology. 117, 500–544 (1952)

1952

[4] [4]

IEEE Transactions on neural networks

Izhikevich, E.M.: Simple model of spiking neurons. IEEE Transactions on neural networks. 14, 1569–1572 (2003)

2003

[5] [5]

T., Iacopi, F.: A Review of Algorithms and Hardware Implementations for Spiking Neural Networks

Nguyen, D.A., Tran, X. T., Iacopi, F.: A Review of Algorithms and Hardware Implementations for Spiking Neural Networks. Journal of Low Power Electronics and Applications. 11, 23 (2021)

2021

[6] [7]

Cambridge University Press (2002)

Gerstner, W., Kistler, W.M.: Spiking Neuron Models: Single Neurons, Populations, Plasticity. Cambridge University Press (2002)

2002

[7] [8]

Neural Computation

Brunel, N., Hakim, V.: Fast Global Oscillations in Networks of Integrate andFire Neurons with Low Firing Rates. Neural Computation. 11, 1621–1671 (1999)

1999

[8] [9]

Stimberg, M., Brette, R., Goodman, D.F.M.: Brian 2, an Intuitive and Efficient Neural Simulator. eLife. 8, e47314 (2019)

2019

[9] [10]

Frontiers in Neuroinformatics

Bekolay, T., Bergstra, J., Hunsberger, E., DeWolf, T., Stewart, T.C., Rasmussen, D., Choo, X., Voelker, A., Eliasmith, C.: Nengo: A Python Tool for Building Large Scale Functional Brain Models. Frontiers in Neuroinformatics. 7, 48 (2014)

2014

[10] [11]

Scholarpedia

Gewaltig, M.O., Diesmann, M.: NEST (NEural Simulation Tool). Scholarpedia. 2, 1430 (2007)

2007

[11] [12]

Frontiers in Neuroinformatics

Hazan, H., Saunders, D.J., Khan, H., Patel, D., Sanghavi, D.T., Siegelmann, H.T., Kozma, R.: BindsNET: A Machine Learning Oriented Spiking Neural Networks Library in Python. Frontiers in Neuroinformatics. 12, 89 (2018). https://doi.org/10. 3389/fninf.2018.00089

work page arXiv 2018

[12] [13]

De Maria, E., Di Giusto, C., Laversa, L.: Spiking neural networks modelled as timed automata: with parameter learning. Nat. Comput. 19, 135–155 (2020). https://doi. org/10.1007/S11047019097279

work page doi:10.1007/s11047 2020

[13] [14]

Frontiers of Computer Science

De Maria, E., Bahrami, A., L'Yvonnet, T., Felty, A., Gaffé, D., Ressouche, A., Grammont, F.: On the Use of Formal Methods to Model and Verify Neuronal Archetypes. Frontiers of Computer Science. 16, 163404 (2022). https://doi.org/ 10. 1007/S1170402000296

2022

[14] [16]

Formal aspects of computing

Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal aspects of computing. 6, 512–535 (1994). Formal Verification of SNNs via Quotient Abstractions 15

1994

[15] [17]

(Eds.), Advanced Manufacturing in Biological, Petroleum, and Nanotechnology Processing, Green Energy and Technology

Katoen, J.P., Kemna, T., Zapreev, I.S., Jansen, D.N.: Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking. In: Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007. pp. 87–101 (2007). https://doi.org/10.1007/9783540712091\_9

work page doi:10.1007/978 2007

[16] [18]

In: Real Neurons Hidden Units: Future Directions at the Intersection of Neuroscience and Artificial Intelligence @ NeurIPS (2019)

Bellec, G., Scherr, F., Hajek, A., Salaj, D., Legenstein, R., Maass, W.: Eligibility Traces Provide a DataInspired Alternative to Backpropagation Through Time. In: Real Neurons Hidden Units: Future Directions at the Intersection of Neuroscience and Artificial Intelligence @ NeurIPS (2019)

2019