# BlockCert: Certified Blockwise Extraction of Transformer Mechanisms

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

## 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 12 of its 16 references that are in the map.
- First posted on arXiv 20 Nov 2025.

## Placed in

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

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Locating and Editing Factual Associations in GPT](https://mlsanity.com/paper/2202.05262/) (2022)
- [Mass-Editing Memory in a Transformer](https://mlsanity.com/paper/2210.07229/) (2022)
- [Toy Models of Superposition](https://mlsanity.com/paper/2209.10652/) (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)
- [TinyLlama: An Open-Source Small Language Model](https://mlsanity.com/paper/2401.02385/) (2024)
- [Editing Large Language Models: Problems, Methods, and Opportunities](https://mlsanity.com/paper/2305.13172/) (2023)
- [Towards Best Practices of Activation Patching in Language Models: Metrics and Methods](https://mlsanity.com/paper/2309.16042/) (2023)
- [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)
- [Knowledge Editing for Large Language Models: A Survey](https://mlsanity.com/paper/2310.16218/) (2023)

## 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 aspires to reverse-engineer neural networks into explicit algorithms, while model editing seeks to modify specific behaviours without retraining. Both areas are typically evaluated with informal evidence and ad-hoc experiments, with few explicit guarantees about how far an extracted or edited model can drift from the original on relevant inputs. We introduce BlockCert, a framework for certified blockwise extraction of transformer mechanisms, and outline how a lightweight extension can support certified local edits. Given a pre-trained transformer and a prompt distribution, BlockCert extracts structured surrogate implementations for residual blocks together with machine-checkable certificates that bound approximation error, record coverage metrics, and hash the underlying artifacts. We formalize a simple Lipschitz-based composition theorem in Lean 4 that lifts these local guarantees to a global deviation bound. Empirically, we apply the framework to GPT-2 small, TinyLlama-1.1B-Chat, and Llama-3.2-3B. Across these models we obtain high per-block coverage and small residual errors on the evaluated prompts, and in the TinyLlama setting we show that a fully stitched model matches the baseline perplexity within approximately 6e-5 on stress prompts. Our results suggest that blockwise extraction with explicit certificates is feasible for real transformer language models and offers a practical bridge between mechanistic interpretability and formal reasoning about model behaviour.