Validating Mechanistic Interpretations: An Axiomatic Approach
Authors: Nils Palumbo
Ravi Mangal
Zifan Wang
Saranya Vijayakumar
Corina S. Pasareanu
Somesh Jha
Venue: ICML 2025 poster (2025)
Keywords: mechanistic interpretability
axiomatic approach
Primary area: social_aspects->accountability_transparency_and_interpretability
TL;DR: The notion of mechanistic interpretation can be ad-hoc. We axiomatize this notion and apply these axioms to validate mechanistic interpretations extracted for two case studies.

Abstract: Mechanistic interpretability aims to reverse engineer the computation performed by a neural network in terms of its internal components. Although there is a growing body of research on mechanistic interpretation of neural networks, the notion of a *mechanistic interpretation* itself is often ad-hoc. Inspired by the notion of abstract interpretation from the program analysis literature that aims to develop approximate semantics for programs, we give a set of axioms that formally characterize a mechanistic interpretation as a description that approximately captures the semantics of the neural network under analysis in a compositional manner. We demonstrate the applicability of these axioms for validating mechanistic interpretations on an existing, well-known interpretability study as well as on a new case study involving a Transformer-based model trained to solve the well-known 2-SAT problem.

Validating Mechanistic Interpretations: An Axiomatic Approach
Nils Palumbo
Ravi Mangal? 2
Zifan Wang²
Saranya Vijayakumar Corina Päsäreanu" Somesh Jha"
Abstract
aspects of vision as well as language models, it has found most success in analyzing small models trained to solve specific algorithmic tasks such as modular addition (Nanda et al., 2023a). Although such small models are not necessar ily of practical use, analyzing them has been fruitful for de- veloping the techniques needed to mechanistically interpret.
Mechanistic interpretability aims to reverse engineer the computation performed by a neural network in terms of its internal components. Although there is a growing body of research on mechanistic interpretation of neural networks, the notion of a mechanistic interpretation itself is often ad-hoc. Inspired by the notion of abstract interpretation from the program analysis literature that aims to develop approximate semantics for programs, we give set of axioms that formally characterize a mechanistic interpretation as description that approximately captures the semantics of the neural network under analysis in a compositional manner. We demonstrate the applicability of these axioms for validating mechanistic interpretations on an existing, well- known interpretability study as well as on new case study involving Transformer-ban based model trained to solve the well-known 2-SAT problem.
Despite the broad interest in mechanistic interpretability, we observe that the notion of mechanistic interpretation has so far been primarily defined in ad-hoc manner. In this work, we propose a collection of axioms that characterize mechanistic interpretation.' Our view on mechanistic interpretability is inspired by the notion of abstract inter- pretation from the program analysis literature (Cousot Cousot, 1977; 1992) that seeks to approximate the semantics of programs in order to make their analysis computationally feasible. Similarly, our axioms are meant capture the property that the mechanistic interpretation should capture the semantics of the model. Further, our axioms also capture the intuition that such an approximation should respect the compositional structure of the neural network not only should the input-output behavior of the mechanistic interpretation be close as possible to the original model, but every step in the reverse-engineered algorithm should be as close as possible to the computation performed by the internal components of the model (i.e., neurons and layers). Our axioms clarify the responsibilities of an analyst; in addition to providing a mechanistic interpretation, an analyst also needs to present evidence to support the fact that the provided interpretation is valid, i.e., satisfies these axioms. Note that our axioms present general framework for validating mechanistic interpretations. Closest to work are recent papers by Geiger et al. (2021) and Chan et al. (2022) that seek to formalize the notion of mechanistic interpretability from a causal perspective. We believe that these formulations are complementary to our axioms.
1. Introduction
Neural networks are notoriously opaque. Mechanistic in- terpretability seeks to reverse-engineer the computation de- scribed by neural network in a human-interpretablee form. Typically, the resulting mechanistic interpretation takes the form of circuit (i.e., program) operating over features (i.e., proper-
symbols). The features refer to numan-interpredd ties of the input (such as edges, textures, or shapes for vision models and part-of-speech tags, named entities, or semantic relationships for language models) that the model represents internally in its representations spaces whereas the circuit refers chain of human-intenn numan-interpretable operations, encoded by the model in its layers, such that each operation processes and transforms the features (Millière & Buckner, 2024). While mechanistic interpretability has been used to analyze
We demonstrate the applicability of our axioms for validat- ing mechanistic interpretations via two case studies the existing, well-known analysis by Nanda et al. (2023a) of model with Transformer-be architecture (Vaswani et al., 2017) trained to solve modular addition, and a new analysis
University of Massoosin-Maadieee "Colorado State Univer- sity "Scale AI 'Carnegie Mellon University. Correspondence to: Nils Palumbo <npalumbo Stttumbo@wisc..du..... Ravi Mangal <ravi.mangal @ colostatc.cdu>.
'In the same sense that group axioms characterize the notion of abstract group in abstract algebra.
Proceedings of the 42nd International Conference Machine Learning. Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).
"Our implementation is available at attps:/ h//gtthu.. com/ nilspa lumbo/ / axi omat ie-vai-vllll vvalidat iddatiinn

---

Validating Mechanistic Interpretations: An Axiomatic Approach
of small Transformer-basel model trained by us to solve Boolean satisfiability problem. For the new case study, we choose Boolean satisfiabilityy challenging yet well- understood problem that serves to highlight new techniques and our axiomatic evaluation criteria for mechanistic inter- pretability. Further, there are many other problems in com- puter science that reduce to it, for example, graph reachabil- ity is reducible 2-SAT. To keep the analysis tractable, we focus on the 2-SAT problem with fixed number of clauses and variables; the problem can be solved in polynomial time (while the more general 3-SAT problem is NP-complete).
erations (Chughtai et al., 2023). Mechanistic interpretability has also been used to refer to analyses that only seek un- derstand specific aspects of the model behavior. Such analy- ses, often referred to as circuit analyses, isolate circuits, i.e., subgraphs of the neural network computational graph, that are responsible for the behavior of interest (Cammarata et al., 2020; Olsson et al., 2022: Wang et al., 2023; Lepori et al.,
2024; Wu et al., 2023b; Lieberum al., 2023; Conmy et al.,
2023). The circuits are validated by measuring the causal effect of ablating the circuit using techniques such activa- tion patching (Vig et al., 2020; Geiger et al., 2021; Heimer- sheim & Nanda, 2024) on a metric that measures the relevant model behavior. In either case, the standards for judging the validity of the mechanistic interpretations produced by such analyses are ad-hoo and do not take the compositional structure of the neural network into account. We axiomatize the standards for making such judgment in this paper.
To apply our axioms, we first need to extract a mechanistic interpretation of the model under analysis. Although such an interpretation is already known for the modular arithmetic model, we present new analysis for the 2-SAT model that is guided by our axioms. Through our analysis, we are able to reverse engineer the algorithm learned by the 2-SAT model-the model parses the formula into a clause-level representation in its initial layers and then uses the later lay- ers to evaluate the formula satisfiability via enumeration of different possible valuations of the Boolean variables. Since we only consider 2-SAT formulas with ten clauses and five variables, such an enumerative approach is computationally feasible and our model has the capacity to encode it. We use novel variants of attention pattern analysis to interpret the first Transformer block of the model. For the second (i.e., final) Transformer block, attention pattern analysis does not suffice and we use automated learning of functions (decision trees) to derive an interpretation. Finally, for both the case studies, we present evidence that the mechanistic interpreta- tions extracted for these models indeed satisfy our axioms.
Related to circuit analysis and the evaluation of mechanistic interpretations is emerging work on causal abstraction analy- sis (Geiger et al., 2021; 2024; Wu et al., 2023a;b; Chan et al., 2022) that extracts causal models to explain certain aspects of neural network behavior and uses techniques similar to activation patching for validating the causal abstractions.
The surveys by Millière & Buckner (2024), Mueller et al. (2024), and Räuker et al. (2023) are excellent resources for a broader and more detailed description of techniques for interpreting the internals of neural networks and the archi- tectural components which form the interpreted units. Ap- pendix A has a further discussion on internal interpretability techniques such prohing and attention pattern analysis.
3. Mechanistic Interpretation Axioms
2. Related Work
Neural networks can be seen as programs in a purely functional language, which we denote Xr, with basic operations corresponding to the commonly used neural net- work layers such as E'bed, Unembed, Lin (i.e., linear), Le,U, Aelf-Attention, Convolution, Residual, and so on. Since \T is purely functional, all these operations are side-effect free-they simply transform inputs into outputs. The syntax of xr is as follows (x E Var):
Work on interpreting neural networks can be divided between techniques that find input features with the largest effect on model behavior (Unput Interpretability) such as gradient-based (Simonyan et al., 2013; Sundararajan et al., 2017; Leino et al., 2018; Smilkov et al., 2017) and activation-based (Olah et al., 2017; Petsiuk et al., 2018; Fong & Vedaldi, 2017; Selvaraju et al., 2019; Wang et al., 2020) attributions, and those that interpret the internal reasoning performed by a model (Internal Interpretabiliry). We focus on the latter.
:== Embed(z) Unembed(a)) | Lin(x) (eLU(()) | Self-Attention(ss) Convolution(z) Residual(z, t) .... to
Mechanistic interpretability typically refers to analyses that seek to understand the model behavior completely, i.e., they seek to reverse engineer, in a human-understandable and hence simplified form, the full algorithm that the neural network learns. Such analyses have tended to focus on an- alyzing toy models trained for algorithmic tasks such as modular addition (Nanda et al., 2023a; Zhong et al., 2023), finding greatest common divisors (Charton, 2023), n-digit integer addition (Quirke& & Barez, 2024), and finite group op-
The decomposition of a model 1 E 'T is a list of programs in \T such that the composition of these programs is syntac- tically equivalent
For example, consider the program := Lin ReLU Lin(x). One possible decomposition of t is the list [Lin, Le,, Lin]. Given decomposition d, we use d[i] to refer to the 7th component of d, d[: as a
shorthand for dii -1] 1] dii 2] o...o d[1] and refer to it as a prefix of t of length i - 1 (with respect to d), and dii ]]
2

---

Validating Mechanistic Interpretations: An Axiomatic Approach
as the shorthand for d[len(d)) d[len(d) - 1] o... d[i] and referred to suffix t.
del: + i.e., the prefix of length i. The a functions are similar probes (Alain & Bengio, 2017) for extracting features from a model's internal activations. The y (or concretization) functions map in the opposite direction they map abstract features or symbols operated on by h to corresponding real-valued representations of those features in l's representation space. The a and y functions in our axioms are directly inspired by the abstraction and concretization operations from the abstract interpretation literature used to map values between the original semantics and the abstract semantics of program (Cousot & Cousot, 1977: 1992). We note that the a and 7 functions need to be individually instantiated every mechanistic interpretation.
The mechanistic interpre- tation of a neural network t E \T is a program in a different, purely functional language AH, that is human interpretable. The basic constructs of λи will tend to be more abstract than the ones supported by Ar; AØ might also be less expressive than AT to aid human- inteppettetrrttaility.. While the specific design of λи and the question of how to judge whether program is human-interpretable is domain-specific and subjective (and therefore difficult to formalize), we focus here on the question of how to judge whether a program h E Ny is a valid mechanistic interpretation of the neural network E \r under analysis.
Mechanistic Interpretation.
Axioms. We define the following axioms for a particular choice of e; in our analysis we say that an interpretation satis- fies axiom with when the statement of that axiom holds.
At the very least, the input-output behavior of h should be similar to t. Ideally, the input-output behaviors of the two programs should coincide on every input but this requirement is much too strong in practice. Assuming that the inputs are drawn from a distribution D, we formalize the weaker requirement that the outputs of the two programs should be equal with a high probability as an axiom. For these equality conditions be practically applicable, h must operate over discrete values. Also, the output type of t. must be discrete, in particular, we assume that an argmax or top-k operator has been applied to the logits. We additionally require that the behaviors of h and are equivalent at the level of individual components (obtained via suitably decomposing these programs) and that replac- ing component of t with the corresponding component of h has negligible effect on the neural network's s output. Definition 3.1 (Mechanistic Interpretation). Given a model E \r of type X + Y and a decomposition de of t, an c-accurate mechanistic interpretation of t, with respect to decomposition de and a distribution D over X, is program h λи with decomposition da such that (en(d)) len(da) ) and Axioms I, 2, 3, and 4 hold.
Axiom 1 bounds the probability that the abstract and the concrete representations computed by the same-length prefix of and t, respectively, do not coincide (after applying a functions to map between the representations). Put differently, the mechanistic interpretation prefixes do not introduce too much error.
Axiom (c-Prefix Equivalence). Vi E [len(d]].
Pr lo: o d 1](x) da(: f + 1] o)) 2 - am/
In contrast, Axiom 2 requires that none of the individual components of the mechanistic interpretation h introduce too much error. Axiom 2 does not imply Axiom since the errors introduced by each component of the mechanistic interpretation can compound in the worst case (Dziri et al., 2023).
Axiom (e-Component Equivalence). Vi E [[en(d]].
Pr Ja, de|: + [](x) = dn o a o de(: (x)) 2 1-6 z~D
Axioms and 4 are similar except that they consider equivalence of the output. Axiom 3 requires that replacing the prefixes of t with the corresponding prefixes of h (after applying appropriate a and functions to map between the representations) has limited effect on t's output. Axiom 4 requires the same when individual components of are replaced by corresponding components of h. Axiom 3 (c-Prefix Replaceability). vi e [len(d)]-
Note that the definition is parametric in decomposition de of as well as the input distribution D. In practice, we will often consider layer or block-wise decompositions of t.
Abstraction and Coneretization. The first four axioms use the notion of a and y functions which we describe here. The intuition is that a neural network t and a corresponding mechanistic interpretation h operate on different types of data representations. While operates over real-valued vectors, to aid interpretability, is intended to operate over human-interpretable features or symbols. Accordingly, a (or abstraction) functions map the real-valued activations (which we also refer to concrete representations) computed by t to the corresponding features or symbols (which we refer to abstract representations) that h operates over. Given a decomposition d, tf we use a to refer to the a function mapping concrete representations computed by
Pr [tx) = di + 1:] o dal: [] oo())) > 1 1 A~D
Axiom (c-Component Replaceability). Vi E [len(d]].
Pr (M()) deli + 1 :] o dali) o ai-1 o di (x)) 2 1-6 znD
We propose two additional axioms, namely, Axioms 5 and 6, that are more informal in nature and we do not consider
3

---

Validating Mechanistic Interpretations: An Axiomatic Approach
them for the analysis presented in this paper. These axioms presented goal for future work and described in Appendix B.
The map used by causal abstraction relate the two DAGs corresponds our abstraction function oz however, it does not have any analog of a concretization function y. Geiger et al. (2025) note that the inverse of abstraction may be used as a concretization operator; however, this may not be feasible in practice, as this choice necessitates the use of set semantics for evaluation of the concrete model when the abstraction operator fails to be invertible. Under the causal abstraction framework, valid interpretation is defined by comparing the effects of interventions on the concrete model with corresponding interventions on the abstract model; in contrast, our notion of a valid interpretation may be viewed as one which is invariant up to a class of interventions, characterized by our axioms, which interleave the concrete and abstract models. While causal abstraction a very general framework for the validation of mechanistic interpretations, in practice, it uses the specific metric of interchange intervention accuracy (Geiger et al., 2022) to validate interpretations and this metric fails to directly evaluate the equivalence of internal representations.
Checking the Axioms. The proposed axioms can be checked statistically. Given a test dataset (which need not be labeled), we can estimate the error rate for each axiom by computing the proportion of test inputs which violate the equality condition specified by the axiom. The number of violations is distributed binomially- the parameter p of this binomial distribution is equal to e. Hence, any method for deriving confidence intervals for the parameter of a binomial distribution can be used to derive confidence intervals for our estimate of e; we use the Clopper-Pearson method (Clopper & Pearson, 1934) in our experiments. Validating the axioms is thus cheap and feasible in practice. These axioms represent minimal set that we believe are necessary albeit may not be sufficient in all cases for characterizing mechanistic interpretation. In future work, we plan to address this by considering analysis of models trained for other problems.
On the other hand, the map defined by causal scrubbing can be seen as an form of concretization, but it does not define an abstraction function. While both these approaches compare the outputs of the concrete and abstract models similar to our Axioms 3 and 4, they tend to omit direct evaluation of the equivalence of internal representations, as in our Axioms and 2. This is potentially problematic since there is no direct validation that the intermediate steps of the mechanistic interpretation correspond to the intermediate steps of the neural network (Scheurer et al., 2023). Further, as causal abstraction and scrubbing lack concretization and abstraction operators respectively, even Axioms 3 and 4 cannot be expressed directly in these frameworks.
Relationship to Existing Approaches. The evaluation of Nanda et al. (2023a)'s seminal paper on mechanistically interpreting the complete behavior exemplifies typical ap- proaches to evaluating a mechanistic interpretation (Zhong et al., 2023; Quirke& & Barez, 2024; Chughtai et al., 2023). The first three pieces of evidence (presented in Sections 4.1, 4.2, and 4.3 in their paper) resemble our Axiom that compares each individual component of the mechanistic interpretation with the corresponding component of the model. However, as there does not exist direct analogue of abstraction, this analysis is primarily observational.
The evidence they present in Section 4.4 of their paper is similar to our Axiom 4 that checks the effect on the output of the model when individual model components are replaced by the corresponding components from the mechanistic interpretation. Notably, they do not present the evidence required by our Axioms 1 and 3. This amounts to not considering the compositional structure of the model and, therefore, the possible compounding of error intro- duced by each component of the mechanistic interpretation; we discuss this further at the end of this section.
Compositionality. While it may appear that our axioms for compositional evaluation (Axioms and 3) follow from their componentwise counterparts (Axioms 2 and 4 respec- tively), this is not the case; for example, while bounds of the form of Axiom I can be derived from Axiom 2, these hold only with far weaker when the number of components is sufficiently high, the derived bounds entirely cease to be meaningful. More details are given in Appendix E; Appendix F includes empirical evidence demonstrating the pitfalls of omitting the compositional axioms.
Causal abstraction (Geiger et al., 2021; 2022; 2024: 2025) and causal scrubbing (Chan et al., 2022) are key existing attempts to formalize the notion of mechanistic interpre- tation. Both of these formulate the abstract and concrete models as directed acyclic graphs (DAG) with a map that relates the two DAGs, While it may seem that, compared to our approach, the DAG formulation is more generic since it admits parallel composition of components in addition to sequential composition, this is not fundamental, in particular, Appendix B.1 discusses how to represent arbitrary computational graphs in our framework.
4. Case Study: 2-SAT
4.1. Data and Model Details
The 2-SAT Problem. Given a Boolean formula, i.c., a conjunction of disjunctive clauses over exactly two literals, the 2-SAT problem is to determine whether there is an as- signment to the formula's variables that makes the formula evaluate to True; the formula is said to be satisfiable, or SAT.
4

