Do Transformers Learn What Theory Predicts? Knowledge Representation-Guided Mechanistic Verification via Causal Abstraction

Knowledge Representation (KR) formalisms provide precise specifications of algorithmic structure, yet it remains unclear whether gradient-trained neural networks implement these specifications even when they are theoretically expressible. Recent formal language theory tells us what Transformers can express—masked hard-attention Transformers recognize the star-free regular languages, equivalent to first-order logic with linear order (FO[<]) and linear temporal logic (LTL)—but not what gradient-trained Transformers will learn.

We ask whether trained networks actually implement the logical circuits that theory predicts, and propose KR-Guided Mechanistic Verification to find out.

The idea is to compile a B-RASP specification into a Structural Causal Model whose variables correspond to prescribed logical operations, then use Distributed Alignment Search to obtain quantitative, falsifiable causal evidence for or against each operation's presence in the trained network. We instantiate this framework on binary increment, a task for which B-RASP prescribes an explicit three-stage circuit implementable by a two-layer Transformer with O(poly(n)) parameters—exponentially fewer states than any fixed-precision recurrent or state space baselines require.

The answer is affirmative: all three prescribed operations are faithfully encoded in dedicated neural subspaces, with wrong-specification controls at chance; Sparse Autoencoder decomposition independently recovers the same logical structure without supervision. Moreover, this structure is not acquired gradually: it emerges as a sharp phase transition during grokking, providing a specification-aligned progress measure that reveals what changes during the generalization transition, not merely that something changes. These results demonstrate that KR formalisms can serve not only as prescriptive specifications of what networks should compute, but as falsifiable causal hypotheses that mechanistic interpretability tools can rigorously test—bridging the gap between symbolic KR and neural computation.