How Spike Star Works

This page traces the verifier from input set to robustness certificate, following the formulation used in the paper. The implementation lives in src/snn_decomp/ (sets/star.py, EffectiveSynapses.py, sets/ftf_star_rep.py).

1. The generalized star set

The input set is a generalized star \(\Theta = \langle \mathbf{c}, V, P\rangle\), representing

\[\llbracket\Theta\rrbracket = \Bigl\{\, \mathbf{x} = \mathbf{c} + \textstyle\sum_{i=1}^{m} \alpha_i \mathbf{v}_i \;\;\text{s.t.}\;\; P(\boldsymbol{\alpha}):\; C\boldsymbol{\alpha}\le \mathbf{d} \,\Bigr\},\]

with center \(\mathbf{c}\), basis vectors \(V=\{\mathbf{v}_1,\dots,\mathbf{v}_m\}\), and a conjunction of linear predicates \(P\). This one representation generalizes hyperrectangles (boxes), zonotopes, and convex polytopes through the choice of \(V\) and \(P\) — a box is \(V=\mathrm{diag}(\epsilon)\) with \(\boldsymbol{\alpha}\in[-1,1]^m\); a zonotope keeps the box predicate but allows non-axis-aligned \(V\).

2. F2F encoding and decoding

First-to-fire latency encoding maps a normalized input \(x\in[0,1]\) to a single spike time

\[\mathcal{L}(x) = \mathrm{round}\bigl((T-1)(1-x)\bigr) + 1 \;\;(x>0), \qquad \mathcal{L}(0) = \infty,\]

so brighter inputs fire earlier (\(x=1\) at \(t=1\)) and a zero input never fires. Decoding scores each class by its first output spike time \(t_c^{\mathrm{out}}\):

\[\begin{split}y_c = \begin{cases} T+1-t_c^{\mathrm{out}}, & t_c^{\mathrm{out}}<\infty,\\ 0, & \text{otherwise,}\end{cases}\end{split}\]

so an earlier output spike yields a larger score, and the predicted class is \(\arg\max_c y_c\).

3. LIF dynamics

Each LIF neuron integrates synaptic current with a leak and a subtract reset:

\[V_{ij}[t] = \beta_i V_{ij}[t-1] + \textstyle\sum_k W_{ijk}\,s_{i-1,k}[t] + b_{ij} - V_{\mathrm{th}}\,s_{ij}[t-1], \qquad s_{ij}[t] = \mathbf{1}\{V_{ij}[t]\ge V_{\mathrm{th}}\}.\]

Under F2F encoding every neuron fires at most once (a has-fired mask prevents re-firing), so the spatiotemporal firing activity is a sparse binary table.

4. Spike patterns and effective synapses

Stacking the per-timestep spike vectors gives the layer spike train \(\mathbf{S}_i\in\{0,1\}^{T\times N_i}\); collecting them across layers gives the spike pattern \(\boldsymbol{\sigma}=(\mathbf{S}_1,\dots,\mathbf{S}_L)\). Because \(\mathbf{s}_{i-1}[t]\) is binary, the synaptic current is a column-masked weight — the effective synapses

\[\mathbf{W}_i^{\mathrm{eff}}[t] = \mathbf{W}_i \odot \mathbf{s}_{i-1}[t]^\top .\]

Once the encoded input spikes and the spike pattern \(\boldsymbol{\sigma}\) are fixed, every effective weight is determined and each finite-horizon update is affine in the star predicate variables. This is the piecewise-affine structure star sets exploit.

5. The spiking star set

Different inputs in the star may produce different spike patterns, partitioning the predicate space into finitely many cells. The spiking star set \(\mathcal{S}=\langle \mathbf{c}, V, P, \Sigma\rangle\) augments the star with the set \(\Sigma\) of reachable patterns and represents the output as a union

\[\llbracket\mathcal{S}\rrbracket = \bigcup_{\boldsymbol{\sigma}\in\Sigma} \bigl\{ f_{\boldsymbol{\sigma}}(\mathbf{x}) \;:\; \mathbf{x}\in\llbracket\Theta\rrbracket \text{ refined to } \boldsymbol{\sigma} \bigr\},\]

where \(f_{\boldsymbol{\sigma}}\) is the affine map on that pattern’s cell. (No Minkowski sum over time — the temporal recurrence is folded into each affine \(f_{\boldsymbol{\sigma}}\), and the reachable set is the union across cells.)

6. Spiking affine propagation

On a cell with fixed pattern, \(f_{\boldsymbol{\sigma}}(\mathbf{x})=A_{\boldsymbol{\sigma}}\mathbf{x}+\mathbf{b}_{\boldsymbol{\sigma}}\), and the star image is exact with the predicate unchanged:

\[f_{\boldsymbol{\sigma}}(\Theta) = \bigl\langle\, A_{\boldsymbol{\sigma}}\mathbf{c}+\mathbf{b}_{\boldsymbol{\sigma}},\; \{A_{\boldsymbol{\sigma}}\mathbf{v}_1,\dots,A_{\boldsymbol{\sigma}}\mathbf{v}_m\},\; P \,\bigr\rangle .\]

Applying the same affine image over a larger predicate region yields a sound enclosure of that component.

7. Enclosure and robustness

The verifier produces a box enclosure of the reachable scores, \(\widehat{\mathcal{R}} = \prod_c [\underline y_c, \overline y_c]\), by bounding each class score (one bound and one margin LP per competing class). The input set is certified robust for class \(c^*\) when

\[\underline y_{c^*} > \overline y_c \quad \text{for all } c\neq c^*\]

(a strict margin; exact ties are not certified).

8. Symbolic relaxation and adaptive latency splitting

Enumerating \(\Sigma\) is exponential, so the verifier never builds it. It starts with one symbolic relaxation over the full input set — relaxing each ambiguous hidden spike decision to a continuous predicate variable with a step-hull over-approximation — and refines only when the relaxation cannot certify the pairwise margins. Refinement splits input F2F latency cells adaptively: no split is purely symbolic; fixing all perturbed-input latencies recovers exact latency-level analysis. The split order affects runtime but not soundness.

Note

The Interactive Playground runs this pipeline live on a 2-input toy with a star (box or zonotope) input, showing the latency cells, the per-class score enclosure, the membrane envelopes, and the spike-train ranges, with a sound margin verdict.