Paper deep dive
The Misery of Mechanistic Interpretability: A Formal Perspective
Tobias Ladner, Matthias Althoff
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract: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.
Tags
Links
- Source: https://arxiv.org/abs/2609.15533v1
- Canonical: https://arxiv.org/abs/2609.15533v1
Trouble viewing inline? Open PDF directly →
Full Text
96,080 characters extracted from source content.
Expand or collapse full text
The Misery of Mechanistic Interpretability: A Formal Perspective Tobias Ladner (tobias.ladner@tum.de) Affiliation: Technical University of Munich, Germany Matthias Althoff (althoff@tum.de) Affiliation: Technical University of Munich, Germany Abstract 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, 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 on 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 Most interpretations of a large language model carry a quiet asterisk: They are not direct interpretations of the model. When we read that a neuron “fires for the Golden Gate Bridge” (Templeton et al., 2024) or that a circuit “implements a comparison operator” (Dunefsky et al., 2024), these claims are often read off an interpretable replacement network (IRN)—an interpretable network to stand in for a dense computation the model actually performs (Marks et al., 2025; Somvanshi et al., 2026). This is necessary as the dense computations of the underlying model result in polysemantic neurons (Elhage et al., 2022), whereas the IRN exposes a short list of human-understandable features. Crucially, these features are only as trustworthy as that stand-in is faithful, i.e., the computation of the IRN matches the underlying model. However, training the IRN to match the underlying model usually results in an approximate stand-in. While the IRN can be patched for individual inputs (Ameisen et al., 2025), whether an interpretation survives an adversarial input is barely tested or verified—even though adversarial examples have been known to exist for a decade (Goodfellow et al., 2015), including for language models (Dong et al., 2025). Moreover, individual patches defeat the purpose of mechanistic interpretability to a certain degree as it aims to replicate the true mechanism of the underlying model. Fig. 1 shows how such a faulty IRN can deceive a safety auditor: On the clean input sentence, the auditor would read off features surrounding “cultivating a pathogen”—a signal the safety auditor would use to refuse the request. We then perturb the input slightly by paraphrasing the sentence, such that the dominant features now describe “workplace culture”—and the auditor would wave the request through. Crucially, nothing of the model changed; what changed is the exposed interpretation by the IRN. The full example is provided in Appendix A. It is worth noting that there are also interpretations that operate on the actual model. For example, circuit tracing methods aim to identify the active subnetworks for any input (Somvanshi et al., 2026); however, those methods do not scale to frontier language models yet (Gao et al., 2025b). Instead, dense computations are replaced by IRNs and circuit tracing is applied on this modified model (Ameisen et al., 2025)—making the faithfulness of IRNs ever more important. Further details are provided in Sec. 7, and we focus for the remainder of this work on the faithfulness of IRNs. Contributions. To summarize, our main contributions are: 1. We first show that IRNs are highly sensitive to adversarial attacks across various model families and IRN types: GPT-2, Gemma 2 2B, Gemma 3 1B, Llama 3.2 1B, and R1-Distill-Qwen 1.5B (Sec. 3). 2. Subsequently, we establish a formal verification framework for the faithfulness of an IRN (Sec. 4). In particular, we show that with the recent progress in formal methods, formal neural network verification can also be utilized in large language models. 3. Finally, we show that verification-aware training substantially narrows the faithfulness gap of IRNs (Sec. 5). Figure 1: Same meaning, different interpretations. On the clean input (left), the most active features describe a “pathogen” sense of culture, and a feature-based safety auditor reading those features blocks the request. With a minor synonym attack (right), the dominant features instead describe a “workplace” sense, and the same auditor would let the request pass. 2 Background on Mechanistic Interpretability Modern language models (Vaswani et al., 2017; Elhage et al., 2021) are typically composed of a token embedding layer, a stack of κ blocks operating on a residual stream, and a decoding layer to predict the next token. Each block k has two sublayers (Fig. 2): A multi-head attention sublayer that mixes information across tokens, and a multi-layer perceptron (MLP) that applies a nonlinear transformation to each token independently. Both add their output back into the residual stream, so we can write the layer-k update as (Vaswani et al., 2017, Eq. 1 & 2) Hk′=Hk−1+Attnk(Hk−1),Hk=Hk′+MLPk(Hk′),H _k\;=\;H_k-1+Attn_k\! (H_k-1 ), H_k\;=\;H _k+MLP_k(H _k), (1) where Hk∈ℝdmodel×τH_k ^d_ model×τ collects the residual-stream vectors of the τ input tokens as columns, and Hk′∈ℝdmodel×τH _k ^d_ model×τ is the post-attention intermediate. We are aware that this is a simplified description of the architecture of frontier models; however, insofar as these models are not proprietary, most model families can be described under this framework (Radford et al., 2019; Gemma Team, 2024; Gemma Team, 2025; Grattafiori et al., 2024; Qwen Team, 2025), and this high-level description is sufficient for our work. An attention layer can usually be interpreted directly as it computes an interpretable relation between tokens (Vaswani et al., 2017, Eq. 1). However, the MLP is hard to interpret: Its neurons are densely entangled and polysemantic (Elhage et al., 2022), i.e., each fires for unrelated inputs. The dominant remedy is to fit an interpretable replacement network (IRN) (Somvanshi et al., 2026), whose activations are sparse and individually meaningful, and to read interpretations off the IRN features as a proxy for the model. We consider two dominant variants in this work, sparse autoencoders and transcoders (Fig. 2), which are also available for many open-weight models. Sparse autoencoder (SAE). A sparsely activated autoencoder (Huben et al., 2024) reconstructs its input at layer k: SAEk(Hk)=Wkdecϕ(WkencHk+bkenc)+bkdec≈Hk,SAE_k(H_k)\;=\;W_k^dec\,φ\! (W_k^enc\,H_k+b_k^enc )+b_k^dec\;≈\;H_k, (2) where the parameters Wkenc∈ℝdIRN×dmodelW_k^enc ^d_IRN× d_ model, Wkdec∈ℝdmodel×dIRNW_k^dec ^d_ model× d_IRN, bkenc∈ℝdIRNb_k^enc ^d_IRN, bkdec∈ℝdmodelb_k^dec ^d_ model are learned per layer. Transcoder (TC). A transcoder (Dunefsky et al., 2024) at layer k reconstructs the output of the multi-layer perceptron from the same input: TCk(Hk′)=Wkdecϕ(WkencHk′+bkenc)+bkdec≈MLPk(Hk′),TC_k(H _k)\;=\;W_k^dec\,φ\! (W_k^enc\,H _k+b_k^enc )+b_k^dec\;≈\;MLP_k(H _k), (3) again with per-layer parameters Wkenc,Wkdec,bkenc,bkdecW_k^enc,W_k^dec,b_k^enc,b_k^dec. Transcoders can also be constructed across different computation blocks (Ameisen et al., 2025). The activation function ϕφ varies by model family: For example, ReLUReLU is used for the GPT-2’s sparse autoencoder and transcoder (Dunefsky et al., 2024), JumpReLUJumpReLU for the Gemma Scope (Lieberum et al., 2024), and TopKTopK for the Llama Scope (He et al., 2024). A mechanistic interpretation at layer k for an input sentence is then read off the active IRN features, e.g., the indices i with ϕ(⋅)(i)>0φ(·)_(i)>0, where a sparsity penalty during training ensures that only a small subset of the hidden features (dIRN≫dmodeld_IRN d_ model) fires for any given input. Subsequently, each feature automatically obtains a human-readable label by summarizing the inputs that activate it (Paulo et al., 2025). This feature-label catalog is also often available along with the IRN (Lin, 2023). Figure 2: Interpretable replacement networks. Large language models typically have a residual stream, which is modified through attention layers and MLPs (shown in purple). As these compute complex updates, interpretable replacement networks (shown in blue) are added to understand the internal behavior of a large language model. Examples are sparse autoencoders (reconstructing the residual stream), and transcoders (reconstructing the output of the MLP). 3 Where Mechanistic Interpretability Breaks A foundational observation in deep learning is that imperceptible input perturbations can flip the prediction of a model entirely—the so-called adversarial examples (Goodfellow et al., 2015). For mechanistic interpretability, we want the active features of the IRN to remain active when a sentence is rephrased in semantically equivalent ways. Otherwise, the human-readable labels attached to those features do not reflect the actual computation, and the IRN fails to replicate the mechanism of the model. This premise follows existing literature on the robustness of interpretations in regular neural networks (Wu et al., 2023; Bassan and Katz, 2023; La Malfa et al., 2021). While most evaluations of IRNs report the reconstruction loss on clean data, adversarial settings are barely evaluated despite early signs of the instability of IRNs: For example, it was shown that sparse autoencoders trained as an IRN are fragile to small adversarial perturbations (Li et al., 2026). In this section, we confirm these results with additional experiments across various open-weight model families and IRN types, evaluated under three levels of natural-language paraphrase: • minor: A single content word is replaced with a WordNet synonym (Miller, 1995). • medium: All content words before the target are replaced with WordNet synonyms. • major: An LLM (Gemma 2 2B-it) rephrases the sentence while preserving the target. Results. Tab. 1 reports the top-2020 Jaccard index11 1 For two discrete sets A and ℬB, the Jaccard index is given by J=|∩ℬ||∪ℬ|J= |A ||A |. between the active feature set of an IRN at the clean input and at an adversarial input. The Jaccard index drops substantially as the perturbation grows: Already at the minor level, the perturbations reduce the worst-layer overlap J¯min J_ (−73%-73\%), and at the major level, the reduction is even larger (−95%-95\%); thus, almost all dominant features change and along with them any interpretation for a safety auditor. We observe this drop for both sparse autoencoders and transcoders. Evaluation details are given in Sec. C.1. Table 1: Attack-derived top-2020 Jaccard upper bound J¯ J of the active feature set under paraphrase perturbations across all layers. minor medium major Model IRN J¯min(↑) J_ \,( ) J¯mean(↑) J_mean\,( ) J¯min(↑) J_ \,( ) J¯mean(↑) J_mean\,( ) J¯min(↑) J_ \,( ) J¯mean(↑) J_mean\,( ) GPT-2 SAE 0.270.27 0.370.37 0.060.06 0.180.18 0.050.05 0.130.13 GPT-2 TC 0.700.70 0.790.79 0.450.45 0.620.62 0.380.38 0.540.54 Gemma 2 2B SAE 0.620.62 0.780.78 0.350.35 0.590.59 0.330.33 0.540.54 Gemma 2 2B TC 0.460.46 0.570.57 0.200.20 0.330.33 0.200.20 0.310.31 Gemma 3 1B SAE 0.550.55 0.690.69 0.300.30 0.490.49 0.300.30 0.440.44 Gemma 3 1B TC 0.470.47 0.670.67 0.180.18 0.420.42 0.200.20 0.380.38 Llama 3.2 1B SAE 0.540.54 0.660.66 0.260.26 0.450.45 0.330.33 0.420.42 Llama 3.2 1B TC 0.560.56 0.640.64 0.250.25 0.400.40 0.210.21 0.350.35 Qwen 1.5B SAE 0.370.37 0.490.49 0.180.18 0.290.29 0.120.12 0.200.20 Thus, the active features of an IRN can change substantially for adversarial inputs. However, please note that the underlying model can indeed also behave differently for an adversarial input, and we would only expect that a robust model maintains its dominant features under adversarial inputs. Moreover, an adversarial attack only witnesses a single bad input: It shows that the Jaccard index can drop at least this far, but cannot rule out an adversarial input where it drops further. The numbers in Tab. 1 are therefore an upper bound J¯ J on the true Jaccard index J∗J^* under adversarial attacks. To obtain guarantees, a faithful IRN of a robust model needs to have a high lower bound J¯ J. 4 Verifying the Mechanism Equivalence of an LLM and its IRNs We have established that an IRN of a robust model has to have a high lower bound on the Jaccard index J¯ J. Crucially, the IRN also has to be faithful for a sensible J¯ J evaluation, i.e., the computation of the IRN should match the underlying model. As an extreme example, imagine an unfaithful IRN that always has the same (safe) features active independently of the model input, e.g., through large biases on these features. Then, J¯ J is always 11 even though the underlying model might be unsafe, and thus it is an insufficient measure as the IRN is not faithful. To guarantee the faithfulness, we develop a framework to formally verify the equivalence of the model and the IRN under adversarial inputs in this section, and obtain J¯ J as a by-product of this equivalence check. We construct a set ⊂ℝdmodel×τX ^d_ model×τ containing all adversarial embeddings of an input sentence. For example, X can contain all semantically equivalent sentences to that input sentence through synonym replacements of each word. As explicitly enumerating all synonym combinations quickly results in a combinatorial explosion, we construct, per token, a convex hull in the embedding space over all synonyms of that token, and then compute the Cartesian product of these convex hulls to obtain X. Then, with ℋkH_k being the propagated set at each layer k, we can state our faithfulness criterion: Definition 1. For a δ∈ℝ+δ _+, we say that an IRN at layer k is δ-equivalent to the underlying model on ℋkH_k if ∀H~k∈ℋk: ∀\, H_k _k ‖H~k−SAEk(H~k)‖∞ \| H_k-SAE_k( H_k) \|_∞ ≤δ, ≤δ, ‖MLPk(H~k)−TCk(H~k)‖∞ \|MLP_k( H_k)-TC_k( H_k) \|_∞ ≤δ, ≤δ, and we say that the IRN is faithful if δ is sufficiently small. Please note that ℋkH_k is a continuous set, e.g., imagine a hypercube with radius ϵ∈ℝ+ε _+ containing all embeddings of the adversarial inputs. To test for δ-equivalence (Def. 1), we can adapt existing neural network verifiers (Kaulen et al., 2025) for our use case. In particular, we construct for each layer k the difference network MLPk(Hk)−IRNk(Hk)MLP_k(H_k)-IRN_k(H_k) as a composite of two parallel paths with difference-based aggregation (Fig. 3), and the verifier tries to prove that the difference is bounded by a given δ. We defer a more detailed description of how these verifiers work to Sec. B.1 and provide optimizations applied in our settings in Sec. B.2, which also gives us J¯ J (Sec. B.3). Figure 3: Mechanism verification as a composite network. (a) The local neighborhood around an input sentence is captured by ℋkH_k so that adversarial inputs are also contained. (b) We can deploy formal verification to bound the maximal difference between the MLPkMLP_k and the TCkTC_k within the local neighborhood. (c) The faithfulness property in Def. 1 holds if the computed difference set is contained in a small box [−δ,δ]dmodel[-δ,δ]^d_ model. The SAE case is analogous, with MLPkMLP_k replaced by the identity (Eq. 2). With such a verifier, we aim to find the smallest verifiable bound δ∗δ^*. As with the Jaccard index J∗J^*, it is usually also not feasible to compute δ∗δ^*, and we need to find bounds: δ¯≤δ∗≤δ¯ δ≤δ^*≤ δ. We can find a lower bound δ¯ δ using adversarial attacks trying to maximize the difference, and the upper bound δ¯ δ needs to be verified. Please note that this is converse to J¯,J¯ J, J, where the lower bound—describing the number of unflippable active features—needs to be verified. We find δ¯ δ by conducting a binary search with sequential verification queries (details in Sec. C.1, Alg. 2). To display the faithfulness gap in figures, we draw the gap between the median δ¯ δ and δ¯ δ over the test dataset as a filled box—thus, the median δ∗δ^* has to be within the filled box—and add whiskers for the 25%25\%- and 75%75\%-quantile of δ¯ δ and δ¯ δ, respectively. AIHow to close the faithfulness gap? Figure 4: Per-layer faithfulness gap on GPT-2. For both IRNs and across all layers, we can verify a substantial faithfulness gap between the computation of the IRNs and the underlying model. Results. Fig. 4 reports the faithfulness gap for both IRNs of GPT-2 (other models in Sec. C.2), where we have verified a substantial faithfulness gap across all layers. For example, we have verified that for layer 11, the SAE is δ-equivalent to the underlying model for some δ<1δ<1. Thus, the reconstructed residual stream under the ℓ∞ _∞ norm has, on average, a smaller difference than 11 given adversarial inputs. To put this number into context, we also observed such differences on the residual stream of the underlying model given adversarial inputs. Unfortunately, our results demonstrate that later layers become less faithful, arguably to a degree that does not allow for meaningful interpretations anymore. We want to stress that this is not an artifact of the (incomplete) verifier, as not only the upper bound found by the verifier is rising, but also the lower bound found by adversarial attacks. We note that the faithfulness gap is generally larger for TCs, which is to be expected as a TC has to replicate the complex computations of the MLP there, and SAEs “only” have to reconstruct their input. Evaluation details are again given in Sec. C.1. 5 Improving the Faithfulness of an IRN These results naturally lead to the question of whether more faithful IRNs can be obtained. Standard training of IRNs usually focuses on the combination of reconstruction and sparsity for interpretability on clean data (Marks et al., 2025; Dunefsky et al., 2024); however, it does not adequately consider adversarial inputs, such that their susceptibility likely degrades the verification results in the previous section. Conceptually, we want to train the IRN in a way so that in Fig. 3c, any sentence for which the error set is like the top plot becomes more like the bottom plot—thereby aligning its manifold with the manifold of the underlying model. We investigate different training regimes in this section to improve the faithfulness of an IRN under adversarial inputs: • Std: The given IRN obtained using standard training is used as a baseline. • PGD: Adversarial training using PGD-found H~k H_k as augmentation (Madry et al., 2018). • Set: Verification-aware training with reachable-set loss (Koller et al., 2025). • LoRA: Low-rank updates typically used for fine-tuning LLMs (Hu et al., 2022). AIVerification-aware training helps to close the gap! Figure 5: Faithfulness gap per training regime. Verification-aware training results in a substantially smaller faithfulness gap between GPT-2 and its SAE at layer 66. Results. We fine-tune OpenAI’s SAE of GPT-2 using these training regimes (more experiments again in Sec. C.2), and show the verification results in Fig. 5 using the same setup as in Sec. 4. Our results show substantially smaller verified upper bounds δ¯ δ on the difference set (≈−90%≈-90\% for Set over Std). Please note that the difference sets live in a high-dimensional space (dmodel=768d_ model=768), and thus the relative error volume is extremely small (≈10−779≈ 10^-779 of Set over Std). Crucially, the retrained IRNs are more sparse and thus interpretable (Set has on average 13.913.9 active features, −81%-81\% over Std). We can also improve the faithfulness of the IRN with efficient low-rank updates (LoRA) despite the verifier requiring robustness in the full space. We anticipate this result to also be of broader interest within the verification community as it might transfer to non-NLP-based models as well. While the retrained IRNs are both easier to verify and harder to attack, we acknowledge that the preservation of active features is still not substantial over the baseline as shown in Fig. 6. From the top-2020 features of the clean input, only 22–33 are provably retained for adversarial inputs, and J¯ J is improved across all tested training regimes. However, as our trained IRNs are much closer to the underlying model (Fig. 5), this Jaccard evaluation is more faithful than for the baseline IRN. Thus, it is reasonable to attribute this result to the underlying model not being very robust. Indeed, the underlying model already flips its next-token prediction for 21%21\% of the minor paraphrases, confirming that the underlying model is itself fragile to these paraphrases. AI… but what if the model is not robust? Figure 6: Top-2020 feature-overlap bounds on the GPT-2 layer-66 SAE. For each training regime the box spans the certified lower bound J¯ J to the attack-derived upper bound J¯ J over the test samples (J¯≤J∗≤J¯ J≤ J^*≤ J); whiskers reach the q25q_25 of J¯ J and the q75q_75 of J¯ J. Further right is more faithful. 6 Vision: Compositional Verification of the Entire LLM In this section, we state our vision for verifying the robustness of a model and the faithfulness of its IRNs across all layers. In particular, Def. 1 assumes a set ℋkH_k capturing all propagated adversarial inputs H~k H_k at each layer k. However, as these verifiers do not scale yet to the full model, we construct ℋkH_k at each layer individually via the convex hull over H~k H_k rather than the propagated input set X. To formally verify the faithfulness, X needs to be propagated to layer k, enclosing all updates through attention layers and MLPs along the way (Fig. 2). While it is possible to enclose the updates of attention layers (Bonaert et al., 2021) and MLPs (Sec. B.1), the resulting enclosures often become too conservative to meaningfully reason about the faithfulness. Moreover, the LLM might be too large for the verifier to reason about the entire model in one query. Thus, we envision a compositional approach visualized in Fig. 7, where each block of the LLM is verified individually analogous to Sec. 4, i.e., each block is verified by determining an input-output set relation, and the faithfulness of the entire model is verified if for any two subsequent blocks, the output set of the former block is contained in the input set of the latter block, and the verified difference set for the IRN of each block, characterized by δ¯ δ, is sufficiently small. The input set of the first block is initialized with X, and the input set of subsequent blocks is initialized via the convex hull of the propagated samples H~k H_k. We can then compute the respective output set of each block and check for containment of the input set of the subsequent block. To realize this efficiently, we require the input sets of each block to be axis-aligned boxes. Figure 7: Compositional faithfulness verification of the entire LLM. Each block (Attn + MLP) is verified locally (Sec. 4), bounding the difference of its IRN by δ¯≤δ∗≤δ¯ δ≤δ^*≤ δ. The whole model is then verified compositionally if, for every pair of subsequent blocks, the propagated output set of the former is contained in the axis-aligned input box ℋH of the latter; otherwise, adaptations are required to the surrounding blocks. For all blocks where the containment cannot yet be shown, there are several approaches to resolve this issue: (i) Neural network verifiers can often obtain tighter results given more computation time, so that a smaller output set might be contained. (i) The input set of the subsequent block is enlarged; please note that this might also affect downstream blocks. Both of these points assume that the model and the IRN are fixed; however, a more realistic scenario is that the developer of the model (i) could also re-train (certain blocks of) the model to make it more robust (as we did for the IRN in Sec. 5) and thus obtain tighter output bounds. (iv) Conversely, if an output set of one block is tightened by such an action, the subsequent block can also be tightened with positive impact downstream. Current state. While verification-aware training shows significant improvements on the bounds of the error set (Fig. 5), we acknowledge that our used sets ℋkH_k are still a bit too small to verify the faithfulness of the entire LLM compositionally (e.g., 5×5× smaller for layer 66 of GPT-2 SAE: Tab. 5). However, we believe that through a combination of (i)–(iv), this gap can be further closed such that our compositional framework becomes feasible. As each point requires a more detailed analysis to develop sophisticated algorithms, we leave this for future work. 7 Related Work Mechanistic interpretability has gained great interest in recent years to understand the inner workings of large language models (Bereska and Gavves, 2024; Zhao et al., 2024; Somvanshi et al., 2026), particularly as the computations are dense and hard to interpret (Elhage et al., 2022; Park et al., 2024). This lack of transparency has inspired two research branches: circuit discovery, which isolates the sub-computation responsible for a behavior, and interpretable replacement networks (IRNs), which substitute a dense computation with a sparse, human-readable stand-in. Circuit-level interpretability. Early work traces circuits over the functional modules of a language model, inspired by circuit discovery in vision models (Olah et al., 2020). For language models, a circuit groups a subset of attention heads active for a certain task (Wang et al., 2023), which can reveal for example a base-10 addition circuit (Feucht et al., 2026), or clusters of neurons that are active for the same tasks (Geiger et al., 2025). Generally, the goal is to discover these circuits automatically (Conmy et al., 2023); however, the individual units within each identified circuit remain polysemantic (Elhage et al., 2022) and thus hard to interpret. Sparse interpretable replacement networks. To disentangle polysemantic neurons, these neurons are replaced with interpretable networks (Huben et al., 2024; Dunefsky et al., 2024). In particular, it was shown that each MLP module computes specific concept updates on the residual stream (Geva et al., 2021; Meng et al., 2022); however, the computations made by the MLP are opaque, making them a natural target for an interpretable replacement. In contrast, the attention modules are usually easier to interpret as one can directly read out to which tokens each token attends (Vaswani et al., 2017). SAEs decompose the residual stream into sparsely activated features reconstructing the residual stream (Huben et al., 2024). These feature neurons are usually arranged in a single wide hidden layer—as it is well known that such architectures are universal approximators if sufficiently wide (Hornik et al., 1989). In practice, various architectures such as gated SAEs (Rajamanoharan et al., 2024a) and dedicated activation functions (Gao et al., 2025a) trade off reconstruction and sparsity. End-to-end dictionary learning optimizes features for functional importance rather than reconstruction (Braun et al., 2024). TCs generalize this concept (Dunefsky et al., 2024), including across layer blocks (Ameisen et al., 2025). There is also a growing research stream in combining both research directions, such that circuits in a model are discovered on the sparse interpretable network replacing the dense computation, both on SAEs (Marks et al., 2025) and on TCs (Ameisen et al., 2025). Across all of these prior works, the IRNs are only evaluated empirically, and never with a worst-case guarantee in adversarial settings. Identifying features and critiquing faithfulness. After an IRN is trained, the sparsely activated features need to be labeled to be understandable for humans. The dominant method here is automated interpretability, where another LLM generates and scores a natural language description of each feature (Bills et al., 2023; Paulo et al., 2025). These descriptions are sometimes also made publicly available in the Neuronpedia ecosystem (Lin, 2023). A labeled feature can also be used to localize the respective computation in the underlying model (Gurnee et al., 2023). However, a growing critique questions the faithfulness of interpretable replacement networks: For example, SAEs trained on randomly initialized models produce auto-interpretation scores similar to trained models (Heap et al., 2026), and SAEs trained on the same model and data learn different features (Paulo and Belrose, 2026). Adversarial attacks can show the fragility of the IRN (Li et al., 2026), and certified defenses against adversarial attacks scale poorly (Kumar et al., 2024). XAI and formal guarantees. Similar critiques have become louder in the broader field of explainable artificial intelligence (XAI): Prominent post-hoc explainers such as LIME (Ribeiro et al., 2016) and SHAP (Lundberg and Lee, 2017) assume linear behavior in the local neighborhood around an input, and sampling-based explainers like Anchors (Ribeiro et al., 2018) lack provable guarantees on their explanations (Wu et al., 2023; Bassan and Katz, 2023; La Malfa et al., 2021). With the development of formal neural network verifiers (Kaulen et al., 2025), explanations with formal guarantees were developed for various threat models (Bassan et al., 2025; Marques-Silva and Ignatiev, 2022). Formal guarantees have also been explored in the context of mechanistic interpretability such as provable circuit discovery on vision models (Hadad et al., 2026). Our work brings this line of research to large language models. 8 Conclusion Mechanistic interpretability tries to make sense of a model’s behavior with the help of interpretable replacement networks. However, these IRNs only approximate the behavior of the model, and this approximation has to be closely matching to obtain faithful interpretations—including in adversarial settings. We show that existing IRNs do not satisfy this fundamental property across five open-weight families (GPT-2, Gemma 2 2B, Gemma 3 1B, Llama 3.2 1B, and R1-Distill-Qwen 1.5B). Our work provides the first formal bounds for the faithfulness gap of IRNs, showing that the recent progress in the field of formal neural network verification can be utilized to verify the components of large language models. We show that this faithfulness gap is substantial across all layers as the IRN does not accurately replicate the mechanism of the model. This gap seems to increase for later layers, likely as the model makes more complex connections there, and current IRNs are not capturing these computations accurately. Naturally, this raises the question of how this faithfulness gap can be closed, where we show that verification-aware training substantially reduces the faithfulness gap (−90%-90\%). This is realized by penalizing the difference set such that the manifolds of both the model and the IRN become aligned. Finally, we generalize this framework to verify the faithfulness and robustness across the entire model. Several caveats remain. Our obtained IRNs—although arguably more faithful—are still approximations and we view this work less as a final answer than as an impulse toward formally verified IRNs. Moreover, even a faithful IRN does not need to be a complete IRN: Too narrow a set of features may simply never represent a (possibly unsafe) feature, leaving it unobserved. Encouragingly, a difference set that stays large despite training is itself a signal that the IRN has too few features, pointing toward dynamic feature expansion backed by universal-approximation guarantees (Hornik et al., 1989). Finally, the main body of this work mainly covers verification results on GPT-2; however, we see the verification of other IRNs primarily as an engineering task, e.g., even the high-dimensional Llama 3.2 1B IRNs can be verified (shown in Sec. C.2.5 along with the remaining model families). Nevertheless, designing large language models and their IRNs with verification in mind would be a valuable research direction. Looking ahead, the per-layer guarantees lay the foundation for the verification of the full model (Sec. 6) and extensions such as cross-layer transcoders. Open research directions include an automatic alignment of the individual components, and obtaining sufficient tightness in the difference set without sacrificing model capabilities. We are excited by the possibilities our approach opens towards a future with trustworthy models and formally verified interpretations. Acknowledgements This work was financially supported by the project AL 1185/33-1 funded by the German Research Foundation (Deutsche Forschungsgemeinschaft, DFG). AI Use Statement In this work, we used generative AI tools to implement our idea for this work, run experiments, assist with literature research, as well as refine the text of this paper. This also includes the generation of all TikZ figures under our guidance and formalizing the required proofs in Lean. We have manually double-checked all AI-assisted work to ensure correctness, and added additional harnesses such as the Lean formalization of our proofs being machine-checked, all AI-assisted code being covered by unit tests, the reported experiments being reproducible, and every claim and citation in the text being checked against its source. Ethics Statement The existence of adversarial examples is well known, including for language inputs with semantics-preserving input perturbations. Our work makes the fragility of interpretable replacement networks explicit, which could in principle guide an adversary who wants an interpretation to be misleading; we consider the disclosure to be clearly beneficial, since the same insight is what allows practitioners to certify when an interpretation may be trusted. Reproducibility Statement All experiments use publicly available open-weight models, interpretability artifacts, and text corpora with their exact sources in Sec. C.1, together with the hardware, software versions, and hyperparameters of every experiment. The accompanying code and Lean formalizations are released as part of the supplementary material. References Althoff et al. (2025) M. Althoff, N. Kochdumper, T. Ladner, M. Perschl, and M. Wetzlinger CORA manual. Technical University of Munich. External Links: Link Cited by: §B.1, §C.1. Althoff (2015) M. Althoff An introduction to CORA 2015. In Proc. of the 1st and 2nd Workshop on Applied Verification for Continuous and Hybrid Systems, Cited by: §B.1, §C.1. Ameisen et al. (2025) E. Ameisen, J. Lindsey, A. Pearce, W. Gurnee, N. L. Turner, B. Chen, C. Citro, D. Abrahams, S. Carter, B. Hosmer, J. Marcus, M. Sklar, A. Templeton, T. Bricken, C. McDougall, H. Cunningham, T. Henighan, A. Jermyn, A. Jones, A. Persic, Z. Qi, T. B. Thompson, S. Zimmerman, K. Rivoire, T. Conerly, C. Olah, and J. Batson Circuit tracing: revealing computational graphs in language models. Note: Transformer Circuits Thread External Links: Link Cited by: §1, §1, §2, §7. Bassan et al. (2025) S. Bassan, Y. Y. Elboher, T. Ladner, M. Althoff, and G. Katz Explaining, fast and slow: Abstraction and refinement of provable explanations. In International Conference on Machine Learning (ICML), Cited by: §7. Bassan and Katz (2023) S. Bassan and G. Katz Towards formal XAI: Formally approximate minimal explanations of neural networks. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Cited by: §3, §7. Bereska and Gavves (2024) L. Bereska and E. Gavves Mechanistic interpretability for AI safety–a review. Transactions of Machine Learning Research (TMLR). Cited by: §7. Bills et al. (2023) S. Bills, N. Cammarata, D. Mossing, H. Tillman, L. Gao, G. Goh, I. Sutskever, J. Leike, J. Wu, and W. Saunders Language models can explain neurons in language models. Note: https://openaipublic.blob.core.windows.net/neuron-explainer/paper/index.html Cited by: §7. Bonaert et al. (2021) G. Bonaert, D. I. Dimitrov, M. Baader, and M. Vechev Fast and precise certification of transformers. In ACM SIGPLAN International Conference on Programming Language Design and Implementation, Cited by: §6. Braun et al. (2024) D. Braun, J. Taylor, N. Goldowsky-Dill, and L. Sharkey Identifying functionally important features with end-to-end sparse dictionary learning. In Advances in Neural Information Processing Systems (NeurIPS), Cited by: §7. Conmy et al. (2023) A. Conmy, A. Mavor-Parker, A. Lynch, S. Heimersheim, and A. Garriga-Alonso Towards automated circuit discovery for mechanistic interpretability. In Advances in Neural Information Processing Systems (NeurIPS), Cited by: §7. Dong et al. (2025) Y. Dong, R. Mu, Y. Zhang, S. Sun, T. Zhang, C. Wu, G. Jin, Y. Qi, J. Hu, J. Meng, et al. Safeguarding large language models: A survey. Artificial Intelligence Review. Cited by: §1. Dunefsky et al. (2024) J. Dunefsky, P. Chlenski, and N. Nanda Transcoders find interpretable LLM feature circuits. In Advances in Neural Information Processing Systems (NeurIPS), Cited by: §1, §2, §2, §5, §7. Elhage et al. (2022) N. Elhage, T. Hume, C. Olsson, N. Schiefer, T. Henighan, S. Kravec, Z. Hatfield-Dodds, R. Lasenby, D. Drain, C. Chen, R. Grosse, S. McCandlish, J. Kaplan, D. Amodei, M. Wattenberg, and C. Olah Toy models of superposition. Note: Transformer Circuits Thread. External Links: Link Cited by: §1, §2, §7, §7. Elhage et al. (2021) N. Elhage, N. Nanda, C. Olsson, T. Henighan, N. Joseph, B. Mann, A. Askell, Y. Bai, A. Chen, T. Conerly, N. DasSarma, D. Drain, D. Ganguli, Z. Hatfield-Dodds, D. Hernandez, A. Jones, J. Kernion, L. Lovitt, K. Ndousse, D. Amodei, T. Brown, J. Clark, J. Kaplan, S. McCandlish, and C. Olah A mathematical framework for transformer circuits. Note: Transformer Circuits Thread. External Links: Link Cited by: §2. Feucht et al. (2026) S. Feucht, T. Haklay, U. Bhalla, D. Wurgaft, C. Rager, R. Sarfati, J. Merullo, T. McGrath, O. Lewis, E. S. Lubana, et al. Arithmetic in the wild: Llama uses base-10 addition to reason about cyclic concepts. arXiv preprint arXiv:2605.01148. Cited by: §7. Gao et al. (2025a) L. Gao, T. Dupre la Tour, H. Tillman, G. Goh, R. Troll, A. Radford, I. Sutskever, J. Leike, and J. Wu Scaling and evaluating sparse autoencoders. In International Conference on Learning Representations (ICLR), Cited by: §7. Gao et al. (2025b) L. Gao, A. Rajaram, J. Coxon, S. V. Govande, B. Baker, and D. Mossing Weight-sparse transformers have interpretable circuits. arXiv preprint arXiv:2511.13653. Cited by: §1. Geiger et al. (2025) A. Geiger, D. Ibeling, A. Zur, M. Chaudhary, S. Chauhan, J. Huang, A. Arora, Z. Wu, N. Goodman, C. Potts, et al. Causal abstraction: a theoretical foundation for mechanistic interpretability. Journal of Machine Learning Research (JMLR). Cited by: §7. Gemma Team (2024) Gemma Team Gemma 2: improving open language models at a practical size. arXiv preprint arXiv:2408.00118. Cited by: Table 3, §2. Gemma Team (2025) Gemma Team Gemma 3 technical report. arXiv preprint arXiv:2503.19786. Cited by: Table 3, §2. Geva et al. (2021) M. Geva, R. Schuster, J. Berant, and O. Levy Transformer feed-forward layers are key-value memories. In Conference on Empirical Methods in Natural Language Processing, Cited by: §7. Girard (2005) A. Girard Reachability of uncertain linear systems using zonotopes. In International Conference on Hybrid Systems: Computation and Control (HSCC), Cited by: §B.1. Goodfellow et al. (2015) I. J. Goodfellow, J. Shlens, and C. Szegedy Explaining and harnessing adversarial examples. In International Conference on Learning Representations (ICLR), Cited by: §1, §3. Grattafiori et al. (2024) A. Grattafiori, A. Dubey, A. Jauhri, A. Pandey, A. Kadian, A. Al-Dahle, A. Letman, A. Mathur, A. Schelten, A. Vaughan, et al. The llama 3 herd of models. arXiv preprint arXiv:2407.21783. Cited by: Table 3, §2. Guo et al. (2025) D. Guo, D. Yang, H. Zhang, J. Song, P. Wang, Q. Zhu, R. Xu, R. Zhang, S. Ma, X. Bi, et al. DeepSeek-R1: Incentivizing reasoning capability in LLMs via reinforcement learning. arXiv preprint arXiv:2501.12948. Cited by: §C.2.7, Table 3. Gurnee et al. (2023) W. Gurnee, N. Nanda, M. Pauly, K. Harvey, D. Troitskii, and D. Bertsimas Finding neurons in a haystack: Case studies with sparse probing. Transactions on Machine Learning Research (TMLR). Cited by: §7. Hadad et al. (2026) I. Hadad, G. Katz, and S. Bassan Formal mechanistic interpretability: Automated circuit discovery with provable guarantees. In International Conference on Learning Representations (ICLR), Cited by: §7. He et al. (2024) Z. He, W. Shu, X. Ge, L. Chen, J. Wang, Y. Zhou, F. Liu, Q. Guo, X. Huang, Z. Wu, et al. Llama Scope: Extracting millions of features from Llama-3.1-8b with sparse autoencoders. arXiv preprint arXiv:2410.20526. Cited by: §2. Heap et al. (2026) T. Heap, T. Lawson, L. Farnik, and L. Aitchison Automated interpretability metrics do not distinguish trained and random transformers. In International Conference on Learning Representations (ICLR), Cited by: §7. Hornik et al. (1989) K. Hornik, M. Stinchcombe, and H. White Multilayer feedforward networks are universal approximators. Neural Networks. Cited by: §7, §8. Hu et al. (2022) E. J. Hu, yelong shen, P. Wallis, Z. Allen-Zhu, Y. Li, S. Wang, L. Wang, and W. Chen LoRA: low-rank adaptation of large language models. In International Conference on Learning Representations (ICLR), Cited by: §C.1, 4th item. Huben et al. (2024) R. Huben, H. Cunningham, L. R. Smith, A. Ewart, and L. Sharkey Sparse autoencoders find highly interpretable features in language models. In International Conference on Learning Representations (ICLR), Cited by: §2, §7. Jaulin et al. (2001) L. Jaulin, M. Kieffer, O. Didrit, and É. Walter Interval analysis. Cited by: §B.2, §B.3. Katz et al. (2017) G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification (CAV), Cited by: §B.1. Kaulen et al. (2025) K. Kaulen, T. Ladner, S. Bak, C. Brix, H. Duong, T. Flinkow, T. T. Johnson, L. Koller, E. Manino, T. H. Nguyen, and H. Wu The 6th international verification of neural networks competition (VNN-COMP 2025): Summary and results. arXiv preprint arXiv:2512.19007. Cited by: §B.1, §4, §7. Koller et al. (2025) L. Koller, T. Ladner, and M. Althoff Set-based training for neural network verification. Transactions on Machine Learning Research (TMLR). Cited by: §C.1, §C.2.3, 3rd item. Koller et al. (2026) L. Koller, T. Ladner, and M. Althoff Out of the shadows: Exploring a latent space for neural network verification. In International Conference on Learning Representations (ICLR), Cited by: §B.1, §B.1, §C.1. Kumar et al. (2024) A. Kumar, C. Agarwal, S. Srinivas, A. J. Li, S. Feizi, and H. Lakkaraju Certifying LLM safety against adversarial prompting. In First Conference on Language Modeling, Cited by: §7. La Malfa et al. (2021) E. La Malfa, A. Zbrzezny, R. Michelmore, N. Paoletti, and M. Kwiatkowska On guaranteed optimal robust explanations for NLP models. In International Joint Conference on Artificial Intelligence, Cited by: §3, §7. Ladner and Althoff (2025) T. Ladner and M. Althoff Fully automatic neural network reduction for formal verification. Transactions on Machine Learning Research (TMLR). Cited by: §B.2. Li et al. (2026) A. J. Li, S. Srinivas, U. Bhalla, and H. Lakkaraju Evaluating adversarial robustness of concept representations in sparse autoencoders. In Conference of the European Chapter of the Association for Computational Linguistics, Cited by: §3, §7. Lieberum et al. (2024) T. Lieberum, S. Rajamanoharan, A. Conmy, L. Smith, N. Sonnerat, V. Varma, J. Kramár, A. Dragan, R. Shah, and N. Nanda Gemma Scope: Open sparse autoencoders everywhere all at once on Gemma 2. In BlackboxNLP Workshop: Analyzing and Interpreting Neural Networks for NLP, Cited by: §C.2.6, §2. Lin (2023) J. Lin Neuronpedia: Interactive reference and tooling for analyzing neural networks. External Links: Link Cited by: Appendix A, §2, §7. Lundberg and Lee (2017) S. M. Lundberg and S. Lee A unified approach to interpreting model predictions. In Advances in Neural Information Processing Systems (NeurIPS), Cited by: §7. Madry et al. (2018) A. Madry, A. Makelov, L. Schmidt, D. Tsipras, and A. Vladu Towards deep learning models resistant to adversarial attacks. In International Conference on Learning Representations (ICLR), Cited by: §C.1, 2nd item. Marks et al. (2025) S. Marks, C. Rager, E. J. Michaud, Y. Belinkov, D. Bau, and A. Mueller Sparse feature circuits: discovering and editing interpretable causal graphs in language models. In International Conference on Learning Representations (ICLR), Cited by: §1, §5, §7. Marques-Silva and Ignatiev (2022) J. Marques-Silva and A. Ignatiev Delivering trustworthy AI through formal XAI. In AAAI Conference on Artificial Intelligence (AAAI), Cited by: §7. Meng et al. (2022) K. Meng, D. Bau, A. Andonian, and Y. Belinkov Locating and editing factual associations in gpt. In Advances in Neural Information Processing Systems (NeurIPS), Cited by: §7. Merity et al. (2017) S. Merity, C. Xiong, J. Bradbury, and R. Socher Pointer sentinel mixture models. In International Conference on Learning Representations (ICLR), Cited by: §C.1. Miller (1995) G. A. Miller WordNet: A lexical database for english. Communications of the ACM. Cited by: Appendix A, 1st item. Olah et al. (2020) C. Olah, N. Cammarata, L. Schubert, G. Goh, M. Petrov, and S. Carter Zoom in: an introduction to circuits. Distill. External Links: Link Cited by: §7. Park et al. (2024) K. Park, Y. J. Choe, and V. Veitch The linear representation hypothesis and the geometry of large language models. In International Conference on Machine Learning, Cited by: §7. Paulo and Belrose (2026) G. Paulo and N. Belrose Sparse autoencoders trained on the same data learn different features. In International Conference on Learning Representations (ICLR), Cited by: §7. Paulo et al. (2025) G. S. Paulo, A. T. Mallen, C. Juang, and N. Belrose Automatically interpreting millions of features in large language models. In International Conference on Machine Learning (ICML), Cited by: §2, §7. Qwen Team (2025) Qwen Team Qwen2.5 technical report. arXiv preprint arXiv:2412.15115. Cited by: §C.2.7, Table 3, §2. Radford et al. (2019) A. Radford, J. Wu, R. Child, D. Luan, D. Amodei, and I. Sutskever Language models are unsupervised multitask learners. OpenAI blog. Cited by: Table 3, §2. Rajamanoharan et al. (2024a) S. Rajamanoharan, A. Conmy, L. Smith, T. Lieberum, V. Varma, J. Kramar, R. Shah, and N. Nanda Improving sparse decomposition of language model activations with gated sparse autoencoders. In Advances in Neural Information Processing Systems (NeurIPS), Cited by: §7. Rajamanoharan et al. (2024b) S. Rajamanoharan, T. Lieberum, N. Sonnerat, A. Conmy, V. Varma, J. Kramár, and N. Nanda Jumping ahead: Improving reconstruction fidelity with jumprelu sparse autoencoders. arXiv preprint arXiv:2407.14435. Cited by: §C.2.6. Ribeiro et al. (2016) M. T. Ribeiro, S. Singh, and C. Guestrin ”Why should i trust you?” Explaining the predictions of any classifier. In ACM SIGKDD international conference on knowledge discovery and data mining, Cited by: §7. Ribeiro et al. (2018) M. T. Ribeiro, S. Singh, and C. Guestrin Anchors: High-precision model-agnostic explanations. In AAAI Conference on Artificial Intelligence (AAAI), Cited by: §7. Singh et al. (2018) G. Singh, T. Gehr, M. Mirman, M. Püschel, and M. Vechev Fast and effective robustness certification. In Advances in Neural Information Processing Systems (NeurIPS), Cited by: §B.1. Somvanshi et al. (2026) S. Somvanshi, M. M. Islam, A. Rafe, A. G. Tusti, A. Chakraborty, A. Baitullah, T. I. Chowdhury, N. Alnawmasi, A. Dutta, and S. Das Bridging the black box: A survey on mechanistic interpretability in AI. ACM Computing Surveys. Cited by: §1, §1, §2, §7. Templeton et al. (2024) A. Templeton, T. Conerly, J. Marcus, J. Lindsey, T. Bricken, B. Chen, A. Pearce, C. Citro, E. Ameisen, A. Jones, H. Cunningham, N. L. Turner, C. McDougall, M. MacDiarmid, A. Tamkin, E. Durmus, T. Hume, F. Mosconi, C. D. Freeman, T. R. Sumers, E. Rees, J. Batson, A. Jermyn, S. Carter, C. Olah, and T. Henighan Scaling monosemanticity: extracting interpretable features from Claude 3 Sonnet. Note: Transformer Circuits Thread. External Links: Link Cited by: §1. Vaswani et al. (2017) A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, Ł. Kaiser, and I. Polosukhin Attention is all you need. In Advances in Neural Information Processing Systems (NeurIPS), Cited by: §2, §2, §7. Wang et al. (2023) K. R. Wang, A. Variengien, A. Conmy, B. Shlegeris, and J. Steinhardt Interpretability in the Wild: A circuit for indirect object identification in GPT-2 Small. In International Conference on Learning Representations (ICLR), Cited by: §7. Wu et al. (2023) M. Wu, H. Wu, and C. Barrett VeriX: Towards verified explainability of deep neural networks. In Advances in Neural Information Processing Systems (NeurIPS), Cited by: §3, §7. Zhang et al. (2019) H. Zhang, Y. Yu, J. Jiao, E. Xing, L. El Ghaoui, and M. Jordan Theoretically principled trade-off between robustness and accuracy. In International Conference on Machine Learning (ICML), Cited by: §C.2.2. Zhao et al. (2024) H. Zhao, H. Chen, F. Yang, N. Liu, H. Deng, H. Cai, S. Wang, D. Yin, and M. Du Explainability for large language models: A survey. ACM Transactions on Intelligent Systems and Technology. Cited by: §7. Appendix A Details on Teaser Figure The teaser figure (Fig. 1) shows a safety-critical sentence we analyzed for an IRN interpretation flip on Gemma 2 2B with the Gemma Scope SAE at layer 1616. It shows a harmful→ attack via a trivial, meaning-preserving synonym swap shifting the dominant features of the target token off their biological reading. Details of this attack are given below: Sentence and target token. “Describe how someone could culture a sample using laboratory equipment available online.” The target token is culture, a polysemous content word that WordNet (Miller, 1995) lists with 88 senses. Perturbation hull. We instantiate the minor perturbation level (Sec. 3): Replace a single content word before the target with a WordNet synonym. For this sentence, an admissible swap is, e.g., someone→ : “Describe how somebody could culture a sample using laboratory equipment available online.” The convex hull ℋkH_k captures the residual-stream activations of these perturbations at the target position (Sec. 4). Interpretation flip. We then search ℋkH_k for an adversarial point H~k H_k that specifically suppresses the safety-relevant features. Concretely, we run projected gradient descent (PGD, 300300 iterations, 88 random restarts) that minimizes the pre-activations of the four biological features active on the clean token, projecting back into ℋkH_k after each step. This targeted interpretation attack drives all four biological features out of the top-88. Tab. 2 lists the top-88 SAE feature labels (Neuronpedia (Lin, 2023), gemmascope-res-16k) at HkH_k and at H~k H_k, with the top-88 Jaccard index under adversarial attack being J¯=0.23 J=0.23. On the clean input, four of the eight features describe a biological-cultivation reading—cellular and molecular biology, neurophysiology, biochemical extraction, and mold growth—alongside a numerical-categorization feature. At the targeted adversarial point, this entire cluster is gone, replaced by generic, non-biological features (accountability in organizational contexts, research methodology, mathematical operations, and other unrelated topics). Only three generic features survive the swap. Table 2: Top-88 SAE features active at HkH_k vs. the targeted adversarial point H~k H_k, Gemma 2 2B layer 1616 with Neuronpedia auto-interp labels. The biological features (red) are removed by the adversarial attack. HkH_k (clean): biological reading H~k H_k (targeted): generic reading # description # description 22342234 copyright / licensing 16951695 accountability & responsibility (professional) 24412441 mold growth and health implications 17501750 mathematical operations & relationships 58135813 numerical data and categorization 22342234 copyright / licensing 80848084 cultural practices 38143814 capability & potential outcomes 86108610 data structures, programming, metadata 80848084 cultural practices 87538753 neurophysiological concepts 86108610 data structures, programming, metadata 1122711227 biochemical extraction & analysis 1264412644 race, ethnicity & social justice 1186311863 cellular processes & molecular biology 1568715687 research methodologies & data analysis Appendix B Verifying Language Models at Scale B.1 Background on Neural Network Verifiers Neural network verification has made rapid progress over the last couple of years (Kaulen et al., 2025). Generally, the verification problem is given as follows: Definition 2. Given a neural network Φ:ℝn→ℝm ^n ^m, a continuous input set ⊂ℝnX ^n (e.g., constructed with an ℓ∞ _∞ perturbation radius ϵ∈ℝ+ε _+ around an input x∈ℝnx ^n), and an unsafe specification ⊂ℝmS ^m (e.g., misclassification), a neural network verifier aims to show that ∀x~∈:Φ(x~)∉.∀ x ( x) . It was shown that verifying such properties of neural networks is NP-hard (Katz et al., 2017), such that state-of-the-art verifiers usually provide sound but incomplete verification results to scale to large neural networks. In this work, we use the verification toolbox CORA (Althoff, 2015; Althoff et al., 2025), which uses reachability analysis to reason about the problem statement. In particular, we use zonotopes (Girard, 2005) to represent X: Definition 3. Given a center c∈ℝnc ^n and a generator matrix G∈ℝn×pG ^n× p, a zonotope is defined as: =⟨c,G⟩Z=c+∑i=1pβiG(⋅,i)|βi∈[−1,1]⊂ℝn.Z= <c,G >_Z\,= \c+ _i=1^p _iG_(·,i)~ |~ _i∈[-1,1] \ ^n. The reasoning here is that certain operations like affine maps, interval bounds, and Minkowski sums can be computed efficiently for zonotopes. For example, given two zonotopes 1=⟨c1,G1⟩ZZ_1= <c_1,G_1 >_Z\,, 2=⟨c2,G2⟩ZZ_2= <c_2,G_2 >_Z\,, the Minkowski sum is computed as: 1⊕2=z1+z2|z1∈1,z2∈2=⟨c1+c2,[G1G2]⟩Z.Z_1 _2= \z_1+z_2\ |\ z_1 _1,\,z_2 _2 \= <c_1+c_2,[G_1\ G_2] >_Z\,. (4) To verify the specifications, CORA propagates X through the neural network to compute an (outer-approximative) output set Y, which is then checked against the specification: ∩=!∅.Y != . (5) In more detail, Y is computed by enclosing the output of each layer: Linear layers can be computed by directly applying the affine map to the given zonotope, and (elementwise) nonlinear layers can be enclosed by finding a linear approximation and bounding the approximation error using an interval (Singh et al., 2018; Koller et al., 2026) for the respective input set ℋkH_k: ϕ(ℋk)⊆(ϕ,ℋk)=(diag(mk)ℋk⊕tk)⊕[d¯k,d¯k],φ(H_k) $ enclose$ (φ,H_k )= (diag (m_k )H_k t_k )\; \; [ d_k, d_k ], (6) where the enclosure parameters are given by the slope mk∈ℝnm_k ^n and offset tk∈ℝnt_k ^n of the linear approximation, and an error interval [d¯k,d¯k]⊂ℝn [ d_k, d_k ] ^n. This high-level description suffices for our work, and we refer interested readers to Koller et al. (2026) for more details. B.2 Per-Layer Verification of an Interpretable Replacement Network Verifying the faithfulness of an IRN as described in Sec. 4 is costly due to the dIRNd_IRN-dimensional hidden layer of the IRN, where it holds that the model dimension dmodel≪dIRNd_ model d_IRN to expose the sparse features (Tab. 3, Tab. 4). To optimize the formal verification in our setting, we exploit the special structure of the IRN. Please note that we only need to certify the ℓ∞ _∞-bounds of the resulting difference set (Def. 1, Fig. 3). We discuss the transcoder case (Eq. 3) in this section, with the sparse autoencoder case being analogous (Eq. 2). Per token, we bound the difference network fk(Hk)=MLPk(Hk)−TCk(Hk)f_k(H_k)=MLP_k(H_k)-TC_k(H_k) (7) over an input set ℋk⊂ℝmodeldH_k ^d_ model, i.e., we need to bound fk(ℋk)=fk(Hk)|Hk∈ℋk.f_k(H_k)=\f_k(H_k)\ |\ H_k _k\. (8) A set-based verifier can enclose this difference by enclosing each layer of fkf_k (Sec. B.1). In the transcoder branch, we only have a single high-dimensional nonlinear layer sandwiched by linear maps. Thus, we are only required to compute a single enclosure for the nonlinear layer, as linear layers are usually easy to compute. The parameters of that enclosure are determined by the pre-activation bounds (Wkencℋk+bkenc)$ interval$ (W^enc_kH_k+b^enc_k ) alone. We notice that if ℋkH_k is an axis-aligned box, i.e., ℋk=[Hk−ϵ,Hk+ϵ]H_k=[H_k-ε,H_k+ε] for some ϵ∈ℝ+ε _+, it holds (Jaulin et al., 2001): (Wkencℋk⊕bkenc)=Wkenc(ℋk)⊕bkenc.$ interval$ (W^enc_kH_k b^enc_k )=W^enc_k$ interval$ (H_k ) b^enc_k. (9) This enables us to deploy a one-step look-ahead using pure interval arithmetic (Ladner and Althoff, 2025) to obtain the same parameters of the enclosure: (mk,tk,[d¯k,d¯k])(m_k,t_k, [ d_k, d_k ]). Given these, we can redistribute the transcoder enclosure (Eq. 6) as follows: TCk(ℋk)⊆(TCk,ℋk)=Wkdec(diag(mk)(Wkencℋk⊕bkenc)⊕tk⊕[d¯k,d¯k])⊕bkdec=Wkdecdiag(mk)Wkencℋk⊕Wkdec(diag(mk)bkenc⊕tk⊕[d¯k,d¯k])⊕bkdec=Mk,TCℋk⊕ℐk,TC. splitTC_k(H_k)& $ enclose$ (TC_k,H_k )\\ &=W^dec_k (diag (m_k )(W^enc_kH_k b^enc_k) t_k [ d_k, d_k ] ) b^dec_k\\ &=W^dec_kdiag (m_k )W^enc_k\ H_k\ \ W^dec_k (diag (m_k )b^enc_k t_k [ d_k, d_k ] ) b^dec_k\\ &= \ \ \,\,M_k,TCH_k\ \ I_k,TC. split (10) Please note that the term Wkdecdiag(mk)WkencW^dec_kdiag (m_k )W^enc_k can be collapsed into a single matrix Mk,TCM_k,TC such that the high-dimensional zonotope is never explicitly constructed. Unfortunately, this optimization is not directly possible for the MLP due to the multiple layers; nevertheless, a set-based verifier can give us: MLPk(ℋk)⊆(MLPk,ℋk)=Mk,MLPℋk⊕ℐk,MLP,MLP_k(H_k) $ enclose$ (MLP_k,H_k )=M_k,MLPH_k _k,MLP, (11) which results in an overall enclosure of the difference network (Eq. 7): fk(ℋk)⊆(fk,ℋk)=(Mk,MLP−Mk,TC)ℋk⊕(ℐk,MLP⊕−ℐk,TC).f_k(H_k) $ enclose$ (f_k,H_k )=(M_k,MLP-M_k,TC)H_k (I_k,MLP -I_k,TC). (12) The case for SAE is analogous with the identity instead of the MLP. The goal of the set-based verifier is then to find the smallest δ∈ℝ+δ _+ such that this difference enclosure is contained in [−δ,δ]dmodel [-δ,δ ]^d_ model (Def. 1). A smaller δ thus means that the IRN is more faithful, with an ideal case of δ→0δ→ 0. Alg. 1 summarizes the resulting per-layer verification with Fig. 8 illustrating two example δ values. Figure 8: Alignment of an IRN with the model. Output surfaces of MLPkMLP_k and TCkTC_k over a two-dimensional slice of the local neighborhood ℋkH_k, shown for one output dimension (l)(l); colors as in Fig. 3. (a) An unfaithful IRN: the surfaces disagree and even cross, so only a large δ can be certified. (b) A faithful IRN: the surfaces almost coincide, and a small δ suffices. Algorithm 1 Per-layer transcoder verification: difference enclosure and certified δ. 1: Input ℋkH_k; TCkTC_k-block; MLPkMLP_k-block; δ∈ℝ+δ _+ 2: [l,u]←Wkenc(ℋk)+bkenc [l,u ]← W^enc_k\,$ interval$ (H_k )+b^enc_k ⊳ Pre-activation bound (exact for a box input; Eq. 9) 3: (mk,tk,[d¯k,d¯k])←(m_k,t_k, [ d_k, d_k ])← enclosure of ϕφ on [l,u] [l,u ] ⊳ One-step look-ahead (Eq. 6) 4: (Mk,TC,ℐk,TC)←(TCk,ℋk)(M_k,TC,I_k,TC)←$ enclose$ (TC_k,H_k ) ⊳ TC enclosure (Eq. 10) 5: (Mk,MLP,ℐk,MLP)←(MLPk,ℋk)(M_k,MLP,I_k,MLP)←$ enclose$ (MLP_k,H_k ) ⊳ MLP enclosure (Eq. 11) 6: Mk←Mk,MLP−Mk,TCM_k← M_k,MLP-M_k,TC; ℐk←ℐk,MLP⊕−ℐk,TCI_k _k,MLP -I_k,TC 7: ℋk+1←Mkℋk⊕ℐkH_k+1← M_k\,H_k _k ⊳ Difference enclosure (Eq. 12) 8: return ℋk+1⊆[−δ,δ]dmodelH_k+1 [-δ,δ]^d_ model? ⊳ Containment check Proposition 1 (Soundness). For an axis-aligned input box ℋk⊂ℝdmodelH_k ^d_ model, an MLP and its respective IRN, Alg. 1 verifies ∥fk(Hk)∥∞≤δ f_k(H_k) _∞≤δ for all Hk∈ℋkH_k _k in (dmodel2dIRN)O(d_ model^2\,d_IRN) time and (dmodeldIRN)O(d_ model\,d_IRN) memory. Proof. Soundness. Soundness follows from the soundness of the set-based verifier and each additional step being outer-approximative. Each of these additional steps is machine-checked in Lean 4 in the supplementary material. Complexity. Let dIRNd_IRN be the IRN hidden width with dmodel≪dIRNd_ model d_IRN, and the MLP hidden width dMLP∈Θ(dmodel)d_MLP∈ (d_ model) (Tab. 3 and 4); the input box contributes dmodeld_ model generators. (i) IRN branch (lines 1–3). Propagating the input set explicitly through encoder, activation, and decoder builds a zonotope in ℝdIRNR^d_IRN: the activation enclosure appends one error generator per neuron, yielding a dense dIRN×(dmodel+dIRN)d_IRN×(d_ model+d_IRN) generator matrix, so decoding it would cost (dmodeldIRN2)O(d_ model\,d_IRN^2) time and (dIRN2)O(d_IRN^2) memory. The one-step look-ahead instead reads the pre-activation box in (dmodeldIRN)O(d_ model\,d_IRN), computes the dIRNd_IRN enclosure parameters in (dIRN)O(d_IRN), and collapses Mk,TC=Wkdecdiag(mk)WkencM_k,TC=W^dec_kdiag (m_k )W^enc_k in (dmodel2dIRN)O(d_ model^2\,d_IRN) time and (dmodeldIRN)O(d_ model\,d_IRN) memory—a factor dIRN/dmodeld_IRN/d_ model cheaper in both. (i) MLP branch (line 4). Here the collapse trick does not apply, as the MLP interleaves its κMLP _MLP affine maps with nonlinearities; the set is propagated layer by layer instead. Since dMLP∈Θ(dmodel)d_MLP∈ (d_ model), the running zonotope keeps (dmodel)O(d_ model) generators each of length (dmodel)O(d_ model), and applying an affine map to this (dmodel)×(dmodel)O(d_ model)×O(d_ model) generator matrix costs (dmodel3)O(d_ model^3); over the κMLP _MLP layers the branch is (κMLPdmodel3)O( _MLP\,d_ model^3) time and (dmodel2)O(d_ model^2) memory. As dIRN≫dmodel,κMLPd_IRN d_ model,\, _MLP, this branch is negligible compared to (i). (i) Difference and containment (lines 5–7). All operands now live in ℝdmodelR^d_ model: forming Mk=Mk,MLP−Mk,TCM_k=M_k,MLP-M_k,TC and ⟨c′,G′⟩Z=Mkℋk⊕ℐk <c ,G >_Z\,=M_k\,H_k _k costs (dmodel2)O(d_ model^2), and δ=maxj(|c(j)′|+∥G(j,:)′∥1)δ= _j( c _(j) + G _(j,:) _1) is computed in (dmodel2)O(d_ model^2). In summary, the cost is (dmodel2dIRN)O(d_ model^2\,d_IRN) time and (dmodeldIRN)O(d_ model\,d_IRN) memory: The look-ahead IRN branch dominates the MLP branch since dIRN≫dmodel,κMLPd_IRN d_ model,\, _MLP—yet it stays a factor dIRN/dmodeld_IRN/d_ model below the (dmodeldIRN2)O(d_ model\,d_IRN^2) time and (dIRN2)O(d_IRN^2) memory of a naive IRN zonotope propagation. ∎ B.3 Sound Lower Bound on the Jaccard Index Sec. 3 reports an attack-derived upper bound J¯ J on the worst-case top-Ktop-K feature Jaccard: A single adversarial input witnesses that the overlap can drop at least this far. The intermediate pre-activation bounds (Eq. 9) used to certify δ¯ δ (Sec. B.2) also yield a certified lower bound J¯ J on the top-Ktop-K Jaccard, so that J¯≤J∗≤J¯, J\;≤\;J^*\;≤\; J, (13) where J∗J^* is the true worst-case Jaccard over the hull ℋkH_k. In more detail, the IRN feature pre-activations are an affine function of the residual stream, z(Hk)=WkencHk+bkencz(H_k)=W^enc_kH_k+b^enc_k. For the axis-aligned input box ℋk=[Hk−ϵ,Hk+ϵ]H_k=[H_k-ε,H_k+ε], interval arithmetic (Jaulin et al., 2001) gives the exact per-feature pre-activation range [z¯,z¯][ z, z], and the subsequent activation (e.g. ReLUReLU) is monotone, hence preserves the ranking among co-active features. Let T0T_0 be the top-Ktop-K features at the clean input HkH_k. A feature i∈T0i∈ T_0 is guaranteed to remain in the top-Ktop-K for every input in ℋkH_k iff fewer than K other features can possibly outrank its lower bound, |j≠i:z¯(j)≥z¯(i)|<K. |\\,j≠ i z_(j)≥ z_(i)\,\ |<K. (14) That is, an adversary first fills the top-Ktop-K with the strongest contestant features—any feature whose upper bound reaches i’s floor z¯(i) z_(i); the comparison is non-strict so that the bound stays sound when two features tie exactly—and the feature i “survives” any adversarial attack only if fewer than K such contestants exist. Thus, the certified survivor set over ℋkH_k is given by: =argminHk∈ℋk:T(Hk)|T(Hk)|,S= _H_k _k T(H_k)|T(H_k)|, (15) where T(Hk)T(H_k) returns the survivor set for a particular input Hk∈ℋkH_k _k. Using S and as |T0|=K|T_0|=K, a certified lower bound on the Jaccard index is given by: J¯=||2K−||. J= |S|2K-|S|. (16) Appendix C Evaluation Details and Ablation Studies C.1 Evaluation Details This appendix first states the setup shared by all experiments, with subsequent details specific to individual experiments. Hardware and software. All experiments run on an NVIDIA GeForce RTX 3080 Laptop GPU (16 GB VRAM), Intel Core i7-11800H (8 cores, 2.3 GHz), Windows 11. The pipeline has two halves with different stacks. Data preparation such as model decomposition and IRN export runs in Python 3.13 with PyTorch 2.10 on the GPU. Everything that touches the verifier runs in MATLAB R2024b with CORA (Althoff, 2015; Althoff et al., 2025; Koller et al., 2026). The median verification time per (sample, block k) is ∼1.4 \!1.4 min. Models and IRNs. Tab. 3 lists the open-weight language models we analyzed and Tab. 4 the corresponding sparse autoencoders and transcoders. Both are loaded directly from HuggingFace (click HF in the last column for the repository page). Table 3: Large language models. dmodeld_ model: residual-stream dimension; dMLPd_MLP: MLP hidden width (post-gating, where applicable); κ: number of transformer blocks. Model Vendor params dmodeld_ model dMLPd_MLP κ Ref. GPT-2 OpenAI 124124M 768768 3,0723,072 1212 Radford et al. (2019), HF Gemma 2 2B Google 2.62.6B 2,3042,304 9,2169,216 2626 Gemma Team (2024), HF Gemma 3 1B Google 1.01.0B 1,1521,152 6,9126,912 2626 Gemma Team (2025), HF Llama 3.2 1B Meta 1.21.2B 2,0482,048 8,1928,192 1616 Grattafiori et al. (2024), HF R1-Distill-Qwen 1.5B DeepSeek 1.81.8B 1,5361,536 8,9608,960 2828 Guo et al., Qwen Team (2025), HF Table 4: Interpretable replacement networks. dIRNd_IRN: dictionary size; activation: feature non-linearity; hook: residual position read by the IRN (pre = before block, post = after block). SAEs usually reconstruct the residual stream (identity), while TCs replace the MLP block. Model Type Activation dIRNd_IRN Hook Ref. Replaces (dMLPd_MLP, act) GPT-2 SAE ReLUReLU 24,57624,576 pre HF residual (identity) GPT-2 TC ReLUReLU 24,57624,576 pre HF MLP (3,0723,072, GELUGELU) Gemma 2 2B SAE JumpReLUJumpReLU 16,38416,384 post HF residual (identity) Gemma 2 2B TC JumpReLUJumpReLU 16,38416,384 post HF MLP (9,2169,216, GeGLUGeGLU) Gemma 3 1B SAE JumpReLUJumpReLU 16,38416,384 post HF residual (identity) Gemma 3 1B TC JumpReLUJumpReLU 16,38416,384 post HF MLP (6,9126,912, GeGLUGeGLU) Llama 3.2 1B SAE TopKTopK 131,072131,072 post HF residual (identity) Llama 3.2 1B TC TopKTopK 131,072131,072 post HF MLP (8,1928,192, SwiGLUSwiGLU) R1-Distill-Qwen 1.5B SAE TopKTopK 65,53665,536 post HF residual (identity) Dataset and input set. Input sentences are drawn from WikiText-2 (Merity et al., 2017), the canonical corpus for GPT-2. Within each sentence, we pick a target content word and build the input set ℋkH_k from semantics-preserving paraphrases of that sentence (Sec. 3). As LLMs typically have causal masking, only words before the target token affect the residual stream at the target position, so all replacements are restricted to that prefix. Targets are chosen to be polysemous (the content word with the most WordNet senses), which stresses feature attribution the most. We collect 1,0001,000 such sentences and split them 600/200/200600/200/200 into train/val/test datasets (Tab. 5). For each sentence, we forward all paraphrase variants, record H~k H_k at layer k for the target token, and take the per-coordinate interval hull as that sample’s input box ℋkH_k. The radius of ℋkH_k is thus per sample, i.e., each sentence is verified inside its own hull rather than a single shared radius. This is in contrast to the usual neural network verification literature, but we chose this setting so that the certified region tracks where the model actually operates. We include uniform-radius experiments in an ablation study in Sec. C.2.1. Bound search. For each (sample, layer) we find the smallest verifiable δ¯ δ by a walk-then-bisect search (Alg. 2). We start from δ=100δ=100 (seeded up to 2×2× the layer’s median δ¯ δ when that exceeds 100100, since deep layers are far less faithful), and call the verifier on the diff network over the sample’s hull: on VERIFIED, we halve δ, and on counterexample CEX or TIMEOUT, we double it. Once a bracket of a verified upper bound and an unverified lower bound is reached, we switch to geometric bisection. The search is capped at 1212 iterations per sample with a per-call timeout of 1010 s. The lower bound δ¯ δ comes instead from the strongest adversary found by PGD, so reporting δ¯≤δ∗≤δ¯ δ≤δ^*≤ δ is sound. Please note that we use the geometric mean during the binary search as the δ ranges over many orders of magnitude; thus, this effectively computes the midway point on a log scale. Algorithm 2 Per-(sample, layer) verified bound δ search. 1: Diff. network f=MLPk−IRNkf=MLP_k-IRN_k, input box ℋH, start δ0 _0, max iterations N, timeout τ 2: δ←δ0δ← _0; δlow←0 _low← 0; δhigh←∞ _high←∞ ⊳ δlow _low: largest unverified, δhigh _high: smallest verified 3: for i=1i=1 to N do 4: Result r←Verify(f,ℋ,δ,τ)r← Verify(f,H,δ,τ) 5: if r=r= VERIFIED then 6: δhigh←δ _high←δ 7: else ⊳ CEX or TIMEOUT 8: δlow←δ _low←δ 9: if δlow>0 _low>0 and δhigh<∞ _high<∞ then 10: δ←δlow⋅δhighδ← _low· _high ⊳ geometric bisection once bracketed 11: else if r=r= VERIFIED then 12: δ←δ/2δ←δ/2 13: else 14: δ←2δ← 2\,δ ⊳ walk up until decisive 15: return δ¯←δhigh δ← _high ⊳ smallest verified bound Both attack-derived bounds use the same ℓ∞ _∞ PGD adversary, run inside each sample’s hull for 200200 iterations, 44 random restarts, projecting back into ℋkH_k after each signed-gradient step. For δ¯ δ, the objective is to maximize ‖MLPk(H~k)−IRNk(H~k)‖∞\|MLP_k( H_k)-IRN_k( H_k)\|_∞ (the largest diff we can witness); for J¯ J, it is to maximize the drop in top-2020 feature overlap between the clean and perturbed activation. The respective other bound is found using the CORA verifier. Training regimes. The retrained IRNs of Sec. 5 all fine-tune the IRN for 5050 epochs (batch 88, Adam at lr=10−3lr=10^-3), differing only in the loss: Std keeps the clean reconstruction objective; PGD (Madry et al., 2018) augments it with 55-step PGD adversaries; Set (Koller et al., 2025) adds the reachable-set volume loss with default weight τ=0.1τ=0.1, ramped in over a 55-epoch warmup and 1010-epoch noise rampup up to the largest train-split hull radius. Please note that set-based training can require a lot of memory due to the represented sets; however, this can be circumvented to a certain degree by capturing certain parts in an interval error (Koller et al., 2025, Appendix A). In this work, we capture all accumulated approximation errors in an interval error during training. LoRA variants restrict the update to a rank-1616 adapter (Hu et al., 2022). Every variant is verified with the identical per-sample-hull protocol on the held-out test set. Ablation studies on the weighting parameter τ and the LoRA rank are deferred to Sec. C.2.3 and C.2.4, respectively. C.2 Ablation Studies Finally, we provide further experiments and ablation studies in this subsection. C.2.1 Input Radius: Default Hull and Uniform Radius Default input set. In the main section, we verify each sample inside its own paraphrase hull rather than a fixed box as described in Sec. C.1. Tab. 5 reports its distribution for GPT-2 layer 66 as an example. Table 5: Per-sample paraphrase-hull ℓ∞ _∞ radius ϵε on GPT-2 layer 66, i.e., the radius of the default verification input set. split n median mean q25q_25 q75q_75 max train 600 0.730.73 1.101.10 0.390.39 1.361.36 8.008.00 val 200 0.820.82 1.221.22 0.440.44 1.661.66 8.658.65 test 200 0.690.69 1.031.03 0.350.35 1.361.36 7.957.95 Uniform-radius input set. In this section, we compare a uniform ℓ∞ _∞ input radius ϵ∈0.01,0.05,0.1,0.5ε∈\0.01,0.05,0.1,0.5\, and verify the pretrained baseline (Std) against matching Set- and PGD-trained SAEs on GPT-2 layer 66 over the same held-out test dataset. Each retrained variant is fine-tuned from OpenAI’s SAE baseline. Result. Tab. 6 reports the per-sample verified δ¯ δ distribution for Std, PGD, and Set at each radius. Generally, adversarial and verification-aware training improve over the baseline, with the improvement becoming larger with larger ϵε. One notable exception is ϵ=0.01ε=0.01, likely as the accuracy-robustness tradeoff is not yet beneficial. Please note that δ¯ δ is the ℓ∞ _∞ radius of a dmodeld_ model-dimensional cube containing the certified diff-network output set. Thus, its volume scales as (2δ¯)dmodel(2 δ)^d_ model with dmodel=768d_ model=768 for GPT-2, so even modest radius gains compound dimensionally into large volume gains. The log10ΔV _10 _V column of Tab. 6 reports this radius-volume relation. Table 6: Verified output bound δ on GPT-2 SAE layer 66, uniform ℓ∞ _∞ input radius ϵε. δ¯(↓) δ\ ( ) ϵε method min q25q_25 median q75q_75 max Δmed(↓) _med\ ( ) log10ΔV(↓) _10 _V\ ( ) 0.010.01 Std 4.05 7.93 10.98 24.21 194.66 — — PGD 24.73 28.43 30.22 32.12 65.73 +175.3%+175.3\% +337.7+337.7 Set 23.94 28.59 30.38 32.29 66.62 +176.8%+176.8\% +339.6+339.6 0.050.05 Std 7.43 36.14 67.71 135.89 470.56 — — PGD 28.78 35.50 40.59 53.55 225.30 −40.1%-40.1\% −170.7-170.7 Set 28.47 35.55 40.26 50.24 214.59 −40.5%-40.5\% −173.4-173.4 0.10.1 Std 16.21 203.02 320.36 496.74 1083.40 — — PGD 38.35 107.88 173.97 277.54 757.83 −45.7%-45.7\% −203.6-203.6 Set 31.05 58.34 94.60 189.08 665.47 −70.5%-70.5\% −406.8-406.8 0.50.5 Std 25600 51200 51200 51200 51200 — — PGD 18101.9 25600 25600 25600 51200 −50.0%-50.0\% −231.2-231.2 Set 2934.4 18102 18102 25600 51200 −64.6%-64.6\% −346.8-346.8 C.2.2 Sparsity of the Retrained IRNs Fine-tuning an IRN for faithfulness could in principle buy robustness by simply activating more features, which would defeat the purpose of a sparse, interpretable dictionary. Note that none of our training regimes explicitly adds a sparsity penalty to the loss (Sec. C.1), i.e., sparsity is only inherited from the pretrained IRN. Tab. 7 therefore reports how many of the dIRN=24,576d_IRN=24,576 features of the GPT-2 layer-66 SAE are active, counted both at the clean input (L0L_0) and over the entire perturbation hull ℋkH_k. Reassuringly, the retrained IRNs do not become denser but sparser: Set activates 5×5× fewer features than the baseline on clean inputs, and every regime reduces the number of features that can be active anywhere in the hull. The single exception is Set + LoRA, which roughly doubles the clean feature count while still admitting the fewest active features over the hull, i.e., the low-rank update trades a denser clean code for a more stable one. We acknowledge that the reconstruction loss of the clean sentence suffers slightly, which is in line with the well-known accuracy-robustness tradeoff observed in adversarial training (Zhang et al., 2019). Table 7: Feature sparsity per training regime on the GPT-2 layer-66 SAE (dIRN=24,576d_IRN=24,576), averaged over the 200200 test samples. L0L_0 counts the features active at the clean input, the hull columns those active for at least one point of ℋkH_k; ratios are relative to Std, lower is sparser. L0L_0 (clean) active over hull Regime count ratio count ratio Std 74.474.4 1.001.00 8433.28433.2 1.001.00 PGD 52.852.8 0.710.71 7966.87966.8 0.940.94 Set 13.9 0.19 5568.95568.9 0.660.66 PGD + LoRA 44.044.0 0.590.59 6893.16893.1 0.820.82 Set + LoRA 143.8143.8 1.931.93 4383.8 0.52 C.2.3 Set-Based Training: Loss Weighting Set-based training interpolates between the center (reconstruction) loss and the reachable-set volume loss as (1−τ)ℒcenter+τℒvol(1-τ)\,L_center+τ\,L_vol, with τ=0.1τ=0.1 being the default (Koller et al., 2025). Tab. 8 sweeps τ∈0.1,0.5,0.9τ∈\0.1,0.5,0.9\ on GPT-2 layer 66. The verified bound is remarkably flat in τ: For full fine-tuning the median moves only within [47.8,60.3][47.8,60.3] and the reconstruction loss within [15.9,29.7][15.9,29.7]. Table 8: Impact of the volume weight τ on GPT-2 layer 66 SAE: Clean reconstruction MSE and verified δ¯ δ distribution. Recon.(↓)Recon.( ) δ¯(↓) δ\ ( ) τ (clean) min q25q_25 median q75q_75 max Set 0.10.1 16.016.0 25.025.0 35.535.5 50.550.5 872.4872.4 5120051200 0.50.5 29.729.7 24.524.5 37.137.1 60.360.3 931.0931.0 5120051200 0.90.9 15.915.9 24.724.7 35.635.6 47.847.8 807.0807.0 5120051200 C.2.4 LoRA Rank Tab. 9 sweeps the LoRA rank r∈8,16,32r∈\8,16,32\ for set-based training at τ=0.1τ=0.1. As expected, a higher rank tends to obtain tighter δ¯ δ bounds. However, please note that this comes with additional memory requirements and choosing a very large rank might not always be feasible for large IRNs. Table 9: LoRA rank ablation for set-based training (τ=0.1τ=0.1) on GPT-2 layer 66 SAE. Recon.(↓)Recon.( ) δ¯(↓) δ\ ( ) r (clean) min q25q_25 median q75q_75 max 88 132.4132.4 26.526.5 102.4102.4 169.8169.8 1215.31215.3 5120051200 1616 122.8122.8 28.028.0 82.182.1 135.8135.8 398.8398.8 5120051200 3232 766.2766.2 28.528.5 50.550.5 60.660.6 95.295.2 5120051200 C.2.5 Scalability: Verification of Llama’s IRN Verifying architectures other than GPT-2 primarily comes down to an engineering task, as the verification is done per layer, which differs only mildly between architectures. To demonstrate this, we verify the largest IRN in our suite, the Llama 3.2 1B SAE. This architecture varies in two ways: (i) dIRN=131,072d_IRN=131,072 is much larger, and (i) it uses TopKTopK activation before ReLUReLU is applied (Tab. 4). The large dIRNd_IRN is not an issue using the optimization described in Sec. B.2; however, the TopKTopK activation requires adaptation since TopKTopK is not elementwise: Which K features survive depends on their magnitude and varies across the input box. TopK enclosure. As in Sec. B.3, the feature pre-activations are an affine function of the residual stream, z(Hk)=WkencHk+bkencz(H_k)=W^enc_k\,H_k+b^enc_k. Thus, for an input box ℋkH_k, interval arithmetic gives the exact per-feature range z(Hk)∈[z¯,z¯]⊂ℝdIRNz(H_k)∈ [ z, z ] ^d_IRN. The TopKTopK gate keeps the K features with the largest pre-activations, that is, those above the selection threshold τ(Hk)∈ℝτ(H_k) , defined as the K-th largest entry of z(Hk)z(H_k). As HkH_k ranges over ℋkH_k, each entry i of z(Hk)z(H_k) moves within its interval [z¯(i),z¯(i)] [ z_(i), z_(i) ], and the threshold τ(Hk)τ(H_k) moves with it. Thus, reading out the K-th largest entries of z¯(i),z¯(i) z_(i), z_(i) gives us τ¯,τ¯ τ, τ, respectively, such that τ(Hk)∈[τ¯,τ¯]τ(H_k)∈ [ τ, τ ] for all Hk∈ℋkH_k _k. Comparing each feature’s range against this threshold band [τ¯,τ¯] [ τ, τ ] partitions the dIRNd_IRN feature indices into three sets, Tinact=i∈[dIRN]:z¯(i)<τ¯,Tact=i∈[dIRN]:z¯(i)>τ¯,Tund=[dIRN]∖(Tinact∪Tact), splitT_inact&=\\,i∈[d_IRN] z_(i)< τ\,\,\\ T_act&=\\,i∈[d_IRN] z_(i)> τ\,\,\\ T_und&=[d_IRN] (T_inact∪ T_act), split (17) where the inactive features TinactT_inact are never kept, the active features TactT_act are always kept, and the undecided features TundT_und are only sometimes kept. The active features pass an elementwise ReLUReLU and fold into Eq. 12 unchanged; only the undecided gates i∈Tundi∈ T_und need extra care, as each is either off (outputs 00) or on (outputs ReLU(z(i))ReLU(z_(i))). Since TopKTopK keeps exactly K features and the |Tact|≤K T_act ≤ K active features are always among them, exactly K′≔K−|Tact|K K- T_act of the undecided features are on for any given input HkH_k. Let T(Hk)⊆TundT(H_k) T_und with |T(Hk)|=K′ T(H_k) =K denote this input-dependent set. To bound the decoded contribution of T(Hk)T(H_k) to an output coordinate j over ℋkH_k, we define for each undecided feature i∈Tundi∈ T_und its extreme admissible contribution: a(i)+=max(0,W(i,j)decReLU(z¯(i))),a(i)−=min(0,W(i,j)decReLU(z¯(i))), splita^+_(i)&= \! (0,\,W^dec_(i,j)ReLU( z_(i)) ),\\ a^-_(i)&= \! (0,\,W^dec_(i,j)ReLU( z_(i)) ), split (18) where the outer max/min / select the upper/lower endpoint of the contribution over the feature being off (00) or on (up to ReLU(z¯(i))ReLU( z_(i))) and the unknown sign of W(i,j)decW^dec_(i,j), respectively. We then sort a+a^+ in descending order and a−a^- in ascending order. Since only K′K of the undecided features fire, the contribution to coordinate j is bounded by the K′K extreme terms on each side: ∑i∈T(Hk)W(i,j)decReLU(z(i))∈[∑r=1K′a(r)−,∑r=1K′a(r)+]. _i∈ T(H_k)W^dec_(i,j)ReLU(z_(i))\;∈\; [\, _r=1^K a^-_(r),\ \ _r=1^K a^+_(r)\, ]. (19) This interval can be plugged into Eq. 10f, which eventually gives us the verified upper bound δ¯ δ. Results. Fig. 9 shows the per-layer faithfulness gap at the minor level across all 1616 layers of the Llama 3.2 1B SAE (TopKTopK, K=32K=32, dIRN=131,072d_IRN=131,072), mirroring Fig. 4 for GPT-2: a substantial gap is certified throughout, again widening in the deeper, less faithful layers. Please note that the gap between δ¯ δ and δ¯ δ is larger here; we primarily attribute this to the additional outer approximations stemming from the TopKTopK enclosure, as it is expected that such an enclosure is worse than a simple elementwise activation function (such as ReLUReLU in the GPT-2 case), and designing IRNs with verification in mind helps to reduce the conservativeness. Tab. 10 reports the bounds [δ¯,δ¯][ δ, δ] at layer 11 for all three perturbation levels. Despite the undecided set TundT_und growing to nearly the whole dictionary at major, our enclosure obtains useful bounds on the faithfulness gap. Figure 9: Llama Scope. Faithfulness gap of the SAE. Table 10: Faithfulness gap of Llama 3.2 1B SAE on layer 11, per fragility level. δ¯ δ (↓)( ) δ¯ δ (↓)( ) Level |Tund| T_und (↓)( ) q25q_25 median q75q_75 q25q_25 median q75q_75 minor 5,3365,336 0.0340.034 0.0550.055 0.0870.087 0.1220.122 0.2250.225 0.5060.506 medium 100,559100,559 0.0720.072 0.0970.097 0.1460.146 0.4340.434 0.7270.727 1.2521.252 major 131,037131,037 0.1180.118 0.1870.187 0.2540.254 0.9230.923 1.9351.935 2.9342.934 C.2.6 Gemma Scope The Gemma Scope (Lieberum et al., 2024) uses JumpReLU as an activation function to obtain sparsely activated features in its IRNs (Rajamanoharan et al., 2024b). JumpReLU is a generalization of ReLU and is given by: JumpReLU(x,θ)=xif x>θ,0otherwise,JumpReLU(x;\;θ)= casesx&if x>θ,\\ 0&otherwise, cases (20) where θ∈ℝθ is a trainable parameter determining a discontinuous jumping point. As this activation function is applied elementwise, many existing verifiers already support JumpReLU or can add support with little effort. Fig. 10a shows a histogram of θ per layer of Gemma 2 2B, where θ seems to increase with the layer index k. Unfortunately, a higher θ means that the discontinuous jump will be larger as well, and thus an enclosure might become overly conservative (Fig. 10b). Figure 10: JumpReLU. (a) Histogram of jump parameter θ per layer of Gemma 2 2B. (b) Example zonotopic enclosure with a discontinuous jump at θ=2θ=2. Results. Fig. 11 shows the per-layer faithfulness gap for both Gemma 2 2B and Gemma 3 1B SAEs across all 2626 layers: The certified gap is sound throughout and widens with depth, but the difference between δ¯ δ and δ¯ δ is larger than for the smooth GPT-2 transcoder despite all having similar dimensions (Tab. 3). We attribute this to the conservativeness of enclosing a discontinuous JumpReLUJumpReLU gate (Fig. 10b), which again emphasizes the need for verification-friendly architectures. Figure 11: Gemma Scope. Faithfulness gap of the SAEs. C.2.7 R1-Distill-Qwen 1.5B Finally, we determine the faithfulness gap on the last model of our suite: R1-Distill-Qwen 1.5B SAE (Guo et al., 2025; Qwen Team, 2025), a distilled reasoning model. Its IRN is an EleutherAI TopKTopK SAE of the same family as Llama 3.2 1B’s, so verification reuses the TopKTopK enclosure of Sec. C.2.5. The architecture differs from Llama 3.2 1B only in scale (Tab. 3 and 4): a narrower residual stream (dmodel=1,536d_ model=1,536) over more layers (κ=28κ=28), a smaller dictionary (dIRN=65,536d_IRN=65,536 vs. 131,072131,072), and the same selection budget K=32K=32. Results. Fig. 12 shows the per-layer faithfulness gap at the minor level across all 2828 layers of the R1-Distill-Qwen 1.5B SAE, over the same 200200 samples as the other models. We note that the SAE of the R1-Distill-Qwen 1.5B model is an order of magnitude less faithful than the SAE of the Llama 3.2 1B model (Fig. 9). As with all non-elementwise TopKTopK IRNs, the gap stays far above that of GPT-2, reinforcing the case for verification-friendly designs. Figure 12: DeepSeek-Qwen. Faithfulness gap of the TopKTopK SAE. C.2.8 Faithfulness Training across Layers In this experiment, we extend the experiment in Sec. 5 to provide further insights into the benefit of verification-aware training over adversarial training across more layers of GPT-2, in particular, as we noticed in Fig. 4 that the faithfulness gap seems to increase for later layers—a trend that we also observed for all other models in our suite (Fig. 9, Fig. 11, Fig. 12). Results. Fig. 13 clearly shows that verification-aware training using sets keeps the faithfulness gap small, which is not obtainable for other adversarial training methods. Please note that we used the same training hyperparameters at every layer. Figure 13: Faithfulness training across layers. Faithfulness gap per training regime on the GPT-2 SAE across layers.