SNNV

SNNV

Sound set-based robustness verification for first-to-fire (F2F) Leaky Integrate-and-Fire spiking neural networks. The spiking star set separates temporal spike patterns from affine propagation, enabling star-set reachability without exhaustive latency enumeration.

Python 3.10+ PyTorch / snnTorch Star-set reachability HiGHS LP MNIST / F-MNIST / CIFAR-10 / GTSRB

The Core Idea

Why SNN verification is hard, and the spiking-star insight that makes it tractable.

How Spike Star Works

Generalized star sets, F2F encoding, spike patterns, effective synapses, affine propagation, adaptive latency splitting.

Interactive Playground

Drag the input star (box or zonotope); watch the latency cells, membrane envelopes, score enclosure, and robustness verdict update live.

Benchmark Results

Per-case browser over MNIST / Fashion-MNIST / CIFAR-10 / GTSRB, with SMT-baseline comparison.

Getting Started

Install with uv and run the first-to-fire reachability demo.