Neural Decompilation: Extracting Verified Sparse Circuits from Transformer Weights

We introduce neural decompilation, a method that extracts readable, executable sparse circuits from trained neural network weights. On 13 RNN classification tasks, decompiled circuits achieve perfect accuracy with 6 formally verified by the Kani model checker across all possible inputs. Applied to production LLMs, we discover that layer-0 K projections are entropy outliers (4.3-7.3 sigma below cross-layer mean) containing discrete attention routing circuits absent in deeper layers. One TinyLlama attention head implements a multi-script classifier whose sparse circuit (2.7% of weights) is causally necessary (ablation Fisher 5.94 to 0.00), functionally faithful (interchange intervention KL = 0.00045, top-1 agreement 97.6%), and cross-architectural (replicated in Qwen2.5-0.5B with Fisher = 5.44). Code: https://github.com/thebasedcapital/neural-decompile