Transformers Implement First-Order Logic with Majority Quantifiers
Authors: William Merrill
Ashish Sabharwal
Venue: Submitted to ICLR 2023 (2023)
Keywords: transformers
complexity theory
logic
interpretability

Abstract: Characterizing the implicit structure of the computation within neural networks is a foundational problem in the area of deep learning interpretability. Can their inner decision process be captured symbolically in some familiar logic? We show that any transformer neural network can be translated into an equivalent fixed-size first-order logic formula which may also use majority quantifiers. The idea is to simulate transformers with highly uniform threshold circuits and leverage known theoretical connections between circuits and logic. Our findings also reveal the surprising fact that the entire transformer computation can be reduced merely to the division of two (large) integers. While our results are most pertinent for transformers, they apply equally to a broader class of neural network architectures, namely those with a fixed-depth uniform computation graph made up of standard neural net components, which includes feedforward and convolutional networks.

Under review as a conference paper at ICLR 2023
TRANSFORMERS CAN BE TRANSLATED TO FIRST- ORDER LOGIC WITH MAJORITY QUANTIFIERS
Anonymous authors Paper under double-blind review
ABSTRACT
Characterizing the implicit structure of the computation within neural networks is foundational problem in the area of deep learning interpretability. Can their inner decision process be captured symbolically in some familiar logic? We show that any transformer neural network can be translated into an equivalent fixed- size first-order logic formula which may also use majority quantifiers. The idea is simulate transformers with highly uniform threshold circuits and leverage known theoretical connections between circuits and logic. Our findings also reveal the surprising fact that the entire transformer computation can reduced merely to the division of two (large) integers. While our results are most pertinent for transformers, they apply equally to a broader class of neural network architectures, namely those with fixed-depth uniform computation graph made up of standard neural net components, which includes feedforward and convolutional networks.
INTRODUCTION
The incredible success of deep learning models, especially very large language and vision models with tens to hundreds of billions of 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 account- ability. the inner working of such networks fundamentally different from classical algorithms and symbolic systems that we understand better? Or can their computation be described symbolically using a familiar symbolic cymbolicformaliinn formalism?
We derive the first, to the best of our knowledge, direct connection between a broad class of neural networks and the well-studied classical formalism of first-order logic. Specifically, we show that transformers-aan and other neural networks with a computation graph that has constant depth and "repetitive" or uniform structure- conettureimplemenn nothing but fixed-size first-order logic expressions, the logic is allowed to have majority quantifiers (M) in addition to the standard existential (2) and universal quantifiers (V). Majority quantifiers simply take a sequence of boolean values and return true if more than half of them true. The resulting logie formalism is often referred as FO(M).
Theorem 1 (Informal version of Cor. 5.1). For any neural network N with constant-depth com- putation graph, there is a fixed-size FO(M) formula @ equivalent to N.
This result immediately provides mechanistic interpretability-it demonstrates that, at least in prin- ciple, the inner decision process of any transformer model can be efficiently translated into fixed- size formula (with respect the input length) in a simple, well-defined logic. The output A(xx) of the transformer on any input is simply the value d(xx of this formula. Similar to decision trees, FO(M) formulae have the property that each sub-expression corresponds to logical constraint, i.e., function mapping the input sequence to truth value. In contrast, the internal modules of trans- former or complex circuit do not satisfy this, as they map between uninterpretable latent spaces. We thus believe that converting transformers (O(M) formulae could be leveraged for interpreting their behavior in future work, although a thorough exploration of this idea lies outside the scope of theoretical contributions in this paper.
Thm. also gives some insight about how to contrast the abilities of transformers and finite-state machines. Classically, the regular languages can be characterized the languages definable in terms

---

Under review as a conference paper at ICLR 2023
of monadic second-orde logical formulae (Büchi, 1960; Elgot, 1961). We have shown transformers can be simulated by first-order formulae with majority quantifiers. Thus, an advantage transform- have finite-state machines is the ability to resolve majority quantifiers over their input. However, transformers are not necessarily strictly more powerful than finite-state machines: it is be simulated by majority quantifiers.
unknown whether second-order monadic quantifiers
We derive this connection between transformers and (M(M) by leveraging a key result in circuit complexity theory: the equivalence of FO(M) with highly uniform threshold circuits, specifically with circuit class known DLOGTTMFFaniifrmm TC (Barrington et al., 1990). Our proof builds upon and significantly tightens prior work by Hao et al. (2022), Hahn (2020), Merrill et al. (2022), and Merrill & Sabharwal (2022) on relating specific types of transformer networks circuit com- plexity classes. We improve prior analysis on two fronts. First, the class log-uniform TC" is much tigher than in previous results. Second, in contrast to their work, we obtain a characterization for fully general model of transformers without limiting assumptions. Our formal model is the first to cover realistic design choices and sizes used in typical transformer implementations.
Specifically, we show that any transformer network with a fixed-depth computation graph can be simulated by highly uniform class of threshold circuits:?
Theorem (Informal version of Thm. 5). For any neural network N with a constant-depth compu- tation graph, there exists a log-uniform, TC circuit family C = I such that, for all x of size n, (z)) (z).
This result, in addition to helping derive Thm. 1, itself has significant implications. It provides much tighter class of transformer-hard problems, i.e., problems to which any transformer can be efficiently reduced, than previously known. It shows that every problem complete for the class of log-unifome TC circuits is transformer-hare Since division (Hesse, 2001; Hesse et al., 2002) is known to be one such problem (Aaronson et al., 2022), this leads to the following rather surprising finding:
Corollary 2.1. For any neural network N with a constant-deptt computation graph and input x, the computation of (xx) can be efficiently reduced to integer division the following sense: for all E
there exist efficiently computable (via log-uniform circuits) integers az(x), bx(x), and in such that the j-th bit of (xx) equals the i5-th bit of (o(()//b((x)
This again allows to view transformers from a novel perspective: namely, computing a bit of the output of a transformer with hundreds of billions of parameters can be easily reduced to dividing two integers. Even very large transformers are, this sense, ultimately simple functions operating at very large scale.
In summary, our findings shed new light into the inner computation of transformers (and other neural architectures) and its connection to first-order logic. While literature on neuro-symbolic models has often viewed symbolic and neural systems as very different from each other, our results show that the boundaries between these two computational paradigms are not as rigid they might seem.
Roadmap. $2 gives definition and examples of FO(M), and then introduces relevant background on computation graphs and circuits for our proofs. $3 presents the constructive algorithm to compile computation graph families into threshold circuit families and justifies its correctness. Specifically, we obtain the result that log-uniform computation graphs (with uniform node types) can be compiled into FO(M) expressions. Then, $4 shows that transformers uniform computation graph families, which implies that they can be compiled into FO(M).
For brevity, will henceforth ahbreviate DILGoooMF-nnnfoom log-uniform.
*Conceptually, our results converting transformers to logical formulae and circuits resemble empirical work extracting discrete "subeircuits" from transformers (Elhage et al., 2021), although we use the term circuit in precise formal sense, rather than mean any discrete rules summarizing model hchavior.
2

---

Under review as a conference paper at ICLR 2023
2
PRELIMINARIES
2.1 FIRST ORDER LOGIC WITH MAJORITY
Transformers can be translated into expressions in (M (hMt do such expressions look like? We provide a definition of first-order logic with majority as well as some examples of simple languages definable in
Informally, FM(M) is first-order logic extended to also have majority (M) quantifiers. We apply FM(M) specifically to string inputs, for which quantifiers will range over indices into the string, over which various predicates can be applied, as in Barrington al. (1990).
Definition 1 (FO(M) indices). The constants and are given indices in FO(M). Other indices can be built using addition or subtraction, or can be variables introduced by existential (3), universal (v), or majority (M) quantifiers.
Definition 2 (FO(M) expressions). For each a E Σ and index i. X(o, i) is predicate that semanti- cally represents whether the i-th token in the input sequence is a. Comparing indices with or < also produces a valid expression, as does combining other expressions with the logical connectives A or V. Finally new expression can by generated by scoping a quantifier (3, V, M) with an associated variable over another expression."
A formula 6 in FO(M) is an expression with no free (i.e., unbound) variables. For every input in E", it evaluates a value in {0, 1}. & can thus be viewed as a function from Σ to {0, 1) defining formal language.
Without loss of generality, we will assume multiple sub-formulae within can be labeled ordered outputs, thus allowing ø to be function from Σ" to {0, 13 for some fixed constant l bounded above by the number of sub-formulae in ạb.
Let Σ = b.. To illustrate the formalism, we provide example languages definable in FO(M):
Example (Bigram matching). The following FO(M) expression defines the regular language of strings containing the bigram ab:
3F i(a, X(b,i+ 1)]-
Example 2 (Skip-bigram matching). The following FO(M) expression defines the language of strings containing the long-distance pattern a a...b, b. resembling the form patterns proposed by Elhage et al. (2021) in their analysis of transformer subcircuits:
3i X(b, i) A رi s i
Example 3 (Majority). The following FO(M) expression defines the counter language "majority", i... the strings with more b's than a's:
Mi (b.
Example I and Example are definable in first-order logic (without majority), which is special case of FO(M), In contrast, Example 3 requires majority predicates (Furst et al., 1981).
2.2 COMPUTATION GRAPHS
A computation graph over datatype S {0, and a countable set of primitive functions $ C
D x D is a directed acyelic graph (DAG) where:
1. Each node labelled by node type: a function f E 3 describing the computation of this node.
In Barrington et al. (1990) this not introduced as a primitive, hut can he simulated using the S predicate. Barrington et al. (1990) define X(i) over binary vocabulary. We generalize this to an arbitrary vocabulary by assuming each token is encoded in one-hot representation. Then X(a, = X( + 8) where is the index of the vocabulary.
'Soeetmess "bit predicate" is also included in the definition of the formalism. It turns out this is not necessary for FO(M), as can be simulated using the other primitives (Barrington et al., 1990).
3

---

Under review as a conference paper at ICLR 2023
2. Each edge represents value D flowing as output from node into another node.
3. I contains the special symbol input, which designates nodes as input nodes. We refer to k as the arity and assume without loss of generality that nodes 0, k 1 are inputs. 6
4. A single node is designated the output node. We assume without loss of generality that the output is the node with the largest index.
A computation graph 9 of arity k parameterizes a function fg : D > D in the standard way: the input nodes are assigned the input values, and the value of each node is computed (traversing the graph in a bottom-up topological order) a function of the values of its children until the output node receives value. At this point, the value of the output node is considered the output of the function. It is worth noting that computation graphs can only process inputs of bounded length. To process arbitrary-length inputs, we will need to generalize them to computation graph families ($2.3).
Two important properties for computation graphs are size(G)) (the number of nodes) and depth (G) (the length of the longest path from an input node to an output node). Additionally, we denote by arity(G, i) the number of inputs to node i.
Threshold circuits. threshold circuit is special case of a computation graph where D {0, and F is the set of threshold functions of the form Ac and م= over D*. defined as follows: 0g a (x) equals if Loeg o S A and otherwise; 22 (x) is defined analogously. Note that typical boolean circuits with AND, OR, and NOT gates are a special case of threshold gates, as is the IDENTITY logical gate.
Similar to the FO(M) case, we will, without loss of generality, allow nodes with the k 2 1 largest indices to all be designated as (ordered) output nodes. A threshold circuit with arity and k' output nodes will thus be function from {0, 13 13* to {0, 1, This will be convenient when simulating neural network components which often 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.
2.3 COMPUTATION GRAPH FAMILIES
A computation graph family over ID and & is mapping from E N to a computation graph G, for processing inputs of size n. Thus, G defines a function from D + ID where fg = f1z (r). Intuitively, computation graph families are useful because they generalize computation graphs to define functions over unbounded-length strings as inputs.
Size, depth, and arity. For computation graph families, the size and depth become functions of the input length n. We define the following functions, which naturally generalize size, depth, and arity computation graph families:
sizeg (n) = size(Gn.)
depth (n) depth(G..)
arity (n, i) = arity(G,,, ()..).
Uniformity. G is an infinite set, computation graph family can be more compactly represented by two programs computing the following functions:
1. nodeg(n, i), which returns the type of node in G, if < size (,),, and @ otherwise.
2. edgeg (n, i,)). which returns the argument index of i into node j if G, contains an edge i j and -1 otherwise. edgeg (n,, i.j) only needs to be defined over i, size(G,,)
A pair of algorithms implementing these two functions uniquely specifies a computation graph fam- ily, it enables building the structure of the computation graph G, for any
By convention in computer science, we computation graph nodes he zero-indexed. For more background on threshold circuits, see Merrill & Sabharwal (2022), Merrill et al. (2022), and Arora& & Barak (2009).
4

---

Under review as a conference paper at ICLR 2023
Table 1: Summary of common notation for computation graph and circuit families.
Graph
Circuit
Output Range
Description
index of node/gate
nodeg (n, 1')
(n,
8
type of node/gate
edgeg (n, (')
(n.
Z
argument number of edge + j
sizeg (n)
(nze
Z
number of nodes/gates in graph/cireuit longest path length in graph/cireuit index of the block r' containing i index of first gate i in block 8' size of block !
depth o
Z
bnode(n, 2)
O. sizeg (n)
bstart(n, i')
00, sizee(n))
bsize(n, 1')
Z
Additionally, it useful to introduce uniformity conditions on computation graph families. 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. In this paper we focus on time-bounded uniformity:
Definition 3 (Uniformity). A computation graph family g is T(n)-uniform iff each of nodeg (n, and edgeg (n,, j) can be computed by a deterministic Turing machine time T(n).
Specifically, we are interested in log-uniform computation graph families where T(n) = Ollogn)
We also introduce stronger notion of column uniformity that captures the highly regular structure of a wide range of commonly used neural network architectures, including the Transformer. This will be useful for tighter bounds by constructing smaller circuits to simulate neural networks:
Definition 4 (Column uniformity). A computation graph family G is ((n)--oolum--nioo) iff
There exists finite sequence of nodes (1C,1=1 such that, for 0 s i sizeg(n),, nodeg(n, i) = Ki mod e.8 edgeg(n,,,) i.j) can be computed by a deterministic Turing machine time T(n).
We define log-column-umifone analogously to log- Jog-urnform, i.e., we let T'n) O(log n).
Threshold circuit families. Threshold circuit families are families of threshold circuits. We will be interested in simulating computation graph families with threshold circuit families.
SIMULATING COMPUTATION GRAPHS WITH CIRCUITS
We provide an algorithm that constructs circuit simulating a given computation graph. Intuitively, the algorithm creates contiguous blocks of circuit gates simulating each node in the computation graph, and routes inputs and outputs between blocks appropriately.
Block mapping. This algorithm depends on a block mapping, which we define as an implementa- tion of the following three functions:
1. The block node bnode(n, i): the index of the node that gate i's block 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
Further, we enforce that valid block mapping must satisfy that, for all i, with i' bnode(n, i),
bstart(n, i') < < bstart(n, :') + bsize(n, i').
Now, consider computation graph G where the primitive functions are computable by log-uniform threshold circuits. In this case, can identify each primitive function f with log-uniform thresh- old circuit family T that computes f. where the first anity>(n) gates are IDENTITY gates reserved for taking input. For such a graph, the nodeg function can be taken to return symbol identifying circuit family T.
Where mod b represents the remainder when divided by b.
5

---

Under review as a conference paper at ICLR 2023
Algorithm Return the type of gate i in circuit C.. procedure nodec(n, i) if i < sizeg (n) then f- nodeg (n. bnode(n, i)) return noder(n, i bstart(n, else return
Algorithm/ 2 Return argument number of edge i + in circuit Cn. Return -1 if no edge exists.
procedure edge<(n, 2,
i' bnode(n, i)
5 bnode(n1,
8/ f bstart(n. m,
8, f bstart m.
if i' j' then
i, fall within the same node of G
f- nodeg (n. i')
return edge (n, J j
85)
else if edge (n, 7', j') 2 0 then
> pij fall in nodes of Gn with an edge
Ty nodeg (n,
b, < - (8: bsize(n, 8¹) pp)
> adjust relative to the output bits of Tr (n) adjust relative to the imput bits of Ty (n)
by j (sj p- edge 8 jr))
if b = by < x then return 8j
else return
else return 0
In this case, our algorithm requires that, for all E', the block size of must match the size of the circuit for the type of block i', i.e., bsize(n,, i') (x (n).
These properties allow to meaningfully identify a graph node i' with block of nodes that will simulate it. This intuition enables us to develop Algorithm and Algorithm 2 for constructing a uniform threshold circuit family from uniform computation graph family.
Let G be a computation graph over finite set of node types B. where each T E 3 is specified by log-uniform circuit family. Let bnode, bstart, and bsize be valid block mapping in the sense above. Then Algorithm 1 and Algoritium 2 define a circuit family C such that
Theorem 3.
1. C and G compute the same function from D + DD ifwe consider the final p gates of each C; to be its output.
2. depthe(n) (n) I depthg (n) maxx depthy (n).
3. (n)) S sizeg(n). maxx (n))
Proof. Assume without loss of generality that the gates of C are topologically ordered. We show by induction over circuit gates j (with j' bnode(ni.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, < i S j. gate i of C (as function of the input nodes of j') computes gate i (s. of nn.eg(n.
Base case. We have two circuits with no gates, so the premises are trivially satisfied.
Inductive case. Assume the premises hold up j. We will show they hold for j + 1. Let T nodeg(n. (n.j'') By Premise 1, we know that the last p nodes of block i' store the output of node i', for i' j'. By Algorithm 2, for each i' such that edge (n, i' j')j")
with 0 < k arity>(n), gates kp through k(p + 1) - of block j' will copy the final gates of block Thus, the first (rityy gates of block j' store the inputs to node
At this point, we use Premise to conclude that the first j bstart(n, gates of block j compute the same function as the first j bstart(n, j') gates of T with respect to this input. Thus, we just need to show that gate j + 1 is also correct. Within Algorithm 2, we fall case i' = j', meaning that gate j 1 of block jr gates the same inputs gate j + of T. By Algorithm 1, the type of gate

---

Under review as a conference paper at ICLR 2023
j+ + 1 in block j' is the type of gate j + 1 of T. We conclude that gate j + in block j' computes the same function the input gates as gate j + in T. If j +1= bsize(n, n', we further conclude that the final p gates of block j" store the output of node j"-
Since a transformer computation graph has constant depth and polynomial size, this theorem allows us to relatively 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 TC circuits, respectively. We omit the details of these here as later ($4) we will prove much tighter result showing that all node types in a broader class of neural networks can, in fact, be computed with much more uniform eircuit class.
be computed by AC and
Formally, let XC denote any family of constant-depth circuits, including AC and TC
Corollary 3.1. Let be computation graph family over finite set of node types. If has constant depth and polynomial size, and every node type in it can be computed by XC circuits, then the function computed by G is in XC
3.1 PADDED BLOCK MAPPING FOR UNIFORM COMPUTATION GRAPH FAMILIES
We now implement block mapping in the where G is log-uniform computation graph. We analyze the runtime of nodeş and edgec to show that is a log-uniform circuit family.
Our block mapping works by simply padding each block the maximum size needed implement any node type in G. We assume that there exists a polynomial function bsize(n) computable by Turing machine in O(log n.) time such that, for each node type sizer(n) (n) S bsize(n).. We will later justify this assumption for transformers in $4. Without loss of generality, we can take bsize(n) be power of 2 by padding
be the smallest power of above its original value."
We then pad each node type circuit T to have size bsize(n) by adding unused dummy nodes. We are ready provide block mapping:
bnode(n, (n, [i/bsize(nt]]
bstart(n, i') = i' bsize(n)
bsize(n, i') bsize(n).
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, these functions are computable in time O(log n). Since nodeg and edgeg are just calling bnode, bstart, and bsize with constant overhead, follows from Thm. 3 that
Theorem 4. Let G be log-unin log-uniform computation graph over finite set of node types B. where each
specified by log- uniffrmo threshold circuit family and sizey computable in time Oloog n). Let bnode, bstart, bsize be the padded block mapping w.r. S. Then G can be simulated by a constant-depth, poly-size, tog-uniform threshold circuit family via Algorithm I and Algorithm 2.
Following from the equivalence of log- fog-uniform TC and FO(M), we obtain
Corollary 4.1. Let G be a log-uniform computation graph over a finite set of node types 3. where each T E 3 is specified by log-uniform threshold circuit family and sizet is computable in time DLOGTIME, Let bnode, bstart, bsize the padded block mapping w.r. B. Then G can simulated by an FO(M) formula.
For both Thm. 4 and Cor. 4.1, the size upper bound from Thm. holds, but we omit it for brevity, The padded block mapping scheme is wasteful in the sense that not every node type needs to receive the maximum block size.
10 bsizeen) remains poly(n) hecause its value at most doubles. It can be computed in O(log time because padding hinary number power of 2 simply involves prepending 1 and converting existing bits to (''s.

---

Under review as a conference paper at ICLR 2023
4 TRANSFORMERS ARE UNIFORM COMPUTATION GRAPH FAMILIES
The last step to make our claim about transformers go through is to justify that the transformer architecture is a log-uniform computation graph family (over node types that can expressed as log-uniform threshold circuit families). For those familiar with neural networks, it should not be surprising that our notion of a computation graph describes a neural network. In order to justify this rigorously though, will show that all core neural network components are computable by log- uniform threshold circuit families, and will also derive size and depth bounds for these families." 1I
4.1 TRANSFORMERS
We will think of each representation in a transformer vector of numbers from Fp. i.c., vectors in Fd. In typical transformer network (Vaswani et al., 2017; Devlin et al., 2019), one may have p = 16 or 32 as a fixed constant determined by the GPU, input length n = 512, model dimension d 768, and a potentially larger feedforward dimension h. In practice, for newer, larger transformer language models, the precision p = 16 (Brown et al., 2020; Zhang et al., 2022).
The model dimension d can be thought of being roughly the same order of magnitude that this is much more aligned with practical transformers than the log-precision model of Merrill & Sabharwal (2022), which effectively assumes dp Ollog n) and thus applies only for values of that are substantially larger than what's used in practical transformers (e.g., dp in this example setting is 12288 whereas log(n) is only 9). Our model and associated result, on the other hand, apply directly to typical implementation choices for several neural net architectures.
Note
The feedforward dimension can be larger than d in practice (Vaswani al., 2017: Raffel al., 2020), but is reasonably still (n)y Rather than assuming specific relationship between n, d, h, will derive our characterization of transformer components in terms of these three hyperparameters.
Putting this all together, we can now define transformer as computation graph family N. The transformer column KCN is a transformer embedding layer followed by L transformer layers, each of which contains self-attention sublayer and feedforward sublayer. These sublayers are in turn constructed from affine transformations, activation functions, layer norms, and self-attention modules. We define these primitives (as well as the embedding component) as the functions in Sv, and in turn represent the transformer column as a finite sequence of these primitives.
4.2 RESULTS
We first justify that the transformer computation graph family is log-uniform, which implies it is log-column- uniform.
gin--olum-uunioomm.
Lemma 1. Any transformer computation graph family N is log-columm-unffom.
Proof. We have the column IC by construction. All that remains to show is that edgeg can be computed in DLOGTIME. All the routing of inputs and outputs between transformer components fixed within the column besides self-attention. For the fixed routing, we can simply store a finite table for each i', j' mod [K] and look up the answer to answer engeg(n, i', j'). For routing into a self-attention component j' at sequence position ty. let i' is the output of the previous layer at position fr. For full attention, we simply return 4.. For causally masked attention, we return ty if by < byr and 0 otherwise. Either way, this logic is clearly possible in DLOGTIME. Thus, we conclude that the transformer computation graph family is
Next, we need to justify that each neural net component used as a node in the transformer computa- tion graph is uniform and that its size is computable in DLOGTIME.
Lemma 2. Assume d, h, |Σ| < (nly(n). Each E 3x is computable by log-uniformm threshold circuit T with sizet computable by a deterministic Turing machine in time O(logn).
While we provide this rigorous justification for transformers. similar arguments can also be made for broader class of neural networks made up of standard neural net components, which includes feedforward and convolutional networks.
8

---

Under review as a conference paper at ICLR 2023
Proof. Out of all the transformer components (Vaswani et al., 2017), activation functions and resid- ual connections are completely "local" (cf. $A), meaning they have fixed-depth, fixed-size circuits function of d, and | Thus, these operations are trivially uniform.
remains to be shown that the other "global" components (embeddings, affine transformations, be computed by uniform threshold circuit families with size computable in DLOGTIME. We do this in $B by reducing each component to summation with uniform local functions. This allows to derive the following:
layer norm, and self attention)
1. By Lem. 8, embedding the input token and position is computable by a uniform threshold circuit family of size most O(IE[d + v1).
2. By Lem. 9, each affine transformation is computable by uniform threshold circuit family of size most ((max log dh log h)).
3. by Lem. 10, the layer norm is computable by uniform threshold circuit family of size at most (d d).
4. By Lem. 11, self attention is computable by uniform threshold circuit family of size at most (n log rt).
For each component type T, we pick function T(n) that is both larger than the size bound for T and computable by deterministic Turing machine in O(log n) time. We pad T with unused nodes to make (n) = [nx).
We conclude that each f E 3N is computable by log-uniform threshold circuit T with sizet computable by a deterministic Turing machine in time O)logn).
This column uniformity implies standard uniformity, and that the overall size is the column size times n. We can now directly obtain the following applying Thm. 4 to transformers:
Theorem 5. For d, h. | S (oly(n), let N be transformer computation graph over vocabulary with model dimension and feedforward dimension h. Then the function N defines over E* is computable by constunt-depth threshold circuit family C with size at most
n O (|E|d d² log d + dh log h + n log
The n comes from the number of columns, and the other factor comes from the size of a column, where the terms follow from the sizes of transformer components derived in Lem. 2. Practically, in an overparameterized transformer, |Σ] or h is often the largest hyperparameter. If so, we would expect the terms |E|d and dh log to dominate the size of the threshold circuit. These correspond to the the circuit gates simulating the embedding layer and the feedforward sublayers, respectively.
Analogously to Cor. 4. 1, we show that transformers can be translated to equivalent FO(M) formulae:
Corollary 5.1. For d, h, ΣΣ] S poly(n), let be a transformer computation graph over vocabulary with model dimension d and feedforward dimension h. Then N can be simulated by an (O formula.
CONCLUSION
We proved that any transformer model can be efficiently translated into fixed-size FO(M) logic formula that computes the same function as the transformer (for all lengths). This result comes by first simulating a transformer with a highly uniform threshold eircuit family, and then leverag- ing the established equivalence of log-uniform circuits and FO(M). Transformers and other neural nets are often discussed 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 transformers also in a simple logic, challenging the premise a rigid division between symbolic and neural models.
would be an interesting future direction to implement our efficient algorithms to convert trans- formers to FO(M) formulae, and leverage this logical representation for increased interpretability of the model. Extending our results to recursive architectures such as RNNs also remains an interesting open problem.

---

Under review as a conference paper at ICLR 2023
REFERENCES
Scott Aaronson, Greg Kuperberg, and Oliver Habryka. TC Constant depth threshold circuits, T#tc0.
2022. URL https::tp//..........
Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cam-
bridge University Press, 2009, URL https: http://ooooooooog.glooooooe.. gwwgle.
wtt../ccccbooooeeeece wttp//cks/oooabuuuoooooooooo htm. attml?id=2a html:Pid-@sjjysso44BB htt.//ow....oog.e..ooooooooo.oo.
Compitattional_oompeeeete
David A. Mix Barrington, Neil Immerman, and Howard Straubing. On uniformity within NC!.
Journal of Computer and System Sciences, 41(3):274-366, 1990. ISSN 0022-0000. doi: https:
URL https: /www. sciencedirect. com/
Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhari- wal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agar- wal, Ariel Herbert- Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel Ziegler, Jeffrey Wu, Clemens Winter, Chris Hesse, Mark Chen, Eric Sigler, Ma- teusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCan- dlish, Alec Radford, Πla Sutskever, and Dario Amodei. Language models are few-shot learners. In H. Larochelle, M. Ranzato, R. Hadsell, M.F. Balcan, and H. Lin (eds.), Ad- vances in Neural Information Processing Systems, volume 33, pp. 1877-1901. Curran Asso- ciates, Inc., 2020. URL https: htttps::/pproceedingg neurips. cc/ htcp/aaper//22////00 Paper
Richard Büchi. Weak second-order arithmetic and finite automata. Mathematical Logic Quar- terly, 6( 6(1-6):66-92 1960. doi: https:/doi.org/100 1ttp:/111100000 http://do..orr/...00000/m/l./l
URL https:
//onl fonlinell aibrarrrr...rrr ra.aary... ry..y.................... wi ley www./oo///oocc.c..cccoo.o..o...o abss/ /10. 20002/mal0 19600060105.
Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. BERT: Pre-training of deep bidirectional transformers for language understanding. In Proceedings of the 2019 Conference of the North American Chapter the Association for Computational Linguistics: Human Language Technologies, Volume (Long and Short Papers). pp. 4171-4186, Minncapolis, Minnesota, June 2019. Association for Computational Linguistics. doi: 10.18653/v1/N19-11 1423. URL https: / // //www. ac web. org/ wowgg//atllogy//////ooooo 9t1p:looooo/1111221111111 9-1233.
Calvin C. Elgot. Decision problems of finite automata design and related arithmetics. Transactions of the American Mathematical Society, 98(1):21-51, 1961. ISSN 00029947. URL http:// www. jstor org/ sttp///babeee911111
Nelson Elhage, Neel Nanda, Catherine Olsson, Tom Henighan, Nicholas Joseph, Ben Mann, Amanda Askell, Yuntao Bai, Anna Chen, Tom Conerly, Nova DasSarma, Dawn Drain, Deep Ganguli, Zac Hatfield-Dodds Danny Hernandez, Andy Jones, Jackson Kernion, Liane Lovitt, Kamal Ndousse, Dario Amodei, Tom Brown, Jack Clark, Jared Kaplan, Sam McCandlish, and Chris Olah. A mathematical framework for transformer circuits. Transformer Circuits Thread, 2021. https:/ttansformer circuitssi http:////////aaamooo/iiiiio
html.
Merrick Furst, James B. Saxe, and Michael Sipser. Parity, circuits, and the polynomial-time hi- erarchy. In Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, SFCS 88, pp. 260-270, USA, 1981. IEEE Computer Society, doi: 1..1109/FFCS..11..... URL bttpss://ool wwt.o/ogg//ooooo 10l wwt.:.1111......... SECS. /tt.0///FFSS............ 1981.35.
Marta Garnelo and Murray Shanahan. Reconciling deep learning with symbolic artificial intel- ligence: representing objects and relations. Current Opinion in Behavioral Sciences, 29:17- 23, 2019, ISSN 2352-1546. doi:
2010..........0..000...00000...0 URL https:
/ //wwww wecienceeirecto httpee/cwo...steeeeaaeaaaae////a tificial Intelligence.
Ar-
Michael Hahn. Theoretical limitations of self-attention in neural sequence models. Transactions of the Association for Computational Linguistics, 8:156-171, 2020. URL https: / www.
acl web. org/ http//anhhhllgyyyoo -tacl-1.111
10

---

Under review as a conference paper at ICLR 2023
Yiding Hao, Dana Angluin, and Robert Frank. Formal language recognition by hard attention transformers: Perspectives from circuit complexity, 2022. URL btttppp://rxiive org/ abs/ 2204.06612
William Hesse. Division is in uniform TC In International Colloquium on Automata, Languages, and Programming, pp. 104-114. Springer, 2001.
William Hesse, Eric Allender, and David A. Mix Barrington. Uniform constant-depth threshold cir- cuits for division and iterated multiplication. J. Comput. Syst. Sci., 65(4):695-716 dee 2002. ISSN 0022-0000.
doi: 10.
URL https://doi..oo
1016/50022-000 0000 (02) 00025-9. 9.
Neeraj Kayal. Lecture notes for topics in complexity theory, February 2015. URL
https: http://wwwwcom
ac http://hhwaaaaaecooooe////ttttta
notes/lec5.00
William Merrill and Ashish Sabharwal. Log-precision transformers are constant-depth uniform threshold circuits. ArXiv, /ttp//2277000299. 2022.
William Merrill, Ashish Sabharwal, and Noah Smith. Saturated transformers are constant-depth threshold circuits. Transactions of the Association for Computational Linguistics, 10, 2022.
Colin Raffel, Noam M. Shazeer, Adam Roberts, Katherine Lee, Sharan Narang, Michael Matena, Yanqi Zhou, Wei Li, and Peter J. Liu. Exploring the limits of transfer learning with a unified text-to-text transformer. Journal of Machine Learning Research, 21(14 2020.
Romal Thoppilan, Daniel De Freitas, Jamie Hall, Noam M. Shazeer, Apoorv Kulshreshtha, Heng- Tze Cheng, Alicia Jin, Taylor Bos, Leslie Baker, Yu Du, Yaguang Li, Hongrae Lee, Huaixiu Zheng, Amin Ghafouri, Marcelo Menegali, Yanping Huang, Maxim Krikun, Dmitry Lepikhin, James Qin, Dehao Chen, Yuanzhong Xu, Zhifeng Chen, Adam Roberts, Maarten Bosma, Yanqi Zhou, Chung-Ching Chang. A. Krivokon, Willard James Rusch, Mare Pickett, Kathleen S. Meier-Hellstern, Meredith Ringel Morris, Tulsee Doshi, Renelito Delos Santos, Toju Duke, Johnny Hartz Søraker, Ben Zevenbergen, Vinodkumar Prabhakaran, Mark Díaz, Ben Hutchin- son, Kristen Olson, Alejandra Molina, Erin Hoffman-John, Josh Lee, Lora Aroyo, Ravindran Ra- jakumar, Alena Butryna, Matthew Lamm, V. O. Kuzmina, Joseph Fenton, Aaron Cohen, Rachel Bernstein, Ray Kurzweil, Blaise Aguera-Arcas, Claire Cui, Marian Croak, Ed Chi, and Quoc Le. Lamda: Language models for dialog applications. ArXiv, 0iss/2001.022333 2022.
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, ukasz Kaiser, and Illia Polosukhin. Attention is all you need. In I. Guyon, U. V. Luxburg, S. Bengio. Н. Wallach, R. Fergus, S. Vishwanathan, and R. Gareet (eds.), Advances in Neural Information Processing Systems, volume 30. Curran Asso- ciates, Inc., 2017. URL https: http:rocceeeiiinn.....eeeeeeeeee pttpcccpppp/e//////00... 3E5ee243547deee 1fbd053cccc48855a 21022222277e11100003eeeeeeeeee -aa.:00ac...aa45aaaaaa...... pdf.
Susan Zhang, Stephen Roller, Naman Goyal, Mikel Artetxe, Moya Chen, Shuohui Chen, Christo- pher Dewan, Mona Diab, Xian Li, Xi Victoria Lin, Todor Mihaylov, Myle Ott, Sam Shleifer, Kurt Shuster, Daniel Simig, Punit Singh Koura, Anjali Sridhar. Tianlu Wang, and Luke Zettlemoyer. OPT: Open pre-trained transformer language models, ArXiv, abs/2205. 000688 2022.

---

Under review as a conference paper at ICLR 2023
A LOCAL AND GLOBAL FUNCTIONS
A.1 COMPOSITION
To justify our modular decomposition of transformers, we first show that the composition of Olog n) -uniform circuit families is also Ollog -unufforrm circuit family, assuming the sizes of the input families in the composition are computable in DLOGTIME.
Lemma 3 (Composition). For a fixed S is d, let fi : D + D be computable by a O(log n)- uniform compulation graph Gi over D, 3 with sizeg, (ni computable in DLOGTIME. Let Di - a O(log vi)-um -uniform computation graph over D,3. Then, for all E ID*, the following is computable by DLOGTIME uniform computation graph G over ID, 3:
fo g(x) 9 (f
where the size and depth of G are at most additive in the size of circuits computing each f; and g.
Proof. Let G* be the computation graph computing the composed function. We first compute the size of each circuit G; in DLOGTIME and call that 8;- To answer nodeg. and edgeş- queries, we then partition the indices between and Σ ;=1 to represent different ft's this requires only a finite number of cases. We use indices 2 to represent the nodes of g. and route the output (last p nodes) of each f; g input.
A.2 LOCAL FUNCTIONS
Lemma 4 (Extended from Hao al., 2022, Lem. 3). Any function 1) + {0, can be computed by depth-3 circuit of size at most 2T + m
Proof. Similar to Hao et al. (2022), we construct a circuit using a DNF representation of f. except that we use combined DNF representation for all output bits of f. The DNF formula has at most 2n terms. The circuit has a NOT gate for each input bit, an AND gate for each DNF term, and, for each of the p output bits, an OR gate combining the outputs of those AND gates (i.e., DNF terms) for which that bit is 1.
Corollary 5.2 (Local functions). Any p-precision arithmetic functionni of numbers can be computed by a depth-3 circuit of size 2Fp + kpp + p.
A.3 GLOBAL FUNCTIONS
Two lemmas of Kayal (2015) on addition with threshold circuits will useful for building circuit families to add floats.
Lemma 5 (Extended from Kayal, 2015, Thm. 5.8). Any symmetric function {0, 1)* - {0, can be computed by a O(logn) unnuffrrmm threshold circuit family of depth 2 and size O(n) (where n is the input bitstring length).
Proof. The correctness of the circuit family is shown by Kayal (2015); uniformity follows from the constructive algorithm in their proof.
Li
Lemma 6 (Extended from Kayal, 2015, Thm. 5.9). The sum of k integers of ls bits each can be computed by O(log -uniforn constant-depth threshold circuit family of size O(13)).
Proof. The correctness the circuit family is shown by Kayal (2015); uniformity follows from the constructive algorithm in their proof.
We can these lemmas analyze adding k floats of precision p, which is notion of global computation in the transformer.
Lemma 7. The sum of k floats of p bits each can be computed by a O n) -niifrrm constant- threshold circuit family of size Ol log k), with constant depending on precision p.
12

---

Under review as a conference paper at ICLR 2023
Proof. The proof procedes by constructing O(log -unuffrrm circuit families to carry out the fol- lowing computations, where each threshold circuit family C has sizeg computable DLOGTIME. truncated to precision p. so thus by Lem.
The composition of these functions gives the correct the sum is computable by O(log n) -uniform eircuit family whose size the sum the constituent circuit sizes. All that remains is to justify the circuit family size for each step.
1. Let = p/2 + exp(p/2). We first map the k p-bit floats ls p'-bit integers representing the same value.
2. Sum the bits in each place value across all & integers, yielding p' integers of size log k.
3. Shift each place value integer that they line up semantically, and add. This corresponds to adding p' integers of size at most log k + p' to produce new integer s.
4. Finally, return the first p non-zero leading bits of as the mantissa, and the number of remaining bits (at most p' p) as the exponent.
Step Floats to ints. This involves local functions applied to each number, so its size is O(k).
Step 2: Summing across place values, Observe that summing & bits across each place value is symmetric function with log & output bits. Thus, by Lem. 5, we have O n -unuforrrm constant- depth threshold circuit family size O(k) that computes each of the log output bits for each place value up to p'. Summing over all log k bits and constant number of place values, the size of the overall circuit for this step is O log
Step Addition. We ignore the size of local functions, since they have fized-size circuit with respect i and thus take ((k) size when applied elementwise. Adding p' integers of size at most log k-pp' can done by a constant-depth threshold circuit family of size 2(log k+p' Ollgg k) using Lem. 6.
Step 4: Ints to floats. This involves local functions applied to the final sum, so its size is O(1).
Summing the sizes of each step yields an overall size of
O(k) + O log k) + O(log* k) + 0(1) = O | log k).
B TRANSFORMER COMPONENTS
B. TRANSFORMER EMBEDDINGS
The initial layer of the transformer embeds token a from vocabulary E, as well as their position from < S n, into a vector e(a,(). Let be an embedding matrix of size [Σ] x d where each row represents the embedding for some Then,
e(a,t)=ve + f(t).
Lemma 8. The transformer embedding layer be computed by constant-depth log log-uniform threshold circuit family of size O([Edd+ + +n).
Proof. The first term of the embedding mechanism be implemented with lookup table encoded as a circuit of size O(E]d). To build the circuit for the second term at position t, we first construct the constant as log n-bit integer. We then apply Lem. 4 to compute ftt in time
2logn + log n + O(n + d).
Thus, the full embedding layer can be computed as a function of an input string w E Σ by constant-depth log-uniform eircuit family of size O(EE) + n).
13

---

Under review as a conference paper at ICLR 2023
B.2 AFFINE TRANSFORMATIONS
Affine transformations form the building block of neural network layers. In a transformer, they occur in the both the self-attention sublayer key, query, value, and output transformations, and in the feedforward sublayer in standard neural network layers.
Lemma 9. An affine transformation from F F can be computed by O n) -uniform circuit family of constant depth and size O(k' log
Proof. For the transformation Wx + b. first compute each w; 3 x in parallel, where @ represents elementwise multiplication. By applying Cor. 5.2 in parallel kk' times, this can be done with circuit of depth 3 and size kk' (2 + 3p) Okk'). We also have k' circuits, each corresponding an index of the output, that compute the sum over the entries of each w; @ x. By Lem. 3, the composition of these two functions is computable by O n) -uniform circuit family of constant depth and size Ol+k') + O'O log k) = O(kk' log k).
The transformer's key, query, value, and output affine transformations with k k' S d. The trans- former also has affine transformations in the feedforward subnetwork with k. k' S (d, hj. So, the size of an affine transformation circuit in the transformer is at most
O(max log d, dh log h, holog df} O(max[d log d, dh l))
B.3 LAYER NORM
The layer norm is applied between sublayers in the transformer. Let p = (1/d) Ei= 24. The layer norm y E Fe of vector x E Fd is computed, for scalars b E Fp.
/ xx uill +
y a
The layer norm over vector of size d can be computed by uniform threshold circuit of constant depth and size O log d).
Lemma 10.
Proof. First compute d using summation over the constant term from 1 to d. This summation has a threshold circuit size of O(d log d) by Lem. 7. Then compute je using similar sum circuit, com- posed with the circuit computing d. Finally, we need compute ||x-
[xx]]]] 14|l which can be reduced to single summation by local functions (squaring and dividing) with O(d) overhead. Applying Lem. compose these functions yields a constant-depth uniform threshold circuit of size Ogd d). O
B.4 SELF ATTENTION
Define de, de S d. The self attention mechanism takes query q E n keys k, E F3e, and values V, 18.. It returns new vector y of size d, computed, for sis n,
y ai aaiZZv.
where = expp(q- k.) and Z = Σ Cij.
Lemma 11. Self attention is computable by O(log n) uniform threshold circuit of constant depth and size O(n logn).
Proof. We can compute each a; using only local functions. Computing takes one sum cireuit over scalars. For just need an addition summation circuit over terms and some local functions to compute each term. can apply Lem. to conclude that the composition of these circuits is computable by uniform threshold circuit of constant depth and size O(n log n).
14


Reviews:
[{"review_id": "h_VhLP07DE5", "reviewer": "Reviewer_51Kn", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "This paper shows that transformers can be represented by FO(M) formula (i.e. first-order logic with majority quantifiers), by showing that transformers can be compiled into a circuit in log-uniform $TC^0$, and then using the equivalence between log-uniform $TC^0$ and FO(M) provided in Barrington et al.1990.\n\nWhile the connection between transformers and circuits is not new, the proof in this paper is clean and subsumes the results in prior work that 1) hard-attention can only recognize $AC^0$ (e.g. Hahn 20, Hao et al. 22) and 2) saturated attention can only recognize $TC^0$ (e.g. Merrill et al. 22).", "summary_of_the_review": "This is a cute paper with interesting results and clean proof ideas, extending the line of work connecting transformers to circuits, and building new connection to formal logic (though the connection to logic is via Barrington 90 and not novel).\nThe paper is well structured overall with some writing details to be improved. ", "strength_and_weaknesses": "Besides the main result that transformers can be compiled into FO(M), there are some interesting implications:\n- If we treat transformer as a complexity class, then one implication of the result is that any problem that is complete for log-uniform $TC^0$ will be \"transformer-hard\". One example is division, which means transformer computation can be reduced to integer division.\n- This opens up the potential to connecting to logical formula, though the exact connection is left as future work.\n\nThe proof is short and clean, and even though there's not much new/complex proof techniques, the connection to the right prior work is clever. The main idea is that:\n- Thm 3, 4: a log-uniform computation graph $\\mathcal{G}$ can be compiled into a circuit in log-uniform $TC^0$.\n  - Cor 4.1: by the equivalence between log-uniform $TC^0$ and FO(M) shown in Barrington et al.1990, $\\mathcal{G}$ can also be compiled into a FO(M).\n- Thm 5, Cor 5.1: a poly-sized transformer can be compiled into a log-uniform $TC^0$ circuit and hence a FO(M) formula, by showing that every transformer component is computable by a poly-sized uniform threshold circuit family.\n\nThe connection between circuits (binary valued) and finite precision float-computation is given in Cor 5.2 (Appendix A.2).\n\nI don't have major complaints about the paper; here are some minor comments/clarifications:\n- the claim that the results help blur the boundary between symbolic and neural methods is interesting but also a bit of a stretch; I'd be more convinced if there's an exact compilation into FO(M) is provided, which is however currently left as future work.\n- footnote 4 on page 3: $X(\\sigma, i) = X(i + s)$: I don't follow this; e.g. why the sum?\n- Before Example 1, \"Let $\\Sigma = \\{a,b\\}$\": does this definition of $\\Sigma$ apply to the 3 examples only, or throughout the paper?\n- Table 1: what's the superscript 9 in $\\mathfrak{F}^9$?\n- Alg 1: I'm missing something here: is this a recursive function? If yes, wouldn't this recursion always return $\\varnothing$, since it's the only base case?\n- Besides Lem 5 & 6, are there other places that use properties specific to _threshold_ circuit?\n- Cor 3.1: not sure why this is called a corollary (of Thm 3?), since this is true by the definition of $XC^0$.\n- Proof of Thm 3: what is $a$ (assigning to $\\mathsf{edge}_{\\mathcal{G}}(n, i', j')$)?", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "Not applicable"}, "extra_text": {}}, {"review_id": "TOCB1AmMG6v", "reviewer": "Reviewer_bNHi", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "The paper establishes a connection between a form of first-order-logic and a significant class of NNs.", "summary_of_the_review": "The result looks important, but my score reflects my limitations in evaluating the work.\n\nQ; where dies FO(M) come from? I could see no reference in S2\nQ You seem to suggest it is more expressive than FO? I suppose the difference is in the ability to count solutions.Also. I assume correctness hold.\nQ:In my weak understanding, you graph->logic transformation and may generate complex Graphs and formulae. Would this be  such a great step in understanbility?\n\n", "strength_and_weaknesses": "Strengths:\nIt looks like an interesting result.\nWeaknesses:\nIt is unclear how useful a result it is.gooh", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "4: The contributions are significant, and do not exist in prior works.", "empirical_novelty_and_significance": "4: The contributions are significant, and do not exist in prior works."}, "extra_text": {}}, {"review_id": "Nssfq2_1hAk", "reviewer": "Reviewer_Yrxd", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "The paper claims that transformer networks can be represented by a constant-size formula of first-order logic with majority quantifiers; in turn, this means that the computation of such networks can be reduced to division, as division is complete for such problems.", "summary_of_the_review": "The construction used to prove the main claim relies on improbably efficient integer arithmetic. It is a significant gap in the proof.", "strength_and_weaknesses": "If correct, the claims in this paper are provocative and would be significant.\n\nUnfortunately, there is a significant gap in the proof and I'm not sure that the claims are true.\n\nIn more detail, in the proposed DLOGTIME-uniform construction of transformer networks, the algorithm uses multiplication and division of the arguments, specifically bnode(n,i) = \\lfloor i/bsize(n)\\rfloor and bstart(n,i) = i * bsize(n). The text claims, \"As bsize(n) = poly(n), these functions are reducible to arithmetic over O(log n)-bit integers, which can be implemented in O(log n) time.\" But, note that this claim is equivalent to arithmetic -- specifically here, multiplication and division -- of n-bit integers being implementable in O(n) time. I am confident that this is not known. A recent breakthrough by Harvey and van der Hoeven finally brought the complexity of multiplication down to O(n log n), but even this is not adequate for the needs of the construction. Since the DLOGTIME-uniformity of the circuits was the core of the argument, this seems to undermine the main claims of the paper.\n\nOf course, it is not known that these operations require superlinear time, so the claims could be weakened to include the hypothesis that multiplication and division are linear-time computable. Since this hypothesis seems doubtful, it certainly undermines the significance (or surprise) of the claims -- we just have that one seemingly unlikely thing implies another.", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "1: The main claims of the paper are incorrect or not at all supported by theory or empirical results.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "Not applicable"}, "extra_text": {}}, {"review_id": "Ges-X6IbTJ", "reviewer": "Reviewer_kJX7", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "This paper presents a simple translation from computation graphs with a constant depth, which describe many neural network models including Transformers, into a class of threshold circuits, i.e., DLOGTIME-uniform $TC^0$, or equivalently, expressions of first-order logic with majority quantifier. As a result, the limit of threshold circuits implies the limit of computation graphs like Transformers. \n\n", "summary_of_the_review": "The reduced threshold circuits closely resemble the topological structure of computation graphs. Given the computation graph has a finite depth, the reduced circuits also have a finite depth. Either conclusion like this made in this paper sound obvious, or there is something significant I do not really understand. To me, it is like claiming all modern computers are just finite-state machines (or regular expressions) because the size of the memory or hard disk can only be finite. \n", "strength_and_weaknesses": "Strengths:\n- although being fairly theoretical, the paper is well-written and properly introduces all the necessary backgrounds\n- the limit (or potential of neural network) models is justified formally and quantitatively, e.g., detailed bound analyses are provided.\n\nWeaknesses:\n- the idea is incremental compared to several recent works, especially MSS22\n- given this is a theory paper, conclusions would be excepted to be rigorous. However, some conclusions are either informal or misleading, including the title. Transformers can be translated (or compiled) into a class of threshold circuits TC0, which is equivalent to FO(M). This does not imply that TC0 or FO(M) can be implemented in Transformers.  Similarly, the fact that integer division is reducible to TC0 does not imply that Transformers is equivalent to some integer division. \n\n\n[MSS22] Saturated Transformers are Constant-Depth Threshold Circuits. William Merrill, Ashish Sabharwal, and Noah A. Smith. Transactions of the Association for Computational Linguistics, 2022.", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "Not applicable"}, "extra_text": {}}, {"review_id": "3Uzn7K5Tl1", "reviewer": "Reviewer_hzSU", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "This paper analyses transformers through the lens of logic, where the goal is explain the computation graph of a transformer (and of some other models) in terms of a formal language. The computation graph of most neural networks with a fixed number of layers is easily seen to be a directed acyclic graph. Hence, it is possible to characterise neural networks in terms of depth-bounded circuits ad the corresponding families AC0 or TC0. Using the well-known connection between (DLOGTIME-uniform)-TC0 and FO(M) - first-order logic with majority quantifiers- the authors show that any computation graph of a transformer can be represented in FO(M).", "summary_of_the_review": "Given my concerns in the review, I recommend a reject.", "strength_and_weaknesses": "Strengths:\n\n- There are big gaps in our understanding of large language models, and so a formal, logic-based analysis of transformers is interesting and  promising.\n\n Weaknesses:\n\n- The connection between circuit classes and neural networks is not new as claimed in the paper (and neither is the connection to logic) -  see, e.g., \"Parberry, Circuit Complexity and Neural Networks, 1994\". The difference is, of course, in analysing the modern neural network architectures with different assumptions (e.g., nonlinearities, real-values, etc), but it is by no means a new idea, as claimed in the paper: \"We derive the first, to the best of our knowledge, direct connection between a broad class of neural networks and the well-studied classical formalism of first-order logic.\" I strongly advise the authors to revisit the classical as well as recent literature on these topics.\n\n- Informally, the result of this paper is to show that any transformer model can be represented by a formula in FO(M). This follows from the fact that each computation graph of a transformer model can be represented by a DLOGTIME-uniform TC0 circuit, and each such circuit corresponds to a formula in FO(M). In my opinion, this is not a very strong result and I could not spot anything specific about transformers in their results.\n\n- The presented result does not tell us what class of functions transformers can capture. It only gives an upper bound on this (and details are not clear to me) in showing that the corresponding computation graphs can always be mapped to FO(M) - how about the other direction? Is it the case that any formula in FO(M) can be *uniformly* captured by transformers? \n\n- There are many related results for neural networks, see, e.g., \"Barcelo et al., The Logical Expressiveness of Graph Neural Networks, ICLR 2020\": they show that a particular class of graph neural networks can *uniformly* capture 2-variable first-order logic with counting quantifiers in the sense that for any formula in this logic, there is a corresponding graph neural network which precisely computes the function that this formula encodes. \n\n", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "1: The contributions are neither significant nor novel.", "empirical_novelty_and_significance": "Not applicable"}, "extra_text": {}}]

Author rebuttal:

Decision: Reject