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
   :doc:`playground` page, and see the per-layer operations in
   :doc:`spike_star`.