PaperlayerView exact revision on arXiv

Source-linked AI summary

The Misery of Mechanistic Interpretability: A Formal Perspective

Tobias Ladner, Matthias Althoff

arXiv:2609.15533v1cs.LGcs.AI

TL;DR

Mechanistic interpretability often relies on IRNs as proxies for dense model computations, but their faithfulness under adversarial inputs is not well established. The paper formally verifies IRN faithfulness and tests verification-aware training. It reports feature instability across five open-weight model families and a substantially reduced faithfulness gap after training.

  • Problem

    IRNs provide human-understandable features as proxies for dense model computations, but their faithfulness is usually assessed on clean data and adversarial survival is rarely tested or verified.

    Source: §1 · p. 1

  • Method

    The authors adapt neural-network verification to bound the difference between an LLM component and its IRN over adversarial input sets, then use verification-aware training to reduce that difference.

    Source: §4 · pp. 4–5, §8 · p. 9

  • Results

    Existing IRNs show substantial faithfulness gaps across five open-weight model families, while verification-aware training reduces the gap by 90%.

    Source: §8 · p. 9

  • Takeaways & Limitations

    Formal neural-network verification can provide bounds on IRN faithfulness and be applied to components of large language models.

    Source: §8 · p. 9

    The verification sets remain too small to verify the faithfulness of the entire LLM compositionally.

    Source: §6 · p. 8

Abstract

from arXiv · show

Mechanistic interpretability has become the dominant lens for understanding frontier language models, as their inner workings are complex and inherently black boxes. To gain insights into these models, interpretable replacement networks (IRNs) are trained at all layers, exposing interpretable features through sparsely activated neurons. However, the faithfulness of an IRN is usually evaluated only empirically on clean data, and we show that even semantically minor input perturbations flip the dominant IRN features-and thus the human-understandable interpretation-across five open-weight model families (GPT-2 small, Gemma 2 2B, Gemma 3 1B, Llama 3.2 1B, R1-Distill-Qwen 1.5B). We propose the first formal verification framework for the faithfulness of an IRN, where reachability analysis certifies a sound upper bound of the faithfulness gap in adversarial scenarios. Moreover, we show that verification-aware training of IRNs substantially tightens this certified bound, restoring a feature-level interpretation that safety auditors can act on. Together, these results give, to the best of our knowledge, the first formal guarantees for mechanistic interpretability of large language models.

1 INTRODUCTION

Mechanistic interpretations commonly rely on interpretable replacement networks (IRNs), so their trustworthiness depends on how closely they match the underlying model. This work highlights adversarial instability in IRN features and introduces formal verification and verification-aware training to address faithfulness.

1 INTRODUCTION

  • IRN features are proxies for dense model computations, so their interpretations are trustworthy only to the extent that the replacement network faithfully matches the model.Dense computations can produce polysemantic neurons, while IRNs expose a short list of human-understandable features.Source: §1 · p. 1
  • Adversarial survival of IRN interpretations is rarely tested or verified, and patching individual inputs partly defeats the goal of replicating the model’s true mechanism.The concern is whether interpretations persist under adversarial inputs, not only whether an IRN matches the model on clean data.Source: §1 · p. 1
  • Small adversarial input changes can alter exposed interpretations even though the underlying model itself has not changed.In the example, a paraphrase shifts the dominant features from a pathogen to a workplace sense of culture, changing a safety auditor’s response.Source: §1 · p. 1, Figure 1 · p. 2
  • The paper demonstrates IRN sensitivity across five open-weight model families, develops a formal faithfulness-verification framework, and shows verification-aware training narrows the faithfulness gap.The listed families are GPT-2, Gemma 2 2B, Gemma 3 1B, Llama 3.2 1B, and R1-Distill-Qwen 1.5B.Source: §1 · p. 2

2 BACKGROUND ON MECHANISTIC INTERPRETABILITY

The paper describes language-model layers as updates to a residual stream and explains why interpretable replacement networks are used to study otherwise difficult-to-interpret MLP computations. It focuses on sparse autoencoders and transcoders, whose sparse features provide human-readable proxies for model behavior.

