Interactive Playground¶
The panel runs a small first-to-fire LIF toy network live (2 inputs, 2 output neurons). The input set is a generalized star (Definition on How Spike Star Works), \(\mathcal{I} = \{\mathbf{x} = \mathbf{c} + V\boldsymbol{\alpha} : \boldsymbol{\alpha}\in[-1,1]^m\}\) — a box when \(V\) is diagonal, a zonotope otherwise. Drag \(\mathbf{c}\), resize with \(\epsilon\), and shear or add a generator to deform the box into a zonotope and watch the certificate respond.
Each input fires once at its F2F latency \(\mathcal{L}(x) = \mathrm{round}((T-1)(1-x)) + 1\); the output neurons integrate the (binary) input spikes, and the class score is \(y_c = T+1-t_c^{\mathrm{out}}\), so the class whose output spikes first wins. The star is partitioned into latency cells; on each cell the spike pattern is fixed, so the output is exact, and the reachable scores are the union of the per-cell outcomes.
Four linked views update as you drag:
Input star & latency cells — the star (box or zonotope) and the latency-cell pieces it is partitioned into, each tinted by its winning class.
Output decision: class-score enclosure — the reachable \((y_0, y_1)\) score points (one per cell), the certified box enclosure \([\underline y_c, \overline y_c]\), and the tie diagonal. Robust when the box sits strictly on one side.
Membrane potentials + envelope — each output’s membrane as a band (min/max over the reachable cells), the center trace, the threshold \(\theta\), and the first-spike marker.
Spike raster + envelope — for each neuron, the could-fire range of timesteps over the star (the spike-train envelope) and the center spike.
The verdict certifies a strict score margin \(\underline y_{c^*} > \overline y_c\) over all reachable cells (a sound check, validated against sampling). Deforming the box into a zonotope changes which latency cells are reachable — so a skewed star can certify where an axis-aligned box cannot.