Summary
This paper provides two contributions which extend previous work showing that finite-precision transformers may be expressed in FOL.
* Firstly, the authors prove that finite-precision transformers can only uniformly attend to bounded-length windows over their input sequence, with the constraints on previous theoretical work (those of Chiang et al. on finite-precision models) being too tight to model the capabilites of real models (which are capable of expressing sentences of the form $a^mb^mc^m$). This motivates them to consider log-precision transformers which are capable of attending to unbounded ranges at $O(\log n)$ precision.
* Secondly, the authors prove that the computation performed by a log precision transformer can be expressed in FO(M) logic, a variant of first order logic presupposing the typical quantifiers (universal, existential) as well as a majority quantifier (if a variable is present $\geq \frac{1}{2}$ of the entries in a set). They prove this by showing that log-precision transformers belong to computation graph families which are computable in log-uniform threshold circuits, which in-turn (leveraging existing results) are expressable in FO(M).
Alongside the proofs for the second claim, they also provide an algorithm which demonstrates how (in principle) one can express computational graph families with circuit families, by breaking up each node in the computational graph into contiguous blocks of circuit gates; also considering the case of log-uniform computation graphs.
Strengths
The paper appears technically sound, though proofs outside of the main text (those in the appendices) were not thoroughly checked (the first claim, regarding limited expressivity of finite-precision transformers, is small and was checked).
The approach taken to demonstrate the FO(M) expressibility draws on existing results from various domains and uses these to extend previous findings on logical expressivity of transformers, thus it is both quite novel and valuable. Whilst these findings remain far from useful for practical mechanistic interpretability, they serve as a useful foundation for work hoping to explore any such applications.
Weaknesses
No major weaknesses were identified.
Two minor weaknesses are:
1. The limited applicability which is only partially addressed in the section on "Mechanistic Interpretability". In particular, the size of a FO(M) sentence required to express a practical transformer would presumably be significant enough that its interpretability would be questionable at best. The authors do conjecture that quantifier depth "of at most 2" may suffice to express transformers, but this has yet to be shown. This criticism is applicable to other technical attempts to produce discrete / tree-like representations of transformers, and so is not a significant drawback, besides saying that any attempts to motivate such research from a practical perspective seem highly optimistic at present.
2. The paper is quite dense in parts, which is understandable. However, two potentially useful figures could be envisioned: 1) a high-level overview of the proof (log-precision transformers -> computational graph -> TC -> FO(M)) 2) A figure illustrating the contiguous circuit construction algorithm from $6.1
## Nitpicks
* 55: "powerful enough *to* express"
* Example 5: Seems incomplete?
* 252: "the second of which" should probably read "one of which" as it is otherwise somewhat confusing why "the second" is being specified
* 310: "without loss of generality" -> "w.l.o.g" to be consistent with previous use
* 355: "Challenging the premise of a rigid division between symbolic and neural models". The mathematical sense in which this is being challenged is quite loose, and so it is not clear that this meaningfully "challenges" the division in the way it is typically framed (in a sense, matrices are symbolic, especially if a model is quantized, but this does not make the model *symbolic* in the way a logician would find useful)
Rating
7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.
Confidence
4: You are confident in your assessment, but not absolutely certain. It is unlikely, but not impossible, that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work.
Limitations
Theoretical limits of the proofs and claims are precise and well-stated. Claims around practical applicability of these results may be slightly overstated.