2 BACKGROUND ON MECHANISTIC INTERPRETABILITY

  • Each transformer block adds the outputs of attention and an MLP back into the residual stream; attention mixes information across tokens, while the MLP transforms each token independently.The described architecture is a simplified high-level account used for the work.Source: §2 · p. 2
  • Because MLP neurons are densely entangled and polysemantic, the paper uses sparse, individually meaningful IRN activations as proxies for interpreting model computations.The two variants considered are sparse autoencoders and transcoders.Source: §2 · p. 2
  • Sparse autoencoders reconstruct the residual-stream input, whereas transcoders reconstruct the MLP output from the same input.Both are considered as layer-specific IRN variants.Source: §2 · pp. 2–3
  • A sparsity penalty limits how many hidden features activate, and labels are assigned by summarizing the inputs that activate each feature.Activation functions vary by model family: examples include ReLU, JumpReLU, and TopK.Source: §2 · p. 3

3 WHERE MECHANISTIC INTERPRETABILITY BREAKS

Across the tested IRNs, paraphrase attacks reduce overlap between clean-input and perturbed-input dominant features, potentially changing their interpretation. The evaluation spans three paraphrase severities, while the authors caution that attack-derived results do not establish the worst possible feature change.

3 WHERE MECHANISTIC INTERPRETABILITY BREAKS

  • Stable active features under semantically equivalent rephrasings are needed for their human-readable labels to reflect the model’s computation.The paper links unstable features to IRNs failing to replicate the model’s mechanism.Source: §3 · p. 3
  • The evaluation tests three paraphrase levels: one WordNet synonym replacement, synonym replacements for all preceding content words, and an LLM rewrite that preserves the target.The section frames these experiments as testing IRN stability under natural-language paraphrases.Source: §3 · p. 3
  • The worst-layer top-20 feature overlap falls 73% under MINOR paraphrases and 95% under MAJOR paraphrases, with substantial drops observed for both sparse autoencoders and transcoders.Table 1 reports the attack-derived top-20 Jaccard upper bound across layers.Source: Table 1 · p. 4, §3 · p. 4
  • An observed attack shows that overlap can fall at least as far as measured, but cannot rule out a still larger drop under another adversarial input.The underlying model may also behave differently on an adversarial input, so the paper says a robust model is expected to maintain its dominant features.Source: §3 · p. 4

4 VERIFYING THE MECHANISM EQUIVALENCE OF AN LLM AND ITS IRNS

The paper formalizes IRN faithfulness as small computation differences from the underlying model over neighborhoods containing adversarial inputs. Its verifier bounds those differences, and GPT-2 results show substantial gaps across layers, especially deeper ones.

Motivation

  • A high feature-overlap score alone cannot establish faithfulness, since an IRN could emit fixed safe features while the underlying model remains unsafe.The framework checks model–IRN equivalence under adversarial inputs and obtains the feature-overlap measure as a by-product.Source: §4 · p. 4

Faithfulness criterion

  • Faithfulness requires a small difference between the IRN and underlying-model computations over a set containing adversarial inputs.The set can be built from per-token convex hulls of synonym embeddings and their Cartesian product.Source: §4 · p. 4

Verification method

  • The verifier constructs a parallel-path difference network and seeks a certified upper bound on its maximum difference within the local neighborhood.For an SAE, the MLP path is replaced by the identity; the figure describes the target as containment of the difference set in a small box.Source: §4 · p. 5, Figure 3 · p. 5
  • Adversarial attacks estimate a lower bound on the smallest verifiable difference bound, while sequential verification queries find an upper bound.The paper uses binary search over verification queries to narrow the interval around the smallest verifiable bound.Source: §4 · p. 5

Results

  • A verifier finds substantial faithfulness gaps for both GPT-2 IRNs across layers, with later layers becoming less faithful and transition circuits showing larger gaps than SAEs.The authors report that both the verifier's upper bound and attack-derived lower bound rise in later layers.Source: Figure 4 · p. 5, §4 · p. 6

5 IMPROVING THE FAITHFULNESS OF AN IRN

Verification-aware training substantially reduces the certified faithfulness gap, while improving feature sparsity. However, feature preservation remains limited, in part because the underlying model itself changes predictions for many paraphrases.

Training regimes

  • The training comparison includes standard training, PGD adversarial augmentation, verification-aware reachable-set loss, and low-rank updates.The paper motivates these regimes because standard reconstruction-and-sparsity training on clean data does not adequately consider adversarial inputs.Source: §5 · p. 6

