Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees

1. Problem Statement

Mechanistic Interpretability (MI) aims to reverse-engineer neural networks into human-understandable functional modules called circuits. A central challenge in this field is circuit discovery: identifying the specific subgraphs (neurons, filters, attention heads) responsible for a model's behavior.

Current state-of-the-art methods rely heavily on heuristics and sampling-based approximations (e.g., zero-patching or mean-patching on discrete input samples). These approaches suffer from critical limitations:

• Lack of Robustness: A circuit found to be faithful on a discrete set of samples may fail under infinitesimal continuous perturbations of the input or the patched activations.
• No Provable Guarantees: There is no formal assurance that the discovered circuit behaves identically to the full model across a continuous input domain.
• Ambiguity in Minimality: Existing definitions of "minimal" circuits vary (quasi-minimal, local-minimal, etc.), and algorithms often converge to suboptimal solutions without rigorous theoretical backing.

The paper addresses the need for a framework that discovers circuits with provable guarantees over continuous domains, ensuring faithfulness, robustness, and minimality.

2. Methodology

The authors propose a novel framework that integrates Neural Network Verification (NNV) with circuit discovery. Instead of sampling, they use formal verification tools to mathematically prove that a circuit satisfies specific properties.

A. Provable Guarantees Definitions

The paper formalizes three types of guarantees:

1. Input-Domain Robustness: The circuit must match the full model's output within a tolerance $\delta$ for all inputs in a continuous region (e.g., an $\ell_p$-ball around a data point), not just sampled points.
2. Patching-Domain Robustness: The circuit must remain faithful even when the non-circuit components are patched with any feasible activation values derived from a continuous input domain, rather than fixed constants (zero/mean).
3. Minimality: Formalizing various notions of succinctness, ranging from Quasi-minimality (removing one element breaks faithfulness) to Cardinally-minimality (the globally smallest faithful circuit).

B. Technical Innovation: Siamese Encoding

To verify these properties, the authors introduce a Siamese Network encoding:

• For Input Robustness: They duplicate the circuit and "stack" it with the full model sharing an input layer. The verifier checks if the distance between the logits of the full model and the circuit (with non-circuit parts fixed) remains below $\delta$ for all inputs in the domain.
• For Patching Robustness: They use a dual-input Siamese network. One branch processes the input $x$ through the circuit, while the other processes a perturbed input $z$ through the full model to generate patching values. The verifier ensures the circuit's output on $x$ matches the full model's output on $x$ even when non-circuit parts are replaced by activations from $z$.

C. Algorithms and Theoretical Connections

The paper establishes deep theoretical connections between monotonicity and minimality:

• Circuit Monotonicity: A predicate $\Phi$ is monotonic if adding components to a faithful circuit preserves faithfulness. The authors prove that if the input and patching domains satisfy specific closure properties, the robustness predicate is monotonic.
• Algorithmic Convergence:
  • Greedy Search (Alg 1): Under monotonicity, a simple greedy removal algorithm converges to a Subset-Minimal circuit (no subset is faithful).
  • Blocking-Set Duality: To achieve Cardinally-Minimal circuits (global optimum), the authors leverage a duality between circuits and "blocking sets" (subgraphs whose removal breaks faithfulness). They formulate the problem as finding a Minimum Hitting Set (MHS) of these blocking sets, solvable via MaxSAT/MILP solvers.

3. Key Contributions

1. Formal Framework for Circuit Discovery: The first framework to derive circuits with provable guarantees over continuous input and patching domains, moving beyond sampling-based heuristics.
2. Theoretical Unification: Discovery of novel theoretical connections between input robustness, patching robustness, and minimality. Specifically, proving that under certain conditions, robustness predicates are monotonic, which guarantees that greedy algorithms find subset-minimal circuits.
3. Novel Algorithms:
   • A Siamese encoding technique to certify robustness using existing NNV tools (like $\alpha$-$\beta$-CROWN).
   • An MHS-based algorithm (Algorithm 2) that approximates or exactly recovers cardinally-minimal circuits, bridging the gap between local and global minimality.
4. Comprehensive Definitions: Formalization of a hierarchy of minimality (Quasi $\to$ Local $\to$ Subset $\to$ Cardinal) and the conditions under which algorithms converge to each.

4. Experimental Results

The authors evaluated their framework on standard vision benchmarks (MNIST, CIFAR-10, GTSRB, TaxiNet) using the state-of-the-art verifier $\alpha$-$\beta$-CROWN.

• Robustness:
  • Input Robustness: The provable method achieved 100% robustness across continuous input neighborhoods, whereas sampling-based baselines achieved only 9.5% to 46.5% robustness. Even small perturbations broke the faithfulness of sampling-based circuits.
  • Patching Robustness: Similarly, the provable method maintained 100% robustness against continuous patching perturbations, while zero/mean patching baselines dropped to 0–63% robustness.
• Circuit Size: Despite the rigorous constraints, the provable circuits had comparable sizes to sampling-based circuits (e.g., 15.8 vs 12.5 neurons for MNIST), demonstrating that robustness does not necessarily require significantly larger circuits.
• Minimality: The MHS-based approach successfully identified circuits that were cardinally minimal or provided tight lower bounds on the minimal size, outperforming greedy search in finding the most succinct explanations.
• Trade-offs: The provable method is computationally more expensive (minutes vs. seconds per circuit) due to the verification queries, but the trade-off yields mathematically guaranteed reliability.

5. Significance

This work represents a paradigm shift in Mechanistic Interpretability:

• From Heuristic to Formal: It transitions the field from relying on empirical sampling (which can be brittle) to formal verification, ensuring that discovered circuits are robust by mathematical proof.
• Safety and Trust: By guaranteeing that circuits hold under continuous perturbations, the work addresses critical safety concerns in deploying AI systems, where small input changes could otherwise invalidate interpretability claims.
• Theoretical Foundation: The establishment of monotonicity and duality principles provides a rigorous theoretical basis for future algorithm design in interpretability, linking it closely with formal methods and optimization theory.
• Scalability Path: While currently limited by the scalability of NNV tools, the paper lays the groundwork for provable interpretability as verification tools continue to scale to larger models.

In summary, the paper establishes a principled foundation for provable circuit discovery, demonstrating that it is possible to automatically find small, faithful, and robust neural network subgraphs with mathematical certainty.