Towards Verifiable Transformers: Solver-Checkable Circuit Explanations

Abstract

Mechanistic interpretability typically discovers circuits and then argues what they do from examples and ablations. We introduce Verifiable Transformers, a framework for turning task-localized circuits into bounded, solver-checkable claims: projected functional equivalence, task-relevant invariance, edge necessity, and robustness to continuous final-residual perturbations. At small scale, we directly verify all four properties for quote-closing and bracket-type circuits, including program-mediated circuits whose attention selection is entirely symbolic. At GPT-2 scale, we remove LayerNorm from a sparsemax/LeakyReLU model after training with a +0.0087 OpenWebText loss increase, replace retained attention heads with synthesized restricted-DSL programs, and calibrate only program-local readouts while freezing and hashing every other parameter. The resulting three-edge quote circuit (embedding $\to$ MLP 0 $\to$ program head $\to$ logits) verifies all four properties over a hash-pinned 1,280-prompt domain in linear real arithmetic: 1,280/1,280 equivalence and invariance, 640 edge-necessity witnesses per edge, and robustness at $ε= 0.01$ with minimum certified radius 0.01515. For two alphabet variants of the same opener-detection/copy-type task, untouched gates expose a localization frontier: bracket-type extraction is exact only with all 144 heads, while the constructed quote artifact verifies with three edges. Naive discovery-based verification failed for measured reasons; at scale, we find we must build the object we can verify. The verified object is a calibrated artifact, not the unmodified model, and all claims are bounded to declared domains.

Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.