Results

  • ≈−90% for SET over STD in the verified upper bound on the difference set; SET also averages 13.9 active features, −81% over STD.The relative error volume is reported as ≈10^-779 for SET over STD, and LoRA also improves faithfulness with low-rank updates.Source: §5 · p. 6, Figure 5 · p. 6
  • Only 2–3 of the clean input's top-20 features are provably retained for adversarial inputs, although J improves across all tested regimes.The authors caution that the feature-overlap result is more faithful to the underlying model after retraining brings the IRNs closer to it.Source: §5 · p. 7, Figure 6 · p. 7
  • The underlying model flips its next-token prediction for 21% of MINOR paraphrases, indicating that its own behavior is fragile to these paraphrases.The authors therefore consider the improved J evaluation consistent with instability in the underlying model, not only the IRN.Source: §5 · p. 7

6 VISION: COMPOSITIONAL VERIFICATION OF THE ENTIRE LLM

The paper envisions verifying whole-model faithfulness compositionally, since current verification does not scale easily to propagated adversarial input sets. The proposed approach checks local blocks and requires each output set to fit the next block's input set, but current sets are too small for end-to-end verification.

Current limitations

  • Verification does not yet scale to the full model, so the proposed construction uses per-layer convex hulls of adversarial samples instead of propagating X.Propagating X through attention and MLP updates can yield overly conservative enclosures, while the whole model may be too large for one verifier query.Source: §6 · p. 7

Compositional approach

  • The vision verifies each LLM block individually and accepts the composition when each block's output set is contained in the next block's input set and each IRN difference bound is sufficiently small.The figure specifies axis-aligned input boxes and notes that surrounding blocks may need adaptations if containment fails.Source: §6 · p. 7, Figure 7 · p. 8
  • For the first block, the input set starts from X; subsequent input sets use convex hulls of propagated samples and must be axis-aligned boxes.The verifier computes each block's output set and checks containment in the next block's input set.Source: §6 · p. 7

Possible remedies

  • When containment fails, possible remedies include more verifier computation, enlarging the next input set, or retraining blocks to tighten bounds.Enlarging one block's input set may affect downstream blocks; tightening an earlier output can also help tighten subsequent blocks.Source: §6 · p. 7

Current state

  • Current H_k sets are still too small for compositional verification of the entire LLM, including being 5× smaller for GPT-2 SAE layer 6; the authors leave closing this gap to future work.They propose combining tighter verification, enlarged input sets, and model or block retraining as possible approaches.Source: §6 · pp. 7–8

7 RELATED WORK

Related work covers circuit discovery and sparse interpretable replacement networks as approaches to understanding model computations. The paper situates its contribution among critiques of explanation faithfulness and formal-guarantee methods.

Circuit-level interpretability

  • Circuit discovery identifies task-related subnetworks, but units within identified circuits can remain polysemantic and difficult to interpret.Examples include attention-head groups for tasks and clusters of neurons active for related tasks.Source: §7 · p. 8

Sparse interpretable replacement networks

  • IRNs replace opaque dense computations with sparse interpretable networks, and prior work applies circuit tracing to these replacements.SAEs reconstruct residual streams with sparse features, while transcoders generalize the replacement-network concept; prior evaluations lacked worst-case adversarial guarantees.Source: §7 · p. 8

Faithfulness critiques

  • Critiques of IRN faithfulness include similar auto-interpretation scores for SAEs trained on random and trained models, and different features learned from the same model and data.The passage also notes adversarial attacks on IRNs and poor scaling of certified adversarial defenses.Source: §7 · p. 9

XAI and formal guarantees

  • Formal guarantees have been developed for explainers and circuit discovery, and this work brings that line of research to large language models.The passage contrasts locally linear or sampling-based explainers with formal-guarantee approaches.Source: §7 · p. 9

8 CONCLUSION

Existing IRNs fail to faithfully reproduce model mechanisms across five open-weight model families, and the paper introduces formal bounds and verification-aware training to address this gap. The bounds remain approximate, and most main-text verification results concern GPT-2.

