# Towards Verifiable Transformers: Solver-Checkable Circuit Explanations

arXiv: https://arxiv.org/abs/2605.24033 · HTML: https://mlsanity.com/paper/2605.24033/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Circuits and mechanistic analysis, one of 13 directions in Mechanistic interpretability.
- Builds on 15 of its 46 references that are in the map.
- First posted on arXiv 21 May 2026.

## Placed in

- Mechanistic interpretability / [Circuits and mechanistic analysis](https://mlsanity.com/mechinterp/circuits-and-mechanistic-analysis/)

## Builds on (most cited first, 15 of 15)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Layer Normalization](https://mlsanity.com/paper/1607.06450/) (2016)
- [Parameter-Efficient Transfer Learning for NLP](https://mlsanity.com/paper/1902.00751/) (2019)
- [Gaussian Error Linear Units (GELUs)](https://mlsanity.com/paper/1606.08415/) (2016)
- [Pointer Sentinel Mixture Models](https://mlsanity.com/paper/1609.07843/) (2016)
- [Deep Sets](https://mlsanity.com/paper/1703.06114/) (2017)
- [Progress measures for grokking via mechanistic interpretability](https://mlsanity.com/paper/2301.05217/) (2023)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Towards Automated Circuit Discovery for Mechanistic Interpretability](https://mlsanity.com/paper/2304.14997/) (2023)
- [From Softmax to Sparsemax: A Sparse Model of Attention and Multi-Label Classification](https://mlsanity.com/paper/1602.02068/) (2016)
- [Adaptively Sparse Transformers](https://mlsanity.com/paper/1909.00015/) (2019)
- [Self-Attention Networks Can Process Bounded Hierarchical Languages](https://mlsanity.com/paper/2105.11115/) (2021)
- [RNNs can generate bounded hierarchical languages with optimal memory](https://mlsanity.com/paper/2010.07515/) (2020)
- [Weight-sparse transformers have interpretable circuits](https://mlsanity.com/paper/2511.13653/) (2025)
- [Transformers Don't Need LayerNorm at Inference Time: Scaling LayerNorm Removal to GPT-2 XL and the Implications for Mechanistic Interpretability](https://mlsanity.com/paper/2507.02559/) (2025)

## Built on by (most cited first, 1 of 1)

- [Certified Mechanistic Edits: Behavioral Guarantees for Skill Removal and Preservation](https://mlsanity.com/paper/2610.03502/) (2026)

## Abstract (arXiv)

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 → MLP 0 → program head → 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.