# Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees

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

## Key facts

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

## Placed in

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

## Builds on (most cited first, 30 of 93)

- [Grad-CAM: Visual Explanations from Deep Networks via Gradient-based Localization](https://mlsanity.com/paper/1610.02391/) (2016)
- [Interpretability in the Wild: a Circuit for Indirect Object Identification in GPT-2 small](https://mlsanity.com/paper/2211.00593/) (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)
- [Towards Automated Circuit Discovery for Mechanistic Interpretability](https://mlsanity.com/paper/2304.14997/) (2023)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Sparse Feature Circuits: Discovering and Editing Interpretable Causal Graphs in Language Models](https://mlsanity.com/paper/2403.19647/) (2024)
- [Mechanistic Interpretability for AI Safety -- A Review](https://mlsanity.com/paper/2404.14082/) (2024)
- [Towards Best Practices of Activation Patching in Language Models: Metrics and Methods](https://mlsanity.com/paper/2309.16042/) (2023)
- [Explainability for Large Language Models: A Survey](https://mlsanity.com/paper/2309.01029/) (2023)
- [A Survey on Neural Network Interpretability](https://mlsanity.com/paper/2012.14261/) (2020)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Finding Alignments Between Interpretable Causal Variables and Distributed Neural Representations](https://mlsanity.com/paper/2303.02536/) (2023)
- [Attribution Patching Outperforms Automated Circuit Discovery](https://mlsanity.com/paper/2310.10348/) (2023)
- [Causal Abstraction: A Theoretical Foundation for Mechanistic Interpretability](https://mlsanity.com/paper/2301.04709/) (2023)
- [Transcoders Find Interpretable LLM Feature Circuits](https://mlsanity.com/paper/2406.11944/) (2024)
- [Open Problems in Mechanistic Interpretability](https://mlsanity.com/paper/2501.16496/) (2025)
- [Abduction-Based Explanations for Machine Learning Models](https://mlsanity.com/paper/1811.10656/) (2018)
- [Have Faith in Faithfulness: Going Beyond Circuit Overlap When Finding Model Mechanisms](https://mlsanity.com/paper/2403.17806/) (2024)
- [A Symbolic Approach to Explaining Bayesian Network Classifiers](https://mlsanity.com/paper/1805.03364/) (2018)
- [Toward Transparent AI: A Survey on Interpreting the Inner Structures of Deep Neural Networks](https://mlsanity.com/paper/2207.13243/) (2022)
- [Interpretability at Scale: Identifying Causal Mechanisms in Alpaca](https://mlsanity.com/paper/2305.08809/) (2023)
- [On The Reasons Behind Decisions](https://mlsanity.com/paper/2002.09284/) (2020)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Model Interpretability through the Lens of Computational Complexity](https://mlsanity.com/paper/2010.12265/) (2020)
- [On the Role of Attention Heads in Large Language Model Safety](https://mlsanity.com/paper/2410.13708/) (2024)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)

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

- [Certified Circuits: Stability Guarantees for Mechanistic Circuits](https://mlsanity.com/paper/2602.22968/) (2026)
- [When Attribution Patching Lies: Diagnosis and a Second-Order Correction](https://mlsanity.com/paper/2606.09899/) (2026)
- [Unifying Formal Explanations: A Complexity-Theoretic Perspective](https://mlsanity.com/paper/2602.18160/) (2026)
- [Provably Explaining Neural Additive Models](https://mlsanity.com/paper/2602.17530/) (2026)
- [From Circuit Evidence to Mechanistic Theory: An Inductive Logic Approach](https://mlsanity.com/paper/2605.21303/) (2026)
- [Verified SHAP: Provable Bounds for Exact Shapley Values of Neural Networks](https://mlsanity.com/paper/2605.24084/) (2026)
- [IFCLoRA: Topology-Aware Rank Allocation for Parameter-Efficient Fine-Tuning](https://mlsanity.com/paper/2607.22251/) (2026)
- [LAWFUL: Law-Aligned Witness for Faithful Use of Latents](https://mlsanity.com/paper/2607.28672/) (2026)
- [The Misery of Mechanistic Interpretability: A Formal Perspective](https://mlsanity.com/paper/2609.15533/) (2026)
- [Representational Simplicity and Circuit Size Dissociate in a Threshold-Dependent Way: A Controlled Test via Adversarial Training](https://mlsanity.com/paper/2609.35890/) (2026)
- [Certified Mechanistic Edits: Behavioral Guarantees for Skill Removal and Preservation](https://mlsanity.com/paper/2610.03502/) (2026)

## Abstract (arXiv)

*Automated circuit discovery* is a central tool in mechanistic interpretability for identifying the internal components of neural networks responsible for specific behaviors. While prior methods have made significant progress, they typically depend on heuristics or approximations and do not offer provable guarantees over continuous input domains for the resulting circuits. In this work, we leverage recent advances in neural network verification to propose a suite of automated algorithms that yield circuits with *provable guarantees*. We focus on three types of guarantees: (1) *input domain robustness*, ensuring the circuit agrees with the model across a continuous input region; (2) *robust patching*, certifying circuit alignment under continuous patching perturbations; and (3) *minimality*, formalizing and capturing a wide array of various notions of succinctness. Interestingly, we uncover a diverse set of novel theoretical connections among these three families of guarantees, with critical implications for the convergence of our algorithms. Finally, we conduct experiments with state-of-the-art verifiers on various vision models, showing that our algorithms yield circuits with substantially stronger robustness guarantees than standard circuit discovery methods, establishing a principled foundation for provable circuit discovery.