8 CONCLUSION

  • Existing IRNs fail to faithfully reproduce the model mechanism across five open-weight families: GPT-2, Gemma 2 2B, Gemma 3 1B, Llama 3.2 1B, and R1-Distill-Qwen 1.5B.The paper reports a substantial faithfulness gap across layers, which appears to increase in later layers.Source: §8 · p. 9
  • The paper provides formal bounds on IRN faithfulness and reports that verification-aware training reduces the faithfulness gap by 90%.Training penalizes the difference set to align the model and IRN manifolds.Source: §8 · p. 9
  • The resulting IRNs remain approximations, and a faithful IRN may still omit unsafe features if its feature set is too narrow.A persistently large difference set may indicate that the IRN has too few features.Source: §8 · p. 9
  • Most main-text verification results concern GPT-2, while verification of other IRNs is presented as an engineering task with examples in the appendix.The paper reports that Llama 3.2 1B IRNs can be verified in Appendix C.2.5.Source: §8 · p. 9
  • The authors identify full-model verification, cross-layer transcoders, automatic component alignment, and tighter difference sets without sacrificing model capabilities as future directions.The paper also presents its per-layer guarantees as a foundation for full-model verification.Source: §8 · p. 9

A DETAILS ON TEASER FIGURE

A targeted attack on a meaning-preserving paraphrase removes the biological feature cluster from a Gemma 2 2B interpretation. The appendix also outlines reachability-based neural-network verification using zonotopes.

A DETAILS ON TEASER FIGURE

  • The example targets “culture” at Gemma 2 2B layer 16, searching a hull built from a single meaning-preserving synonym swap before the target token.Projected gradient descent uses 300 iterations and eight random restarts to suppress the four biological features active on the clean token.Source: A DETAILS ON TEASER FIGURE · pp. 14–15
  • At the targeted adversarial point, all four clean-input biological features leave the top eight, and the top-8 Jaccard index is 0.23.The attacked features are replaced by generic, non-biological ones; Table 2 identifies the biological features removed by the attack.Source: A DETAILS ON TEASER FIGURE · p. 15, Table 2 · p. 15

B.1 BACKGROUND ON NEURAL NETWORK VERIFIERS

  • Neural-network verification propagates an input set through the network to compute an outer-approximative output set, then checks that set against a specification.The appendix describes CORA reachability analysis with zonotopes; affine operations and interval bounds can be computed efficiently for these sets.Source: §B.1 · pp. 15–16

B.2 PER-LAYER VERIFICATION OF AN INTERPRETABLE REPLACEMENT NETWORK

The appendix describes a sound, per-layer verifier for bounding IRN faithfulness, a certified lower bound on feature overlap, and evaluation choices and ablations. Verification-aware training generally improves the output bound while retrained IRNs remain sparse.

B.2 PER-LAYER VERIFICATION OF AN INTERPRETABLE REPLACEMENT NETWORK

  • For the transcoder branch, the verifier uses pre-activation bounds and interval arithmetic to collapse a high-dimensional zonotope rather than explicitly constructing it.A smaller certified δ means the IRN is more faithful; Figure 8 illustrates that closer agreement between output surfaces permits a smaller δ.Source: §B.2 · pp. 16–17, Figure 8 · p. 17
  • The per-layer verifier soundly certifies an ℓ∞ bound on the difference between an MLP and its IRN in O(d_model^2 d_IRN) time and O(d_model d_IRN) memory.It exploits a one-step look-ahead for the transcoder branch; the MLP branch is negligible when d_IRN is much larger than d_model and κ_MLP.Source: §B.2 · pp. 17–18

B.3 SOUND LOWER BOUND ON THE JACCARD INDEX

  • The verifier also derives a certified lower bound on top-K feature Jaccard by counting which clean top-K features are guaranteed to survive throughout the input hull.A feature survives when fewer than K other features can possibly reach or exceed its lower-bound pre-activation.Source: §B.3 · p. 18

C.1 EVALUATION DETAILS

  • Evaluation builds a separate paraphrase hull for each target sentence and searches for the smallest verifiable δ, reporting it alongside a PGD-derived lower bound.Retrained IRNs use 50 epochs, with STD, PGD, and SET differing in their training losses; held-out samples use the same verification protocol.Source: §C.1 · pp. 19–20

C.2.1 INPUT RADIUS: DEFAULT HULL AND UNIFORM RADIUS

  • Across uniform input radii, adversarial and verification-aware training generally improve over the baseline, with larger gains at larger ε except at ε = 0.01.Table 6 reports verified output bound δ for GPT-2 SAE layer 6 at the tested uniform radii.Source: §C.2.1 · p. 21, Table 6 · p. 21

