Thank you for the overall supportive review of our work!

You currently cite the survey of Geiger et al. (2024) for causal scrubbing (line 109). However, I believe it was first introduced in Chan et al.

We fixed this in the revised version.

First of all, many thanks for an extremely thorough and insightful review. We greatly appreciate the effort.

Major comments

1.1 The key thing that would improve this paper, in my opinion, is making it clearer, especially key technical details. I found sections 4 and 5 difficult to follow - the concepts of coset concentration and irrep sparsity are introduced, without much motivation, and are then not necessary to explain the algorithm. I would personally reverse the flow of 4 & 5.1 and work backwards:

We have rewritten section 5.1 and started with (Eq 4) to make the final result clearer. We think it is better to keep 4 & 5.1 seperated, to clearly distinguish between our work and previous work. Section 4 is also not necessary to understand our circuit, but helps clarify how our approach unifies the previous ones.

1.2 I find the term "compact proof" quite cryptic, and it took me until about page 7 to figure out what was going on. A decent part of the confusion is that you use proof to refer to what I'd normally call a program. I would have benefitted a lot from an intuitive explanation in the intro or start of section 6 (ideally both, plus something in the abstract). Something like:

Thanks for this suggestion. We agree that the introduction was vague about this concept and we have added a slightly modified version of your suggestion in the introduction.

2. I find the term "compact proof" somewhat confusing. To me, proof connotes showing something rigorously about abstract mathematical objects . But perhaps this is just taste, and this notion of proof is common in e.g. the field of formal verification?

What we refer to as compact proofs can be thought of as proofs of statements about abstract mathematical objects (the model weights) in the standard mathematical sense. A compact proof of a model $M$ consists of two parts:

• Let $W$ be the space of weights and $D$ the space of inputs (let's say uniformly sampled, but you could also try to prove statements for a different distribuition). Then for a map $C:W\to\mathbb{R}$ (depending on the interpretation), we prove an inequality $C(w)\leq \mathbb{E}_{x\in D}[Acc(w,x)]$ i.e. it is a sound lower bound for the accuracy. In our case the map $C$ is "run the algorithm in Appendix E and return the final number you get in Step 7". Note that the proof of this inequality does not depend on model or dataset size.

• Use the model weights to calculate $C(w)$. This can be thought of as proving that $C(w)$ is what it is, with length of proof equal to the execution time. The bulk of the proof's length is this step.

But indeed we also refer to a definition of compact proofs that is common in formal verification (though we don't find it necessary to think in these terms to understand it): A fully formal proof in logic is a tree where each node is the application of an axiom of the theory. (In the dependent type theories used by, Coq, Agda, Lean, etc., a fully formal proof is a well-typed abstract syntax tree of the theory.). By "compact" we just mean "short", i.e., the number of nodes in the tree is small (or, in dependent type theories, where the worst-case time to check validity grows as roughly the busy-beaver number of the size of the AST, we mean that the proof-checking time is short).

I'm somewhat skeptical of compact proofs as an interpretability metric, for several reasons - I would love to be convinced otherwise though: 2.1 They bound accuracy, not loss.

Our current strategy to generate compact proofs works by bounding the margin of the logits. This strategy can be modified to instead bound the cross-entropy loss. However, this adaptation to a loss bound is rather crude and results in fairly weak bounds. This isn't an inherent limitation of the compact proofs framework; rather, our paper was simply more focused on accuracy than on loss. See Appendix J for details.

Minor comments

Minor comments

3. I don't understand what Figure 1 is trying to show, a shame as you clearly put in effort there! How is S3 mapped to points on a hexagon? What are the terms in the top row with 4 vertices circled? What does adding them mean? What is X_12? Etc I recommend significantly clarifying or changing the figure

Thanks for the input. The points on the hexagon are one way to arrange elements of $S_3$. The way it is done is not very important, the relevant part is that the group $S_3$ acts on this via reflections/rotations (and other kinds of symmetries). In our example, right multiplication by $(123)$ acts via rotation by $120^\circ$. We decided to remove the upper part. We appreciate any feedback, if you think it would make the figure easier to understand.

4. Obviously, it would be great to replicate the paper's results on other groups! A5, A6, S4 seem natural to try. I predict the results to hold up though.

We have extended Appendix K with results for A5 as well as some discussion of difficulties we face in applying our interpretation to other groups. Unfortunately, we are fairly restricted in the size of groups we can train models for --- for large groups like A6, we lack the computational resources (training cost per epoch is proportional to $|G|^3$), while for small groups like S4, there are too few training points and we do not observe the grokking phenomenon at all.

5. I find the definition of compact proofs somewhat odd - what exactly does it mean to be a valid lower bound for any explanation string? It strikes me as odd that your compact proof must first begin by eg verifying if a subset of G is a subgroup, when that seems independent of the model.

The interpretation string / verifier setup is introduced in order to correctly formalize the notion of an interpretation corresponding to a specific model rather than all models. Thus, the interpretation string is allowed to vary with the model being interpreted. On the other hand, we cannot allow the verifier to vary with the model -- if it could, for each model, we could trivially define the verifier to output the model's true accuracy in constant time.

For similar reasons, we do not allow the verifier to vary over the group being trained on. If it did, we could again construct an (asymptotically) trivial solution by, say, memorizing a lookup table of all models that attain good accuracy on a specific group up to some precision.

11. Line 196: What does it mean for a subset of G to be common to a family of cosets? Cosets are subsets of G, so surely the intersection of a family of cosets is a set of subsets, not a subset?

We mean that the subset $X\subseteq G$ is a member of both families, i.e. is an element of their intersection (which indeed is a set of subsets). We edited this part and hope it is clearer now.

12. Line 436: Why do you refer to neurons as functions G->R rather than G->R^2? They have two inputs, x and y, right?

We decompose the pre-embedding part of the MLP into a left and right part with corresponding left and right neuron, as defined in Section 3.2.

Lemma F.3: Are you arguing that all have the decomposition described here? If not, which ones do, and does this correspond to the irreps learned by the model?

Generally, this is not true. This lemma is true in case that H\G/H has two elements, which applies to our situation of H=S4 and G=S5. (It might be the case that the lemma is true in more general cases). We added a comment below Lemma F.3.

Note that the validity of the compact proof does not depend on this lemma holding. The proof instead leverages bi-equivariance to verify that the output is maximized at the correct logit by computing a single forward pass. In principle, in cases where the lemma holds, we can prove model accuracy using zero forward passes, but we do not do this.

14. In table 2 in Appendix G, why does the minimal -set size go above 5? Naively, it feels like an irrep of S5 should always be able to permute a set of 5 vectors.

Given a permutation representation $f:G\to S_n$, we can consider $f$ as a degree-$n$ linear representation of $G$ consisting of permutation matrices. There exists a $\rho$-set corresponding to this permutation representation (and thus a $\rho$-set of size $n$) if and only if $\rho$ is present in the decomposition of $f$ into irreps.

For instance, if $G=S_5$ (and $f=id$), the corresponding linear representation admits two subrepresentations: the one-dimensional trivial irrep and the four-dimensional standard irrep. It's therefore impossible for e.g. the other four-dimensional irrep to have a minimal $\rho$-set size of $5$.

Major comments contd 2

Can you learn a and a $\rho$-set that explains a cluster of neurons?

This is precisely how we arrive at bounds on accuracy. We explicitly write down $\rho$-set circuits (the idealized model) and then bound their distance in output space from the original model.

Does [a cluster of neurons corresponding to a $\rho$-set] have size $k^2$ exactly?

This is typically true, with two caveats:

• Sometimes (as briefly mentioned in footnote 9 of the revised text), there are more than one neuron corresponding to a single pair of the double summation. These "duplicate neurons" are a minor technical detail that can be dealt with easily as long as the sum of magnitudes of all neurons corresponding to each pair is uniform across all pairs (Observation B.2.7). Empirically this is indeed the case
• More importantly, for some models there are no neurons corresponding to a substantial number of pairs in the double summation, i.e. the number of neurons in the circuit is much less than $k^2$; this failure mode is labeled ($\rho$-bad) in the revised text. In this case we do not fully understand the model's performance, and correspondingly we are unable to obtain good bounds. (If there are only a handful of missing neurons, we can simply add them to the idealized model and bound the discrepancy in output logits due to these neurons.)

3.3 I found the claim in Lines 502-503 that causal interventions can only yield weaker positive evidence to be overstated - this applies to the interventions used in Stander et al, but IMO those are pretty weak interventions and not that compelling by the standards of current mechanistic interpretability. This doesn't mean there don't exist more compelling causal interventions.

We agree and modified this sentence to make a more careful claim. Indeed the main thing lacking in casual scrubbing is not the strength of evidence in either direction (there's a sense in which casual scrubbing can be seen as a sampling-based proof), but rather an adequately developed notion of compactness that can be used to evaluate the quality/depth of the explanation (the brute force explanation is the best, as far as causal scrubbing is concerned).

4. Separately, I'm extremely skeptical that compact proofs will scale beyond very toy networks (let alone to frontier systems). Being robust to worst case scenarios on the entire space of inputs seems highly unrealistic to me for eg a language model or image model. Methods don't have to scale to be interesting, of course, but this limits my excitement about the method. I'd value arguments for why the method might extend to eg imperfect coverage of the input space.

It's worth noting that proofs are worst-case over the unexplained portion of the model weights but average case over the input distribution. We can easily deal with imperfect coverage of the input space by simply discarding that portion of the input space from the accuracy bound, resulting in either 1) a decreased accuracy bound for the entire space or 2) a less compact proof, if the discarded portion is dealt with another way, say using brute force. Chernoff's concentration inequality can be used to get less crude bounds on the "typical" case behavior w.r.t. inputs (there is work in progress on this). Additionally, ARC Theory's work on surprise accounting in heuristic arguments can be seen as a way to generalize compact proofs from worst-case over model weights to typical-case over model weights.

We made some more comments about the compact proofs approach in our general response.

5. I'd be very curious to see how well "the square of the size of the smallest rho-set correlates with the probability that rho is learned,” eg using the numbers in Chughtai et al. This would significantly clarify the results in Chughtai et al re universality if true.

The statement we intended to make is: The order of frequencies in Figure 7 of Chughtai et al. is the same as the ordering of the rho-set size in Table 3. We have clarified this in section 7.1 and hope this also addresses minor comment 15.

To evaluate the clarity, I've tried to go through the revised paper pretending I was seeing it for the first time, and still find it dense and unclear:

• Equivariance: I wouldn't know what you meant by equivariance given the description in the abstract & intro, despite this seeming a crucial contribution (I am familiar with the word, but not what it meant here). I recommend adding a 1 sentence definition to the intro - the formal definition in line 239 would have clarified things a lot.
  • It would also be good to state in the abstract that this focuses on S5 specifically
• Compact proofs: I would not understand what it means in the abstract. In the introduction the prose is significantly improved, but I expect I would still be confused. In particular, when I see program on the model my mind jumps to "weird wording for running the model on some input" and when I see formal proof I imagine "something a human wrote", through referring to brute force immediately after helps clarify. More broadly I find the whole concept fairly unintuitive - you're using an explanation to provide guarantees on the model's performance, but the guarantees don't actually require or assume an explanation, it's that the explanation motivates a guarantee creation process, and the metric is "fraction of inputs on which we can guarantee correctness" and think it would benefit from more exposition
• A narrative that would feel clearer to me would be something like the below - is this correct?
  • When we have a precise mechanistic explanation of a model, we would like to rigorously show that this works.
  • The real model will differ somewhat from this ideal explanation, due to noise or imperfections in our analysis
  • To rigorously validate our analysis, we would like to bound this deviation, in a way that gives us formal guarantees, not just approximations. We focus on guarantees of the form "on X% of all possible inputs, the model gets the right answer"
  • A formal guarantee essentially looks like a (potentially extremely long) mathematical proof, typically produced by an algorithm not a human.
  • The simplest formal guarantee is to brute force try every possible input to the model - this works on any model, does not require a mechanistic explanation, and is a perfectly tight bound.
  • But we believe that a mechanistic explanation should let us produce a formal guarantee via a faster algorithm than just trying every possible input, eg by exploiting symmetries predicted by the explanation. We hope that we can get a speedup while still finding a fairly tight bound. The resulting algorithm can be run on any model, but will only produce good guarantees on models with the properties predicted by the explanation. Being able to provide an efficient guarantee on model's performance therefore provides strong evidence for the correctness of our explanation.
• I still don't really get figure 1 - how do x and y correspond to what's on the hexagon? How did you map those elements of S3 to those points? Why is (123) a rotation by 120 degrees? Presumably (12) is not a rotation of 60 degrees, since it has order 2. Currently this figure adds negative clarity for me
• Section 4:
  • I understand the desire to keep prior work and your work separate, but I think that swapping section 5 and section 4 (or moving section 4 to an appendix) would significantly improve clarity. Section 4 might add value to a reader familiar with Chughtai et al and Stander et al, but are needless complication to those who aren't (and you can add a reference to the section on prior work at the start of the section on your work).
  • As is, the paper reads like "a review of concepts/empirical observations in prior work, and why you believe them to be limited and having a bunch of degrees of freedom", which the reader must try to understand and keep in their heads, followed by your algorithm, which, as far as I can tell, doesn't require the reader to understand the prior work at all.
  • If the goal is to emphasise how your paper makes a contribution going beyond past work, I think this is still done well by swapping the section, as you can then explain how each observation follows from your algorithm, and point out all the details left unspecified by prior work that you fill in.
  • Nit: I think it would also help to emphasise that coset concentration and irrep sparsity are empirical, approximate observations, not mathematical properties of the network - wording in line 188 like "left embeddings are constant" feels too strong
• Section 5: Beginning the section with equation 2 is a significant improvement! Thank you
  • It would help to define a,b,b',B immediately after the equation - the reader should be able to understand what this equation means without needing to read the next several paragraphs
  • Nit: It would be good to say that the logits are (approximately) a linear combination of such terms

Thanks to the authors for their detailed responses and improvements. My biggest concern was lack of clarity. I appreciate the improvements, but this is still a fairly complex paper and I think there's significant room for improvement - I detail my thoughts in another comment for space.

• Compact proofs:
  • Thanks for your explanation of how compact proofs can be used on loss, I find this persuasive (at least that it's not a theoretical flaw - I won't believe that it's solvable in practice until I see good empirical demonstrations of this)
  • "better explanations are better compressions" While I agree with this, I do not agree that this implies that good explanations lead to better compact proof generation algorithms. Compact proof generation algorithms seem like a fairly peculiar thing, and like they eg need to exploit specific symmetries in the model to work, which I don't think necessarily need to be part of a good explanation
  • "We believe that as we increase the the size of the group these differences become more dominant." Sure, but this paper only provides empirical evidence on S5, and you provide no evidence that the algorithm works on eg S4 or S6. I acknowledge that S6 or S7 are a pain to train, but I think that given that you only provide evidence that your explanation is correct on a single group size, the empirical speedup is a better quantity than the asymptotic value.
  • Thank you for the clarification that it's worst case over model weights not input space, this is a fair point
• Empirical evidence:
  • Thanks for these, I find Figures 5, 7 and 8 to be convincing evidence that your interpretation is correct.
  • Nit: It'd be good to say that you find the rho, B and a via the algorithm in appendix B.3
• Minor comments:
  • I disagree with your statement in line 511 that causal interventions do not provide a precise notion of explanation quality - various metrics like faithfulness and completeness are used in the circuit finding literature. I'm sympathetic to complaints that these are bad metrics, but imprecise seems the wrong criticism. Most of my criticisms would be that we don't know exactly what we're measuring or how to set it up right, but it seems that similar is true for compact proofs
  • "We see this as a feature (the metric can be customized to account for variation in what we are trying to explain about the model) rather than a bug." I think this is a reasonable statement, but worth explicit discussion in the paper (or appendix if you remain highly space constrained). It sounds like compact proofs if used correctly, can be a flexible tool, but like it has a bunch of footguns if you don't set up the problem correctly, and get less interesting results than expected. This seems worth warning/instructing readers about
• My overall take is that this is an interesting paper that covers a lot of ground and does meaningful theoretical work. I'm personally not particularly optimistic about proof-based approaches to interpretability, but I'm happy to see careful and rigorous work making progress here, like this paper. I do still have concerns about this paper, notably around it being hard to read to people without significant background in this area. I will increase my score to an 8, as I consider this paper to be a meaningful contribution to the literature that I would be sad to see rejected, but would give it a 7 if that was an option, as there's still significant room for improvement on clarity of writing

Thanks a lot for the updates! I think the clarity has been substantially improved, and am happy to "update" my score from a lukewarm 8 to a wholehearted 8. I'm excited about the paper, and think this is a useful contribution to the literature.

Some notes:

• For the contributions in the introduction, contribution 1 should probably be moved to 2 or 3, I think, since it's now deprioritised to section 6.
• For the camera ready, it might be nice to add a more informal appendix giving advice to researchers trying to use compact proof-style approaches in other domains. I consider boosting such research to be the most interesting outcome of this paper, but would guess there's a bunch of tacit knowledge or more general statements that could be made, beyond what's come out of the specific setting of group composition. For example, I think a lot of the discussion in the rebuttals re whether compact proofs are a reasonable technique was valuable, and would be good to communicate somewhere.

Thank you for your thorough review!

2. The fact that the compact proofs derived in this work only get approximately a 50% success rate is concerning, as it implies that the framework using rho-sets is possibly not general enough.
3. Unifying is too strong a word to use in the title when rho-set compact proofs only work approximately 50% of the time.

We agree that we do not have a complete understanding of the ~50% of models for which we are unable to obtain nonvacuous bounds. More precisely, for these models, we cannot explain how the individual neurons together contribute to a complete algorithm (e.g. when Observation B.2.4 doesn't hold). Nonetheless, most of our observations do hold consistently. When restricting our attention to individual neurons, our observations and explanations via $\rho$-sets are consistently valid and in that case they indeed unify the observations in previous work, as shown in Section 7 and Lemma F.3. To put things into perspective, we would like to stress that the baseline explanation presented in previous work is not rigorous enough to yield any nonvacuous bound. Attempts to make it more rigorous have also yielded vacuous bounds as we discussed in the paper (Appendix C). We agree with reviewer ZpTx that this is a strength of the compact proof approach: The fact that for ~50% of models we get a vacuous bound helped us to discover that we don't sufficiently understand these specific models.

4. As someone who has familiarity with representation theory, it's still quite hard to understand the rho-set construction and specifically how it can be identified within the network. $...$ since it's unclear how you arrived at this rho-set interpretation by mechanistically inspecting the network, it's not clear how other people can use this to come up with compact proofs for other datasets.

We added section B.3 to the appendix, detailing the step-by-step process by which we discovered the rho-set circuit. We describe concrete tests that were used to validate each step, so that the reader could rediscover the circuit themselves.

1. While compact proofs are an interesting way to approach interpretability, it's unclear whether they could be used to help interpret neural network solutions for datasets where no or limited explicit information is known about the distribution it was sampled from (e.g. any language task, CIFAR-10, etc.).

Q1: Can compact proofs be used on datasets without "closed-form" solutions?

In this case you need to specify what you are trying to measure or what the dataset is that you care about. The behaviour/mechanism you try to explain typically has a specific dataset that exhibits this behaviour. So you could restrict your dataset entirely to these specific examples and, if desired, apply the brute force method for all other inputs to attain a compact explanation for the entire dataset.

For example, it may be possible to explain GPT2's Indirect Object Identification (IOI) (Wang et al. 2022) circuit within the compact proofs framework by constructing a guarantee that GPT2 outputs the correct indirect object for a large proportion of the samples in a synthetic dataset. (E.g. all sequences of the form "X and Y went to the store. Y gave a store to", where X and Y vary over all tokens corresponding to names of people.) A guarantee of this form would be over a "closed-form" distribution instead of the entire training corpus, yet would still provide a meaningful explanation of how a realistic model performs a specific task that is more precise than existing work. We believe examples such as these are interesting directions for future work.

Furthermore, we would like to make a few general comments about compact proofs.

The case of larger realistic models such as LLMs are the cases we ultimately care about -- we think of our work as proof of concept. We believe that exploring to what extent compact proofs can be scaled to more realistic settings is an important direction for future research. Less strict variants of compact proofs, e.g. using sampling or restricting to certain subsets of interest, could be a compromise that is easier to scale.

If we think of interpretations sitting on a spectrum between "worst-case" and "average-case" behaviour over the unexplained portion of model weights, most mechanistic interpretability research falls into the latter category, whereas our work covers the former. We think it is valuable to explore the other end of the spectrum and see how far one could take it.

We find that existing methods to evaluate the faithfulness or compactness of an interpretation in a rigorous and quantative way are limited and have shortcomings (see the references mentioned in the introduction). In fact, in the literature, the notion of interpretation itself is still rather vague. We believe these notions are important to make precise to establish a more rigorous science of interpretability. The compact proofs approach addresses these points, but it is not yet clear how well it will scale. This leaves the question open of how we are to measure these quantities and how we should formalize the notion of an interpretation.