Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees

Itamar Hadad; Guy Katz; Shahaf Bassan

cs.LGFeb 18, 2026

Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees

Authors: Itamar Hadad, Guy Katz, Shahaf Bassan

Organizations: School of Computer Science and Engineering, The Hebrew University of Jerusalem

Abstract

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.

Figures & tables

Figure 1: Illustration of the Siamese encoding for certifying the guarantee in Def. 1 .

Figure 2: Illustration of the Siamese encoding for certifying the guarantee in Def. 2 . Gray neurons denote non-circuit units whose activations are patched with those of the full model.

Figure 3: A toy Boolean circuit.

Dataset	Sampling-based Circuit Discovery			Provably Input-Robust Circuit Discovery
Dataset	Time (s)	Size ( $\|C\|$ )	Robustness (%)	Time (s)	Size ( $\|C\|$ )	Robustness (%)
CIFAR-10	0.23 $\pm 0.52$	16.47 $\pm 9.08$	46.5 $\pm 5.0$	2970.85 $\pm 874.23$	19.18 $\pm 10.16$	100.0 $\pm 0.0$
MNIST	0.31 $\pm 0.89$	12.56 $\pm 2.30$	19.2 $\pm 4.0$	611.93 $\pm 97.14$	15.84 $\pm 2.33$	100.0 $\pm 0.0$
GTSRB	0.11 $\pm 0.33$	28.91 $\pm 4.69$	27.6 $\pm 4.0$	991.08 $\pm 162.91$	29.59 $\pm 4.45$	100.0 $\pm 0.0$
TaxiNet	0.01 $\pm 0.00$	5.77 $\pm 0.80$	9.5 $\pm 3.0$	180.00 $\pm 40.39$	6.82 $\pm 0.46$	100.0 $\pm 0.0$

Table 1: Circuit results from Algorithm 1 , where

\Phi

is defined either by bounding logit differences under input sampling or by verifying the bound using the siamese encoding.

Figure 4: Examples of ResNet circuits at the filter level on CIFAR-10. Filters are numbered within each layer, with non-circuit filters in gray and residual connections shown as dashed lines. We compare circuits from the sampling-based discovery and the provably robust variant, highlighting components unique to the provable circuit in green.

Dataset	Zero Patching			Mean Patching			Provably Patching-Robust Patching
Dataset	Time (s)	Size ( $\|C\|$ )	Rob. (%)	Time (s)	Size ( $\|C\|$ )	Rob. (%)	Time (s)	Size ( $\|C\|$ )	Rob. (%)
CIFAR-10	0.1 $\pm$ 0.3	65.1 $\pm 3.0$	46.4 $\pm 6.0$	0.0 $\pm 0.0$	64.1 $\pm 3.6$	33.3 $\pm 5.7$	5408.5 $\pm 1091.0$	65.6 $\pm 1.6$	100.0
MNIST	0.1 $\pm 0.3$	20.0 $\pm 1.5$	58.0 $\pm 5.3$	0.0 $\pm 0.0$	19.2 $\pm 1.8$	55.7 $\pm 5.3$	714.9 $\pm 207.1$	17.0 $\pm 2.3$	100.0
GTSRB	0.3 $\pm 0.9$	32.6 $\pm 4.2$	38.0 $\pm 4.4$	0.0 $\pm 0.0$	33.4 $\pm 4.2$	40.5 $\pm 4.5$	2907.2 $\pm 721.7$	34.3 $\pm 4.1$	100.0
TaxiNet	0.0 $\pm 0.1$	5.8 $\pm 0.8$	57.1 $\pm 5.0$	0.0 $\pm 0.1$	5.4 $\pm 0.7$	63.3 $\pm 4.9$	175.7 $\pm 52.7$	5.4 $\pm 0.6$	100.0

Table 2: Circuit results from Algorithm 1 , where

\Phi

is defined either by bounding logit differences under zero patching, mean patching, or by verifying the bound using the siamese encoding.

Panel of Figure 5 — Figure 5: (a) Circuit size vs. MHS of blocking sets size, with the dashed equality line $y{=}x$ as the lower bound. (b) Convergence of circuit size over the first 10 minutes; shaded region shows deviation.

Appendix figures & tables17 assets

Supplementary material from the paper’s appendix.

Appendix