C.2.2 SPARSITY OF THE RETRAINED IRNS

  • Retrained IRNs do not generally become denser: SET activates five times fewer features than baseline on clean inputs, and each regime reduces the features that can activate over the hull.SET + LORA is the exception for clean feature count, roughly doubling it while retaining the fewest active features over the hull.Source: §C.2.2 · p. 21

C.2.3 SET-BASED TRAINING: LOSS WEIGHTING

The appendix extends certified faithfulness-gap analysis across set-training choices and several non-GPT-2 IRN families, including activation-specific verification methods. The reported gaps remain substantial across these models, with TopK and JumpReLU enclosures associated with additional conservativeness.

C.2.3 SET-BASED TRAINING: LOSS WEIGHTING

  • For GPT-2 layer 6, sweeping τ from 0.1 to 0.9 leaves the verified-bound median within [47.8, 60.3] and reconstruction loss within [15.9, 29.7].Set-based training interpolates between reconstruction-center loss and reachable-set volume loss; τ = 0.1 is the default.Source: §C.2.3 · p. 21, Table 8 · p. 22

C.2.4 LORA RANK

  • Higher LoRA rank tends to tighten set-based training’s δ bounds, but increases memory requirements and may be infeasible for large IRNs.The ablation sweeps ranks 8, 16, and 32 at τ = 0.1 on GPT-2 layer 6.Source: §C.2.4 · p. 22, Table 9 · p. 22

C.2.5 SCALABILITY: VERIFICATION OF LLAMA’S IRN

  • For Llama’s non-elementwise TopK gate, interval threshold bounds divide features into always-kept, never-kept, and undecided sets to bound their decoded contributions.Exactly K′ undecided features are active for each input; bounding their K′ extreme contributions yields an interval used to compute the verified upper bound δ.Source: §C.2.5 · pp. 22–23
  • Across all 16 Llama 3.2 1B SAE layers, a substantial faithfulness gap is certified, widening in deeper layers; useful layer-1 bounds persist even at MAJOR perturbations.The authors attribute the wider gap between the lower and upper bounds partly to outer approximations required by the TopK enclosure.Source: §C.2.5 · p. 23, Table 10 · p. 23

C.2.6 GEMMA SCOPE

  • Gemma Scope uses elementwise JumpReLU with a trainable threshold θ; larger θ means a larger discontinuity, which may make its enclosure overly conservative.Figure 10a shows θ by layer for Gemma 2 2B, while Figure 10b illustrates a zonotopic enclosure at θ = 2.Source: §C.2.6 · p. 24, Figure 10 · p. 24
  • Across 26 Gemma 2 2B and Gemma 3 1B SAE layers, certified gaps widen with depth, and their bounds are more conservative than for the smooth GPT-2 transcoder.The authors attribute the larger bound difference to enclosing discontinuous JumpReLU gates.Source: §C.2.6 · p. 24, Figure 11 · p. 25

C.2.7 R1-DISTILL-QWEN 1.5B

  • The R1-Distill-Qwen 1.5B SAE is an order of magnitude less faithful than the Llama 3.2 1B SAE at the MINOR level, with gaps far above GPT-2’s.The comparison covers all 28 model layers and uses the same 200 samples as the other models.Source: §C.2.7 · p. 25, Figure 12 · p. 25

C.2.8 FAITHFULNESS TRAINING ACROSS LAYERS

The authors extend faithfulness-training comparisons across GPT-2 layers, where gaps appeared to increase at greater depth. Set-based verification-aware training keeps the gap small across layers, unlike the other adversarial training methods tested.

C.2.8 FAITHFULNESS TRAINING ACROSS LAYERS

  • The experiment extends the earlier comparison across GPT-2 layers because gaps appeared to increase in later layers, a trend also observed across the other models.The same training hyperparameters were used at every layer.Source: §C.2.8 · pp. 25–26
  • The per-layer comparison uses identical training hyperparameters, so the reported differences are assessed under a consistent setting across layers.The authors state that the same training hyperparameters were used at every layer.Source: §C.2.8 · p. 26
  • Across GPT-2 layers, verification-aware training using sets keeps the faithfulness gap small, unlike the other adversarial training methods tested.Figure 13 presents the per-layer comparison.Source: Figure 13 · p. 26, §C.2.8 · p. 26

Related papers

Loading 2609.15533v1…