---

Validating Mechanistic Interpretations: An Axiomatic Approach
For example, the formula (2 is satisfiable, with a satisfying assignment 45 = Tr = False, 22 False (written also as zo, (2)) If a formula has no sat- isfying assignment, it is said to be unsatisfiable, or UNSAT.
4.2.1. FIRST BLOCK AS PARSER
To reverse-engineer the first block's behavior, we start by examining the attention patterns, i.., the attention scores (by default, post-softmax unless stated otherwise) calculated by both blocks on given input formulas. Figure I shows the attention scores on a formula from our test set. We clearly see patterns emerge- most tokens in the first block attend heavily to the first token, while tokens in position 4i + 2, 0 S < 10, that we refer to as the second literal positions, primarily attend to themselves and the previous token, i..., to the two literals in each clause." Attention from the readout token is nearly uniform. This suggests that the first block parses each clause, storing the parsed clause information in the token representations output by the first block in the second literal positions.
Dataset. We construct a dataset of randomly generated 2-SAT formulas with ten clauses and up to five vari- ables, eliminating syntactic duplicates. We use a solver (Z3 (De Moura & Bjørner, 2008)) to check satisfiability for each formula. We built a balanced dataset of 10 SAT and 10t UNSAT instances; we used 60% (also balanced) for training, and the rest for testing. For model analysis, we construct a separate dataset with 10 SAT and 109 UNSAT instances split as before in to train and test sets.
Each formula is represented as string. For example, (arg (xz) V-r22) is represented as (( -22): s" where indicates that the formula is SAT (u would indicate UNSAT). We tokenize these formulas by considering each Ti its negation -T;, and each of the symbols in the set {G (.),:,& s, u as a separate token. The colon token (+:) is the final token in the input and we consider the next token predicted by the model as the output; hence, we refer to this token as the readout token and refer its position as the readout position.
In the second block, the attentions heavily focus on these second literal positions, suggesting that the model uses the parsed clause information contained in these representations to classify. This allows us to restrict our analysis of the first block to the second literal positions and the readout position. To further validate this decision, we compute the average attention score from each head on each token across the test set (see Figure 6 in Appendix D.1). The results show strong periodicity with period 4, following the pattern seen in Figure 1.
Model Architecture and Training. We use a two-layer ReLU decoder-only Transformer with token embeddings of dimension d= = 128, learned positional embeddings, one attention head of dimension d the first layer, four attention heads of dimension d/4 = 32 in the second, and n = 512 hidden units in the MIP (multi-layer perceptron). We use full-batch gradient descent with the AdamW optimizer, setting the learning rate 7 = 0.001 and weight decay parameter A = 1. We perform extensive epochs of training (1000 epochs), recognizing the combinatorial nature of SAT problems and the need for thorough exploration of the solution space. We obtained a model with 99.76% accuracy on test data. All our experiments were run on an NVIDIA A100 GPU.
We perform additional distributional and worst-case analysis of attention patterns (described in Appendix D.I) and these analyses confirm the parsing hypothesis for the first block.
Interpretation. Based on our analysis of the attention patterns for the first block, we hypothesize that is parsing the input sequence of tokens into list of clauses (Listing 5 in Appendix D.1). The behavior of attention is enough to form this hypothesis, as the sparse attention patterns show that information primarily flows from tokens in a clause to the token in the second literal position in the same clause; hence we can view the action of the first block as computing representation for each clause in the input. In this sense, analyzing the MLP in the first block is not necessary to identify the semantic function of the first block.
4.2. Mechanistic Interpretability Analysis
The network can be naturally decomposed into its blocks and we describe the analysis of each in the following two sections. We note that our axioms help guide our analysis, particularly for the second block. As our goal is to understand the algorithm used by the model to determine satisfiability, we refrain from analyzing behavior which does not affect the final prediction. Thus, we focus on the model's prediction at the readout position. Figure 5 in Appendix D describes our decomposition of the model into the concrete components de [i].
We show in Sec 4.2.3 that we can successfully validate this hypothesis using our axioms. As we ll see in the analysis of the second block in Sec 4.2.2, we cannot always count on self-explanatory attention patterns; for the second block, we will be forced analyze the much harder-to-interpre ML.P
4.2.2. SECOND BLOCK AS EVALUATOR
From the first block's analysis, we know that the inputs to the second block can be described, in an abstract sense, as
*Formulas are of the form, (zoZ1) ((2))))) 8, so token posi- tions 1 and 4i + correspond to the literals of the 2th clause.
5

---

Validating Mechanistic Interpretations: An Axiomatic Approach
imeetionn
Heat Attetio
Statweriss Stares
Bork AltertinSoons
Foltbor
Ication
Attention scores for all heads the first sample of the test set, the formula (-wo-ar ( (2) =23) (42 (42- (=))(==o0==())))))
Figure 1:
The x-axis represents the source (key) positions and the y-axis represents the destination (query) positions for the attention mechanism.
144
Nauno Sepu Sweftlen
+6:d0n Recuoon
Figure 2: Output coefficients of hidden neurons computed via the composition of the output layer of the MLP and the unembedding matrix projected to the SAT logit.
Figure 3: Average activation of neuron 10 from SAT formulas, UNSAT formulas, and formulas satisfiable with particular assignments to the variables.
ding operation are both linear, so their composition is again linear. From this perspective, then, the MLP's effect on the classification is fully captured by weighted sum of the post- activation outputs of the hidden neurons. We refer to these weights as neuron output coefficients for the SAT logit. This is the sense in which observe sparsity; see this clearly, see Figure 2. There are only 35 neurons which have non- negligible absolute coefficient (> 10-9); one of these has significantly lower coefficient than the others along with con- sistently low activation values on the samples in our analysis training set resulting in a negligible effect on the SAT logit. Hence, we restrict our analysis to the remaining 34 neurons.
the list of clauses in the formula. As the model's output is label SAT or UNSAT, the interpretation of the second block a function that checks satisfiability given a list clauses. This means that the core logic of the model is encoded primarily in the second block.
Identifying the Key Pathway. We observe that the unembedding vector for UNSAT is nearly the negative of that of SAT (in particular, ||WSAT + W-INSAT]|| < 10-5 and their cosine similarity is 11 up to floating point precision), and hence, their logits are likewise negatives of each other. Also, for all formulas in the dataset, either the SAT or the UNSAT logit output at the readout position is much larger than the logits for all other tokens. Hence, the effect of components on classification can be fully described by their effects on the SAT logit. Furthermore, we observe that the effect of the attention mechanism on the SAT logit is consistently suppressive and varies little between samples. Hence, the core pathway necessary to identify SAT flows through the MLP the readout position. Unlike the first block, we cannot identify an interpretation directly from the behavior of attention. See Appendix D.2 for more details.
Evaluation in the Hidden Neurons. Note furthermore that all the non-negligible coefficients are positive; hence, the effect of each of the relevant neurons is purely to promote SAT. This suggests that the neurons may each recognize some subset of SAT formulas instead of recognizing charac- teristics of UNSAT formulas. Figure 3 shows that the typical activation of one such neuron on SAT formulas is highly dependent on the assignment the variables which satisfies the formula. This suggests that the MLP may implement very simple algorithm: that of exhaustive evaluation. In par- ticular, if we treat the formula á as a Boolean function fø. & is SAT if and only fa is not the constant False function. Hence, we can identify SAT formulas by a brute-fore tech- nique which computes the truth table of the corresponding
Sparsity in the MLP Hidden Layer. We begin our analysis of the MLP by noting that, somewhat surprisingly, it exhibits sparsity in the hidden neurons. We conclude this by first ob- serving that the second layer of the ML. and the unembed-
6

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Boolean functions and checks whether any entry is True.
combination of assignments considered for computing each Boolean output (see Tables 2 and 3 of Appendix G for two different neuron interpretations). We evaluated the completeness of the neuron interpretations, i.e., their ability to correctly evaluate all 2-SAT formulas, using Z3 (De Moura & Bjørner. 2008). The rest of the model, namely, the MLP's output layer and the unembedding layer, performs a logical OR over the Booleans output by the previous component and outputs True if the formula is SAT. Listing 6 and 7 in Appendix D.2 describe the mechanistic interpretation of the second block and the entire model, respectively, using Python syntax.
We'll see that this is indeed the case; hence, we will refer to these neurons as evaluating neurons. However, the behavior of the neurons is somewhat more complex than the most natural form, in which each neuron specializes in identifying formulas satisfiable with one of the 32 possible assignments. In particular, as seen in Figure 3, some neurons are affected by multiple assignments to the variables. The notation o!...] means that the corresponding Boolean function fa evaluates to True when the variables are assigned the shown truth values. For instance, [[TTFF]] indicates that formula @ is satisfiable with 21, 24 set to True and 22, 23 set to False
A natural hypothesis is then that each of the evaluating neurons evaluates ó on some set of assignments, with some overlap between neurons; we refer to such interpretations of neuron activation behavior as disjunction-only since they take the form h : o(...] h V h. However, we observe that the actual behavior is less intuitive: in some cases, satisfiability with an assignment can decrease activation on some evaluating neurons. Hence, we also consider more general Boolean expressions in terms of the $[...''s as neuron interpretations. We find that our axiomatic analysis provides clear way to quantify the trade-off between interpretability and fidelity of the different interpretations.
4.2.3. CHECKING THE AXIOMS
First Block, Since the input to the neural model is a se- quence of token IDs, Og here is the function that translates token IDs into tokens. To derive on and 71, we first compute canonical representation for each possible clause v/.
Drawing from the observation that the output of attention on the second token of each clause is largely a function of the two tokens in the clause alone (ignoring all other past to- kens), we compute the representation output by block 1 for clause & in each position i by masking attention such that it is only applied to the left and right literals in the clause. The canonical representation for va is the average of the rep- resentations derived for each position i. a1 [Tensox] + [Literal, Li teral)]. where Li Literal is the type con- sisting of the x; and their negations, maps the list of rep- resentations output by the first block to a list of clauses by comparing (via cosine similarity) the representations in the second positions 4i + 2 with the canonical clause representations and returning the clauses with the most- similar representations. ?1 [Literal, Li teral)] + [Tensor] maps a list of clauses to a list of canonical clause representations. For positions other than 4i + 2, 7/1 returns the mean representation in that position across the training set. For position 4i + 2, returns the canonical representa- tion for the clause in position i. See Listing 1 and Listing 3 of Appendix D for pseudocode for 0₁ and 7/1, respectively.
As decision trees can represent arbitrary Boolean functions, we use standard decision tree learning to learn the more general interpretations of neurons; specifically, we learn classifiers trained predict whether a neuron's 's activation is above below a threshold (0.5 in our experiments) given all the features (!...] for a formula o. Deriving the simpler disjunction-only interpretation is easier; we do so by identifying the assignments a such that the empirical mean, calculated over our analysis training set, of a neuron's 's post-activation value on formulas satisfied by a is above the threshold. For instance, in Figure 3, these are the assignments that cause the post-activation score to be above the threshold.
Finally, we observe that the output coefficients of the eval- uating neurons for the SAT logit are consistently high (> 2.9 in all cases). which means that a high activation on any individual evaluating neuron forces prediction of SAT; see Appendix D.2 for more details. In this sense, the action of MLP's output layer and the unembedding layer is conceptu- ally close to logical OR operation. We now have enough in- formation to describe our interpretation of the second block.
Prefix Equivalence. For each clause position i, a1 outputs a clause & = IVr. r. where / and are literals, and, as such, we consider the clauses r V and ( r equal. With this notion of equality, we obtain an c of approximately 0.0000374 (corresponding to perfect matching on the test set) between the abstract states output by on de [1] and dx[1] og. When we enforce order consistency, we obtain much worse e of 0.849; however, as the abstract state is order independent and the second block's behavior does not vary significantly with the order of variables in a clause, an order-dependent notion of equality is not necessary here.
Interpretation. Based on our analysis, we decompose the interpretation of the second block into two components. We hypothesize that the second block up to the MLP's hidden layer evaluates the input formula with different assignments and outputs the results of these evaluations a list of Booleans. The neuron interpretations describe the precise
*We always report e in terms of the upper bound of a one-sided 95% (lopper-Pearson confidence interval.
7

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Component Equivalence. As this is the first component, component equivalence and prefix equivalence are identical, hence the results are the same as above.
components has minimal effect on the model's s output be- havior: specifically, we get 0.0128 for the decision tree interpretations, and R 0.00290 for the disjunction-only interpretations. If we drop the amplification step discussed above for 72, we significantly affect the model's predictions: we get an e of approximately 0.249 (i.e. over 24% of sam- ples are affected) for the decision tree interpretations and ap- proximately 0.135 for the disjunction-only interpretations.
Prefix Replaceability. We obtain z 0.0418, i.e. substi- tuting the first component of the model with "n d, [1] o Oo affects the final output 4.2% of the time. In particular, this quantifies the effect of replacing the actual first-block representation of ':' with its mean value across the dataset and the effect of ignoring attention to previous clauses when computing the canonical clause representations.
Component Replaceability.
As above, we obtain R 0.0128 for the decision tree interpretations, and R2 0.00290 for the disjunction-only interpretations.
Component Replaceability. As this is the first component, component and prefix replaceability are identical, hence the results are the same as above.
Output Layer of Second Block, For our analysis, we consider the model to be composed with a function which returns True if and only if the top logit at the readout position SAT. The output type of this composed model and the mechanistic interpretation are identical; hence og and "/3 are both the identity function.
Hidden Layer of Second Block. The output of the second concrete component is pair consisting of the residual from attention and the post-activation outputs of the hidden neurons; 02 (Tensor, Tensor) + [bool] maps these to Boolean vector representing whether or not sufficiently high activation (> 0.5) has occurred at each of the 34 evaluating neurons. ?/2 [boo1] - (Tensor, Tensor) simply returns a constant value for the residual (the mean on the analysis training set); the MLP's hidden neurons have zero activation except for the evaluating neurons with True values in the corresponding position in the abstract state vec- tor, which we assign an arbitrary large activation (2 in our experiments). Note that this is higher than the threshold for a2; we observe that this amplification is necessary for a re- liable interpretation; see below. See Listing and Listing 4 of Appendix D for pseudocode for 22 and 72, respectively.
Prefix Equivalence. Since prefix equivalence incorporates the mechanistic interpretation of the previous component, we need to consider both the decision tree and the disjunction-only version of the previous component. We obtain very close matching in both cases, with 0.0128 for the decision tree interpretations and x 0.00290 for the disjunction-only interpretations.
Component Equivalence. We obtain a very close match with E ~ 0.00433.
Prefix Replaceability. As this is the final component of the network and 0g and 73 are the identity, this is the same as prefix equivalence.
Prefix Equivalence. We obtain ~ 0.182 when using the decision tree neuron interpretations, compared with approximately 0.309 for the disjunction-only interpretations in which our neuron models activate on formulas satisfiable with any of a set of assignments. This means that the disjunction-only interpretations are much worse predict- ing the intermediate state of the model. This is the only place where this simplifying choice has a cost with respect to the validity of the mechanistic interpretation; aside from component equivalence below, the disjunction-only interpretations differ little from the decision trees in all other respects. This illustrates the need to check the axiomatic properties at component level for the model under analysis.
Component Replaceability. equivalence for the reason above.
Same as component
5. Case Study: Modular Addition
Nanda et al. (2023a) train a model with single Transformer block to perform modular addition. The model is given input of the form a b and returns a + b mod P at the '=' token where P is fixed to be 113. They claim the following mechanistic interpretation of the concrete model (see Listing 8 in Appendix H for the pseudocode for the abstract components):
Component Equivalence. We again obtain = 0.182 for the decision tree interpretations and 0.309 for the disjunction-only interpretations. The similarity in the values for prefix and component equivalence is because the interpretation of the first component perfectly matches the behavior of neural network, up to literal order, on the analysis test set.
1. Encoding of inputs: The embedding matrix represents a and b as sin(waa), sin(wyb). cos(wwa), and cos(web) for key frequencies wa- = (2kr)/ / P for k E {14, 35, 41, 42, 52).
2. Computation of sum-of-angles identities:
The attention and MLP input layer compute cos(wx(a++)))) and sin(wx (a + b)) using trigonometric identities.
3. Difference-of-angles identities and argmax: The MLP output layer and the unembedding matrix
Prefix Replaceability. In both cases, substituting the first two concrete components with the first two abstract
8

---

