The Core Idea

The verification challenge

A spiking neural network (SNN) communicates through sparse spike events. In a first-to-fire (F2F) Leaky Integrate-and-Fire (LIF) network, each neuron integrates incoming current into a membrane potential, fires a spike when the potential crosses a threshold, and resets. The network’s decision depends on which neuron fires first — that is, on spike timing.

This makes robustness verification hard for three reasons:

  • Temporal state. The output depends on membrane memory accumulated over the whole time horizon, not on a single feed-forward pass.

  • Discrete events. Threshold crossings and resets are non-smooth: a small input change can move a spike to a different timestep.

  • Combinatorial latency. A naive verifier enumerates firing schedules over time; the number of schedules grows combinatorially in the horizon and the number of perturbed inputs.

Standard neural-network verifiers are built for smooth feed-forward maps and do not represent this spike-driven temporal structure.

The spiking-star insight

SNNV’s contribution is the spiking star set: a symbolic representation that separates the temporal spike pattern from the affine propagation.

  • The temporal part is the discrete firing schedule (which input fires at which timestep). The set of possible inputs is partitioned into latency cells, one per firing schedule.

  • The affine part is the propagation of the input through the network given a fixed spike pattern. With the pattern fixed, membrane integration and the linear layers compose into a single affine map, so the input set maps to an output set exactly. The input set is a generalized star x = c + Σ αᵢ vᵢ, C·α ≤ d — one representation that covers boxes, zonotopes, and convex polytopes.

The reachable output is the union of these per-pattern affine images. The verifier encloses it with per-class score bounds and certifies a strict classification margin. To avoid enumerating the exponentially many patterns, it keeps one symbolic relaxation of the ambiguous spike decisions and refines by adaptive latency splitting only where the margin is not yet certified — sound at every depth.

Note

Walk through this decomposition interactively on the Interactive Playground page, and see the per-layer operations in How Spike Star Works.