Panel of Figure 6 — Figure 6: Boolean toy network with XOR aggregation: $y=v_{1}\oplus v_{2}\oplus v_{3}\oplus v_{4}\oplus v_{5}$ . With $v_{1}=x_{2}$ , $v_{2}=v_{3}=x_{1}$ , $v_{4}=v_{5}=x_{1}\oplus x_{2}$ , and $v_{6}=x_{2}\oplus x_{2}=0$ the full model computes $f_{G}(x_{1},x_{2})=x_{2}$ .

Dataset	Model	Examined Granularity	# Components
MNIST	FC	Neurons	31
GTSRB	CNN	Filters	48
CIFAR-10	ResNet	Filters	72
TaxiNet	CNN	Filters	8

Appendix

Table 3: Granularity and number of components considered for circuit discovery across the benchmark models.

Layer / Block	Output Dim.	Details
Input	$32\times 32\times 3$	CIFAR-10 image
Conv1	$16\times 16\times 8$	$3\times 3$ , stride 2
Residual Block 1
Conv1	$8\times 8\times 16$	$3\times 3$ , stride 2
ReLU	$8\times 8\times 16$	non-linearity
Conv2	$8\times 8\times 16$	$3\times 3$ , stride 1

Appendix

Table 4: Full architecture of the ResNet2b model used in Bak et al. (2021) for the CIFAR-10 benchmark

Layer	Output Dim.	Details
Input	$32\times 32\times 3$	GTSRB image
Conv1	$32\times 32\times 16$	$3\times 3$ , padding 1, ReLU
AvgPool1	$16\times 16\times 16$	$2\times 2$
Conv2	$16\times 16\times 32$	$3\times 3$ , padding 1, ReLU
AvgPool2	$8\times 8\times 32$	$2\times 2$
Flatten	$1\times 2048$	–

Appendix

Table 5: Architecture of the GTSRB-CNN model used in ( Bassan et al., 2025a ) .

Layer	Dimensions	Activation
Input	$28\times 28=784$	–
Fully Connected (fc1)	$784\rightarrow 13$	ReLU
Fully Connected (fc2)	$13\rightarrow 11$	ReLU
Fully Connected (fc3)	$11\rightarrow 10$	–

Appendix

Table 6: Architecture of the fully connected MNIST network. The model has 31 hidden neurons in total, which we treat as the granularity for circuit discovery.

Layer	Output Dim.	Details
Input	$27\times 54\times 1$	TaxiNet image
Conv1	$27\times 54\times 4$	$3\times 3$ , padding 1, ReLU
Conv2	$27\times 54\times 4$	$3\times 3$ , padding 1, ReLU
Flatten	$1\times 5832$	–
FC1	$5832\rightarrow 20$	ReLU
FC2	$20\rightarrow 10$	ReLU

Appendix

Table 7: Architecture of the CNN regression model used for TaxiNet, following the VeriX framework ( Wu et al., 2023a ) .

Dataset	$\epsilon_{p}$	Sampling-based Circuit Discovery			Provably Input-Robust Circuit Discovery
		Time (s)	Size ( $\|C\|$ )	Robustness (%)	Time (s)	Size ( $\|C\|$ )	Robustness (%)
MNIST ( $\delta{=}2.0$ )
	$0.005$	0.015 $\pm 0.003$	12.57 $\pm 2.29$	46.0 $\pm 5.0$	677.36 $\pm 183.65$	14.51 $\pm 2.41$	100.0 $\pm 0.0$
	$0.009$	0.016 $\pm 0.013$	12.56 $\pm 2.30$	25.3 $\pm 4.4$	663.60 $\pm 181.13$	15.76 $\pm 2.25$	100.0 $\pm 0.0$
	$0.010$	0.309 $\pm 0.889$	12.56 $\pm 2.30$	19.2 $\pm 4.0$	611.93 $\pm 97.14$	15.84 $\pm 2.33$	100.0 $\pm 0.0$
	$0.050$	0.027 $\pm 0.065$	12.57 $\pm 2.29$	0.0 $\pm 0.0$	1700.05 $\pm 562.36$	28.75 $\pm 6.67$	100.0 $\pm 0.0$

Appendix

Table 8: Effect of varying the input neighborhood size

\epsilon_{p}

under a fixed tolerance

\delta

. Reported values are means with standard deviations. For robustness (a binary variable), we report the standard error (SE). Bold values indicate robustness percentages. Rows highlighted in gray correspond to the results selected in the main paper.