Validating Mechanistic Interpretations: An Axiomatic Approach
computes cos(w; (a b - c)) for each key frequency and for each E 2p, adds the computed cosines, and then selects the maximizing the sum, which occurs at c" aa a + b mod P.
dynamies of models but also help in the development of techniques for automated mechanistic interpretability analyses by serving as a useful evaluation metric.
As all abstract components but the last one output con- tinuous values, we must discretize the output of each abstract component for Axioms 1 and 2 to be meaningful. For the first component, we apply a simple discretization of rounding up three decimal points; for the second component, we define an equivalence class which treats abstract states equivalent when their downstream effects on both the abstract and concrete models are identical. Dis- cretizations of this form are quite general: an equivalence class up to the next discrete-valued intermediate value is expressible for any abstract model with discrete-valued output. Axioms 3 and 4 ensure that any diseretization does not impact end-to-end behavior. The a and y functions for each component are linear maps learned from data. See Appendix H for more details.
Impact Statement
We believe that work on mechanistic interpretability in particular and on internal interpretability of neural networks in general is essential for increasing trust in neural networks and mitigating their risks. In this context, the work pre- sented in this paper is of a foundational nature and advances the interpretability research agenda by clarifying the notion of a mechanistic interpretation. Therefore, we do not foresee direct path from our work to negative societal impacts.
Acknowledgments
Nils Palumbo and Somesh Jha partially supported by DARPA under agreement number 885000, NSF CCF-FMITT-1836978 and ONR N00014-21-1-24992.
We apply our approach to this model and confirm that the Nanda et al. (2023a)'s mechanistic interpretation satisfies our axioms, noting that, in their paper, while Nanda al. (2023a) provide evidence similar to Axioms 2 and 4 in support of the validity of their interpretation, they do not provide any evidence as required by our Axioms and 3.
References
Abnar, S. and Zuidema, W. Quantifying attention flow in transformers. In Jurafsky, D., Chai, J., Schluter, N., and Tetreault, J. (eds.), Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, pp. 4190-41977 Online, July 2020. Association for Computational Linguistics. doi: 10. 10.18653/112222.ac--mmiii main.33.. URL https: //aclanthology org org wttp///2...////// acl mallmmain... 385.
In particular, with the above discretization we obtain a very strong e of 0.000335, which corresponds to perfect matching. However, it is important to note that results with simple discretizations indicate that the model's behavior is not fully captured. In particular, we obtain Axioms and 2 for the second component when, instead, we discretize by rounding to a single decimal place. There are important tradeoffs to the application of this type of discretization: while enables the analyst to eliminate variation which has no impact on the downstream behavior of the model, it also limits the ability of Axioms 1 and 2 to validate the internal behavior.
of from
Alain, G. and Bengio, Y. Understanding intermediate layers using linear classifier probes, 2017. URL https:
net / wttp:/oormmddddd///1raa..a
Allen-Zhu, Z. and Li, Y. Physics of language models: Part 1, context-free grammar, arXiv preprint arXiv:2305. 136733 2023.
6. Conclusion
Bastings, J. and Filippova, K. The elephant in the inter- pretability room: Why use attention as explanation when we have saliency methods? In Proceedings of the Third BlackboxNLP Workshop on Analyzing and Interpreting Neural Networks for NLP, pp. 149-155, 2020.
We presented a set of axioms that characterize a mechanistic interpretation and enable judgment of the interpreta- tion's validity with respect to the neural network under analysis. Using the axioms as guide, we analyzed Transformer-baset model trained to solve the 2-SAT problem. We applied our axioms to validate the mechanistic interpretation of this 2-SAT model and a model trained to solve the modular addition task. Our axioms provide an automated and quantitative way of evaluating the quality of mechanistic interpretation (via the values). Not only the e's serve as useful progress measures (in the sense of Nanda et al. (2023a)) to understand the training
Belinkov, Y. Probing classifiers: Promises, shortcomings, and advances. Computational Linguistics, 48(1): 207-219, March 2022. doi: 10.1162/coli a 00422.. URL https: http:s//aclaattholoooo wrg/ cl-1.7.
Belrose, N., Furman, Z., Smith, L., Halawi, D., Ostrovsky, I., McKinney, L., Biderman, S., and Steinhardt, J. Eliciting latent predictions from transformers with the tuned lens. arXiv preprint arXiv:2303.00 08/ 12, 2023.

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Bibal, A., Cardon, R., Alfter, D., Wilkens, R., Wang. X., François, T., and Watrin, P. Is attention explanation? introduction to the debate. In Muresan, S., Nakov, P., and Villavicencio, A. (eds.), Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 3889-3900, Dublin, Ireland, May 2022. Association for Computational Linguistics. doi: 10.18653/ 269. URL https: //aclanthology: wwwp://hww..ooo..ooo/0/22....... wwtpo/ggg/22...
Cousot, P. and Cousot, R. Abstract interpretation frame- works. Journal of logic and computation, 2(4):511-547, 1992.
Crabbé, and van der Schaar, M. Concept activation regions: generalized framework for concept-based ex- planations. Advances in Neural Information Processing Systems, 35:2590-2607 2022.
acl lon...n......
De Moura, L. and Bjørner, N. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pp- 337-340. Springer, 2008
Burns, C., Ye, H., Klein, D., and Steinhardt, J. Discov- ering latent knowledge in language models without supervision. In The Eleventh International Conference on Learning Representations, 2023. URL https: //openreview http:eiiwwwweeeeeeeeee www.eeeffouur forum? -d-oommmi----KKuyohhhh..
Dziri, N., Lu, X., Sclar, M., Li, X. L., Jiang, L., Lin, B. Y., Welleck, S., West, P., Bhagavatula, C., Bras, R. L., Hwang, J. D., Sanyal, S., Ren, X., Ettinger, A., Harchaoui, Z. and Choi, Y. Faith and fate: Limits of transformers on compositionality. In Thirty-sevntth Conference on Neu- ral Information Processing Systems, 2023. URL https: / / //ppneevieew net/ for um ? (eteerdddFkkkkryree
Cammarata, N., Carter, S., Goh, G., Olah, C., Petrov, M., Schubert, L., Voss, C., Egan, B., and Lim, S. K. Thread: Circuits. Distill, 2020. doi: 1/.23995/disttlll000224,
http:://distill.uuu/20//iiiiii
Chan, L., Garriga-Alonso, A., Goldwosky-Dill. N., Greenblatt, R., Nitishinskaya, J., Radhakrishnan, A., Shlegeris, B., and Thomas, N. Causal scrubbing, method for rigorously testing interpretability hypotheses. Al Aligument Forum, 2022.
Ebrahimi, J., Gelda, D., and Zhang, W. How can self-attention networks recognize dyck-n languages? In Findings of the Association for Computational Linguistics: EMNLP 2020. pp. 4301 0306, 2020.
Charton, F. Can transformers learn the greatest common divisor? arXiv preprint MxXiv:230.115944 2023.
Elhage, N., Nanda, N., Olsson, C., Henighan, T., Joseph, N., Mann, B., Askell, A., Bai, Y., Chen, A., Conerly, T., DasSarma, N., Drain, D., Ganguli, D., Hatfield- Dodds, Z., Hernandez, D., Jones, A., Kernion, J., Lovitt, L., Ndousse, K., Amodei, D., Brown, T., Clark, J.. Kaplan, J., McCandlish, S., and Olah, C. A mathematical framework for transformer circuits. Transformer Circuits Thread, 2021. https:/transformer httpii/spp//222///aaooooo.//
Chefer, H., Gur, S., and Wolf, I.. Transformer interpretabil- ity beyond attention visualization. In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR), pp. 782-791, June 2021.
Chughtai, B., Chan, L., and Nanda, N. A toy model of universality: reverse engineering how networks learn group operations. ICML'23. JMLR.org. 2023.
Fong, R. C. and Vedaldi, A. Interpretable explanations of black boxes by meaningful perturbation. 2017 IEEE International Conference Computer Vision (ICCV), 2017.
Clopper, C. J. and Pearson, E. S. The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika, 26(4):404-413, 1934. ISSN 00063444. URL http://wwer jat.ssstooor. /ttp://ttt..rttttttee/////3.09.
pp.
Geiger, A., Lu, H., Icard, T., and Potts, C. Causal abstractions of neural networks. Advances in Neural Information Processing Systems, 34:9574-9586, 2021.
Conmy, A., Mavor-Parker, A. N., Lynch, A., Heimer- sheim, S., and Garriga-Alonso, A. Towards automated circuit discovery for mechanistic interpretability. In Thirty-seventh Conference on Neural Informa- tion Processing Systems, 2023. URL https: // //oppeeeview.eeee net htwprr/vwweeeeee//orriiieee--eee
Geiger, A., Wu, Z., Lu, H., Rozner, J., Kreiss, E., Icard, T., Goodman, N., and Potts, Inducing causal structure for interpretable neural networks. In Chaudhuri, K., Jegelka, S., Song, L., Szepesvari, C., Niu, G., and Sabato, S. (eds.), Proceedings of the 39th International Conference on Machine Learning, volume 162 of Proceedings of Machine Learning Research, pp. 7324-7338. PMLR, 17-23 Jul 2022. URL https: httpas//prrceeee /ttp///pppcecn..../////////////p mir s.r.press/vl22. 62,
Cousot, P. and Cousot, R. Abstract interpretation: unified lattice model for static analysis of programs by construc- tion or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAY symposium on Principles of programming languages, pp. 238-252, 1977.
html.
10

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Geiger, A., Wu, Z., Pout, C.,, Ieard, T., and Goodman, N. Finding alignments between interpretable causal variables and distributed neural representations. In Locatello, F. and Didelez, V. (eds.), Proceedings of the Third Conference on Causal Learning and Reasoning, volume 236 of Proceedings of Machine Learning Research, pp. 160-187, PMLR, 01-03 Apr 2024. URL https: / /ttp:///ccccceeegs.cceo mlr press/v222 /v366/ geiger24a html.
Kim, B., Wattenberg, M., Gilmer, J., Cai, C.,, Wexler, J., Viegas, E,, et al. Interpretability beyond feature attribution: Quantitative testing with concept activation vectors (tcav). In International conference on machine learning, pp. 2668-2677. PMLR, 2018.
Leino, K. Sen, S., Datta, A., Fredrikson, M.. and Li, L. Influence-directed explanations for deep convolutional networks. In 2018 IEEE International Test Conference (ITC), pp. 1-8. IEEE, 2018.
Geiger, A., lbeling, D., Zur, A., Chaudhary, M., Chauhan, S., Huang, J., Arora, A., Wu, Z.., Goodman, N., Potts, C., and Icard, T. Causal abstraction: foundation for mechanistic interpretabilityy, 2025. URL https: /awxiv.vvvv.///a// wwtp:/vvoorr.ooooooooo abs//////////// 2301 04709.
Lepori, M. A., Serre, T., and Pavlick, E. Un- covering intermediate variables in transform- ers using circuit probing. In First Conference Language Modeling, 2024. URL https: / opoorpeeieeeee ew. net/ forum? d=gUNey LNxx.
theoretical
Gurnee, w., Nanda, N., Pauly, M., Harvey, K., Troitskii, D., and Bertsimas, D. Finding neu- rons in a haystack: Case studies with sparse probing. Transactions on Machine Learning Re- search, 2023. ISSN 8835-8856. URL https:
Li, K., Hopkins, A. K., Bau, D., Viégas, F., Pfister, H., and Wattenberg, M. Emergent world representations: Exploring sequence model trained on synthetic task. In The Eleventh International Conference Learning Representations, 2023, URL https:
//openreview wwweeeewwwwwweeeeeeeeeee htte:/oorummii=dy11eeee
/ //openreview,
Hao, Y., Dong, L., Wei, F., and Xu, K. Self-attention attri- bution: Interpreting information interactions inside trans- former. In Proceedings of the AAAI Conference on Ar- rificial Intelligence, volume 35, pp. 12963-12971, 2021.
Lieberum, T., Rahtz, M., Kramár, J., Irving, G., Shah, R., and Mikulik, V. Does circuit analysis interpretability scale? evidence from multiple choice capabilities in chinchilla. arXiv preprint arXiv: arXiv:2307.09458. 2023.
Heimersheim, S. and Nanda, N. How to use and interpret activation patching. arXiv preprint arXiv:2404. 1..122444...555,, 2024.
Lindner, D., Kramar, J., Farquhar, S., Rahtz, M., MeGrath, T., and Mikulik, V. Tracr: Compiled transformers as a laboratory for interpretability. In Oh, A., Naumann, T.. Globerson, A., Saenko, K., Hardt, M., and Levine, S. (eds.), Advances in Neural Information Processing Sys- tems, volume 36, pp. 37876-37899, Curran Associates, Inc., 2023.
Hewitt, J. and Liang, P. Designing and interpreting probes with control tasks. In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing (EMNLP-IJCNE) pp. 7733-2743, 2019.
Liu, B., Ash, J. T.,, Goel, S., Krishnamurthy, A., and Zhang, C. Transformers learn shortcuts to au- tomata. In The Eleventh International Conference Learning Representationss 2023. URL https: / //openevveew net
Huben, R., Cunningham, H., Smith, L. R., Ewart, A., and Sharkey, I.. Sparse autoencoders find highly interpretable features in language mod- els. In The Twelfth International Conference on Learning Representations, 2024. URL https:
Lu, K., Wang. Z., Mardziel, P., and Datta, Influence patterns for explaining information flow in bert. Ad- vances in Neural Information Processing Systems, 34: 4461-4474, 2021.
//oppeeeview.eeee..ee wet.e/nnee//oorr 1d==1d=776 6bwRSseK..
Jain, S. and Wallace, B. C. Attention not Explanation. In Burstein, J.. Doran, C., and Solorio, T. (eds.), Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Human Language Technologies, Volume (Long and Short Papers), pp. 3543-3556, Minneapolis, Minnesota, June 2019. Association for Computational Linguistics. doi: 10. 10.18655/W1NN11-133577 URL www.aannwwwooooooooooooooeaeeee. wwt//N1-1//111111
Millière, R. and Buckner, C. A philosophical introduction to language models part ii: The way forward, 2024.
Mueller, A., Brinkmann, J., Li, M., Marks, S., Pal, K.,
Linguistics:
Prakash, N., Rager, C., Sankaranarayanan A., Sharma, A. S., Sun, J., Todd, E., Bau, D., and Belinkov, Y. The quest for the right mediator: A history, survey, and theoretical grounding of causal interpretability, 2024. URL hwtps:ttp//.o.....t.. /ttp/v..vvv/////////////////ae http:s///xxxxxxxxx/aa//e http://awxwv..oaaa//////ee////// 01441.8..111. 01416.

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Nanda, N., Chan, L.,, Lieberum, T., Smith, J., and Steinhardt, J. Progress measures for grokking via mechanistic interpretability, In The Eleventh International Conference on Learning Representations, 2023a. URL https: //openreview .eeee/.weeeeeeeeeeeeee.eee.eeeee forum? i d= 9XFSbDPmdW.
Scheurer, J., Phil3, tony, Thibodeau, J., and Lindner, D. Practical pitfalls of causal serubbing. Al Alignment Forum, 2023.
Selvaraju. R. R., Cogswell, M., Das, A., Vedantam, R., Parikh, D., and Batra, D. Grad-cam: Visual explanations from deep networks via gradient-based localization. International Journal of Computer Vision, 128(2)3336-359 Oct 2019. ISSN 1573-1405. doi: 10. 10.100776112266-01140022288 7. URL http: /tttp::/dxxco/ htt.:/..107//11111 019 01228-7.
Nanda, N., Lee, A., and Wattenberg, M. Emergent linear representations in world models of self-supervised se- quence models. In Proceedings of the 6th BlackboxNI.P Workshop: Analyzing and Interpreting Neural Networks for NLP, pp. 16-30, 2023b.
Simonyan, K., Vedaldi, A., and Zisserman, A. Deep inside convolutional networks: Visualising image classification models and saliency maps. 2013.
Olah, C., Schubert, L., and Mordvintsev, A. Feature visualization. Distill, 2017. URL https: //dds//disssi.i///
Smilkov, D., Thorat, N., Kim, B., Viégas, F,, and Watten- berg, M. Smoothgrad: removing noise by adding noise, 2017.
Olsson, C., Elhage, N., Nanda, N., Joseph, N., DasSarma, N., Henighan, T., Mann, B., Askell, A., Bai, Y., Chen, A., Conerly. T., Drain, D., Ganguli, D., Hatfeel-Doddss, Z., Hernandez, D., Johnston, S., Jones, A., Kernion, J., Lovitt, L.., Ndousse, K., Amodei, D., Brown, T., Clark, J., Kaplan, J., McCandlish, S., and Olah, C. In-context learning and induction heads. Transformer Circuits http:/amafooommrriiiiiiiiispapap
Sundararajan, M. Taly, A., and Yan, Q. Axiomatic attri- bution for deep networks. In International Conference on Machine Learning, 2017. URL https: /api. semanticschond org. wttp.rooppps::11177555553333333.
Thread, 2022. contex--leaming-ande ind--iidccciionnnnddddlee...... hwwds/index..tmll
Tenney, I, Das, D., and Pavlick, E. BERT rediscovers the classical NLP pipeline. In Korhonen, A., Traum, D., and Mårquez, L. (eds.), Proceedings of the 57th Annual Meet- ing of the Association for Computational Linguistics, pp. 4593-4601, Florence, Italy, July 2019. Association for Computational Linguistics. doi: 10. 10..8866/111P19114522 URL https: http:///aaaaaatttaaaaeee org /.rggPP.. wwt/prg-g--- PP19-1452
Petsiuk, V., Das, A., and Saenko, K. Rise: Randomized input sampling for explanation of black-box models. In BMVC, 2018.
Pruthi, D., Gupta, M., Dhingra, B., Neubig, G., and Lipton, Z. C. Learning to deceive with attention-based explanations. In Jurafsky, D., Chai, J., Schluter, N., and Tetreault, J. (eds.), Proceedings of the 58th Annual Meeting of the Association for Computa- tional Linguistics, pp. 4782-4793, Online, July 2020. Association for Computational Linguistics. doi: 10.18653/1120222adlmmmm //aclanthologe wwwpgy...rr//e/.. 200..22200000 .cl.2...ccl--m
Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A. N., Kaiser, L., and Polosukhin, I. Attention is all you need. Advances in neural information processing systems, 30, 2017.
Vig, J. and Belinkov, Y. Analyzing the structure of attention in a transformer language model. In Linzen, T., Chrupala, G., Belinkov, Y., and Hupkes, D. (eds.), Proceedings of the 2019 ACL Workshop BlackboxNLP: Analyzing and Interpreting Neural Networks for NLP, pp. 63-76, Florence, Italy, August 2019. Association for Computational Linguistics. Linputttionalllnniiiisssssss doi: 10.18653/v1/W19-440000
URL https: 432.
Qiang, Y., Pan, D., Li, C., Li, X., Jang, R., and Zhu, D. Attcat: Explaining transformers via attentive class activation tokens. Advances in Neural Information Processing Systems, 35:5052-5064, 2022.
URL httph:tpp///// a antho oog - .rgg /w/g 9-4808.
Quirke, P. and Barez, F. Understanding addition in transformers. In The Tweifth International Conference on Learning Representations, 2024. URL https: / //openreview wwt.:orrtttfiiieemmm YXVWZZ...
Vig. J., Gehrmann, S., Belinkov, Y., Qian, S., Nevo, D., Sakenis, S., Huang, J., Singer, Y., and Shieber, S. Causal mediation analysis for interpreting neural nlp: The case of gender bias. arXiv preprint arXiv:2004.1 12265, 2020.
Räuker, T., Ho, A., Casper, S., and Hadfield-Menell, D. Toward transparent ai: A survey on interpreting the inner structures of deep neural networks. In 2023 IEEE Conference on Secure and Trustworthy Machine Learning (SaTML..) pp. 464 483. IEEE, 2023.
Wang. H., Wang, 7., Du, M., Yang, F,, Zhang, Z., Ding, S., Mardziel, P., and Hu, X. Score-cam: Score-weighted visual explanations for convolutional neural networks. In Proceedings of the IEEE/CVF conference on computer vi- sion and pattern recognition workshops, pp. 24-25, 2020.
12

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Wang, K. R., Variengien, A., Conmy, A., Shlegeris, B., and Steinhardt, J. Interpretability in the wild: circuit for indirect object identification in GPT-2 small. In The Eleventh International Conference on Learning Representations, 2023. URL https:  //ppnreeiie.n.o htt.://oooomm.....ssaS.s..
Zou, A., Phan, L., Chen, S., Campbell, J., Guo, P., Ren, R., Pan, A., Yin, X., Mazeika, M., Dombrowski, A.-K., Goel, S., Li, N., Byun, M. J., Wang, Z., Mallen, A., Basart, S., Koyejo, S., Song, D., Fredrikson, M., Kolter, J. Z., and Hendrycks, D. Representation engineering: A top-down approach to ai transparency, 2023.
Wang, X., Mao, S., Deng, S., Yao, Y., Shen, Y., Liang, L., Gu, J., Chen, H., and Zhang, N. Editing conceptual knowledge for large language models. In Findings of the Association for Computational Linguistics: EMNLP 2024, pp. 706-724, 2024.
Weiss, G., Goldberg, Y., and Yahav, Thinking like transformers. In International Conference on Machine Learning, pp. 1180-11099 PMLR, 2021.
Wiegreffe, S. and Pinter, Attention is not not explanation. In Inui, K., Jiang, J., Ng, V., and Wan, X. (eds.), Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference Natural Language Processing (EMNLP-IJCNL)) pp. 11-20, Hong Kong, China, November 2019. Association for Computational Linguistics. doi: 10.18653 1002. URL ht https://aclantie http:///aaaahhoogyooorreeoee wtwp//19ooooo/111111///1
Wu, Z., D' O'Osstellnckk, K., Geiger, A., Zur, A., and Potts, C. Causal proxy models for concept-based model explanations. In International conference on machine learning, pp. 77313-37334 PMLR, 2023a.
Wu, Z., Geiger, A., Icard, T., Potts, C., and Goodman, N. Interpretability scale: Identifying causal mechanisms in alpaca. Advances in neural information processing systems, 36:78205-78226, 2023b.
Yeh, C.-K., Kim, B., Arik, S., Li, C.-L., Pfister, T., and Ravikumar, P. On completeness-aware concept-based explanations in deep neural networks. Advances in neural information processing systems, 33:20554-2085 2020.
Ych, C.-K., Kim, B., and Ravikumar, Human-centered concept explanations for neural networks. In Neuro- Symbolic Artificial Intelligence: The State of the Art. pp. 337-352. IOS Press, 2021.
Zhang, Y., Backurs, A., Bubeck. S., Eldan, R., Gunasckar, S., and Wagner, T. Unveiling transformers with LEGO:
A synthetic reasoning task, 2023. URL https:
//ppreeieeew. net f 2id= JDN- RÉQfrb.
Zhong, Z., Liu, Z., Tegmark, M., and Andreas, J. The clock and the pizza: Two stories in mechanistic explanation of neural networks. In seieth-eeventh Conference on Neural Information Processing Systems, 2023. URL ht tps: wet.:/rummfom //openreview, net. formm? d= 5wmbQc1 We.
13

