Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees

TL;DR

This work leverage recent advances in neural network verification to propose a suite of automated algorithms that yield circuits with provable guarantees, focusing on three types of guarantees: *input domain robustness*, ensuring the circuit agrees with the model across a continuous input region; *robust patching*, certifying circuit alignment under continuous patching perturbations; and *minimality*, formalizing and capturing a wide array of various notions of succinctness.

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 (11)

• Figure 1: Illustration of the Siamese encoding for certifying the guarantee in Def. \ref{['circuit_robustness_Def']}.
• Figure 2: Illustration of the Siamese encoding for certifying the guarantee in Def. \ref{['patching_robustness_property']}. Gray neurons denote non-circuit units whose activations are patched with those of the full model.
• Figure 3: A toy Boolean circuit.
• 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.
• 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.

Theorems & Definitions (28)

• Definition 1: Input‐robust circuit
• Definition 2: Patching‐robust circuit
• Definition 3: Quasi‐Minimal Circuit
• Definition 4: Locally‐Minimal Circuit
• Definition 5: Subset‐Minimal Circuit
• Definition 6: Cardinally‐Minimal Circuit
• Proposition 1
• Proposition 2
• Proposition 3
• Definition 7