Dataset	$\delta$	Sampling-based Circuit Discovery			Provably Input-Robust Circuit Discovery
		Time (s)	Size ( $\|C\|$ )	Robustness (%)	Time (s)	Size ( $\|C\|$ )	Robustness (%)
MNIST ( $\epsilon_{p}{=}0.01$ )
	$0.50$	0.083 $\pm$ 0.329	19.72 $\pm$ 1.50	15.6 $\pm$ 3.8	460.14 $\pm$ 36.59	22.02 $\pm$ 2.52	100.0 $\pm$ 0.0
	$2.00$	0.309 $\pm$ 0.889	12.56 $\pm$ 2.29	19.2 $\pm$ 4.0	611.93 $\pm$ 97.14	15.84 $\pm$ 2.33	100.0 $\pm$ 0.0
	$3.00$	0.013 $\pm$ 0.001	9.44 $\pm$ 1.92	34.0 $\pm$ 4.7	577.41 $\pm$ 35.84	12.27 $\pm$ 2.52	100.0 $\pm$ 0.0
TaxiNet ( $\epsilon_{p}{=}0.005$ )

Appendix

Table 9: Variation on tolerance level

\delta

, with input neighborhood size

\epsilon

fixed to the dataset-specific values used in the main experiments. Reported values are means with standard deviations. For robustness (a binary variable), we report the standard error (SE). Rows highlighted in gray correspond to the results selected in the main paper.

Dataset	Metric	Sampling-based Circuit Discovery			Provably Input-Robust Circuit Discovery
		Time (s)	Size ( $\|C\|$ )	Robustness (%)	Time (s)	Size ( $\|C\|$ )	Robustness (%)
MNIST	Logit-diff	0.31 $\pm 0.89$	12.56 $\pm 2.30$	19.2 $\pm 4.0$	611.93 $\pm 97.14$	15.84 $\pm 2.33$	100.0 $\pm 0.0$
	Winner–Runner	0.13 $\pm$ 0.60	5.18 $\pm$ 1.05	73.0 $\pm 4.4$	638.57 $\pm$ 20.94	12.04 $\pm$ 5.79	100.0 $\pm 0.0$
	Abs-Max	0.014 $\pm$ 0.012	25.55 $\pm$ 2.90	6.0 $\pm 2.4$	362.61 $\pm$ 55.73	28.11 $\pm$ 2.37	100.0 $\pm 0.0$

Appendix

Table 10: Comparison of circuit discovery methods under alternative output metrics. Reported values are means with standard deviations. For robustness (a binary variable), we report the standard error (SE). All methods use the same configurations as in the main experiments.

Figure 7: Comparison of similarity and coverage metrics between provably-robust and sampling-based circuits. We report symmetric measures (IoU, Dice), a symmetric difference ratio, and asymmetric coverage ratios ( provable over sampling , sampling over provable ) to illustrate both overlap and directional differences.

Dataset	$\boldsymbol{\epsilon_{p}}$	$\;\boldsymbol{\|C_{p}\setminus C_{s}\|}\;$	% of full net	$\;\boldsymbol{\|C_{s}\setminus C_{p}\|}\;$	% of full net
MNIST	0.005	2.64	7.76%	0.70	2.06%
	0.007	3.32	9.76%	0.74	2.18%
	0.010	4.10	12.06%	0.81	2.38%
	0.020	6.24	18.35%	0.58	1.71%
	0.030	7.73	22.74%	0.39	1.15%
	0.040	10.94	32.18%	0.24	0.71%

Appendix

Table 11: Set differences between the provably-robust circuit

C_{p}

and the sampling-based circuit

C_{s}

. For each

\epsilon_{p}

, we report (i) the number of units appearing only in the provably-robust circuit

|C_{p}\setminus C_{s}|

, (ii) the number appearing only in the sampling-based circuit

|C_{s}\setminus C_{p}|

, and (iii) the corresponding percentages relative to the full network size for that dataset.

Figure 8: Provable-robust circuit size over time on MNIST for different neighborhood radii

\epsilon_{p}

. Shaded regions denote the standard deviation.

Panel of Figure 9 — Figure 9: Grad-CAM heatmaps comparison for a GTSRB input and its adversarial counterpart, shown at the last convolutional layer across three models (the full model, the provably robust circuit, and the sampling-based circuit).