---

Validating Mechanistic Interpretations: An Axiomatic Approach
A. More Related Work
Probing. Probing involves training a separate supervised classifier to predict buman-understandable features of the data from the model's internal activations (Alain & Bengio, 2017: Zou et al., 2023) and has found wide applications for understanding the representations learned by language models (Tenney et al., 2019; Li et al., 2023; Nanda et al., 2023b; Burns et al., 2023; Belrose et al., 2023; Huben et al., 2024; Gurnee et al., 2023; Wang et al., 2024). Even though probe might be successful in predicting features from internal activations, it need not imply causal relationship between these features and the model output (Belinkov, 2022). It has also been questioned whether the model activations genuinely represent the feature of interest or the probe itself learns these features by picking up on spurious correlations (Hewitt & Liang, 2019). However, recent works have demonstrated that for Transformer-basee language models probes can be used to steer the model's output behavior by manipulating the identified internal representations (Zou et al., 2023; Li et al., 2023).
Related probing is the work on concept-base -aaeet reasoning (Kim et al., 2018; Crabbé & van der Schaar, 2022; Yeh et al., 2021; 2020) that extracts representations of high-leve concepts as geometric shapes in the neural network representation space (i.e., the activation spaces of inner layers of neural networks) and quantifies the impact of these high-level concepts on model outputs via attribution-based techniques.
Attention Pattern Analysis. There is a large body of work that attempts to understand the behavior of Transformer- models by analyzing the attention patterns computed by the self-attention layer (Allen-Zhu & Li, 2023; Zhang et al., 2023; Ebrahimi et al., 2020; Vig & Belinkov, 2019; Hao et al., 2021; Qiang et al., 2022; Lu et al., 2021; Abnar Zuidema, 2020; Chefer al., 2021; Liu al., 2023). However, there is an active ongoing debate about the validity of attention patterns as tool for interpreting model behavior (Jain & Wallace, 2019; Pruthi et al., 2020; Bibal et al., 2022; Bastings & Filippova, 2020; Wiegreffe & Pinter, 2019).
B. Axioms of Mechanistic Interpretation
Axioms 5 and 6 are stated more informally. Unlike the earlier axioms requiring the observed behaviors of the mechanistic interpretation and the neural network coincide, these axioms are concerned with the compilability of the mechanistic interpretation into a neural network. Both axioms assume the existence of semantics-preservee (denoted by compiler ). While Axiom 5 requires the compiled version of i to have the same structure and parameters as t (i.e., syntactic equivalence), Axiom 6 requires the compiled version to only have the same structure as t. The requirements imposed by these last two axioms are hard to establish in practice, and we do not consider them for the analysis presented in this paper. We present these axioms as a goal for future work. Recent work on compilers from the RASP language (Weiss et al., 2021) to Transformer models is promising step in this direction (Lindner et al., 2023).
compiler from d to Ar
Axiom 5 (Strong Mechanistic Derivability). h is mechanistically derived from if there exists a semeanies-preserving compilation compiler Xx (h) of h in dT such that compiler Xr (h) and t are syntactically equal.
Axiom 6 (Weak Mechanistic Derivability). h is mechanistically derivable from t if there exists a cemantics-preservee Au compilation compiler Xr (h) of h in Dr such that compiler Xr (h) has the same architecture (with the same number of parameters) as f.
B.1. Extension to Circuits
While we focus on end-to-end analyses, our axioms are compatible with the analysis of subgraphs of a larger model.
B. 1. AXIOMS FOR ARBITRARY COMPUTATIONAL GRAPHS
We can extend our axioms to operate directly on the graphs G and G': we present a generalization of Axioms through be- low. Let G (V,E) be the concrete model expressed as a computational graph and let G' (V', EE) be the computational graph, isomorphic to G, representing the abstract model. Let the isomorphism between G and G' be I1 and call the input and output vertices of G, in and out, respectively; while this can be easily extended to multiple input and output vertices, we present the single input, single output case for simplicity. Let execule (z) return a mapping val : V + Val with the values of all intermediate nodes where Val is the set of all possible values (i.e., vectors of reals) that the nodes can take. For a (partial) assignment to the vertices assign: V - Val with fin) S V' S V, propagate (appagate(G)assssee (assigg)) returns a mapping of the same type val: V + Val which is the result of execution of G where the provided intermediate assignments override the standard results of execution for those vertices. In this way, we can represent arbitrary interventions on G and G'.
14

---

