Writing Provably Correct Spiking Circuits with LLMs

Neuromorphic algorithms are usually designed by hand, and gradient training of spiking networks struggles with tasks that need long-lived discrete state. We ask whether a large language model (LLM) can act as the circuit designer. An LLM Writer (Claude Opus) reads a plain-language specification of a task and of an integer leaky-integrate-and-fire network model (S0), and writes every weight, threshold, leak and delay without running the network. On 13 streaming tasks (arithmetic, divisibility, bounded-depth Dyck-1 and modular-arithmetic expressions) we made 5 attempts each. All 65 networks pass the official scorer. A product-automaton search proves 57 of them correct for every input length and 7 more for every length below a bound set by the 32-bit membrane limit (all bounds above 6.5 × 10^7 steps); 1 is wrong on a length-20 input that the scorer never tries. Trained on input-output streams of length up to 10, surrogate-gradient BPTT finds exact networks on the four tasks with one bit of state (171/180 runs), at 10–24× the Writer's size, and none on the other 9 tasks (0/487); training on longer streams adds only mul13 (4/10). Our re-implementations of EventProp and of a convex spiking-network trainer find none on the seven original hard tasks either (0/105 and 0/63). The written networks also run with fewer synaptic operations than the gradient-trained ones (2.3–6.2× fewer, best against best), and all 66 written networks on the original 11 tasks export bit-exactly to the Neuromorphic Intermediate Representation (NIR). We do not claim that spiking networks are untrainable in general.