Figure 10: Clean input $\mathbf{x}$ , its perturbed version $\mathbf{z}\in B^{p}_{\epsilon_{p}}(\mathbf{x})$ with $\epsilon_{p}=0.015$ , and the corresponding difference heatmap.

Panel of Figure 11 — Figure 11: (a) Activation maps of the shared first-layer filters present in both the provably robust and sampling-based circuits. (b) Activation map of the additional first-layer filter included only in the provably robust circuit. Blue indicates negative activations; red indicates positive activations. White denotes neutral or near-zero values.

Dataset	$\epsilon_{p}$	Zero Patching			Mean Patching			Provably Patching-Robust Patching
		Time (s)	Size ( $\|C\|$ )	Rob. (%)	Time (s)	Size ( $\|C\|$ )	Rob. (%)	Time (s)	Size ( $\|C\|$ )	Rob. (%)
MNIST ( $\delta{=}0.5$ )
	$0.005$	0.054 $\pm$ 0.182	19.87 $\pm$ 1.55	87.0 $\pm 3.4$	0.013 $\pm$ 0.001	19.19 $\pm$ 1.87	93.0 $\pm 2.6$	671.08 $\pm 36.86$	11.32 $\pm$ 2.56	100.0 $\pm 0.0$
	$0.009$	0.013 $\pm 0.000$	19.92 $\pm 1.51$	65.9 $\pm 5.0$	0.013 $\pm 0.001$	19.13 $\pm$ 1.88	64.8 $\pm 5.0$	583.59 $\pm 44.99$	16.75 $\pm$ 2.26	100.0 $\pm 0.0$
	0.010	0.060 $\pm 0.322$	19.96 $\pm 1.50$	58.0 $\pm 5.3$	0.016 $\pm 0.003$	19.16 $\pm 1.84$	55.7 $\pm 5.3$	714.87 $\pm 207.08$	17.03 $\pm 2.30$	100.0 $\pm 0.0$
	$0.050$	0.015 $\pm 0.005$	19.76 $\pm 1.50$	1.2 $\pm 1.2$	0.015 $\pm 0.003$	19.09 $\pm 1.81$	1.2 $\pm 1.2$	598.41 $\pm 156.96$	23.20 $\pm 1.17$	100.0 $\pm 0.0$

Appendix

Table 12: Variations on patching neighborhood size

\epsilon_{p}

with fixed tolerance

\delta

. Reported values are means with standard deviations (formatted as {mean

\pm

std}). For robustness (a binary outcome), we report the mean robustness with its standard error (SE), and display robustness values in bold . Rows highlighted in gray correspond to the results selected in the main paper.

Dataset	$\delta$	Zero Patching			Mean Patching			Provably Robust Patching
		Time (s)	Size ( $\|C\|$ )	Rob. (%)	Time (s)	Size ( $\|C\|$ )	Rob. (%)	Time (s)	Size ( $\|C\|$ )	Rob. (%)
MNIST ( $\epsilon_{p}{=}0.01$ )
	$0.25$	0.142 $\pm$ 0.476	21.36 $\pm$ 1.87	48.6 $\pm$ 5.9	0.013 $\pm$ 0.000	21.22 $\pm$ 1.74	52.8 $\pm$ 5.9	523.67 $\pm$ 41.31	19.42 $\pm$ 2.01	100.0 $\pm$ 0.0
	0.50	0.060 $\pm$ 0.322	19.96 $\pm$ 1.50	58.0 $\pm$ 5.3	0.016 $\pm$ 0.003	19.16 $\pm$ 1.84	55.7 $\pm$ 5.3	714.87 $\pm$ 207.08	17.03 $\pm$ 2.30	100.0 $\pm$ 0.0
	$1.00$	0.013 $\pm$ 0.000	16.88 $\pm$ 1.85	61.2 $\pm$ 4.9	0.013 $\pm$ 0.001	16.11 $\pm$ 1.93	66.3 $\pm$ 4.8	690.42 $\pm$ 44.38	11.37 $\pm$ 2.64	100.0 $\pm$ 0.0
TaxiNet ( $\epsilon_{p}{=}0.01$ )

Appendix

Table 13: Variation of tolerance level

\delta

with fixed patching neighborhood size

\epsilon_{p}=0.01

