A Logic for Expressing Log-Precision Transformers
Authors: William Merrill
Ashish Sabharwal
Venue: NeurIPS 2023 poster (2023)
Keywords: transformers
logic
reasoning
circuit complexity
mechanistic interpretability
TL;DR: We prove that any function a transformer computes can be expressed in first-order logic with majority quantifiers.

Abstract: One way to interpret the reasoning power of transformer-based language models is to describe the types of logical rules they can resolve over some input text. Recently, Chiang et al. (2023) showed that finite-precision transformer classifiers can be equivalently expressed in a generalization of first-order logic. However, finite-precision transformers are a weak transformer variant because, as we show, a single head can only attend to a constant number of tokens and, in particular, cannot represent uniform attention. Since attending broadly is a core capability for transformers, we ask whether a minimally more expressive model that can attend universally can also be characterized in logic. To this end, we analyze transformers whose forward pass is computed in $\log n$ precision on contexts of length $n$. We prove any log-precision transformer classifier can be equivalently expressed as a first-order logic sentence that, in addition to standard universal and existential quantifiers, may also contain majority-vote quantifiers. This is the tightest known upper bound and first logical characterization of log-precision transformers.

A Logic for Expressing Log-Precision Transformers
William Merrill New York University wil willm@nyu. edu
Ashish Sabharwal Allen Institute for Al ashishs@allenai org
Abstract
One way to interpret the reasoning power of transformer-basee language models is describe the types of logical rules they can resolve over some input text. Recently, Chiang et al. (2023) showed that finite-precist can be equivalently expressed in generalization of first-order logic. However, finite-precision transformers are a weak transformer variant because, as we show, a single head can only attend to a constant number of tokens and, particular, cannot represent uniform attention. Since attending broadly is a core capability for transformers, we ask whether a minimally more expressive model that can attend universally can also be characterized in logic. To this end, analyze transformers whose forward pass is computed in log precision on contexts of length n. We be equivalently expressed
transformer classifiers
prove any log-precision transformer classifier a first-order logic sentence that, in addition to standard universal and existential quantifiers, may also contain majority- vote quantifiers. This is the tightest known upper bound and first logical characterization log rog-precision transformers.
Any log-pree oog-precision transformer can be re-expressed as sentence in FO(M) logic, e.g.:
Mi. a()) A Mj. b(j) ^ -3k, l. (a(k) Ae<
(m a's followed by b's, i.e. 6m)
aaaabbbb
aaabbbbb x
baaaabbb X
Figure A first-order logic with majority (FO(M)) sentence for a "" In addition standard and 3 quantifiers over string indices, FO allows majority quantifiers (M) that take majority-vote across indices. a(i) indicates whether token i is (and analogously for b). We prove FO(M) can express any function computed by a log- ongprrccssinn transformer.
Introduction
The incredible success of deep learning models, especially very large language and vision transformers with hundreds of billions parameters (Brown et al., 2020; Thoppilan et al., 2022), has come the cost of increasingly limited understanding of how these models actually work and when they might fail. This raises many concerns, such as around their safe deployment, fairness, and accountability. Does the inner working of transformer defy description in simpler symbolic system that we can better understand? Or can transformer computation be described using a familiar symbolic formalism? Understanding how to view the reasoning process of a transformer in terms of logic could potentially expand our ability to formally reason about their behavior over large domains of inputs.
Chiang et al. (2023) provide partial answer to this question, showing that any transformer classifier can be expressed as sentence in a variant of first-order logic with counting
37th Conference on Neural Information Processing Systems (NcurIPS 2023).

---

quantifiers and modular arithmetic over input position indices. Specifically, counting quantifiers take the form == : ((i) where z a count variable and a position index. They show that there exists single sentence in this logic that computes the output of the transformer for any input string of any length. This a powerful result because shows that a simple logical formalism is fully sufficient to describe all the complexity of massive finite-precisin on kiitt--reecssion transformers: any function that cannot be defined in first-order counting logic with modular indexing cannot be expressed by the transformer.
transformer. It also provides an upper bound
However, Chiang et al.' 's result is not fully general because it relies on the transformer precision being fixed with respect to the transformer's ' context length. More generally, as we will demonstrate in Section 3, peeiie-preiiionn transformers are a fundamentally weak variant of transformers: crucially, cannot express uniform attention patterns, which are a core algorithmic primitive of transformers (Weiss al., 2018). In fact, we show that they can only attend to constant number of input positions, which may be seen as rather limited generalization of hard attention." For example, Chiang et al. show that their logic for finite-precision transformers cannot recognize a """", whereas in practice, transformers can (Bhattamishra et al., 2020).² This motivates studying formal model of transformers where precision grows with context length (which we formalize as tog-precision), making it possible to capture uniform attention well as other broad attention patterns. This is useful both for recognizing a a and more generally for reasoning globally over the input.
We demonstrate that log- log-precision transformer classifiers can also be expressed as sentences in simple logic: first-order logic with majority, or FO(M). over inputs strings (Barrington et al., 1990). In addition to standard existential and universal quantifiers, FO(M) has majority quantifiers that return true iff more than half the propositions they quantify are true. It also allows comparing input positions (e.g., E < l in Figure 1) and accessing their individual bits. Our main result is as follows:
Theorem (Informal version of Theorem 2). For any log-precision transformer T, there exists an (M(M) sentence é that computes the same function as T, i.e., Φ(z) = ((x) for any input string x.
Upper bound. Theorem 2 shows transformers with more than finite precision can also be expressed in a simple extension of first-order logic, going beyond Chiang et al. (2023)'s result. On the other hand, (M) is a strict superset of Chiang al. 's counting logic; it can simulate counting quantifiers (see Section 2.2) and allows non- non- modular position comparisons. Thus, handling more general class of transformers powerful enough to express uniform attention slightly weakens the bound.
Still, our result constitutes (to our knowledge) the tightest upper bound on log-precision transformers line of complexity-theoreee work analyzing the
and the first defined in terms of logic, building power of transformers (Hahn, 2020; Merrill et al., 2022; Liu et al., 2023; Merrill & Sabharwal, 2023). In particular, FO(M) strengthens the upper bound of log-space-une (2023). The refined bound adds to the limitations of transformers identified by Merrill & Sabharwal (2023): for example, it establishes unconditionally that log-precisiin precision transformers cannot compute boolean matrix permanents, and shows that, in certain formal sense, integer division and matching parentheses are among the formally hardest problems that transformers can solve (see Section 4).3
TC" by Merrill & Sabharwal
Mechanistic interpretability. Beyond providing upper bound on the reasoning problems solv- able by transformers, we believe Theorem 1 could guide the design of "transformer-complee programming languages similar in spirit to RASP (Weiss et al., 2018). RASP is declarative program- ming language designed to capture transformer computation, and Lindner et al. (2023) implement a compiler from RASP into transformers. Unlike RASP, FO(M) can provably express any transformer (Theorem 1), which we believe justifies using it (or an equivalent but more user-friendly variant) as a target language for programs extracted from transformers.
Similar to a decision tree, an FO(M) sentence has the interpretable property that each sub-sentence corresponds to constraint on input (see Figure 1). In contrast, the internal modules of a transformer or circuit do not satisfy this since they map between arbitrary latent spaces. We speculate this property
1 Hard attention is provably substantially weaker than general attention (Hao et al., 2022: Merrill et al., 2022). Technically, the empirical results of Bhattamishra et al. (2020) are for a""b"" " a harder variant of a """... 'To be clear, Theorem is one-sided: every transformer can be expressed as an FO(M) sentence, but not necessarily the other way. Moreover, we believe that many FO(M) sentences cannor be expressed by transformers. An exact logical characterization of transformers remains open problem.

---

could facilitate interpreting models by translating them to (M(M), though a careful exploration of the algorithmic and HCI aspects of this idea lies outside the current paper's theoretical scope.
Contributions. Our results shed new light on how to view the computation inside transformers in terms of logic. Specifically, our main contributions to prove the following:
Fixed-precins sxxed-precisio transformers can only attend to a fixed number of tokens, and those with precision less than log log cannot uniformly attend over length-n contexts (Proposition 1).
2. Log- og-prreciion transformer classifiers can expressed as sentences in FO(M) (Theorem 2).
2 Preliminaries: Transformers and FO(M)
Let be a finite alphabet. We denote by the Kleene star operator, i.e., for set X, X = - X". We will view transformers and (M(M) sentences both as functions from Σ - (0,1), and show that any function a transformer computes can also computed by an FO(M) sentence.
2.1 Transformers
We view the transformer precision p as function of the context length n, writing p(n) where appropriate. Let I., be the datatype of p-precision floats, i.e., tuples (m, e) where m, e are signed integers together taking p bits. Using |x] to mean the size of integer I, a float represents the value m.2" pn-22-im/+11, Following Appendix A of Merrill & Sabharwal (2023), we define p-truncated addition (+, )). multiplication (-), and division (/) over Dy We now define transformer encoder binary classifier over D,,, largely adopting Merrill & Sabharwal's notation.
Definition 1. A p-precision transformer T with heads, d layers, model dimension m (divisible by h), and feedforward width w is specified by:
1. An embedding function ó E x N -> D whose form is defined in Appendix C.1:²
2. For each S f S and < k < h, a head similarity function sf. D x D -> DDp whose form is defined in Appendix C.2;
3. For each f d and 1 S k S head value function of. Dh Wm/h whose form is defined in Appendix C.2;
4. For each < d, activation function f (I) (DZ7/hg* D + D whose form is defined in Appendix C.3 and implicitly uses the feedforward dimension w;;
5. An output classifier head ε : DD {0, 1} whose form is defined in Appendix C.4.
Definition 2. We define the transformer computation and output as function of an input x E Σ>"
1. Embeddings: For < < n, h = ((x,, 1).6
2. Self Attention: For < E 1, (multihead) self-attention block & + 1 computes
attention heads:
(+ (hi, h()
1+1 (h)), 1gg
where Z =
Σ
5k e+1
(h,, h2).
Zi,
j=1
3. Activation Block: For 0 S S d - 1, activation block E ++1 aggregates the head outputs to
produce h++,
h f+1
f f P+1
f+1 a,h h().
4. Classifier Head: The network prediction on x E Ed is x(h)).
*(101, 010) represents 1.012 222 This closer to the IEEE standard than the m 2" semantics used in Merrill & Sabharwal (2023), letting us define the minimum representable float more realistically in Proposition "Increasing the classifier's output space arity (e.g.. transformer that predicts the next token) or switching proof longer goes
causal attention of decoder-only model would not change results. However, through if decoder can generate tokens that get added the input at the next step (cf. Pérez al.. 2019).
d, like is actually function of the context length n. and Appendix C.I enforces that & is computable in Ollog n) time, standard choices of positional embeddings would satisfy.

---

We say T(x)= - x((h(,)) and LT is the language of z E E' such that T(x) - 1. We refer to 6, s/ u/, fe, and x. as the core functions in T, and to embeddings, self attention, activation, and the classifier head as the components of T. We write 0y for the concatenated vector of parameters for the functions Φ, & f", and Ki for all < S d and 1 < k S h.
We define log-precision transformer as one where is at most Ol and is a "simple" function, i.e, computable O(log n) time. In our model, the weights 0r defining ' are fixed, but the precision p used to compute the forward pass can depend on n (see Footnote 13 for generalization).
2.2 First-Order Logic with Majority
As will show, transformers can be translated into sentences in (M But what do such sentences look like? Informally, (M(M) is first-order logic extended to also have majority (M) quantifiers. Following Barrington et al. (1990), our sense of FO(M) takes strings in En as input and returns 0 or 1 to define a formal language. In this setting, quantifiers range over indices (positions) into the string. Predicates can be applied to the variables introduced by these quantifiers.
Definition 3 (FO(M) index). Indices in FO(M) are integers denoting positions in the input string:
1. The constant 1, representing the first token's position.
2. The constant n, representing the last token's 's position.
3. Strings (c.g.. i. j. k) representing variables ranging over positions to n.
4. Any index built by applying addition or subtraction to other indices.?
Definition 4 (FO(M) formula). Formulas in (M(M) are constructed follows:
1. Let > be finite alphabet. For each
and any index i, oii), e.g., a(i), is formula that
is true if the i-th input token is a.?
2. For any indices j, the formula bit(i. j) returns the j-th bit of the binary expansion of i. 10
3. For two indices i, i j. i S j. and 2 j are formulas with their conventional semantics.
4. For two formulas Φ, 20.0 A v and V tb are formulas with their conventional semantics.
5. For any formula & (which may refer to i), the following are valid formulas:
(a) Bi é means some value of i in [1, n.]] makes @ true.
(b) Vi. c means all values of i in [1, vi] make e true.
(c) Mí. & means 2 n1/2 values of in [1, n] make @ true.
We use parentheses where necessary to disambiguate the order of operations. General formulas may contain free (i.e., unbound) variables: e.g., Vi. i = j. A sentence is an (O formula 6 with no free variables. Sentences represent functions from from Σ' to {0, 1} and thus define a formal language."
Extensions. Beyond Definition 4, FO(M) can express counting and threshold quantifiers in terms al., 1990). Given a formula d, a counting quantifier creates new formula : e that is true iff Φ is true across exactly k values of i. Threshold quantifiers 3s and 32 work similarly but check if Φ is true for at least or most k values of i. In addition, show in Appendix A that (O(M) can express conditional majority quantifiers, which create a formula Mi o [ that is true iff &b true for at least half the values of that make & true.
of majority quantifiers (Barrington
2.2.1 Examples
To illustrate the formalism, we provide example languages definable in FO(M) with Σ = (a. First, we show two languages that do not require majority quantifiers express:
Example 1 (Bigram matching). Strings containing the bigram ab: 3i [a(1) A b(i + 1)]
Example 2 (Skip-bigram matching). Strings containing the long-distance pattern a... (cf. "induc- tion heads" of Elhage et al. 2021): 3i [b()) A 3j [j < i a[j]]]
Barrington et al. (1990) did not introduce this as a primitive, but it can be simulated using the < predicate. 'We write parentheses to indicate the order of operations.
'Barrington et al. (1990) define Qi()) for b E (0, 1}. We generalize this to an arbitrary vocabulary > by assuming each token is mee-hot-encoded a (i) Q1(12 + s) where is the index of in the vocabulary.
"This predicate included in the logic technical reasons; see Barrington et al. (1990).
One can also take multiple sub- sentences within @ to be labeled as ordered outputs, thus allowing @ to be function from E¹ (0, 1)ah for some fixed constant k.

---

In contrast, Example 3 is a simple example that requires majority quantifiers (Furst et al., 1984):
Example 3 (Majority). Strings with more b's than a's: Mi [b(i]]
Figure I showed how (M) can be used to recognize patterns like am''". A similar idea can be used to model parentheses matching (Barrington et al., 1990):
Example 4 (1-Dyck). The well-balanee parentheses language (with opening and closing):
Vi. (3a, b. (F* : a(j) Aj s 1) A ( b(j) ^j < Ab S a)) A Mi. a(i) A Mj. b(j)-
Example 5 (Integer Arithmetic). Iterated addition (i.e., summing n n-bit numbers), iterated multipli- cation, and division (Hesse, 2001) can all be expressed in FO(M).
3 Finite Precision Transformers Cannot Attend Universally
Attention heads that spread attention weight uniformly across inputs have been observed in trans- former LMs (Merrill et al., 2021) and make soft attention fundamentally more powerful than hard attention (Hao et al.. 2022: Merrill et al., 2022). In particular, uniform attention an important primitive that transformers can use to solve tasks involving counting (Bhattamishra et al., 2020; Chiang et al., 2023), taking majority votes (Merrill et al., 2022), and matching parentheses or sorting (Weiss et al., 2021). A transformer with sufficient precision can easily implement uniform attention by setting the keys and queries across all positions be constant. However, attention heads with finite precision cannot represent uniform attention over long sequences as a consequence of the following:
Proposition 1. Let a E TR" S.I. Σi= a; = and à its nearest p-precision float approximation.
1. Then the number of nonzero entries of å is upper bounded by its precision: specifically, à has most 22 nonzero entries.
2. Moreover, if p < log log and a is uniform (i.e., = 1/n), then à = Ō.
Proof. The smallest positive value representable by a p-precision float is 2 (pmmm -2+2Pe11) which is bounded below by 2-2"+1 Letting k 2"" it holds that 2 2-2"+1 = 2/k. So if ā; gets the minimum value, then a; 2 1/k. Since E, ag = 1, there can be at most A indices satisfying this property. This implies there can be most l: nonzero entries in ā. If k and is uniform, 1/n is less than half of the minimum representable value of 2/k: Thus, 0.
Proposition says that attend over bounded-length windows, making them similar to hard-attention transformers (Hao et al., 2022). Morever, they cannot compute uniform attention over contexts of length n with less than log log n precision. This explains why Chiang al. (2023) prove finite- tette-preeision transformers provably cannot recognize am"" while in practice transformers have been shown to learn even its harder variant a "m c even with long context lengths (Bhattamishra et al., 2020), In essence, their upper bound only applies in the asymptotic regime when n 22".
transformers are artificially limited because they can only
In contrast, transformers in practice have enough precision both to compute uniform attention and recognize " on practical context lengths. More concretely, the 6 representation allows uniform attention over 26+2 10 tokens and normal 16 allows 210+2' as 10 tokens, both well above the typical context window of transformers. This motivates a formal model of transformers with enough precision to compute uniform attention and recognize languages such as a="".
4 Main Result: Expressing Log-Precision Transformers in FO(M)
By Proposition 1, precision must grow with the context length n (p > log log n) for transformer to compute uniform attention and other attention patterns with unbounded range, like practical transformers. In this paper, analyze any transformer with up Olognn precision. We show that any function computable by log precision transformers can be expressed in FO(M):
We account for the division of p into and Pe rather than treating them together. Our minimum value differs slightly from numpy but is the same order of magnitude. Moving to float8 lowers the length upper
bound for uniform attention 23+2² zu 2048, which suggests float8 LMs will have limited length generalization.
5

---

Theorem 2. Let T be a pre-preciioon transformer with a parameter vector 0T fixed for all context lengths n. Then, there exists an FO(M) sentence & that computes the same function as T, i.e. ((x) = (1) for any input string
Theorem 2 is the tightest known upper bound for log log- preciieciiion transformers and shows that it is still possible to characterize transformers in a simple variant of first-order logic even with log- precision and uniform attention. As alluded to earlier, Theorem immediately implies that any problem complete for FO(M) (or a larger class) is also transformer-hard. Since integer division and Dyck language membership follows, perhaps surprisingly, that the entire computation of any transformer on input can be reduced single integer division finite number of Dyck-language queries:
known be coo (Hesse, 2001; Aaronson et al., 2022), it
Corollary 2.1. Let T be a transformer satisfying Theorem 2. For any input x, there exist first-order definable integers a, b, and i (dependent any x, there also exist forst-order definable strings W1, Wm such that ((x) is forstorder definable in terms of the membership of the w, 's in k-Dyck.
T and x)) such that ((x) equals the i-th bit of La/b]. For
5 Preliminaries for Proving Theorem 2
5.1 Computation Graphs
A compulation graph G over a datatype D S {0, 13* and countable set of primitive functions
3 C D D is a directed acyclic graph where:
1. Each node is labelled by a node type: function f E 3 computed by this node.
2. Each edge represents value ID flowing as output from one node into another node. We consider the edges flowing into node j to have an order, i.e., be numbered.
3. & contains the special symbol input, which designates k nodes as input nodes. We refer as the arity and assume w.l.o.g. that nodes O..... h-- 1 are inputs."
4. A single node taken as the output node (w.l.o.g.. g., the node with the largest index).
A computation graph G of arity k parameterizes function D - ID in the standard way: the input nodes assigned the input values, and the value of each node is computed (traversing the graph in bottom-up topological order) as function of the values of its children until the output node receives value. The value of the output node is considered the output of the function. It worth noting that computation graphs can only process inputs of bounded length. To process arbitrary-length inputs, we will need to generalize them computation graph families (Section 5.2).
For a computation graph G. size(G)) is the number of nodes, depth(G) is the length of the longest path from input node to the output, and arity(G, i) is the number of inputs node i.
Threshold circuits. threshold circuit special case
computation graph where D {0. 1} and F is the set of threshold functions of the form IçA and Aza over IDD", defined as follows: (z)(z)= = 1 if E. o < A and otherwise; 0 (x) is defined analogously. Typical AND, OR, and NOT gates are a special case of threshold gates, as is an IDENTITY gate.!
We allow nodes with the A 2 1 largest indices to all be designated as (ordered) output nodes. A threshold circuit with arity A and k' output nodes will thus be function from {0, 1 to {0, 1 This will be convenient when simulating neural network components that output multiple bits.
We will find it useful to consider threshold circuits as kind of compilation target for computation graphs: in other words, we will be concerned with simulating computation graphs defined over more complex functions and data types into threshold circuits.
5.2 Computation Graph Families
A computation graph family over IB and is mapping from E N to computation graph Gn, for processing inputs of size n. Thus, G defines a function from D - D, where G(x) = (.).
Theeoemm2 2 can also be extended to apply to log precissnn transformers with log-uniform weights, i.e., where 0 can grow in size and precision with n (see Appendix B).
MB convention in computer science, we computation graph nodes be zero-indexed.
For more background on threshold circuits, Merrill & Sabharwal (2023) and Merrill et al. (2022).

---

Intuitively, computation graph families are useful because they generalize computation graphs to define functions over unbounded -lengd strings as inputs.
Size, depth, and arity. For computation graph families, the size, depth, and arity become functions of the input length sizeg(1) (n) = size deptt ş (n) = depth(Gn), arity (n. = arity(Gn::)) i).
Uniformity. The infinite set can be alternatively represented by two functions:
1. nodeg (n, i), which returns the type of node i in G, if S Size(G,),, ) and @ otherwise. For example, node i computes the logical AND of its imputs, then nodeg [m, =
2. edgeg (n. i) which returns the argument index of i into node if G, contains an edge + J and -1 otherwise. edge, (n, (n,,,, i.j) only needs be defined over i.j size(G,,). For example, if G, contains node j with three incoming edges, the second of which comes from node i, then edgeg(n, (n, i.
pair of algorithms implementing these two functions uniquely specifies a computation graph family, it enables building the computation graph G,, for any n. Uniform computation graph families (generalizing uniform circuits; cf. Arora & Barak, 2009) are families where nodeg and edgeg can be computed efficiently, i.e., under some constraints on space or time:
Definition 5 (Uniformity). A computation graph family G is T(n)--uiffrm iff nodeg i) and edgeg(n, i, can be computed by a deterministic Turing machine in time T(n). We focus on log-uniform computation graph families: i.c., where [n) = Ologn)).
Threshold circuit families. These are simply families threshold circuits. We will be simulating computation graph families with threshold circuit families. Log-uniform TC is the class of languages recognized by log-uniform constant-depth, poly-size threshold circuit families. See Merrill & Sabharwal (2023); Liu et al. (2023); Arora & Barak (2009) for more background on TC and circuits.
Proof of Theorem
The idea is simulate a transformer with log-uniform TC circuit family. Since log-uniform TC" FMM, this would imply any transformer can be expressed in FO(M). First, we note that transformers are log-unifore computation graphs:
Lemma 1 (Proof in Appendix B.1). A transformer T is a log-uniform computation graph family and oulput components.
where & contains embedding, self-attention, feedforward, fereettention.feefoovwrrll
Further, each core module of the transformer can be simulated by a log-uniform TC circuit family:
Lemma (Proof Appendix B.2). Let T be log-precision transformer with fixed parameters 0y. Then each component
computable in log-uniform TC
Intuitively, we can now simulate a transformer in -oi-urrfom TCº by just simulating each of its components with a threshold circuit and routing their inputs and outputs appropriately. However, we will need two more technical conditions to verify that this construction indeed log-uniform:
Lemma 3 (Proof in Appendix B.3). Let T be a log-precision transformer with fixed parameters 0T. There exists a function bsize(n) that is power of 2 and computable in O(logn) time s.f. size=(n) & bsize(n) for all F E 3.
Lemma 4 (Proof in Appendix B.4). If is a log-uniform TC family and sizez(n) I bsize(n). (x) for all a and sizez bsize(n).
there exists log-uniform TCº family F' s.I. F(x)= FF)))
Combined, Lemmas 3 and 4 show that each F E $ is computable by log-uniform TC family with size bsize(n)) that is power of 2 and computable time (log n). We will show these conditions imply a transformer T can be simulated by a TC family (Theorem 3) and moreover that C is log-uniform (Corollary 3.2). By the equivalence of log-uniform TC" and FO(M) (Barrington et al., 1990), we then conclude that any log- log-rricision transformer can be expressed in FO
Past work (Merrill & Sabharwal, 2023) analyzes transformers with a similarly named but weaker notion of uniformity, namely log-space (rather than log-time) uniformity.
7

---

Algorithm nodec(n. i) Return the type of gate i in circuit Cn.
Algorithm 2 edgec(n,i,))
Cn contains an edge -> j. return the argument number of that edge. Otherwise, return -1.
1: F <- nodeg (n, bnode(n,,)) i))
1: i' K bnode i)
2: if * then
2: j' +- bnode (n,
3: return nodez(n, bstart(n, 1')
3: 8: f bstart m,
4: else return 0
4: 8 f bstart m. j')
5: i' j' then
6: J < node (n, 1')
7: return (n, Sis - 85)
8: else if edgeg 2', 2 0 then
9:
b, + i - (s, bsize(n, d') p(n))
10:
by b- (s, p(n) edgeg (n. j'))
11:
if; =b < <((n) then return j $j
12: else return -1
13:
else return -1
6.1 Simulating Computation Graph Families with Circuit Families
We give algorithms that take a computation graph family and define a circuit family simulating it. Intuitively, the algorithms creates contiguous blocks of circuit gates simulating each node in the computation graph and route inputs and outputs between blocks appropriately.
Block mapping. This algorithm depends block mapping, which is an implementation of the following three functions:
1. The block node bnode(n, i): the index of the node that gate i's block is simulating,
2. The block start bstart(n, i'): the smallest gate index in the block simulating node i'.
3. The block size bsize(n, i'): the number of gates in the block simulating node i'.
Further, we enforce that valid block mapping must satisfy that, for all i, with i' bnode i), bstart(n, i') S i < bstart(n, E') + bsize(n, i').
Let G be a computation graph whose primitive functions are computable by log-uniform threshold circuits. We can identify each primitive function with a log-uniform threshold circuit family F that computes it, where the first arity, (n)) gates are IDENTITY gates reserved for taking input. For such graph, nodeg can be taken to return symbol identifying circuit family F. In this case, our algorithm requires that, for all i', the block size of must match the size of the circuit for the type of block i", i.e., bsize(n,, i') = sizenodeg (n.5r)(1)) (1t). These properties let us meaningfully identify graph node i' with block of nodes that will simulate it. This intuition enables us to develop Algorithms 1 and for constructing uniform threshold circuit family from a uniform computation graph family.
Theorem 3. Let G be a computation graph over a finite set of node types 3. where each F E $ is specified by log-uniforn circuit family. Let bnode, bstart, and bsize be valid block mapping in the sense above. Then Algorithms and define circuit family C such that
1. C and G compute the same Dj + D function (let the final p gates of each C2 be its output).
2. (n) I depthg (n) = y
3. sizec(n) I sizeg(n) (n). max, size
Proof. Assume w.l.o.g. that the gates of C are topologically ordered. We show by induction over circuit gates) j (with bnode(n., j)) that:
1. For all i' <." the last nodes of block i' store the value of node i'.
2. For all i such that bstart(n, j¹) <i S j. gate i of C (as a function of the input nodes of j') computes gate i bstart(n, n. j') of nn.
Base case. We have two circuits with gates, the premises are trivially satisfied.
Inductive case. Assume the premises hold up to j. We will show they hold for j + 1. Let T nodeg(n.)) j'). By Premise 1, we know that the last p nodes of block i' store the output of node i', for
8

---

j' By Algorithm 2. for each i' such that edge i' with 0 S k < xrity,(()) gates kp through k(p+ + 1) of block j' will copy the final p gates of block i'. Thus, the first h arity (n)) gates of block j' store the inputs to node j'.
At this point, we use Premise 2 conclude that the first j bstart(n, gates of block j' compute the same function as the first) j bstart(n, j') gates of F with respect to this input. Thus, we just need to show that gate j + 1 is also correct. Within Algorithm that gate j + 1 of block j' gates the same inputs as gate j + 1 of F. By Algorithm 1, the type of gate j + 1 in block j' is the type of gate j + of F. Thus, gate j + in block j' computes the same function of the input gates as gate + 1 in F. If j + 1 = bsize(n. n. j'), we conclude that the final gates of block j' store the output of node j".
we fall in case i' = JJ. meaning
Let XC" denote any family of constant-depth, poly-size circuits, including AC and TC
Corollary 3.1. Let G be a constant-depth, poly-size computation graph family over a fonite 3. If every node type in B can be computed by XC circuits, the function computed by G is in XC".
Since transformer has constant depth and polynomial size, Corollary 3.1 lets us easily recover prior results about hard-attention transformers (Hao et al., 2022: Hahn, 2020) and saturated attention transformers (Merrill et al., 2022) using a common framework. All one has to do is show that all individual node types in such transformers can be computed by AC and TC circuits, respectively.
Corollary 3.1 established that Algorithms 1 and 2 construct circuit family that simulates G. With the right block mapping, C will be log- log-uniform as long as G and its node types are log-uniform. Corollary 3.2. Let G be log-uniform, constant-depth compulation graph family over a finite 3. where each F E 3 is specified by a fog-uniform TC family with size=(n) (n) = bsize(n) that is a power 2 computable in O(log n) time. Then G can be simulated by log-uniform TC family C that obeys the size and depth properties of Theorem 3.
Proof. Let C be the circuit family defined by Algorithms 1 and 2 given G and the following block mapping: bnode(n, i) li/bsize(n)) bstart(n, :') = i' bsize(n), bsize(n, i') = bsize(n2). Since bsize(n) is power of 2, bnode and bstart are reducible to left and right shifting over O(log n)- bit integers, which can be implemented in O(log n)) time. Thus, each block mapping function is computable in time O(log n). Since nodeg and edgeg are juej calling functions computable in time Ollog n) with constant overhead, we conclude that C, the circuit family they define, log-uniform, and it is already known to simulate G with constant depth and polynomial size by Theorem 3.
7 Conclusion
We proved that any log-precision transformer classifier can be translated an FO(M) sentence that computes the same function (on all inputs of any length). This result comes by first simulating a transformer with a highly uniform threshold circuit family, and then leveraging the established equivalence of log- uniform circuits and FO(M). Transformers and other neural nets are often discussed in contrast with symbolic models based on logical formalisms (Garnelo & Shanahan, 2019)-an immediate implication of our result is that it is possible to express the inner workings of transformers also in a simple logic, challenging the premise of a rigid division between symbolic and neural models. Our results also provide the tightest known upper bound on log-precision transformers.
While it is striking that a full transformer can be translated (M(M), we believe the bound is not tight. In particular, we conjecture that it is possible to simulate any transformer with an FO(M) sentence of quantifier depth of at most 2, which could be proven by establishing a hierarchy theorem describing the FO(M) quantifier depth needed simulate a T TC family of a certain size. It would also be an interesting extension to translate real transformers to FO(M) sentences. In this sense, we believe our results provide a theoretical foundation to guide mechanistic interpretability work (cf. Weiss et al., 2021; Lindner et al., 2023).
sentence in a logic as simple as
Our findings provide a novel view into transformer classifiers and their limits. It would be exciting for future research to extend our results to account for other common practical uses of transformers, such for long-form generation, chain-of-thought reasoning, and in-context learning.
Formally, 3 just needs contain and
9

---

Acknowledgments
We thank Paul Beame, David Chiang, anonymous reviewers, and researchers at the Allen Institute for Al for feedback. WM was supported by an NSF graduate research fellowship and in part by NSF award 1922658.
References
Aaronson, S., Kuperberg, G., and Habryka, O. TC Constant depth threshold circuits, 2022. URL Zoo: T#tc0.
Arora, S. and Barak, B. Computational Complexity: A Modern Approach. Cambridge University Press, 2009.
Barrington, D. A. M., Immerman, N., and Straubing. H. On uniformity within NC Journal of Computer and System Sciences, 41(3):274-366, 1990.
Bhattamishra, S., Ahuja, K., and Goyal, N. On the ability and limitations of transformers to recognize formal languages. In EMNLP, 2020.
Brent, R. P. and Zimmermann, P. Modern computer arithmetic, volume 18. Cambridge University Press, 2010.
Brown, T., Mann, B., Ryder, N., Subbiah, M., Kaplan, J. D., Dhariwal, P., Neelakantan, A., Shyam, P. Sastry, G., Askell, A., Agarwal, S., Herbert- Voss, A., Krueger, G., Henighan, T., Child, R., Ramesh, A., Ziegler, D., Wu, J., Winter, C., Hesse, C., Chen, M., Sigler, E., Litwin, M., Gray, S., Chess, B., Clark, J., Berner, C., McCandlish, S., Radford, A., Sutskever, and Amodei, D. Language models are few-shot learners. In NeurlPS, 2020.
Chiang, D., Cholak, P., and Pillay, A. Tighter bounds on the expressivity of transformer encoders. ICML, 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:/transffomeerccrniiti
Furst, M. I., Saxe, J. B., and Sipser, M. Parity, circuits, and the polynomial-time hierarchy. Mathe- matical systems theory, 17:13-27, 1984.
Gareel,, M. and Shanahan, M. Reconciling deep learning with symbolic artificial intelligence: representing objects and relations. Current Opinion Behavioral Sciences, 29:17-23, 2019. ISSN 2352-1546.
Hahn, M. Theoretical limitations of self-attention neural sequence models. TACL, 8:156-171, 2020.
Hao, Y.. Angluin, D., and Frank, R. Formal language recognition by hard attention transformers:
Perspectives from circuit complexity. TACL, 10:800-810, 2022.
Hesse, W. Division in uniform TC In International Colloquium on Automata, Languages, and Programming, pp. 104-114. Springer, 2001.
Hunter, P., Bouyer, P., Markey, N., Ouaknine, J., and Worrell, J. Computing rational radical sums in
uniform TCO. Foundations of Software Technology and Theoretical Computer Science, 2010.
Lindner, D., Kramár, J., Rahtz, M., McGrath, T., and Mikulik, V. Tracr: Compiled transformers as a laboratory for interpretability. arXiv, abs/2301.05062, 2023.
Liu, B., Ash, J. T., Goel, S., Krishnamurthy, A., and Zhang, Transformers learn shortcuts to automata. In ICLR, 2023.
10

---

Merrill, W. and Sabharwal, A. The parallelism tradeoff: Limitations of log-preee log-precision transformers. TACL, 11:531-545, 2023.
Merrill, W., Ramanujan, V., Goldberg, Y., Schwartz, R., and Smith, N. A. Effects of parameter norm growth during transformer training: Inductive bias from gradient descent. In EMNLP, 2021.
Merrill, W., Sabharwal, A., and Smith, N. Saturated transformers constant-depth threshold circuits. TACL, 10, 2022.
Pérez, J., Marinković, J., and Barceló, P. On the Turing completeness of modern neural network architectures. In ICLR, 2019.
Thoppilan, R., Freitas, D. D., Hall, J., Shazeer, N. M., Kulshreshtha, A., Cheng, H.-T., Jin, A., Bos,
T., Baker, L., Du Y., Li, Y.. Lee, H., Zheng, H., Ghafouri, A., Menegali, M., Huang, Y., Krikun, M., Lepikhin, D., Qin, J., Chen, D., Xu, Y., Chen, 7.., Roberts, A., Bosma, M., Zhou, Y., Chang, C.-C., Krivokon, I. A., Rusch, W. J., Pickett, M., Meier-Hellstern K. S., Morris, M. R., Doshi, T., Santos, D., Duke, T., Søraker, J. H., Zevenbergen, B., Prabhakaran, V., Díaz, M., Hutchinson, B., Olson, K., Molina, A., Hoffiman-John, E., Lee, J., Aroyo, L., Rajakumar, R., Butryna, A., O., Fenton, J., Cohen, A., Bernstein, R., Kurzweil, R., Aguera-Arcas B., Cui, C., Croak, M., Chi, E., and Le. Q. LaMDA: Language models for dialog applications. ArXiv, abs/2201.082 00122900,0899, 2022.
Lamm, M., Kuzmina,
Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L.,, Gomez, A. N., Kaiser, L. u., and Polosukhin, I. Attention is all you need. In NeurlPS, 2017.
Weiss, G., Goldberg, Y.. and Yahav, E. On the practical computational power of finite precision RNNs for language recognition. In ACL, 2018
Weiss, G., Goldberg, Y., and Yahav, E. Thinking like transformers. /CML, 2021.
Xiong, R., Yang, Y. He, D., Zheng, K., Zheng, S., Xing, C., Zhang, H., Lan, Y., Wang, L., and Liu, T.-Y. On layer normalization in the transformer architecture. In ICML, 2020.


Reviews:
[{"review_id": "RNVTMcpwsO", "reviewer": "Reviewer_27Gc", "summary": "In this paper, the computational power of transformers is studied subject to floating point precision and related to that of first-order logic. In particular, the authors show that (1) fixed-precision is not sufficient to compute uniform attention for arbitrary context lengths and (2) log-precision can be simulated by first-order logic with majority. The latter is shown by establishing that log-precision transformers can be simulated by a family of log-uniform circuits which is known to be equivalent to first-order logic with majority.", "questions": "- Is there a straightforward argument that generalizes the results for decoder architectures or are the results in fact limited to encoder architectures?\n- In the conclusion the threshold circuit family is referred to as highly uniform. What is the meaning of highly in this context?\n", "limitations": "- The definition of the transformer resembles the encoder part of the full transformer architecture. If the results do not generalize to the transformer decoder this should be addressed as a limitation.", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- Some of the existing theoretical results on the computational power of transformers seem to only partially support observations in practice. For example, it has been shown that the language $a^nb^n$ provably can not be recognized by a fixed-precision transformer while experiments indicate the opposite. The paper contributes to better understanding this gap by deriving theoretical results for log-precision transformers that seem to resemble observations in practice although practical implementations are in fact fixed-precision.\n- While the expressive power of log-precision transformers has been characterized by first-order logics in previous work, the paper established the tightest bound so far.\n- The extensive use of transformers and language models in formal domains such as programming languages and theorem proving makes the connection between transformers and formal logics particularly interesting.\n", "weaknesses": "- The role of positional encoding is not discussed in the analysis. Yet, fixed-precision and log-precision has direct implications on the ability to represent a positional encoding.\n- Merrill & Sabharwal (2023) show that a log-precision transformer can be simulated by a uniform $TC^0$ circuit family which at first seems fairly similar to the result in this paper. Merrill & Sabharwal bound space and prove the result for logspace-uniform $TC^0$ whereas in this paper the authors bound time and prove the result for log-uniform $TC^0$. I think this is not obvious and making it more explicit would help to understand the contribution of this paper.\n- No definition of circuit complexity is given in the paper. \n", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your review! We’d like to address some of your comments and suggestions around the role of positional encodings, different notions of uniformity, and other aspects of the paper.\n\n## Positional encodings\n\n> The role of positional encoding is not discussed in the analysis. Yet, fixed-precision and log-precision has direct implications on the ability to represent a positional encoding.\n\nAs discussed in C.1, our results go through for any positional embeddings that are log-precision and computable in time O(log n) (where n is seq length) as a function of the natural number i representation position. Because it takes O(log n) bits to uniquely specify a natural number in the range [0, n], these assumptions are met for any natural type of positional encoding. We will better highlight the role of positional encodings in Section 4.\n\n## Logtime vs. logspace uniformity\n\n> Merrill & Sabharwal (2023) show that a log-precision transformer can be simulated by a uniform circuit family which at first seems fairly similar to the result in this paper. Merrill & Sabharwal bound space and prove the result for logspace-uniform whereas in this paper the authors bound time and prove the result for log-uniform. I think this is not obvious and making it more explicit would help to understand the contribution of this paper.\n\nThanks for the feedback! We will clarify the distinction when we introduce logtime-uniformity in the Preliminaries.\n\nRelatedly, you asked what we mean by “highly uniform” in the conclusion. We are simply referring to logtime-uniform as opposed to logspace-uniform, which we will clarify. We say “highly uniform” because logtime uniformity is so strong that it collapses circuit families to logical formulas, meaning there is just a single description of the computation for any input size.\n\n## Other questions\n\nWe will add some high-level background on circuit complexity as well as references to standard texts at the beginning of the preliminaries section.\n\n> Is there a straightforward argument that generalizes the results for decoder architectures or are the results in fact limited to encoder architectures?\n\nThis is a good question that we have also been thinking about recently. There is not a simple result or corollary that holds for decoder-models, but it is possible to use these results as a tool to obtain a different upper bound for decoder architectures. As this is quite involved in its own right it is out of scope for this paper, but it forms the basis of our current follow-up research.\n"}, {"review_id": "unk8c1xaPH", "reviewer": "Reviewer_kdtb", "summary": "The paper presents a theoretical analysis on the expressiveness of transformer-based models. In particular, the authors have managed to prove that the any log-precision transformer is equivalently expressible as normal first-order logic plus majority-vote quantifiers, FO(M). This yields the tightest known upper bound of log-precision transformers.", "questions": "Minor:\n- Figure 1 on page 1 is admittedly a great motivation example but we don't know the exact meaning of an and b until page 4. It is perhaps a good idea to shed more words about Figure 1 earlier.\n- line 80, 'atend'", "limitations": "The authors have adequately addressed the limitations.", "rating": 7, "confidence": 3, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "The result is of significant theoretical interest and can potentially bridge well-studied first-order logic and widely used transformer architecture (e.g., via mechanistic interpretability work). The paper is nicely structured and with well crafted examples. To the best of my knowledge, I don't see major gaps in their proof derivations.", "weaknesses": "I don't see any significant weakness in this paper.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thanks for your review! We appreciate that you found our work to be of theoretical interest. As you suggest, we will clarify the notation used in Figure 1 in the caption so that it is more self-contained."}, {"review_id": "swGQDPvoqF", "reviewer": "Reviewer_NeeV", "summary": "This paper provides two contributions which extend previous work showing that finite-precision transformers may be expressed in FOL. \n* 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.\n* 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).\n\nAlongside 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.", "questions": "None", "limitations": "Theoretical limits of the proofs and claims are precise and well-stated. Claims around practical applicability of these results may be slightly overstated.", "rating": 7, "confidence": 4, "soundness": 4, "presentation": 3, "contribution": 3, "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). \n\nThe 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. \n\nTwo minor weaknesses are:\n1. 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.  \n2. 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\n\n## Nitpicks\n* 55: \"powerful enough *to* express\"\n* Example 5: Seems incomplete?\n* 252: \"the second of which\" should probably read \"one of which\" as it is otherwise somewhat confusing why \"the second\" is being specified\n* 310: \"without loss of generality\" -> \"w.l.o.g\" to be consistent with previous use\n* 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)\n", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your review! We appreciate your suggestions for making the paper less dense. If accepted, we will add a high-level overview of the proof toward the end of Section 4, as you suggest. A figure illustrating the Algorithm from 6.1 would also be nice if space permits - we will consider whether it is possible to add this without pushing too much other important content to the appendix.\n\nRegarding the potential interpretability limitations, we agree that a very large/deep logical formula on its own wouldn’t help anyone better understand a transformer (although it could enable finding meaningful substructures or facilitate formal verification). Therefore, we think that the quantifier depth of FOM formula is quite important for its interpretability, and are actively thinking about a depth-2 / low-depth FOM simulation as a follow-up.  (see also response to R4)"}, {"review_id": "Ata8YczzDZ", "reviewer": "Reviewer_ihd9", "summary": "In this submission, the authors generalize an expressivity result of transformers from Chiang et al. (2023), who showed that finite-precision transformers can be equivalently expressed in a counting generalization of first-order logic. In the paper at hand, the authors generalized this result that log-precision transformers, i.e., that scale with the input size, are expressible in First-order logic with majority votes, FO(M). This formalism is needed to express uniform attention patterns, to, for example, express counting languages such as a^m b^m. The authors provide a well-written introduction to the topic and rigorous proof.", "questions": "- I wonder how the claim that uniform attention is necessary relates to the findings of “ALiBi” of Press et al. (ICLR, 2022)? \n- What are the author’s opinions on the next steps to tighten the bound further? \n- Would you consider moving Lemma 2 to the main part of the paper? What are your opinions on that?", "limitations": "The bound is not tight. The missing tightness of the provided bound would have deserved its own section or a more involved explanation. It is only partially touched on at the end of the conclusion.\n", "rating": 7, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- A novel bound for the expressive power of transformers, which generalizes previous results; the problem is interesting to the NeurIPS community. Transformers are ubiquitous.\n- The paper is well written; the transformer formalization and FO(M) is well-explained with the NeurIPS community in mind. Examples are provided (section 2).\n- Intuition paragraphs are provided after the main results and parts of the proof (second half of the paper), making it ok to follow.", "weaknesses": "- Although not necessary for this type of theoretical work, there would have been room to conduct some interesting experimental results to visualize and empirically analyze the authors claims\n- The most important lemma (I feel), Lemma 2, is moved to the appendix and scattered across multiple sections there with little intuition given. The reviewer found this the most interesting part and more important for understanding the proof than section 6.1, as the simulation is straight forward.\n", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your review and questions!\n\n> Would you consider moving Lemma 2 to the main part of the paper? What are your opinions on that?\n\nWe appreciate this point and agree that having some discussion of the Lemma 2 proof in the main paper could give more intuition about why the result at large goes through. The reason we originally put Lemma 2 in the appendix is because its full proof is really quite large: there is a separate sub-lemma for each transformer component in Section C. We thus don’t think we can fit the full proof in the main paper. Perhaps a good middle ground would be to add a paragraph giving a proof sketch of Lemma 2 in the main paper, and then refer the reader to the appendix for the details about each component.\n\n> What are the author’s opinions on the next steps to tighten the bound further?\n\nWe believe a promising direction would be to analyze the width of the circuit required to simulate a transformer. Intuitively at least, we believe there should be a connection between the circuit  width and the quantifier depth of an equivalent FO(M) formula. Working out the details here could allow us to say something like “any transformer can be simulated by an FO(M) formula of quantifier depth at most d” (for some constant d).\n\nAt the same time, it could be interesting to conduct some experiments on the ability of transformers to learn different formal languages definable in FO(M). Varying crucial properties like the quantifier depth could generate hypotheses about which problems within FO(M) may be out of reach for transformers.\n\n> I wonder how the claim that uniform attention is necessary relates to the findings of “ALiBi” of Press et al. (ICLR, 2022)?\n\nGood question! Under ALiBi, the positional bias in principle will introduce some deviation from uniform attention, although we believe the deviation can be quite small. This is because the parameter norm of the network will likely grow over time (cf. [Merrill et al., 2021](https://arxiv.org/abs/2010.09697)) and the magnitude of qk will scale roughly quadratically in the parameter norm. It follows that the magnitude of qk can dominate the positional bias term of AliBi, especially for the heads with a low value of m (cf. AliBi paper, Section 3). We thus think it is possible to closely approximate uniform attention with AliBi, even if there will be some slight deviation from it.\n"}]

Author rebuttal:

Meta-review: The reviews are unanimous in favor of acceptance. First of all, this is an important question. Since the take-off of large language models, whether and how they can reason becomes sort of a mystery. Some prior work focuses on the revelation of some of their properties through empirical investigation. Yet, principled theoretical analysis is relatively scarce. The conclusion of this paper is interesting that LLMS describe logical rules and its inference is equivalent to resolution over those logical rules. The simplification made in this paper is reasonable. We have decided to recommend this one for poster presentation. Yet, after discussion we believe still there is room for improvements. More discussion regarding related work would present readers with a more comprehensive understanding about how to understand this paper’s insight against the backdrop of other theoretical work. For example, now some paper thinks LLMs are similar to Turing machines, and some papers thinks LLMs construct “templates” for reasoning implicitly, which are similar to logical rules. Maybe the discussion would go over the page limit. But considering it in the appendix is a plus. Secondly, we would like this paper to have a more comprehensive discussion in the future work. There is still some aspects in the LLMs that are left out in this paper. For example, the prompting mechanism. Can we extend the results here? Of course, the suggestions regarding this paper’s notation and presentation is also hugely recommended to be incorporated.
Decision: Accept (poster)