# Compact Proofs of Model Performance via Mechanistic Interpretability

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

## Key facts

- Cited by 18 papers in the map (data through 14 Oct 2026).
- Placed in Circuits and mechanistic analysis, one of 13 directions in Mechanistic interpretability.
- Builds on 24 of its 48 references that are in the map.
- First posted on arXiv 17 Jun 2024.

## Placed in

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

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

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Scaling Laws for Neural Language Models](https://mlsanity.com/paper/2001.08361/) (2020)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Training Compute-Optimal Large Language Models](https://mlsanity.com/paper/2203.15556/) (2022)
- [Emergent Abilities of Large Language Models](https://mlsanity.com/paper/2206.07682/) (2022)
- [Interpretability in the Wild: a Circuit for Indirect Object Identification in GPT-2 small](https://mlsanity.com/paper/2211.00593/) (2022)
- [In-context Learning and Induction Heads](https://mlsanity.com/paper/2209.11895/) (2022)
- [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)
- [Transformers learn in-context by gradient descent](https://mlsanity.com/paper/2212.07677/) (2022)
- [What learning algorithm is in-context learning? Investigations with linear models](https://mlsanity.com/paper/2211.15661/) (2022)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Uniform convergence may be unable to explain generalization in deep learning](https://mlsanity.com/paper/1902.04742/) (2019)
- [How to use and interpret activation patching](https://mlsanity.com/paper/2404.15255/) (2024)
- [How does GPT-2 compute greater-than?: Interpreting mathematical abilities in a pre-trained language model](https://mlsanity.com/paper/2305.00586/) (2023)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [A Toy Model of Universality: Reverse Engineering How Networks Learn Group Operations](https://mlsanity.com/paper/2302.03025/) (2023)
- [Toward Transparent AI: A Survey on Interpreting the Inner Structures of Deep Neural Networks](https://mlsanity.com/paper/2207.13243/) (2022)
- [How Transformers Learn Causal Structure with Gradient Descent](https://mlsanity.com/paper/2402.14735/) (2024)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems](https://mlsanity.com/paper/2405.06624/) (2024)
- [A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation](https://mlsanity.com/paper/2305.11391/) (2023)
- [Formalizing the presumption of independence](https://mlsanity.com/paper/2211.06738/) (2022)

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

- [Interpretability as Compression: Reconsidering SAE Explanations of Neural Activations with MDL-SAEs](https://mlsanity.com/paper/2410.11179/) (2024)
- [Towards a unified and verified understanding of group-operation networks](https://mlsanity.com/paper/2410.07476/) (2024)
- [The Story is Not the Science: Execution-Grounded Evaluation of Mechanistic Interpretability Research](https://mlsanity.com/paper/2602.18458/) (2026)
- [Path Channels and Plan Extension Kernels: a Mechanistic Description of Planning in a Sokoban RNN](https://mlsanity.com/paper/2506.10138/) (2025)
- [Certified Interventional Fidelity: Anytime-Valid, Adaptive Evaluation of Causal Claims in Mechanistic Interpretability](https://mlsanity.com/paper/2607.08349/) (2026)
- [Modular addition without black-boxes: Compressing explanations of MLPs that compute numerical integration](https://mlsanity.com/paper/2412.03773/) (2024)
- [Learning the symmetric group: large from small](https://mlsanity.com/paper/2502.12717/) (2025)
- [Evaluating Explanations: An Explanatory Virtues Framework for Mechanistic Interpretability -- The Strange Science Part I.ii](https://mlsanity.com/paper/2505.01372/) (2025)
- [ConceptGuard: Neuro-Symbolic Safety Guardrails via Sparse Interpretable Jailbreak Concepts](https://mlsanity.com/paper/2508.16325/) (2025)
- [Knowing without Acting: The Disentangled Geometry of Safety Mechanisms in Large Language Models](https://mlsanity.com/paper/2603.05773/) (2026)
- [Input Pathways Shape Few-Shot, Not Zero-Shot, Binding in Tiny Transformers: A Fully-Enumerable Study](https://mlsanity.com/paper/2607.04926/) (2026)
- [Provably Overwhelming Transformer Models with Designed Inputs](https://mlsanity.com/paper/2502.06038/) (2025)
- [Towards a Law of Iterated Expectations for Heuristic Estimators](https://mlsanity.com/paper/2410.01290/) (2024)
- [Committed SAE-Feature Traces for Audited-Session Substitution Detection in Hosted LLMs](https://mlsanity.com/paper/2604.18179/) (2026)
- [Interactions Between Crosscoder Features: A Compact Proofs Perspective](https://mlsanity.com/paper/2606.09940/) (2026)
- [Can Graph Learning Learn Circuits?](https://mlsanity.com/paper/2608.08536/) (2026)
- [Certified Mechanistic Interpretability: Lifting Single-Input Findings to Bounded Neighbourhoods](https://mlsanity.com/paper/2609.26112/) (2026)
- [Certified Mechanistic Edits: Behavioral Guarantees for Skill Removal and Preservation](https://mlsanity.com/paper/2610.03502/) (2026)

## Abstract (arXiv)

We propose using mechanistic interpretability -- techniques for reverse engineering model weights into human-interpretable algorithms -- to derive and compactly prove formal guarantees on model performance. We prototype this approach by formally proving accuracy lower bounds for a small transformer trained on Max-of-K, validating proof transferability across 151 random seeds and four values of K. We create 102 different computer-assisted proof strategies and assess their length and tightness of bound on each of our models. Using quantitative metrics, we find that shorter proofs seem to require and provide more mechanistic understanding. Moreover, we find that more faithful mechanistic understanding leads to tighter performance bounds. We confirm these connections by qualitatively examining a subset of our proofs. Finally, we identify compounding structureless errors as a key challenge for using mechanistic interpretability to generate compact proofs on model performance.