. Reported values are means with standard deviations (formatted as mean

\pm

std). For robustness (a binary outcome), we report the mean robustness with its standard error (SE), and display robustness means in bold . Rows highlighted in gray correspond to the results selected in the main paper.

Explore similar work

Feb 26, 2026

Certified Circuits: Stability Guarantees for Mechanistic Circuits

Understanding how neural networks arrive at their predictions is essential for debugging, auditing, and deployment. Mechanistic interpretability pursues this goal by identifying circuits--minimal subnetworks responsible for specific behaviors. However, existing circuit discovery methods are brittle: circuits depend strongly on the chosen concept dataset and often fail to transfer out-of-distribution, raising doubts whether they capture the concept or merely dataset-specific artifacts. We introduce Certified Circuits, which provide provable stability guarantees for circuit discovery. Our framework wraps any black-box discovery algorithm with randomized data subsampling to certify that inclusion decisions over circuit components--neurons or edges of the model graph, depending on the base algorithm--are invariant to bounded edit-distance perturbations of the concept dataset. Unstable components are abstained from, yielding circuits that are more compact and more accurate. We validate across three architectures (ResNet, ViT, GPT-2) on vision (ImageNet and four OOD datasets) and language (IOI, IOI-Hard, Greater-Than) tasks. Certified circuits achieve up to 56% higher accuracy and up to 80% fewer components, and remain reliable where baselines degrade. Certified Circuits puts circuit discovery on formal ground by producing mechanistic explanations that are provably stable and better aligned with the target concept. Code: https://github.com/AlaaAnani/certified-circuits.

Alaa Anani, Tobias Lorenz, Bernt Schiele +2

Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbrücken, Germany · CISPA Helmholtz Center for Information Security, Saarbrücken, Germany

Circuit Discovery Mechanistic Interpretability Circuits in Language Models

Ask PDF

Apr 15, 2026

Seeing Through Circuits: Faithful Mechanistic Interpretability for Vision Transformers

Transparency of neural networks' internal reasoning is at the heart of interpretability research, adding to trust, safety, and understanding of these models. The field of mechanistic interpretability has recently focused on studying task-specific computational graphs, defined by connections (edges) between model components. Such edge-based circuits have been defined in the context of large language models, yet vision-based approaches so far only consider neuron-based circuits. These tell which information is encoded, but not how it is routed through the complex wiring of a neural network. In this work, we investigate whether useful mechanistic circuits can be identified through computational graphs in vision transformers. We propose an effective method for Automatic Visual Circuit Discovery (Vi-CD) that recovers class-specific circuits for classification, identifies circuits underlying typographic attacks in CLIP, and discovers circuits that lend themselves for steering to correct harmful model behavior. Overall, we find that insightful and actionable edge-based circuits can be recovered from vision transformers, adding transparency to the internal computations of these models.

Nina Żukowska, Wolfgang Stammer, Bernt Schiele +1

Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbrücken, Germany

Transformer Interpretability Mechanistic Interpretability Circuit Discovery Vision Transformer VLM Interpretability

Ask PDF

Mar 31, 2026

Tracking Equivalent Mechanistic Interpretations Across Neural Networks

Mechanistic interpretability (MI) is an emerging framework for interpreting neural networks. Given a task and model, MI aims to discover a succinct algorithmic process, an interpretation, that explains the model's decision process on that task. However, MI is difficult to scale and generalize. This stems in part from two key challenges: there is no precise notion of a valid interpretation; and, generating interpretations is often an ad hoc process. In this paper, we address these challenges by defining and studying the problem of interpretive equivalence: determining whether two different models share a common interpretation, without requiring an explicit description of what that interpretation is. At the core of our approach, we propose and formalize the principle that two interpretations of a model are equivalent if all of their possible implementations are also equivalent. We develop an algorithm to estimate interpretive equivalence and case study its use on Transformer-based models. To analyze our algorithm, we introduce necessary and sufficient conditions for interpretive equivalence based on models' representation similarity. We provide guarantees that simultaneously relate a model's algorithmic interpretations, circuits, and representations. Our framework lays a foundation for the development of more rigorous evaluation methods of MI and automated, generalizable interpretation discovery methods.

Alan Sun, Mariya Toneva

Carnegie Mellon University · Max Planck Institute for Software Systems

Mechanistic Interpretability Transformer Interpretability

Ask PDF