Validating Mechanistic Interpretations: An Axiomatic Approach
We define abstraction operator Oy for each concrete node E V and concretization operator % for each abstract node o' E V' a and are the corresponding functions which apply the corresponding mappings each vertex in the graph. Finally, define (elec)(v)(val) val(v) for val V + Val and E V; we overload and let select(V") (val)))) = val( for V _ V and r' E V'.
We can then define extensions of Axioms to 4 below:
Axiom 7 (e-Prefix Equivalence). Vu V.
Pr lo select(v) execute(() select((((v)) execute((") amn(s)) 2 xnD
Axiom 8 (e-Component Equivalence). Ve E V.
Og select(v) ezccute(G)(x))
Pr mnD
2 -1-c
select([I(v)) propagate((") select([I(p)) U (II(in))) erccute(G)(x))
where p = predecessors(1))
Axiom 9 (e-Prefix Replaceability), Vu E V.
select(out) (xecute(C))x)
|
Pr zwD
select(out) propagate (G)) o select(fin, u}) o execute(G")) ain (z) 2 21-6
Axiom 10 (e-Component Replacabillyy.. Ye V.
select propagate(G) o select(fin, u}}o o propagale((") o select (I(in)))o a execute(G)(r))
)
Pr DnD
select execute(())r) =
2 21-6 21-c
where p = predecessors(u)
Note that our Axioms 1 to 4 are equivalent to these formulations, specialized to linear computational graphs.
In linear computational graphs, all dependencies on ancestor nodes are mediated by a node's predecessor; hence, there a limited need to consider parallel interventions, which involve simultaneously performing independent interventions on multiple nodes of the graph. In the case of prefix equivalence and prefix replaceability, any parallel interventions on linear graphs are equivalent the intervention on the final node in the sequence and hence have no additional effect. While parallel extensions of component equivalence and component replaceability would strengthen evaluation in the linear setting, considering parallel interventions is particularly important in the nonlinear case.
Consider the following scemario: there are two sibling nodes in the graph that encode redundant computations and the concrete states output by both these nodes contain information needed by the downstream circuit. Also, let us say that the corresponding abstract model fails to faithfully capture the computation performed by either of these nodes. However, this failure may not be captured by the axioms without parallel interventions since the redundant copy of the computation in the sibling concrete node masks any intervention applied to the other concrete node.
One potential solution is to merge such redundant sibling nodes in the analyzed graph G, however, this prevents checking equivalence of the nodes independently. A more general solution is to extend Axioms 7 through 10 to accommodate arbitrary parallel interventions. We present a preliminary formulation of an axiom for parallel intervention below; a final formulation left to future work. In particular, this axiom cannot be efficiently evaluated its current form.
We first extend erecute and propagate accommodate execution of arbitrary mixtures of the graphs G and G'. These behave before, except that any concrete inputs to abstract operation are abstracted prior to execution, and, similarly, any abstract inputs to a concrete operation are concretized prior to evaluation. Let ënterleave(GG. G', V') be graph identical to G except that the operations for any nodes v E V' are replaced with the operations for the corresponding nodes II(r) in G'. Let conditional abstract(V") be mapping on the values of the nodes v e V identical to am(() for v & V and the identity u E V". We can now express an axiom which generalizes Axioms 7, 8, and 10 to parallel interventions: Axiom 11 (e- (e-Equivalence), VV' VV
Pr select(v) o (ictiiiooo__bsstrrc(((() execule( select(v) o conditional (abbstaatstt"'' execute CnccuteiinterleueeGG.CC (x)
21-c
15

---

Validating Mechanistic Interpretations: An Axiomatic Approach
The condition of Axiom 11 can be made even stronger by the treeification (Chan et al., 2022) of the graphs G and G' prior to evaluation. This allows, for each node V, independent selection of the set of ancestors whose operations are replaced with their abstract equivalents. With treeification, Axiom 11 can express prefix replaceability as well, leading it to generalize Axioms 7 through 10.
B. 1.2. LINEARIZING CIRCUITS
We can directly validate arbitrary circuits with the standard linear- -aaaar axioms. In particular, we will describe how, for any computational graphs G = (V. E) and G' = (V', F*), which represent the concrete model and the abstract model h, respectively, we can construct a linearized computational graph. It is enough show the construction for G.
We will do so by propagating partial assignments to the vertices e E V through topologically sorted sequence of operations which compute the values of each node v as a function of the values of the predecessors. First, we extend Xy to include multivariate functions/ [211 ..,....,TT.)) for o E Var. Suppose that op: : V + Xr returns the operation op(v) computed by node each node e, and let predecessors(e) return the predecessors of node u in the argument order of op(v). For simplicity, we assume that G has exactly one input node in and exactly one output node out.
Let : [[V]] V be a topological ordering of G. Let idæ V + [[V]], the inverse of o, return the position of each node v in the topological ordering o. We again extend ÀT to include the function execute_opp (optuttt__________eeee__eeeeee p, ()nw))) which, given m-ary function f. node V. partial assignment to the vertices env V - [olu{1} and sequence of input nodes p [m]] + V such that env(p()) E Val for each 1 S i S m. returns an updated environment env' of the same type, identical to env except that en (v) = (enn(((())).... en)(((m)))))) Finally, for val E Val, let inpul_enuuval) be a partial assignment to the vertices syppu__ne(vval:: V > Val u {1} which is 1 everywhere but in, where we have taput_env(( (onl(va))(n)) = val.
Noting that (1( must always be in, we can define decomposition of as follows:
d, = (select(out) o exccauee_oploplo([V)) htwp:///oooooooooooyrreeeeeeeeod
o execute_opleeeeoe wwt.:o/poooll...rccccsrrrooooo/o
o input_enc.
C. Remark on Extensional Equivalence
Scheurer et al. (2023) presents an example illustrating the extensional equivalence problem: in particular, they demonstrate that causal scrubbing cannot distinguish between two mechanistic interpretations with equivalent input-output behavior but which differ in internal behavior. See Figure 4 for the two models. We make copies of the 3g and x nodes in model (b) to ensure that the two models are isomorphic.
As observed by Scheurer et al. (2023), the two are indistinguishable to causal scrubbing, noting that we assume that xy and x1 are both positive. This is a necessary consequence of the resampling technique used by causal scrubbing to derive its interventions. In particular, causal scrubbing replaces the values of concrete nodes with randomly selected values which are equivalent up to the abstract model.
Clearly, the concrete model is invariant with respect resampling ablations derived from interpretation (a), which is identical to the concrete model. But, likewise, there is effect from the corresponding intervention derived from interpretation (b). For instance, resampling conerete values of node (4), 2 up to equivalence in the abstract state of xn can have no effect. Hence, both interpretations are evaluated as perfect by causal scrubbing. For the same reason, these interpretations cannot be distinguished by interchange intervention accuracy (Geiger et al., 2022): interchange intervention accuracy replaces the values of intermediate nodes with those derived with different sets of inputs and evaluates the rate at which these interventions have an identical effects on the output of the abstract model on and the abstracted output of the concrete model.
If we restrict the set of allowable and by functions, for example to linear mappings alone, Axioms through 4 can distinguish between the two hypotheses. In particular, as no more than two points on the curve (ar, 1/4) can be collinear, Axiom I cannot hold with 0 on any distribution with more than four points in its support when we restrict a and y to be linear.
In the general case, with unrestricted a and y, the interpretations are again indistinguishable. However to obtain this result, we must conduct meaningful computation in the abstraction and concretization functions, e.g. a1(x) = 71(x)= = 1 while not directly evaluated by the axioms, any analyst with a bias towards keeping complexity in the interpretation would prefer
16

---

Validating Mechanistic Interpretations: An Axiomatic Approach
(0)
(0)
20
21
21
(2)
(3)
(2)
(3)
30
21
370
21
()
(5)
(4)
(5)
370
21
mn
m1
(6)
(6)
30 >
(a)
(b)
Figure 4: Extensionally equivalent mechanistic interpretations considered by Scheurer et al. (2023). Model (a) is the concrete model and the ground truth interpretation. Model (b) is the abstract model.
the ground-truth interpretation.
D. More Details on Mechanistic Interpretability Analysis of the 2-SAT Model
The decomposition of the original Transformer 2-SAT solver is shown in Figure 5.
The abstraction operators from our analysis are shown in Listings and 2 and the concretization operators are shown in Listings and 4.
D.1. First Block as Parser
Decomposed Attention Analysis. The parsing behavior in the first block cannot be fully described by ooken-to-token attention, and hence, we further decompose the standard QKdeccompoiition of Elhage et al. (2021) to account for positional factors as well. In Transformer, each token's initial embedding is the sum of a positional embedding and a token embedding; hence, rather than viewing attention as from destination embeddings to source embeddings, we can equivalently express the pre-softmax scores the sum of four sets of preferences- nosition-to-token attention, and ciattionto--osition attention. In particular mechanism as follows.5 Given token lare in position Pse to token last in position &st. the pre-softmax score is
attention, token-to-position attention, decompose the first block's 's self-attention
(tsrc TWE T + Pare "WPos") WK T We (Wetsa + WOSSPaa) (tsrc TWET T + Parc TWoos") Wok (Wgtaa + WPosPás)
-tar TWE Woo + tw WEE" WWK Wrostsc +
Par TWPos" "iPossWox' WFlas + Pare" TWros" Wox W
= typ TWiok-+tkk + tue T W p Psc + Pare QK
T pos-s-oo tas + Paee T W War peo-spp -pos
QK
Past:
where WE and Woss are the token and positional embedding matrices, WoK is the QK matrix, fr and las are the source and destination tokens, while Paee and Past are source and destination positions.
WWe use the QK circuit notation Elhage et al. (2021)
17

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Argmax
Unembed
Concrete component
Feedforward
ReLU
Feedforward
Concrete component
Attention
Feodforward
ReLU
Fesdforward
Concrete companent
Attention
Embedding
Figure Breakdown of the concrete model into concrete components, corresponding to the components de
Our observations in Figures and 6 suggest that the tokens relevant to the final classification decision, are in position 4i + 2 for 0 S i < 10, which, given the structure of the inputs to the model, are the second tokens of cach clause of the form 3; or mx, for S 5. If we restrict our view to destination tokens at this position, we can express the effects of the four components of the first block's QK circuit as shown Figure 7. With the somewhat odd exception of the first clause, and, in particular, first clause with second literal ii -wn, attention strongly deprioritizes the parentheses but has weak preferences for the source token otherwise. Outside of destination tokens xp and -To, preferences for source position are fairly consistent, and hence, the core effect is combination of position-to- cesttion-to-posiiionn preferences (see the bottom right of Figure 7) and a preference against punctuation (the parentheses tokens '(" and ')"). This can be seen in the token-to to-position preferences the bottom left, with an exception in the case of token 2, which may behave differently as all tokens to the left belong to the first clause, limiting the importance of learning more specific attention patterns. A general preference against punctuation can seen in the token-to- to-pititon preferences (top left) as well. For the first several clauses, positional preferences encode preference for the positions where parentheses occur, open parentheses in particular; however, the preference against parentheses shown in the token-to- token-to-position attention scores (corresponding to Wrtkk-po0) counteract that effect to result in net effect of attention to the first literal of the clause.
Distributional Attention Analysis. To illustrate how these four components of the QK circuit work together typical formulas, we can use the values of the four QK matrices to compute the attention scores in expectation given a uniformly distributed choice of literals. To compute the attention scores in expectation, we only consider destination positions (p = 4í + 2 for some i). Call the token in that position, t, and the full embedding passed to attention, e. To compute the expected pre-softmax attention score on position p' < p (defining t' and e' similarly), we first check if p' contains punctuation. If p' (mod 4), 'C and if p' (mod 4), ')' For such and E' we can use our decomposition
18

---

Validating Mechanistic Interpretations: An Axiomatic Approach
alpha_0 identity
def clause_ reasssrrppretntttioon Cecionnlitennn (literal_ literal_r): # Generate the input tensor for the formula with 10 copies of the clause inputs toks (1Or [iterall_.. literal_r)] 10)
embeds = eebeld (inpuss)
attn_out = embed + model. blocks [0]. attention
embeds,
10
(14+ 114+++2. gluue_posittoos__md__prreee (i)
(i)
11
12
block out = atin_ou out model. blocks [0]. mal(mmtppttttooo out)
We derive the canonical representation by averaging across second literal positions return mean(block,.
15
[4a clause_idx for clause_idx range(10))
16
17
c representations
clause
Or( clause_representation (1, r)
for 19
for literals literals
20
21
22
def alpha 1 oottput): bblck_ Lorok__oouppssssiiiis for in r10)e(10)] accon_llitralloouppre
24
25
Calculate cosine similaritics between the actual representations output at # the second variable positions and the canonical clause
26
# representations. select the clauses which best match return
[argmax_cosine
soipessssieeeeooeeos_eeeessessee sims (out, clause_ rlauss_eeprsssntattionn))
out
Listing 1: Abstraction operators for the first block in Python pseudocode.
def alpha_2 (resssrrrallllad__mllll
mlp_output residual_and threshold=0.5):
return [mlp_output[i] threshold for i in evaluating_neuron
alpha_3 3 = identity
Listing 2: Abstraction operators for the second block in Python pseudocode.
into the four sets of preferences to calculate an expected score:
E Ed W'Keee= E (T Wiok- work t wrlk P + D t+ oT WP
Wiik-tink
ET Wrok
ST Walk p + Ep W wpenstoo
nT Wpos pus
W took-tok tokk
He + ST Wiink ppe +
bit
telit
poss--ta Hok Hok QK
ve + p Wpessspa spoc
Dit
tEla
where we overload notation and use f, t' as tokens, indices, and the corresponding one-hot representations, and similarly for the positions p and p' and where lit is the set of literals.
p' does not contain punctuation, then we know that t' a variable (x; or ma; for some i), and similarly for Using
19

---

Validating Mechanistic Interpretations: An Axiomatic Approach
gamma_0 identity
Mean output from the first transformer black, by position, on the training set mean_ wwean_boock__oot mean modell. intermediatc_ouupptt ("block_1", x) for in train)
Constant on everything but second token positions
def (aaima_[(clausss]
output mot copy (
# Substitute the corresponding canonical clause representation
10
for i, clause enumerate clauses):
11
oulput[4xi+2] clause aaauss_repreeentattion [clause]
12
return output
Listing 3: Concretization operators for the first block in Python pseudocode.
Mean residual from attention for the readout token on the training set mean attn out mean modell. intermediate_oouppss (" ("aiupuussattttttion_bllia ""attention_block22" x)[-1] for in train)
# Output a constant residual term, and map predicted activations to # a large constant value
def gamma_2 acttivation ceattttoonmoeel_eee
high_ aigh_activation=))
conereiicnnnttniaationnn torch (mlp_width)
for i, model_out zip (ereeellaatng_neurrolll if model_out:
activation_moee__ooe
10
mlp_ mlp_out_conneeee coppouttconn [i] high activatio
12
return mean_attn_out mlp_out__conrretteee ulp_oou_conerctization
13
14 gamma_3 = identity
Listing 4: Concretization operators for the second block in Python pseudocode.
that, we use our decomposition into the four sets of preferences calculate expected score:
E
e
E
lT Wook-mok tT Wiik + p² W W-Pus--u Hokk
++ pp W pipss QK
QK
P.
TT Wrik--ook QK
+ E nT wotkkokkppe pos Ey
W wonnemook
tok
+ 1/ W
pmm---pp pos
QK
QK
QK
Wook-Hok QK
+
-pos QK
1'p +
Mitt
lit
tr'
1
Σ
tok
+
T
W
pos
pas
lit
QK
tEGi
After taking the softmax of the resulting values, the result shown in Figure 8.
Worst-case Attention Analysis. We can also show that the parsing behavior occurs by a worst-case analysis of the attention scores, iee. what is the minimum weight from attention to the first token of the clause and to the clause as a whole? This allows us to dispense with any distributional assumptions, and to validate that the inconsistent preferences for particular literals (i.e. the differences in preferences when the destination token is no). Given the definition of softmax,
20

---

Validating Mechanistic Interpretations: An Axiomatic Approach
(scom) lisers cluuti
Average stberion sccees (3ker))
Aucroge sttee SOUBET teset)
Perogg-atertion sooes 10err!
Auerage atterion soxes tolent
644
0.10
6.00
CLO4
2.50
3.00
Faation
Paaticc
Pastiin
Figure 6: Average attention scores, grouped by source token position, for heads, calculated over the set. In the first block, further average across destination token positions restricted positions 4i + 2, where 0 é < 10 is the clause index. For the second block, only consider the readout token as the destination.
Token Taken Attention Scores
Position to Taken Attention Scores
Score
Destination
Destiratto
-0
42
Source
Source
Token Position Attention Scores
Position to Position Attention Scores
Oesthatten
54-
Figure 7: Decomposed QK circuit the first block's ' attention mechanism; the subset where the destination token the second variable of clause is shown.
compute the minimum weight the first token of clause i by the second token of clause i follows:
min score softmax
1++1,4++2 (0)
min
min ( Σ f544+22 gocore (1-2())
1gtokare2
min s.
< min
2Etokaa m (00 Σ Σjs4ivj4444 max (ole 4:+r))
where tok; is the set of all possible tokens in position and where score, (()) and score (Ø) refer to the pre- and post-softmax attention scores with destination token in position d and source token in position and where the input formula é. For the full clause, the approach similar, except we add the term -uin colers (2 ac04a the numerator.
Now, we can derive the minimal and maximal scores for and and d using our decomposition of the QK circuit:
min score,.a(e) (dlow=t)
-pps min tpos QK
ttok QK
+ min ttok 3.t r'Etok,
s. r'ttok
dd
QK
1.6
21

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Softmax Score
Destiaation
18
22-
30
34
13
22
23
24
27
0.0
Source
Figure 8: Softmax of expected attention scores by position for the second token of each clause, showing that for each second token position, attention on literal positions in the corresponding clause are expected to dominate, consistent with our interpretation of the first block's attention mechanism as parser.
Minimum softmax attention score
0.8
0.7
0.6
0.5
0.4
0.3
First token of clause
0.2
Full clause
2
6
8
Clause number
Figure 9: Minimum post-softmax attention weights for each clause.
and similarly for the maximum (noting that if s d, we must have t' t as well).
The results are shown in Figure 9, and demonstrate that regardless the choice of formula, the majority of attention will be placed on the clause as whole, except in the case of the first clause, which case any additional attention is to the first '(" token, which contains no useful information.
perform similar analysis the attention of the ::' token. We observe in Figure 1 that the attention of the ':' token in the first block is near uniform. To see why this occurs, see Figure 10, which fully describes the first-block attention of ':', These are derived from the four QK matrices using the known position scores are consistently very small and have very little variation. As above, we can use this set of preferences to calculate a lower bound on the attention paid by the !!' token to any individual token:
Now,
40 of the token. The attention
ming, score
min score 1
sofemax 1,40
min,, score
40c max,, soore (2)
where score (:) refers to the "." token's pre-softmax attention to token in position i. We derive that the minimum attention paid to any token by ":" is approximately 0.0209, and we can similarly show that the maximum attention to any token 0.0285; hence, the u." token's attention can never vary far from the as 0.0244 paid by uniform attention.
Interpretation. Listing 5 shows our extracted mechanistic interpretation of the first component as Python code.
22

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Score
Notbd))
0.00
Source Token
1)ttx1)
Nottx2)
Nott33)
-005
N)ttx4)
10
11
12
13
15
25
26
22
39
29
30
32
36
56
37
38
38
40
Figure 10: Pre-softmax attention scores by the ":" token each token, by position and token type.
def parse_ clauses ffomuula: list J) -> [ [lit. (lit. ]it return [ formula (4+)+ for i in range (10)]
Listing 5: First component's mechanistic interpretation in Python syntax.
D.2. Second Block Evaluator
Abstract Attention Analysis. We showed in Section 4.2.1 that the behavior of the first block is accurately captured by interpretation which, after the application of 71, outputs canonical representations for each clause at the second literal positions and is constant at all other positions. Prefix replaceability, in particular, enforces this property directly. Furthermore, we must only study attention with the readout token as the destination to explain the output behavior; hence, we can characterize the behavior of attention in the second block solely by the preferences of each head in the readout token position to the canonical clause representations in the second literal positions, dramatically reducing dimensionality.
In this way, the key behavior of attention the second block is fully described by Figure 11. Each of the four charts shows the preferences each clause by the corresponding head; the columns correspond to the first literal of the clause and the rows to the second.
We see that the behavior of attention is nearly identical for a clause and its equivalent mirror image (i.e. the attention score on (1 V r) is approximately the same as that on (r V Z)); this is as expected given that, logically, / V = r v We can also see that each head prefers clauses containing certain literals (for instance, head 0 prefers negated literals as well as Tgg and ir)); each clause receives high score from some head (so no clauses are overlooked by the attention mechanism).
While we might read far more into these patterns, this is mistake in this case. In this instance, the behavior of attention is, in fact, not relevant to the underlying algorithm and serves only obscure the underlying behavior. As discussed in Section 4.2.2, we can much better understand attention in concert with the first layer of the MLP; collectively, these components encode the observed evaluating behavior, as discussed in more detail below.
Identifying the Key Pathway. We observe that the unembedding vector for UNSAT is nearly exactly the negative of the unembedding vector for SAT (IIWSAT + WUNSATT xs 6.2 x 10-"); ; hence, the SAT logit and the UNSAT logit are almost exactly negatives of each other; furthermore, the model's output token is always SAT or UNSAT. Across all formulas in the analysis dataset, the minimum value of the logit associated with the prediction (either SAT or UNSAT) slightly over while while the maximum logit on any other token across the dataset is below -9. Hence, we can consider the behavior of the SAT logit exclusively.
Next, we show that the key pathway that determines classification passes through the second block's ML.. For an input formula, the effect of the second block's 's attention mechanism through the residual connection on the SAT logit simply the dot product of the post-attention embedding in the readout token position with W:SAT, as we can see in Figure 12, this value is fairly consistent across the dataset and always negative; so positive SAT logit and hence a SAT classification must depend on the action of the MI.P.
23

---

Validating Mechanistic Interpretations: An Axiomatic Approach
PaetO
Hewr3
1000
Figure 11: Second-block abstract attention preferences.
2000
-6
Efter on SKT oph tive restu trom seced secedd ammettin
Gonggny
Figure 12: Effect of the residual connection from the second block's 's attention mechanism on the SAT logit. x-axis shows the effect on the SAT logit and y-axis is the number of instances in the analysis test dataset.
Figure 13: Average total effect on the SAT logit across all relevant neurons from SAT, UNSAT, and formulas satisfiable with particular assignments to the variables.
Evaluation in the Hidden Neurons. As discussed in Section 4.2.2, only 34 hidden neurons have a significant effect on classification; hence, we focus on the behavior of these neurons. As observed in Figure 12, the effect of the residual stream from the second block attention the SAT logit reduces the SAT logit by less than 6 units for all formulas in the analysis test dataset. Furthermore, as observed in Section 4.2.2, the model always predicts SAT or UNSAT, and the SAT and UNSAT logits are tied (in particular, they are negatives). Hence, the model will predict SAT when the collective effect of these 34 neurons is to increase SAT by > 6 units. We have observed that the expected behavior of these neurons is strongly dependent on which assignments to the variables satisfy the formula Φ.
natural question to ask is whether, whether these neurons will collectively increase the SAT logit sufficiently to output SAT on SAT formulas regardless of which assignment to the variables satisfies the formulas. Calculating this in the same way do for an individual neuron in Figure 3, obtain Figure 13, which shows that, indeed, the collective effect of the evaluating neurons (recall that we refer to the 34 relevant neurons evaluating neurons) correctly identifies SAT formulas regardless of how the formulas are satisfiable. It may seem odd that the average effect of SAT is significantly below the minimum of the effects for formulas satisfiable with any given assignment, as any SAT formula belongs to one such category; this is an artifact of the fact that no neuron has a large effect for all SAT formulas, and that each specializes in a subset.
Now, each of these neurons has a large positive (> 2.9) output coefficient (recall that output coefficient of a neuron the weight in the weighted sum expression constructed by composing the output layer of the MLP and the unembedding matrix projected to the SAT logit), ignoring all other neurons; hence, the model outputs SAT if any evaluating neuron activates sufficiently strongly. In this sense, the effect of the final output components (the MI.P's output layer, the unembedding matrix, and the residual from attention) can be viewed as an OR operation.
activation above 2 units any of the evaluating neurons is enough to force SAT,
However, in reality, individual neurons do not consistently reach activations of 2 2 (for example, see Figure 3, in which the average output value for formulas satisfiable with assignment TFFFF is approximately 1. 1.5), and multiple neurons
24

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Decision Tree F1 Scores by Neuron
Decision Tree F1 Scores by Neuron 4 LLaff Nodes
Decision Tree FI Scores by Neuron Unrestricted Size
2 Leaf Nodes
Deeciato Tree Sccres
0.6-
0.5-
Decidio Thea
Dec Maee Tree
0.4
0.2
0.2
02
0.0
Maximum Effect Logit
Maximum Effection SAT
Naximum Effect SAT
Figure 14: Fl scores of decision tree interpretations classifying high (> 0.5) activation of MLP hidden neurons.
O[FTTFF]
False
True
Low Activation
High Activation
Figure 15: Decision tree interpretation for unit 29 of the second block MLP's hidden layer, maximum leaf nodes: two.
recognize given SAT formula. Hence, moderate activation may be necessary across several neurons to predict SAT in some cases; this may explain the redundancy in evaluation behavior between neurons seen in Appendix G. For simplicity in our interpretation (in particular, to allow replacing a numerical weighted sum with Boolean operations) we handle this by using varying thresholds between the corresponding a and y functions for the MLP's hidden layer (in particular, 72 outputs an activation of 2 for neurons whose interpretation predicts high activation, while 0.5 is considered a high activation in the case of az)); as noted in the paragraph titled Hidden Layer of Second Block in Section 4.2.3, if 7/2 and ag both use the lower threshold, replacing the neural network components with our interpretation longer has minimal effect on classification.
We observe that each assignment to the variables has some neuron for which formulas satisfiable with that assignment result in significant increase to the SAT logit average, as we'd expect if the model was implementing the natural exhaustive enumeration algorithm for satisfiability checking. In particular, every assignment a has some neuron which increases the SAT logit by at least 2.9 units on average on formulas where a is a satisfying assignment; however, the average-case analysis hides the complexity of the behavior of these neurons. We can see this by noting that for every relevant neuron that on average demonstrates high activation for formulas satisfiable with some assignment a, we are able to find some formula satisfiable with which fails to result in sufficient activation for the neuron.
Interpreting Neurons via Decision Trees.
We'll focus on the general decision tree classifiers discussed in Section 4.2.2 here. We train decision tree classifiers on the thresholded activations of each evaluating neuron the analysis training set; this allows us learn an arbitrary Boolean function in the features ([...). We observe that these decision trees do indeed reliably predict activation. In particular, even very limited-size decision trees are reasonably strong predictors of the behavior of the neurons; we limit our decision trees to four leaf nodes in our experiments. Figures 15, 16, and 17 illustrate the effect on the decision trees as we lift this constraint. Figure shows that more complex decision trees are not significantly better predictors of the behavior of the neurons.
Implementation of Decision Trees by the Model. To see how the model implements the decision trees, we'll Il consider the effect of the composition of the second block MLP's hidden layer with the attention mechanism on the canonical representa-
25

---

Validating Mechanistic Interpretations: An Axiomatic Approach
(ITTIFF]
False
True
Low Activation
[[FFFF]]
@[TTTT]]
Low Activation
High Activation
Low Activation
Figure 16: Decision tree interpretation for unit 29 of the second block MLP's hidden layer, maximum leaf nodes: four.
tions the clauses, using the abstract attention approach discussed earlier. As the pre-softmax attention score by each head on the second literal of a clause is fixed value for each clause (recall that Yi leaves the representation of the readout token con- stant), express the effect of attention precisely in terms of the number of occurrences of each clause, as show next.
For head h and clause I V let the pre-softmax attention score paid by h to the clause be w/vr- Moreover, the output of the OV circuit is likewise a fixed vector for each clause, call it v Say that our formula contains list of n clauses (n2 10 for all our experiments) where the 7th clause is 4 V r;. Then, the attention paid to the 7th clause by head h is:
softmax([w) (er beji...))
Ey=1
ves
and hence the output of the attention mechanism (call it 0) at the readout token is, by rearranging terms,
Eieuerreta (o
Eietitretia covntottt.
1=1
where countivr(d (Ø) is the number of occurrences of / in the formula & and where the number of attention heads and where is the fixed representation of the readout token ':'
Now, consider the action of the MLP's hidden layer on this value: in particular, consider the effect on specific neuron n, where wn is the corresponding column of the MLP's input weight matrix and b, is the corresponding bias value.
The pre-activation score for n will then be:
Eieurreu evv coundivr (0)u/er
bn + w
T 0 b, + +w
T
+
Eieuer e countivr (6)
h=1
Enetit e covntcont (d) olvr
bn
T e, +
+
Exelitrena efrrcouuttv
An m Σ Eielitreta 4vr countivr
Cn +
hml Eielitrett diyy connttive (Φ)
where we define the following constants: = b, + wHe e,, d/ = e wive, h.m
dl w lvv
Givr
Note that the numerator and denominator of the fraction describing the contribution of head are both linear functions of the number of occurrences of each clause in the formula.
26

---

Validating Mechanistic Interpretations: An Axiomatic Approach
(IFTTFF]
False
True
Low Activation
(IFFFFT]
ΦTTTTT]]
([FTTFT]
High Activation
[FFTTT]]
Low Activation
OITFFFT]
O[FFTFF
High Activation
High Activation
Low Activation
Low Activation
4ITFIFT]
(ITFTFF)
Low Aclivation
High Activation
Low Activation
Figure 17: Decision tree interpretation for unit 29 of the second block MLP's hidden layer, unlimited leaf node count.
We'll briefly describe how <|a] and -ø[a] can be implemented with a single neuron for an arbitrary assignment to the variables in this formulation (in particular, we can ensure activation if and only if the condition that Φ is satisfiable by a or not satisfiable by a holds), and then analyze the behavior of a neuron with an interpretation of this form.
As the formula Φ is in conjunctive normal form, Φ[a] true and only if none of the clauses V in evaluate to false given the assignment øla] in neuron if we let d' be constant, Ctvr 0 for / VV r which are true given assignment a, and let Civy -00 for I V r which are false given a, and then let be a large positive number. Then, if Φ[a], countivr(o) = 0 for 1 Vr unsatisfiable given a, so the output is C.. Otherwise, if -o(a), counlivr > 0 and so the output is -cc. After applying ReLU, the activation of unit n is a large positive number when ø[a] and zero otherwise. Similarly, we can implement -o(a] by assigning Cn to negative number and letting Civr oc for V r which are false given a.
the variables (in particular, this holds if neither I nor holds given a). We can then implement h.n
h.n
Ann
Now, suppose that we want to implement some DNF expression e in the Φ[-.] without negation of any o(--.. Say that e con- tains & conjuncts e; for < S & and that the attention mechanism has at least & heads. We can extend the ideas in the imple- mentation of Φ[a] one for follows: let Cn k; now, consider head h with corresponding conjunet e; as in the d[a] case, let qvr = 0 for /Vr r which are not true for every assignment appearing in e,. As in that case, ş satisfies e; if and only if no clause violates the constraint (following from the assumption that e; is a conjunction of øla,] which appear without negation, A.n as, for an e of this form to be satisfied, each clause in e must be true for each assignment ay). Hence, if we let Civr = -1 for Ivr which violate e;, let d'y, = for such IVr r and d', some negligible value for Irr which do not violate the condition, the contribution of head to the expression is if e; satisfied and -1 otherwise (as the numerator will be U and the denomina- tor will be v t e where is the number of clauses violating the condition). Hence, all conjuncts e, fail to be satisfied, the out-
27

---

Validating Mechanistic Interpretations: An Axiomatic Approach
def evaluate_ stiisitltttisssibbiitty
clauses: list [lit lit]l.
neuron_ing cuuro__nterpprctation list [Callable [[
lit III, bool 11
[
return
neuron cetianitterpppeee inteeepcclluueee (clauses)
for neuron_inted in neuron neuron_ interpretatiroos]]
def
(satisfiabilities: list -> bool: return any anatisfiabbllitio
10
Listing 6: Second block's mechanistic interpretation. First, it applies series of functions, namely, the neuron interpretations, to the parsed clauses from the first block (evaluate satis sasssiiaabilyy and then, it applies OR operation
def abstract_mode (formula: list [tok]] ~> bool:
return predict_ satisfiability
evaluate_ evaluate_satisfaabill satisfiability
parse clauses (formula)))
Listing 7: Mechanistic interpretation of full model; see Listings 5 and 6 for the component interpretations.
put will be else, some e, must be satisfied, so the output will at least k: -k (k-1) 1) = 1, and, hence, the neuron will activate.
Interpretation. Listing 6 shows our derived mechanistic interpretation for the second block. Listing 7 shows the mechanistic interpretation for the entire model.
E. Importance of Prefix Axioms: Theoretical Evidence
While it may appear that each componentwise axiom implies the corresponding prefix axiom, for instance, that Axiom 2 implies Axiom 1, this is not the case. While it is possible to derive a bound, the resulting bound is extremely weak, and, for Axioms and 4, we cannot derive even such a weak bound without additional assumptions.
E.1. Equivalence Axioms
Suppose that Axiom 2, component equivalence, holds with a fixed eg- We will show that prefix equivalence (Axiom 1) holds at component i with an of ieg; if the number components is at least [ the bound becomes useless.
Let PE, be the event that x D satisfies the prefix equivalence condition for component i... that 0ş de: i 1](x)) dal: 1] oo(x) and and let CF2 be the event that satisfies the component equiva- lence condition for component i.c. that a; o del: i + [xxx) dxli] a--1 o del: (z)). Call Pr[PE:] pi.
Now,
Pr [att o d/: i (x) = d i i + (x)
Pi+1
anD
Pr Prlait1 o del: i + (z) = d,li + aa o d/:it [](x) du od/: 1](x) dxl: 2 ao(=))))
Pr Prlatt o :::: (x) d, + 00 d/: i ()))) A a; o d/: + 1](x) d, oo
aND p
Pr[CE411 A PE,),
noting that a; o d/l: i 1](x) = | i +1] (z) implies d + 1- 1) d/: i 1](x) = dul: 2 an(x)) by the
definition of the d notation.
28

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Now, we have that
Pr|CE,+ A PE, 1 Pr(-(CE PE.]
= - - Pr(--C V -PE] 2 1 - (Pr(-CE + Pr(-PPE))-
Hence, Pr(CE++1] We have P1 1 En prefix equivalence and component equivalence are identical for the first component, and so 2 1 deg. and we are done.
eo by component equivalence, have p++1 (co + pı)) and so p++1 Pi c0.
we assume that CF and PE are independent, we could derive a stronger bound:
Pr|CE:+1 A PE. = Pr(CE,,,)Pr(PE)) 2 (1 - eo)p:
from which derive Pr (1 - (o)'.) However, even this stronger bound grows very weak as depth increases, illustrating the need to evaluate mechanistic interpretation compositionally.
E.2. Replaceability Axioms
We only derive bound in the case that 7/4 ar and that all concrete components invertible. Assume component replaceability, Axiom 4 is satisfied.
Similarly to Appendix E. let the PR, and CR2 be the events that x ~ D satisfies the prefix replaceability and com- ponent replaceability conditions for component i, i.e. that (xx) = di + :] o 7 o da[: + 1] (o(x) and that [1] - o del: (x). respectively. By the assumption that all concrete components are invertible, PR, iff de(: 1] 7/2 d i (x( and CR, iff d + 1] = % o dn a;-1 o del: (z)) Call Pr[PR.] pt.
t(x) = de (i + :] % o di
Now,
Pi+1 = Pr [t(x) 2 d i 2] ao(x)
aND
Pr
IND
2 Pr
7+11 7=
d: + 1](x)
aND
2 Pr
AND
[ of
o4aca: 1|())
]
= Pr
aND
((x) = [4l--::onooddi--ooo)))444---111- od [](x)
= Pr
t(x) = + +
RND
= Pr(CR A PR.
by the assumption that all concrete components are invertible and that = a, The proof proceeds as before.
In particular, even with strong conditions such as these, we derive a bound which grows very weak as depth increases, and hence, we observe maintaining Axioms I and 3 in addition to Axioms and essential for reliable evaluation. See Appendix for empirical evidence for this fact.
F. Importance of Prefix Axioms: Empirical Evidence
We can demonstrate the importance of the prefix axioms by simulating errors in the interpretation of the 2-SAT model; specifically, every clause output by the first component of the abstract model replaced by randomly sampled clause 1 % of the time (the slight difference in e.g. the epsilons for component and prefix equivalence for the first component are due to independent sampling); results are shown in Table
29

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Table 1:
Comparison of results of experiments with synthetic error injected into the first component of the abstract model to original experimental results.
Noised first abstract component
Original abstract model
Axiom
Component 1 Component
Component 3
Component
Component
Component 3
Axiom 1:
Prefix Equivalence
0.0955
0.212
0.0315
0.0000374
0.182
0.0128
Axiom 2: Component Equivalence
0.0942
0.182
0.00433
0,0000374
0.182
0.00433
Axiom 3: Prefix Replaceahility
0.0583
0.0312
0.0318
0.0418
0.0128
0.0128
Axiom 4: Component Replaceability
0.0581
0.0128
0.00433
0.0418
0.0128
0.00433
The evaluation of the componentwise axioms are identical to the original results except the first component, these axioms do not take error propagation into account. The prefix axioms, on the other hand, show the extent to which errors in the earlier components result in downstream errors.
Taking error propagation into account is particularly important when we consider deeper models. While we can derive worst-case compositional bounds from the componentwise results, this may not actually describe model behavior; in particular, as the number of components increases, the derived bound rapidly becomes meaningless (see Appendix E for more details). For example, in our case, the aggregation operation in the final component enables prefix equivalence to improve with depth; hence, restricting ourselves to the pure worst-case analysis derived from component-only analysis would suggest that our interpretation is far less reliable end-to-end than is actually the case.
G. Neuron Interpretations for the 2-SAT Model
Tables 2 and 3 show the decision tree based and disjunction-only neuron interpretations, respectively.
H. More Details on Mechanistic Interpretability Analysis of the Modular Addition Model
Pseudocode for the abstract model is shown in Listing 8. The concrete model is likewise broken into three corresponding components. The embedding matrix corresponds to encoding_of_inee _iiputtts the attention mechanism and the input layer of the MLP correspond to sum_ lfti_o__aa__ of_angles, and the output layer of the MLP and the unembedding matrix correspond to di ifffeeeceeooo _al___of__ggg__aaeeeee langlls_aaggge aaraar...a.... The abstraction and concretization operators are linear maps learned using the continuous-valued abstract values (e.g. prior rounding) and the corresponding concrete intermediate representations on the training set, using the original train/test split of Nanda et al. (2023a).
Note that, in Nanda et al. (2023a)'s paper, the third component is further decomposed into two pieces; specifically, the difference-of- of--alllss identities and the summation (along with the argmax) steps are considered separate. The difference-of- angles identity is computed using the MI. output layer and the unembedding matrix while the summation step is computed via the unembedding matrix. As there is no canonical factorization of the unembedding matrix, there exists no natural decom- position of the concrete model into these two components we analyze the composition of these two components instead.
As noted in Section 5, the discretization operators necessary for compatibility with Axioms 1 and 2. Without rounding on the first component, we obtain epsilons of I for Axioms and 2; epsilons for Axioms 3 and 4 are unaffected by rounding.
For the second component, we apply the equivalence class formulation described in Section 5; however, we strengthen the equivalence criterion by ensuring that equal samples affect neither concrete nor abstract model behavior. This was chosen to avoid the need to sample from the equivalence class on concretization or to select a canonical representative for each class; doing so would have been needed to correctly evaluate Axioms 3 and 4 without such a guarantee. When sampling in this way feasible, an equivalence relation up to the abstract only model is sufficient. Pseudocode given in Listing 9.
As for the first component, obtain epsilons of I for Axioms 1 and 2 without applying the equivalence class mapping; by construction, the epsilons for Axioms 3 and 4 are unaffected by the equivalence class operation. Note that simple discretization operators do not suffice: we once again obtain an of I for Axioms I and 2 when rounding to a single decimal place. While strong results with the discretization described above show that the abstract and concrete representations of the output of the second component are equivalent up to their downstream impact on both the concrete and abstract models, results with simpler discretizations indicate that the the concrete representation does not represent the abstract state exactly.
30

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Legend
When
10 Mary
Key / Value
John
Query
Class of Heads Layor.Hood
Output
Previous Token Heads
S1+1 went
2.2 4.11
to
the
store
Negative Name Mover Heads
S2 John
Duplicate Token Heads
Induction Heads
11.0
3.0 (0.10)
5.5 6.9 (5.8 5.)
gave a
Name Mover Heads 9.9 9.6 1000
drink
S-Inhibition Heads
END
Backup Name Mover Heads
7.3 79 8.6 8.10
9.0 9.7 10.1 10.2 10.6 1010 11.2 11.9
Figure 18: The IOI circuit, reproduced from Wang et al. (2023).
A Sketch of Application to Circuits: Indirect Object Identification
As described in Appendix B. our axioms may be extended to evaluate circuits-type interpretations, may be applied directly by linearization of the computational graph of the circuit.
To illustrate the process, we'll describe how the circuit for Indirect Object Identification (IOI) (Wang et al., 2023) may be evaluated. The IOI circuit consists of five broad categories of heads:
1. Previous token heads, which copy information from the prior token
2. Duplicate token heads, which identify whether there exists any prior duplicate of the current token
3. Induction heads, which serve the same function duplicate token heads, mediated via the previous token heads
4. S-inhibition heads, which output a signal suppressing attention by name mover heads to duplicated names
5. Name mover heads, which copy names except those suppressed by the S-inhibition heads for output
Note that each of these attention heads computes a well-defined interpretable function which can be represented in our framework. Figure 18 shows the structure of the circuit. We'll now illustrate the process by which the circuit may be analyzed via the linearization technique from Appendix 1.2 or the graph axioms from Appendix B.I.I. The circuit in Figure 18 cannot be directly evaluated, it must be made isomorphic decomposition of the concrete model.
To do so, will first expand the circuit in Figure 18 head-hy-head graph. Next, for each block with interpreted head, we construct dummy nodes in the interpretation which correspond uninterpreted heads; the interpretation claims that these are uninvolved in the IOI task, these nodes compute the identity function, constant function or some other no-op which is independent of the 1OI task.
Now, we must account for computations performed uninterpreted blocks and MLPs. We can express the computation performed by a block of a transformer as simple computational graph: each interpreted head, and well as the dummy node corresponding to the uninterpreted heads, takes the incoming residual stream an input and returns an update to the residual stream. These updates added the residual stream and processed by the remaining components, such as the MLP and any normalization. which produce the final residual output by the block. For simplicity, we combine any uninterpreted layers into this operation. These nodes, abstractly, update the program state from the potentially redundant input information. In this way, we can construct isomorphic concrete and abstract models from any circuit of this form.
We derive the concrete and abstract models shown Figure 19. Note that structuring the circuit in this way allows us clearly define and evaluate hypothesis on how redundant copies of given abstract concept are combined downstream.
31

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Uninterpreted Heads
Block 2 Haad 2
Copy Previous Token
Identity
Block 0 MLP Block
Update State
Uninterpreted Heads
Block 0 Head
Block Head 10
Duplicate Detection
Duplicate Detection
Identity
Taken and Position Embeddings
Update State
(a) Concrete Model
(b) Abstract Model
Figure 19: Concrete and abstract models derived from the IOI circuit.
32

---

Validating Mechanistic Interpretations: An Axiomatic Approach
For example, the model might retain independent duplicate copies of the information, one copy per head, retain only the most recently-computed value, aggregate redundant copies with some weighting.
At this point, we can apply either the linearization technique of Appendix B.1.2 or the generalized axioms of Appendix B.1.1 to evaluate the hypotheses. We do not fully evaluate IOI with our axioms here as Wang et al. (2023) leaves key components of the interpretation unspecified. In particular, the authors do not clearly state how the model combines the information pro- duced by redundant heads performing the same function, and the authors do not conclusively state what the duplicate-token suppressing information output by the S-inhibition heads represents. For example, that information may be represented as the suppressed token itself, via either relative or absolute positions, combination of token and position information. A complete analysis with our axioms would enable the analyst to derive clear evidence for the correct hypotheses.
33

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Table 2: General neuron interpretations derived by decision tree learning neuron activations. A neuron activates if the corresponding condition in the second column holds.
Neuron
Interpretation (General Case)
10
OFFFFF FTTFF A O FFFFT A (TTTTT OTTFFF] OFFFT]] OFFFFF] (-O[FTTFF) FTFFF) OFFTFF)
29
36
41
48
55
TTTFF
77
FFFTT o FTTTF
81
96
TFTTF A O FFTFF
150
FTFTF A - 6 TTFFF
185
(FFFTT FTTTTT] TTTFT TFFTF - TTITT
189
195
201
TTFFT A O TFTFF
224
OFFFFT
231
6FFTFTT A [FFFTF]]
245
6TFFFT TTFTT TTFTTT (FFFTFF) @TFTFE] TTFFFT TTTTF
261
291
304
317
326
334
Φ (FFTTFF] A (FFFTT
374
TTFFT TFTTF A (FFFFF
380
TFFFT
411
TTFFT
416
@TTFEE
435
( A
(6TTFTF) (FTEFE]
450
#FFFTTT A (IFFFFF
482
áITTTT A FFFTTF
490
((FTTFFT) A (TTTTTT V (6 FTTFT] AOTTTTT A (TTTTFT)
492
STFFFT]
495
OFFFFE
499
-(FFTEEAA-OFTTHE)> A A (6FFFTE))
34

---

Validating Mechanistic Interpretations: An Axiomatic Approach
Table 3: Disjunction-only neuron interpretations derived by finding satisfying assignments that correlated with high average neuron activation value over the analysis training set. A neuron activates if the corresponding condition in the second column holds.
Neuron
Interpretation (Disjunction-OOlly)
10
(FFFFF V V TFTFF Vo[TFFFR)
29
FTTFF OTFFFF OFFFFF FTFFFF
36
41
48
OTFFF FTTFF
55
[TTTFF] TTTTFT
77
$[FFTTF] V (FFTTT V (FTTTT]
81
6FFTTTF] V 6FFTTT]]
96
TTFTTF
150
FTFTF
185
FFFFTT
189
FITTT
195
@TFFTF] V TETTF V (TTTFT
201
(TTFFT OFFFFT
224
231
FFFFTT 6FTTTT]
245
@ OFFFFF V FTFFT V (FFTFT]
261
TTFTT
291
d[FFTT]] OIFTIT TTFTT
VOTTTT]]
304
FFTTF
317
TFFFT
326
@TTFFF V O TTTTF (TTTTT
334
FFTTFF TTFTT TFFTT
374
380
411
TTFFF TTTFFT]
416
@TFTFF (TTTFF
435
ØTTFTF]
450
6[FFTFF) V FFFFT OFFFFT V (FFTFT]
482
TTTTT
490
FTTTE
492
@TFTFF (TFTFT) (TTTTFT
495
FFFFF FFFFF
499
35

---

Validating Mechanistic Interpretations: An Axiomatic Approach
modulus 113 key_freqs = [14, 35, 41, 42, 52] cos_sin tuple list [ist[floatt] [
def encoding_of_inpuce
a: int
b: int
tuple [cole[cos... sin cos sin
10
cos_a = [cou
(cos (2 *
pi a modulus) ) for in fregs
11
cos_b = (co * pi b modulus)) for f in key_fregs
(cos
sin_a Tround (2
pi / modulus)) for in key_
sin_b b [round (sind
pi b modulus)) for in sey_freq
14
15
return (cos_a, sin_a), (cos_b, sin_b)
16
def sum_of (ngles
18
components: tuple cin_sin, cos_sin].
19
RquivalenceClass:
20
(cos_a, sin_a), (cos_b, sin_b) = components
cos_ab cb for ca. sa. sb in zipscos a, s cos_b, sin_b)
sb
23
24
25
sin_ab ab cb sb
27
for ca. sa, cb sb in zipscos_a, sin_a, cos_b, sin_b)
28
29
return EquivalenceClass (cossssaah _b, sin_ab)
32
def difference angles_argmax
argmax (angle_sums sums_class EquivalenceClass) -> int: cos ab, sin_ab ab extract angle_sume sums (angle_sune) sums sumssclassss_s cos ab minus_c
33
34
36
cab cos
pi modulus) sab sin (2 pi modulus) for cab, sab, in ccos_ab_ sin_ab, key_freqs)
37
38
for in range (modulus)
41
42
return argmax (map (sum, cos_ab a.l_abmminu__)))
43
44
def modular addition cnfffrrence_o__angles__eee sum_of_anglest encoding of in__inuts (a, b)
modular_addition (a: int, b: int) int:
46
47
48
Listing 8: Mechanistic interpretation of the modular arithmetic model
def cquivalent cos_sin. sin, b: cos_sin) -> bool:
abstract_eg ee = abstract_componente (3](a) = abstract_componentt (3](b)
concrete_ed
concrete_component return abstract_eq and conerete_cq
gammaas (a)))) comerete_components [3 (aammas ((1(b))
Listing 9: Equivalence relation for second component of mechanistic interpretation of the modular arithmetic model
36


Reviews:
[{"review_id": "WZNWL9Djlv", "reviewer": "Reviewer_LJQi", "summary": "The paper introduces a formal framework for assessing mechanistic interpretations of neural networks. The authors propose a set of axioms inspired by abstract interpretation from program analysis to systematically evaluate whether a given mechanistic interpretation accurately captures a model’s internal computations. The proposed framework emphasizes compositionality, requiring that each step in the interpretation aligns with the corresponding computations in the network. The axioms are validated through case studies on Transformer-based models trained to solve the modular addition and the 2-SAT problem. Experimental results demonstrate that the axioms provide a structured way to evaluate interpretability quantitatively.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your thoughtful comments, we respond in detail below.\n\n## Q1. It is unclear how well this approach generalizes to larger models\n\nWe emphasize that our key contribution is our framework (i.e., axioms) for evaluation of mechanistic interpretations and not particular techniques to derive them. Hence, while deriving/finding mechanistic interpretations is more difficult on larger models, it does not impact the applicability of our approach. As an illustration, consider the application of our framework to IOI [1].\n\nThe IOI circuit for GPT-2, at a high level, identifies the indirect object by identifying all names in a sentence, filtering out any duplicated names, and selecting the remaining name.\n\nThe analysis in [1]. is at the level of attention heads, and consists of five broad categories of heads:\n\n1. **Previous token heads**, which copy information from the prior token\n2. **Duplicate token heads**, which identify whether there exists any prior duplicate of the current token\n3. **Induction heads**, which serve the same function as duplicate token heads, mediated via the previous token heads\n4. **S-inhibition heads**, which output a signal suppressing attention by name mover heads to duplicated names\n5. **Name mover heads**, which copy names except those suppressed by the S-inhibition heads for output\n\nEach of these attention heads computes a well-defined human-interpretable function and are representable in our framework; each may be modeled as an independent node in the computational graph. Each depends on the residual stream flowing into the corresponding layer; the subsequent residual stream is then a function of the preceding residual stream and all interpreted attention heads. As only attention heads are interpreted, the remainder of a block is an identity function in the abstract model. In this way, we can construct isomorphic concrete and abstract computational graphs for arbitrary circuits.\n\nAppendix B.1 describes how the resulting computational graphs may be linearized, allowing the application of axioms 1 through 4, and how to extend our axioms to operate natively on nonlinear computational graphs.\n\nMoreover, our framework provides a principled approach for evaluating a number of key questions left by [1] for future work. In particular, the authors of [1] hypothesize that S-inhibition heads output relative, and not absolute positions of duplicated names, but do not clearly demonstrate that this is the case. Applying our axioms to the corresponding abstract models would permit the analyst to identify the better hypothesis. \n\nHowever, we again emphasize that our focus is on the evaluation framework, and not methods for deriving mechanistic interpretations. Thus, while the analysis of GPT-2 Small and other larger models is compatible with our axioms, conducting such an analysis and deriving mechanistic interpretations is out of scope for our work.\n\n[1] Wang et al. Interpretability in the Wild: A Circuit for Indirect Object Identification in GPT-2 Small. 2022.\n\n## Q2. Significant manual effort may be necessary\n\nWe agree that significant effort is necessary for the analyst to derive a mechanistic interpretation, but it should be noted that mechanistic interpretability is in general a time-consuming and highly manual process. While automated approaches to deriving interpretations are an interesting direction of research in their own right, our work is about evaluation of derived mechanistic interpretations and not about techniques to derive an interpretation.\n\n## Q3. How sensitive are the axioms to the choice of abstraction and concretization functions?\n\nThe axioms may be sensitive to this choice, but we should note that these are essential components of the interpretation; interpretations which claim that the same abstract function is computed over different representations are not the same, and hence their evaluations should not be either. It is the analyst's responsibility to choose these functions appropriately, and our axioms are useful for identifying which choice more closely matches the behavior of the model.\n\n## Q4. Are the proposed axioms sufficient to validate mechanistic interpretations?\n\nYes, our axioms are sufficient, presenting a strong set of criteria to ensure that the behavior of the concrete model and the claimed mechanistic interpretation are interchangeable and behave in the same way. We recognize that stronger axioms are possible, and, in particular, we propose two additional axioms, Axiom 5 and 6 in the appendix. These strengthen the evaluation, but are difficult to operationalize, and we believe that Axioms 1 through 4, as presented in the main body, already constitute an effective evaluation valuable to the mechanistic interpretability community. Our work represents a first step in the direction of formally validating mechanistic interpretations. We hope that our work inspires a conversation in the community and leads to further improvements to evaluation techniques.", "claims_and_evidence": "The major claims made by the paper are:\n1. Mechanistic interpretability can be rigorously defined through a set of axioms that ensure both input-output fidelity and internal component alignment.\n2. Valid interpretations should respect compositionality, meaning that replacing parts of a model with their interpreted counterparts should minimally affect outputs.\n3. The proposed axioms can be empirically validated using statistical tests.\n\nThe claims are supported through experimental validation. The case studies show that the axioms can characterize valid mechanistic interpretations.", "methods_and_evaluation_criteria": "The evaluation methods used in the paper are reasonable and align with the goal of assessing mechanistic interpretability. The authors apply their framework to two models, including an existing modular addition Transformer and a novel 2-SAT-solving Transformer. These evaluation strategies provide the empirical foundation for the proposed axiomatic approach.", "theoretical_claims": "The paper argues that mechanistic interpretations can be formally validated using an axiomatic approach. The theoretical framework is sound, and the derivations appear correct.", "experimental_designs_or_analyses": "The experimental setup is well-structured and supports the claims:\n1. The 2-SAT model’s interpretation is carefully analyzed using attention patterns, decision trees, and abstraction-concretization mappings.\n2. The modular addition model’s interpretation is validated through discretization techniques and statistical checks.\n3. The impact of different abstraction choices (e.g., disjunction-only vs. full decision tree interpretations) is explored, demonstrating trade-offs in interpretability fidelity.", "relation_to_broader_scientific_literature": "The work extends prior research on mechanistic interpretability by providing a formal framework.", "essential_references_not_discussed": "The paper discusses the most relevant work in mechanistic interpretability.", "other_strengths_and_weaknesses": "Strengths:\n1. The paper is well-written and presents a clear, formal framework for mechanistic interpretability.\n2. The proposed axioms provide a structured way to evaluate interpretations, filling a gap in prior work.\n3. The experimental validation is thorough, with strong empirical support for the claims.\n\nWeaknesses:\n1. The method primarily evaluates small-scale models trained on synthetic tasks (e.g., modular arithmetic and 2-SAT). It remains unclear how well this approach generalizes to larger, practical models.\n2. Following 1, the axiomatic framework may require significant manual effort when applied to real-world models.", "other_comments_or_suggestions": "N/A.", "questions_for_authors": "1. How sensitive are the axioms to the choice of abstraction and concretization functions?\n2. Is the proposed axioms sufficient to validate mechanistic interpretation?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "pyN8WKhgvh", "reviewer": "Reviewer_RksT", "summary": "This paper is a first effort to draw a parallel between mechanistic interpretability and abstract interpretation from programming language theory. This is a natural analogy, and its very exciting to see contact between these two areas. The authors introduce four axioms for how an abstraction interpretation of a neural network should operate. Then, they present two case studies. In the first, they train a two layer transformer on SAT solving and then develop a mechanistic interpretation by looking at attention heads and MLP activations. In the second, they reevaluate the modular arithmetic algorithm presented in Nanda (2022) under their framework. Both analyses are successful.", "questions": "", "limitations": "", "rating": 5, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your detailed comments, and for your strong support for our work! We respond in detail below.\n\n## Q1. What happens when only some of the axioms are adhered to?\n\nIn appendices D and E, we include a discussion of what happens when we consider component axioms (Axioms 2 and 4) alone; in this case, we do not consider compositionality of the interpretation. Likewise, considering replaceability alone invites the problem of the interpretation being extensionally equivalent (equivalent in terms of input-output behavior) to the model under analysis but lacking intensional equivalence (equivalence in terms of internal structure) [1].\n\n[1] Scheurer et al. Practical pitfalls of causal scrubbing. AI Alignment Forum. 2023.\n\n## Q2. How should the $\\epsilon$ values be contextualized?\n\nWe may view the $\\epsilon$ as a form of error, in the sense that $1 - \\epsilon$ is the accuracy with which the abstract model or intervened concrete model predicts the behavior of the original concrete model. In our experiments, we observe values of $\\epsilon$ in the full range of 0 to 1. We observe values of up to 1 for bad interpretations, as well as values of 0 for interpretations which perfectly match the behavior of the model (the only reason the paper does not report any $\\epsilon$ values of 0 is because we compute Clopper-Pearson confidence intervals). In this sense, $\\epsilon$ describes the probability that the behavior of the concrete and abstract models differ, and is meaningful in itself. We should add that $\\epsilon$ is, in addition, useful for relative comparisons, identifying which interpretation better matches the underlying behavior of the model.\n\n## Q3. Relationship of our framework with causal abstraction and causal interventions\n\nWe will make a note about Remark 35 of [2], thank you for the suggestion! However, it is important to note that $\\tau^{-1}$ may not always be a feasible choice for concretization. In particular, $\\tau$ will not be invertible in general, and hence this necessitates application of set semantics, which may be infeasible in the concrete domain, and hence for replaceability. In addition, we should note that it is not necessarily the case that abstract interpretations align individual high level with individual low level variables.\n\nWhile our axioms do not exactly follow the structure of interchange intervention (in particular, the interventions are not derived by substituting intermediate states from different inputs), they may be regarded as performing a specific class of causal interventions, which are soft interventions of the type described in [2].\n\nThe replaceability axioms may be viewed as interventions on the original concrete model. If we consider component replaceability and $x_i$ is the input to the $i^{\\text{th}}$ concrete component, the intervention performed in component replaceability replaces the constraint $x_{i+1} = d_t\\[i\\](x_i)$ with the constraint $x_{i+1} = \\gamma_i \\circ d_h\\[i\\] \\circ \\alpha_{i-1} x_i$. The equivalence axioms may be defined as analogous soft interventions on the corresponding abstracted prefixes of the concrete model.\n\nFrom that perspective, our axioms present a principled choice for a standardized set of causal interventions, which we believe is very valuable to the mechanistic interpretability community. In particular, while frameworks such as that of [2] are very broad, that breadth means that there is no clear standard choice for evaluation, hence causal abstraction analyses continue to emphasize interchange intervention accuracy, which does not directly evaluate the equivalence of internal representations.\n\n[2] Geiger et al. Causal Abstraction: A Theoretical Foundation for Mechanistic Interpretability. 2024.\n\n## Q4. The framework is evaluated only on toy models.\n\nWe do not intend the case studies presented to serve as an evaluation of our framework, but as an illustration of how it may be applied. Our framework can indeed be used to validate interpretations of larger models; see the response to Q1 of reviewer LJQi for more details. As the reviewer notes, our primary contribution is the new framework for evaluation of mechanistic interpretations and not particular techniques to derive them.", "claims_and_evidence": "There are some claims about connections to causal scrubbing/abstraction that I would be curious to hear more about. What are the issues that come from only adhering to some of your axioms, and what are some precise examples where this approach differs from causal abstraction? Maybe something you could add something about this to your thorough appendix!", "methods_and_evaluation_criteria": "I would say that the weakest part of the paper is that you don't include baseline evaluations that help contextualize your error terms. Sure, some of the error terms look really low, but without context new metrics are very difficult to understand! How about is the larger error you see in the MLP for the SAT solving mechanistic interpretation?\n\nIs there some evaluation metric that is more similar to interchange intervention accuracy from causal abstraction stuff? Getting an impression of how much of the model behavior your mechanistic interpretation matches would be great!", "theoretical_claims": "N/A", "experimental_designs_or_analyses": "The experimental design seems very good to me. Easy to understand and well-written.", "relation_to_broader_scientific_literature": "Mechanistic interpretability is in need of more theoretical work that grounds out the field in existing theoretical frameworks. Prior work looks to formal theories of causality, but this work begins to build a bridge to program language theory which is a rich and well-studied field with formal foundations that mechanistic interpretability could use!", "essential_references_not_discussed": "You should check out this paper:\n\nhttps://arxiv.org/pdf/2301.04709\n\nWhich goes much further into the causal abstraction theory and connection to mechanistic interpretability. In particular, I would be curious what you make of Remark 35 given that you claim in this paper that causal abstraction lakes the concretization and abstraction operations.\n\nI think you would find it deepens the connections to this work greatly!", "other_strengths_and_weaknesses": "This paper is an original take on mechanistic interpretability and brings over exciting new tools and ideas from programming language theory. The experiments are simple, but they clearly demonstrate the relevant concepts. \n\nThe biggest weakness of this paper is that its evaluated on toy models, but I would say the primary contribution is the new framework and concepts that they are introducing to mechanistic interpretability.", "other_comments_or_suggestions": "N/A", "questions_for_authors": "Could you give an intervention-based definition for the axioms you defined? Or maybe just explain whether/how interventions are being performed in your experiments on transformers? I think that interventions are being performed for each of the axiom verifications, but it would be cool to have it spelled out", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "tnOktijZLS", "reviewer": "Reviewer_zQST", "summary": "This paper introduces a set of axioms aimed at formalizing mechanistic interpretability for neural networks, inspired by abstract interpretation concepts in program analysis. The authors define mechanistic interpretations as human-interpretable programs that approximately replicate the computations of neural networks. To validate such interpretations, they propose six axioms that focus on input-output equivalence and component-level fidelity. The paper applies these axioms in two case studies: a previously known transformer-based modular arithmetic model and a novel transformer trained to solve the 2-SAT problem. Empirical analysis confirms the axioms can quantitatively validate mechanistic interpretations, contributing a structured evaluation framework.", "questions": "", "limitations": "", "rating": 2, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your thoughtful comments, we respond in detail below.\n\n## Q1. Case studies are too simple; it is unclear whether the approach is applicable to larger models\n\nWe note that our framework is already compatible with larger models and more complex architectures, and we emphasize that our main contribution is our evaluation framework (i.e., axioms) for validating mechanistic interpretations and not techniques to derive mechanistic interpretations. Hence, any increased difficulty of deriving mechanistic interpretations on larger models does not affect the applicability of our approach. See our response to Q1 by reviewer LJQi for more details.\n\n## Q2. How does the proposed axiomatic approach scale to larger, real-world models, particularly when intermediate states are high-dimensional continuous vectors rather than discrete symbols?\n\nAs noted above, our approach is compatible with larger models. We note that the intermediate states of the concrete model are, in all cases (including for 2-SAT and modular arithmetic models), high dimensional continuous-valued vectors. Our requirement that the intermediate states be discrete is only for the abstract model. In particular, we require this as we agree that mechanistic interpretations cannot hope to achieve equality of high-dimensional continuous vectors in Axioms 1 and 2.\n\nHowever, we emphasize that our requirement is natural for useful mechanistic interpretations, in particular, as any interpretations which operate on high dimensional continuous vectors will not generally be human-interpretable and hence will be of limited utility.\n\n## Q3. Essential references not discussed\n\nThank you for the references, we will incorporate them into the paper. We should note that while [1] proposes an axiomatic framework for interpretability, it considers input interpretability only. [2] is primarily a survey of the architectural components interpreted and techniques such as probing for identifying the representations of abstract values, and reflects the class of concrete programs which $\\lambda_T$ must represent.\n\n[1] Sundararajan, Mukund, Ankur Taly, and Qiqi Yan. \"Axiomatic attribution for deep networks.\" International conference on machine learning. PMLR, 2017.\n[2] Mueller, Aaron, et al. \"The quest for the right mediator: A history, survey, and theoretical grounding of causal interpretability.\" arXiv preprint arXiv:2408.01416 (2024).", "claims_and_evidence": "The main claims of formalizing and empirically validating mechanistic interpretations through axioms are reasonably supported. However, critical claims about the general applicability and scalability of the proposed axiomatic framework beyond simplistic algorithmic tasks lack clear and convincing evidence. While results on toy examples (2-SAT, modular addition) are encouraging, the absence of larger or practically relevant neural network benchmarks diminishes the robustness of broader claims.", "methods_and_evaluation_criteria": "The proposed axioms and evaluation methodology make conceptual sense for assessing mechanistic interpretations on small-scale, algorithmically transparent models. However, the chosen tasks—modular arithmetic and 2-SAT problems—are relatively trivial compared to practical neural network applications, limiting the generalizability and real-world relevance of the proposed evaluation criteria.", "theoretical_claims": "The theoretical claims are clearly presented, and definitions of the axioms appear sound. I reviewed the definitions and the axiomatic formulations carefully. While the theoretical framing seems correct, no significant issues emerged. However, the theory primarily covers simple computational models, and extending it theoretically or empirically to more complex and realistic architectures would enhance its value significantly.", "experimental_designs_or_analyses": "The experimental validation provided is sound but limited. The analyses (attention patterns, decision tree extraction for neuron activations) for the chosen examples are adequate, though they only apply to very simple Transformer architectures trained on straightforward tasks. The robustness of these axioms when applied to larger and more complex datasets, or real-world tasks, is unclear. More diverse experimental setups would substantially strengthen the paper.", "relation_to_broader_scientific_literature": "The paper situates itself effectively within existing literature, clearly distinguishing its contribution from related approaches such as causal abstraction and causal scrubbing. It successfully positions its axiomatic framework as complementary and extending prior works by emphasizing compositional evaluation.", "essential_references_not_discussed": "The paper neglects discussion of broader interpretability frameworks beyond the program-analysis-inspired perspective. Moreover, broader causal interpretation literature could have further contextualized and strengthened the motivation behind formal axiomatic approaches.\n\n- Sundararajan, Mukund, Ankur Taly, and Qiqi Yan. \"Axiomatic attribution for deep networks.\" International conference on machine learning. PMLR, 2017.\n- Mueller, Aaron, et al. \"The quest for the right mediator: A history, survey, and theoretical grounding of causal interpretability.\" arXiv preprint arXiv:2408.01416 (2024).", "other_strengths_and_weaknesses": "The paper's strength lies in providing clear formalization and axioms for validating mechanistic interpretations, filling an important gap in the literature. The theoretical clarity and detailed empirical evaluation on chosen tasks are commendable.\n\nHowever, the primary weaknesses include:\n\n- Limited practical relevance due to simplistic and overly specialized choice of tasks (2-SAT and modular arithmetic).\n\n- Lack of demonstration or discussion on scalability to real-world, complex neural networks and tasks.\n\n- The approach might become less meaningful or too restrictive for networks with significantly richer internal structures or continuous-valued intermediate states.", "other_comments_or_suggestions": "None.", "questions_for_authors": "- How does the proposed axiomatic approach scale to larger, real-world models, particularly when intermediate states are high-dimensional continuous vectors rather than discrete symbols? \n\n- Could you provide concrete guidance on determining appropriate abstraction functions \\alpha and concretization functions \\gamma in realistic settings with large neural networks?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {"ethical_review_concerns": "N/A"}}, {"review_id": "4MSSEYqb8n", "reviewer": "Reviewer_QoaE", "summary": "They propose a framework to quantify the effectiveness of a total decomposition of a model into sequential interpretable components. They find that this framework is able to validate (by showing a high probability in each of the equations of their axioms) explanations they create for the model components of a transformer trained to classify satisfiable 2-sat formulas. They also use their axioms to validate a previous interpretation (from [Nanda et. al. 2023 https://openreview.net/forum?id=9XFSbDPmdW]) for a transformer performing modular addition.\n\n## update after rebuttal\n\nI find that my opinion of the approach remains after the rebuttal period, and retain my initial score.", "questions": "", "limitations": "", "rating": 2, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your helpful comments, we respond in detail below.\n\n## Q1. More experiments are required to evaluate the framework by analyzing practical foundation models using the axioms from B.1\n\nWe sketch how the circuit for IOI in GPT-2 [1] may be expressed and analyzed in our framework in the response to Q1 of reviewer LJQi. Evaluating circuits in our framework is straightforward given a fully-specified mechanistic interpretation. However, in practice, we observe that popular mechanistic interpretations such as the IOI circuit leave many key details unspecified. Circuit analyses of this type can be strengthened by evaluating using our framework as it forces the analysts to spell out all the details; we hope that such studies will be conducted in future work.\n\n[1] Wang et al. Interpretability in the Wild: A Circuit for Indirect Object Identification in GPT-2 Small. 2022.\n\n## Q2. Framework should be evaluated in comparison to baseline evaluation frameworks\n\nWe agree that evaluation of this type would be valuable, however, we note that we are the first to propose an axiomatic framework for the evaluation of mechanistic interpretations, presenting a natural and principled set of criteria; we believe that this already constitutes a valuable contribution to the community. We hope that our work inspires further conversation in this direction, and leave such an analysis to future work.\n\n## Q3. How do the axioms handle residual connections?\n\nWe can express residual connections via concrete functions which return the residual stream as part of a tuple of values. See the analysis of the 2-SAT model for an example: the second concrete component returns both the residual stream and the hidden layer of the MLP. Appendix B.1 discusses a variation of Axioms 1 through 4 which operate on nonlinear graphs, and in this case no change is necessary.\n\nIn general, we may treat the residual connection as computing the identity function in the abstract model; we discuss this in more detail in the response to Q1 for reviewer LJQi.\n\n## Q4. Are the axioms for some fixed $\\epsilon$?\n\nYes, that is correct. In definition 3.1, we define an interpretation as $\\epsilon$-accurate when Axioms 1 through 4 are satisfied with that fixed value of $\\epsilon$; we will clarify this.\n\n## Q5. Axioms in high-dimensional vector spaces\n\nWe do state that our axioms require that the abstract states be discrete (lines 128-130), however we will improve clarity.  No such restriction applies to the concrete model. While lines 410-420 illustrate an important tradeoff of discretization techniques, this is not a weakness of our axioms. Noting that our equivalence class formulation for discretization generalizes comparison up to a tolerance, any evaluation approach which considers equivalence of intermediate values (essential to have any hope at resolving the extensional equivalence problems of the type discussed in [2]) will observe the same behavior.\n\nAlso see response to Q2 of reviewer zQST.\n\n[2] Scheurer et al. Practical pitfalls of causal scrubbing. AI Alignment Forum. 2023.\n\n## Q6. Why do the axioms capture explainability better than other approaches?\n\nFirstly, our axioms define clear standards to evaluate. Approaches such as causal abstraction are overly broad, making it unclear to the analyst how their interpretation should be evaluated. If we view the equalities in our axioms as tests under causal interventions, we propose a specific and natural set of interventions which ensure that both internal and output behaviors of the interpretation and the concrete model match, and moreover that the corresponding abstract and concrete components are interchangeable.\n\nSecondly, we were motivated to formulate our axioms in a manner which captures validation techniques already used informally in the mechanistic interpretation community to evaluate interpretations.\n\nFinally, our axioms improve upon existing approaches by considering all of internal equivalence, output equivalence, and compositionality. We discuss the importance of compositional evaluation in appendices D and E. As shown by [2], evaluating only on outputs does not ensure that the intermediate values agree. \n\nWe discuss these differences in more detail in section 3. We should note that we do not claim that our axioms cannot be improved upon; rather, our work represents a first step at formalizing validation of mechanistic interpretations. We hope that work in this direction continues and that our work inspires further improvements to evaluation techniques.\n\nRegarding the specific approach mentioned, as described above, techniques which neglect the equivalence of internal values invite the problem of only establishing extensional equivalence [2].\n\n## Q7. Why the non-homogeneous architecture?\n\nOur goal was to identify the simplest architecture with high accuracy, which we observed with this architecture.\n\n## Q8. What is the loss function?\n\nWe use a next-token prediction objective.", "claims_and_evidence": "I find that they successfully demonstrate their method in toy examples. However, there are a few points that would be required to analyse their claims and methods in my opinion: \n- Their axioms at face value require a full decomposition of a network into interpretable components. Since it is exceedingly unlikely that full model interpretations will exist for practical problems, one needs to interpret their axioms for sub-networks in practice; They go over how to re-interpret their axioms for these cases in Appendix B.1. I would argue that to sufficiently prove the utility of their framework, some practical example of existing foundation models should be experimentally analysed using their axioms as interpreted in B.1.\n- Further, Their method is demonstrated, but not evaluated relative to anything else. For example one could design experiments where a model has a ground truth interpretation, and then show their method evaluates the correct interpretation in a better way than a false but plausible interpretation relative to some baselines.", "methods_and_evaluation_criteria": "Their toy examples are appropriate, but more work and experiments would be required to evaluate their framework in practical foundation models. Also, their methods should be evaluated in their identification of good interpretations versus other baselines.", "theoretical_claims": "Checked the arguments of appendix D and found no issues.", "experimental_designs_or_analyses": "Yes, I checked over the details of the experiments in section 4 and 5 and found no issues.", "relation_to_broader_scientific_literature": "The broader context of this work is in the addition of their framework to the set of methods for evaluating the degree of validity of human-interpretations for model components.", "essential_references_not_discussed": "Not to my knowledge.", "other_strengths_and_weaknesses": "Weaknesses exist in terms of utility of their approach versus other methods for evaluating explainability of interpretation of model components.\n\nTheir interpretability analysis on the case study in section 4 is well done.", "other_comments_or_suggestions": "- I’m not sure if axiom is the right or best terminology for the inequalities called as such. A better description would be to treat those as “degrees of explainability”. I.E. the probability in the respective “axiom” quantifies the degree of explainability of the interpretation across prefix equivalence, prefix replaceability, etc …\n- Typo 118 right: “functions need to be individually instantiated every mechanistic interpretation.”\n- Since the computational graph is not just a sequence, how does the residual work with indexing and in all the axioms when switching from human and model components with alpha/gamma? Perhaps a sentence stating how to handle residual connections in general in the main text.\n- Are the axioms for some fixed epsilon? Maybe denote them as Axiom i (\\varepsilon) to be explicit.\n- Be explicit when stating the axioms that the equality in the probability for each axiom is appropriate for the axioms when it does not take place in a high dimensional vector space, but rather the discrete (human-interpretable) output space or the human interpretable space. This is mentioned later in sentence at line 389 right when discretizing is necessary to evaluate the interpretation in section 5.\nThe discussion following this in line 418 right, highlights a general weakness of these axioms when the equality is evaluated in a high dimensional vector space, since discretization may be necessary to apply their axioms to a given model interpretation, as was the case for section 5. “[discretization] limits the ability of Axioms 1 and 2 to validate the internal behavior.”", "questions_for_authors": "- Why do these axioms in particular capture explainability well in a more appropriate way than some others? For example we could have formulated a single axiom where for any nondecreasing sequence i_n of indexes in [len(d)], we have the \\varepsilon-replaceability of all components between i_{2k} , i_{2k+1}.\n- Why the non-homogenous architecture in experiments, where the second layer has more attention heads?\n- What is the loss function for training in experiments of section 4? Is it the usual next token prediction, or binary cross entropy on the sequence classification?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: In the context of neural network interpretability, this paper focuses on evaluating mechanistic interpretations that aim to capture, in an intelligible way, the computations performed by predictive models. Drawing inspiration from the concept of abstract interpretation found in program analysis literature, the authors adopt an axiomatic approach for assessing mechanistic interpretations. Specifically, they introduce four axioms to validate the capacity of a given mechanistic interpretation to approximately capture the semantics and compositional structure of the predictive model. The applicability of this axiomatic validation approach is examined in two case studies involving transformer architectures: one involving satisfiability of 2-CNF formulae and another on modular addition.

While this study has received mixed reviews, ranging from "Strong Accept" to "Weak Reject," reviewers generally agree on the novelty and flexibility of the axiomatic validation approach. However, there are concerns regarding the current evaluation on toy models and its potential scalability to more complex and realistic architectures. Additionally, some reviewers noted a lack of detailed comparison with causal abstraction approaches. Considering the reviews and the authors' responses during the rebuttal, the strengths of this paper—particularly the originality of the proposed framework—outweigh its weaknesses. Accordingly, I recommend a "Weak Accept" for the paper.

In a revised version, I suggest including a detailed discussion on how well this axiomatic validation approach can be extended to larger predictive models used in practice. Adding more case studies (deferred to the Appendix) could indeed further demonstrate the practical applicability of this approach.
Decision: Accept (poster)