Logical Languages Accepted by Transformer Encoders with Hard Attention
Authors: Pablo Barcelo
Alexander Kozachinskiy
Anthony Widjaja Lin
Vladimir Podolskii
Venue: ICLR 2024 poster (2024)
Keywords: transformer encoders
languages
AC0
first order logic
linear temporal logic
counting terms
parity
majority
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
TL;DR: We show that all languages definable in first-order logic with arbitrary unary numerical predicates can be recognized by transformer encoders with unique hard attention

Abstract: We contribute to the study of formal languages that can be recognized by transformer encoders. We focus on two self-attention mechanisms: (1) UHAT (Unique Hard Attention Transformers) and (2) AHAT (Average Hard Attention Transformers). UHAT encoders are known to  recognize only languages inside the circuit complexity class ${\sf AC}^0$, i.e., accepted by a family of poly-sized and depth-bounded boolean circuits with unbounded fan-ins. On the other hand, AHAT encoders can recognize languages outside ${\sf AC}^0$), but their expressive power still lies within the bigger circuit complexity class ${\sf TC}^0$, i.e., ${\sf AC}^0$-circuits extended by majority gates.
We first show a negative result that there is an  ${\sf AC}^0$-language that cannot be recognized by an UHAT encoder. On the positive side, we show that UHAT encoders can recognize a rich fragment of ${\sf AC}^0$-languages, namely, all languages definable in first-order logic with arbitrary unary numerical predicates. This logic, includes, for example, all regular languages from  ${\sf AC}^0$. We then show that AHAT encoders can recognize all languages of our logic even when we enrich it with counting terms. Using these results, we obtain a characterization of which counting properties are expressible by UHAT and AHAT, in relation to regular languages.

Published as a conference paper at ICLR 2024
LOGICAL LANGUAGES ACCEPTED BY TRANSFORMER ENCODERS WITH HARD ATTENTION
Pablo Barceló
Alexander Kozachinskiy
IMC, PUC Chile & IMFD Chile & CENIA Santiago, Chile
IMFD and CENIA
Santiago, Chile.
pbarcelo@uc.ct cl
a alexander 2lexxnder..ozachinnee koa.deerrkkkchinssyyeeeees......
Anthony Widjaja Lin
Vladimir Podolski
University of Kaiserslautern-ann
Tufts University Medford, USA
& Max-Planck Institute for Software Systems Kaiserslautern, Germany awl rrlnnmmpi-sie
vladimir. ptw.immmr.ooolllkiitfttf.oo
ABSTRACT
We contribute the study of formal languages that can be recognized by trans- former encoders. We focus on two self-attention mechanisms: (1) UHAT (Unique Hard Attention Transformers) and (2) AHAT (Average Hard Attention Transform- ers). UHAT encoders are known to recognize only languages inside the circuit complexity class AC i.e., accepted by family of poly-sized and depth-bounded boolean circuits with unbounded fan-ins. On the other hand, AHAT encoders can recognize languages outside AC"), ), but their expressive power still lies within the bigger circuit complexity class TC i.e., AC -circuits extended by majority gates. We first show a negative result that there is an AC "C -language that cannot be recog- nized by an UHAT encoder. On the positive side, we show that UHAT encoders can recognize rich fragment of AC -an-uangs namely, all languages definable in first-order logic with arbitrary unary numerical predicates. This logic, includes, for example, all regular languages from AC We then show that AHAT encoders can recognize all languages of our logic even when we enrich it with counting terms. Using these results, we obtain a characterization of which counting prop- erties are expressible by UHAT and AHAT, in relation to regular languages.
INTRODUCTION
Transformers have revolutionized natural language processing by facilitating the efficient and effec- tive modeling of intricate contextual relationships within text (Vaswani et al. (017). This remarkable
capability has sparked numerous investigations into the potential boundaries of transformers' power
(Hahn 2020 Yao et al., 2021, Pérez al. 202T, Weiss al. 2021 Hao
2022 Chiang &
Cholak 2022 Bhattamishra et al. 2020 C Chiang et al. 2023] Merrill et al. 2022 Merrill & Sabhar-
2023), One natural method for addressing this question to explore the classes of formal languages that these architectures can recognize. This approach provides an insight into their strengths and limitations. The response to this question naturally relies on the specific features al- lowed within transformer encoders. These encompass the interplay between encoders and decoders, the kind of functions used for positional encodings and attention mechanisms, and considerations of fixed or unbounded precision, among other factors.
While the capacity transformers that incorporate both encoders and decoders to recognize lan- guages is well understood today (indeed, such architectures Turing-complete and can thus rec- ognize any computable language (Pérez et al. 2021)), a precise characterization of the languages accepted by transformer encoders is lacking. Unique Hard Attention Transformers (UHAT) are class of transformer encoders that has been subject of many recent papers. As was shown by Hao et al. (2022). UHATs recognize only languages AC i.e., recognized by families of Boolean cir- cuits of unbounded fan-in that have constant depth and polynomial size. Intuitively, this means that

---

Published as a conference paper at ICLR 2024
UHAT's are weak at "counting" (more precisely, reasoning about the number of occurrences of vari- ous letters in the input word). For example, consider the following languages: majority and parity. The first one corresponds to the set of words over alphabet {a, b} for which the majority of positions are labeled by a, while the second checks if the numher of positions labeled a is even. That these languages are not in AC follows from a groundbreaking result in circuit complexity theory (Furst et al. 1981 Ajtai 1983). Hence, they are neither accepted by UHAT's However, which fragment of the AC languages can actually be recognized by UHAT's remains an unresolved question.
We start by showing that not all AC languages can be accepted by UHATs. This is obtained by combining results of [Ajaai (1983) and |Hahn] (2020). Based on the previous observation, we focus on identifying a rich fragment of AC that can in fact be embedded into the class of UHAT'. To achieve this, we use the characterization of AC the class of languages expressible in (AIl))), the extension of first-order logic (FO) with all numerical predicates defined in relation to the linear order of word (Immerman 1999). We show that UHATs recognize all languages definable in FMnM).). the restriction of AOl)))) with unary numerical predicates only (Barrington et al. 2005). The logic (M(Mon) highly expressive. Unlike FO, can express non-regular languages like fa= n > 0}. Remarkably, it contains all regular languages within AC which includes examples like (an)*
a language not definable in FO. Additionally, our result subsumes the result of Yao et al. (2021)
where it is shown that Dyck languages of bounded nested depth can be recognized by UHATs. These languages are regular and belong to AC hence they are expressible in (O
To establish the result that UHAT's recognize all languages definable in FO we take slightly circuitous route: rather than directly formulating FO(Mon) sentences as UHAT', we show that each formula in (.T..MMo)), the extension of linear temporal logic (T.TL.) (Clarke et al. 2018) with arbitrary unary numerical predicates, can be equivalently represented as an UHAT. The proof for FO(Mon) then derives from Kamp's seminal theorem (Kamp) 1968). which establishes the equiva- lence between languages definable in FO and LTL. The advantage of dealing with LTL, in contrast to FO, lies in the fact that all LTL formulas positions on a word, unlike FO formulas which possess arbitrary arity. This property aligns well with the expressive capabilities of UHATs, facilitating a proof through structural induction.
unary in nature, i.e., they are interpreted as sets of
While the fact that UHAT is in AC" implies limited counting abilities of such encoders, recent work has shown that a slight extension of the hard attention mechanism can help in recognizing languages outside AC (Hao et al. 2022). Instead using unique hard attention, this model uses averuge hard attention (AHAT), which refers to the idea that the attention mechanism returns the uniform average value among all positions that maximize the attention. To what extent does AHAT enrich the counting ability of UHAT? In answering this question, we introduce a logic named LTL(C, +). which is an extension of (Mon) that naturally incorporates counting features. We show that any language that can be defined within LTL(C, +) can also be identified by an AHAT. The logic LTL((C, +) can express interesting languages lying outside AC" including majority and parity. More generally, our result implies that AHAT' are equipped with a powerful counting ability: all permutation- languages over a binary alphabet and all permutation closures of regular languages (which are in general not context-free) can be recognized by AHATs.
As corollary, we provide a characterization of the "counting properties" of regular languages which can be captured by UHAT and AHAT. Two approaches for understanding counting properties of regular languages can be found in formal language theory: (1) Parikh-equivalene
and (2) taking petter-permuaation closure. Both approaches "remove" the ordering from the input string, and as result only the letter-count (more popularly called Purikh images) of an input string matters. In the setting of (1) (e.g. see (Parikh) 1966, Kozen 1997)), machine is allowed to (ry all letter reorderings of the input string w, and accepts iff the machine accepts some letter reordering of w. According to the well-known Parikh's s Theorem (Parikh 1966), each context-free language can in this way be captured by regular language, e.g., {0"1" n 0} can be captured by (01)*. We show in this paper that each regular language is Parikh--quivalent to UHAT language, despite the fact that PARITY is not in UHAT. In the setting of (2), a machine must accept all letter permutations of an input string w. The letter-permutation closure of a regular language is not necessarily regular, e.g., such a closure language of (abe)* consists of all strings with the same number of a's, b's, and c's, which is not even context-free. In this setting, although UHAT cannot capture regular languages like PARITY, AHAT can surprisingly capture all regular languages.
2

---

Published as a conference paper at ICLR 2024
Related work. There has been very little research identifying logical languages that can be accepted by transformers. The only example we are aware of is the recent work by Chiang et al. (2023), in which variant of first-order logic with counting quantifiers is demonstrated to be embed- dable into transformer encoders with a soft attention mechanism. The primary distinction between their work and our results is the choice of the attention mechanism. Additionally, the logic examined in their paper does not have access to the underlying word order being considered. This implies that some simple languages, such as a" which definable in FO, are not definable in their logic.
Due to the space constraints, some of the proofs are omitted and can be found in the online version of this paper (Barceló al. 2023
2 BACKGROUND NOTIONS AND RESULTS
2.1 TRANSFORMER ENCODERS
An encoder layer is function that takes sequence of vectors, Vo...., Vn-1, in Rd as input, where 2 produces an output sequence of vectors of the same length, Vo:... Vn 1. in RR with 2 0. The length of the sequence, n, can be arbitrary, but input and output dimensions, d and e, are fixed for an encoder layer. For the first part the paper we employ unique hard attention mechanism, meaning that a position only attends to the element with the highest attention score.
Formally, an encoder layer with unique hard attention is given by two affinte transformations A, B: R - I² and one feed-forward neural network W; 1ddd R' with ReLU activation func- tion. For i {O,...,,, n 1}. we set
a- j:
where ji (O,...,, }) is the minimum element that maximizes the attention score (Av;, Bv₃) over j E (0,...,n 1}. The 0,s are often known as attention vectors. After that, we set
v N ((;,,a))
i= 0,
It is well-known that feed-ford forward neural networks with ReLU activation express the function max(#, x. y}. Thus, we may assume that N can be an arbitrary composition affine functions with max.
Transformer encoder. A unique hard attention transformer encoder (UHAT is defined simply as the repeated application of encoder layers with unique hard attention.
2.2 LANGUAGES ACCEPTED TRANSFORMER ENCODERS
Next, define how transformer be used to accept languages requires extending transformer encoders with three features: a function for representing alphabet symbols vectors (which, for the purposes of this paper, we represent as one-hot encodings), another function that provides information about the absolute positions of these symbols within the input word, and vector that used for checking whether the word should be accepted or not. The function that provides information about positions is often referred to as a positional encoding, and is essential for recognizing properties of ordered sequences of vectors. fact, without positional encoding, encoders treat input sequences as invariant to permutations (Pérez et al., 2021).
finite alphahet. This
Consider a finite alphabet Σ and T be an UHAT that takes a sequence of vectors over IR as input and converts it into sequence of vectors over I A language L C Σ is accepted by T, if there is an embedding function f: Σ + Rd a positional encoding function p: x + IR and a vector t E R', such that for every E L we have 7" T'(w) (w) > O, and for every E Σ L we have (w) < O. Here, T' Σ+ + R defined as follows. Let to = an an E Σ" and suppose the output of T when given the input sequence f(ao) + p(0, n). ... 1() p(n 1, n) the
sequence Vo. -- Then we set (www) -t. vo).
'Some of the previous papers, for instance Hao et al. 2022 allow to use in UHAT only rational numbers. We find this too restrictive because functions such as cos and sin are widely used in practice. Nevertheless, we that results hold with this restriction, by taking good-enough approximations by rational numbers.
3

---

Published as a conference paper at ICLR 2024
2.3 FIRST ORDER LOGIC ON WORDS
We assume familiarity with first-order logic (FO), Let Σ be a finite alphabet. A word to = ag.-.up-1 in Σ+ is represented as a structure So whose domain is {0, (0,....7 1}. This struc- ture includes a binary relation < that is interpreted as the linear order on the domain, and for each where as a. Given an FO sentence over words, that is, an FO formula without free variables, we denote the language of all words w E E+ satisfying Sa F Φ as [()). If an L C Σ+ satisfies I = L(Ø), for some FO sentence 6, then we say that I, is definable in FO.
symbol a E Σ, there is a unary relation Pa containing positions i O,...,n
Example 1. First-order logic (FO) enables us to define certain languages of interest. Here, we present an illustrative example. Initially, we recognize that we can employ FO to define a relation first(z) == - < 2) that exclusively holds true at the first position of a word. Correspondingly, can define a relation last(z) := -3y(2 < y) that holds solely at the last position of the word.
Moreover, it is possible to define a binary relation succ y) := x < y A -3z(x < z A 2 < y), which defines the successor relation within the domain. With these expressions, we can show that FO is capable of defining the language (ab)*:
Ei (first(a)) A Pa())) A Ex (last(x) A Pa(x)) A Valy (succ(z, v) + (P) ++ Pa(s))).
That is, the first symbol of the word an a, the last one is b, every a followed by b, and every b is preceded by a.
2.4 UNARY NUMERICAL PREDICATES
is known that FO sentences can only define regular languages. In turn, there are regular languages that are not definable in FO, An example is the language (aa)", which contains those words formed solely by the symbol a that are of even length. However, there a straightforward extension of FO that can define this language: all we need to do is add unary predicate even(z). which holds true at position i in a word and only if is even. In fact, extending FO with the predicate even(x) allows us define the language (aa)* using the following formula, which indicates that the last symbol in the word satisfies the unary predicate even: V.Pa (c) A Vy(last(y) - even(y)).
The extension of FO with unary numerical predicates can then be useful for defining languages. We define a unary numerical predicate θ as an infinite family of functions
On : (0.....77) n) + {0,
n n>0 O.
Given a word @ in Σ of length n, for n >> O, we have that the predicate +(x) holds in position i in w if and only if 0 (i) 1 (so far, we do not use the value of 0, at n as positions are numbered from to n 1. We will use this value in Section 4). Notice that under our definition, the truth of a unary numerical predicate at position in the word w depends not only on é but also on the length of the word w. As we will explore further, this characteristic is advantageous for defining interesting languages in FO extended with arbitrary unary numerical predicates. Following the literature, we write FO(Mon) for such an extension (Barrington et al. 2005).
Example 2. Consider, for example, the non-regular language {a"b" n >> 0). We show that it can be expressed in FM(M) with the help of a unary numerical predicate Ozx) such that (n = iff n is even and n/2 1. In fact, it suffices use the formula: 3r (0(z) Pa(x) A Vy(y < x -- Pa (y)) A Vy(r < y + Po(y))) This formula expresses that the middle point of ø exists, is labeled as a, and all positions smaller than i are also labeled a, while all positions larger than i are labeled as b. This example illustrates the significance of unary numerical predicates depending on both the position and the length of the word over which the formula is evaluated.
The definition of the language L(Ø) C Σ defined by an FO(Mon) sentence & is analogous to the one we provided for FO.
3 AC LANGUAGES ACCEPTED BY UHATS
3.1 NOT ALL LANGUAGES IN AC ARE ACCEPTED BY UHATs.
Hao et al. 20022 proved that languages accepted by UHAT' belong the circuit complexity class AC i.e., the class of languages accepted by families of Boolean circuits of unbounded fan-in,
4

---

Published as a conference paper at ICLR 2024
constant depth, and polynomial size. We combine results by Ajtai (1883) and Hahn 2020) show that the opposite is not the case, i.e., there are AC languages that are not accepted by UHAT'.
As shown in Ajtai 1983). J. there is an -family of circuits {Cn; {0, 1J"h + {0, hey such that for all n. the cireuit Cn accepts all strings with at at least 2n/3 ones and rejects all strings with at most 12/3. Consider a language approximate majority, consisting of strings accepted by circuits from {Cr). J. This language is in AC by construction. However, as we state next, it cannot be recognized by an UHAT. This result is proved by using a property of UHAT's established [Hahn (2020).
Proposition 1. There is no UHAT that accepts the language approximate majority.
Viola (2009) shows that } can be made polynomial-tine computable, which implies the exis- tence polynomial-time computable language from AC that cannot be accepted by an UHAT.
3.2
MAIN RESULT: FO(Mon) LANGUAGES ARE ACCEPTED BY UHATS
Proposition | tells us that not all AC languages are accepted by UHATs. In this section, we identify significant subset of AC" languages that can be accepted by UHATs. To accomplish this, rely on the characterization of the class AC" those languages that can be defined in FO extended with arbitrary numerical predicates. Our main result establishes that as long as we restrict ourselves to unary numerical predicates, translation into UHATs is possible.
Theorem 1. Let E be a finite alphabet and & an FO(Mon) sentence over words from the alphabet E. There is UHAT that accepts L(6)).
Proving this result by induction on FO(Mon) formulas, which would the most natural approach to tackle the problem, turns out to be difficult. The challenge arises because the FO formulas obtained by induction can have arbitrary arity, and transformer encoders do not seem capable of handling the requirements imposed by such formulas. To address this issue, take different approach. We employ Kamp's Theorem, which establishes that the languages definable in FO are precisely those that are definable in linear temporal logic (LTT.) (Kamp) 1968).
3.3 USING (Mon) TO PROVE OUR MAIN RESULT
We first explain how LTL is defined, as this is crucial to understanding the remainder of the paper. Let Σ be finite alphabet. LTL formulas over Σ are defined as follows: if Σ, then a an LTL formula. Additionally, LTL formulas are closed under Boolcan combinations. Finally, if ø and ui are LTL formulas, then X and @Uù are also LTL formulas. Here, X referred to as the next operator, and U as the until operator.
LTL formulas are unary, i.e., they are evaluated over positions within word. Let w au.... Qn-1 be a word in Σt, and let i = O...., 1. We define the satisfaction of an LTL formula á over w at position i, written as (w., i) }= Φ), inductively as follows (omitting Boolean combinations):
(w, i) }= a if and only if a = a, for a E Σ. (w, i) = X if and only if
and (w,, i - Φb In other words, & holds in the next position after i (if such position exists).
(w. i) = @UT if and only if there exists position j j= == i,..... 72 1 for which (10 } sb and such that (w, k) } & for every l with i l < j. That is, ø holds starting from position i until the first position where 1 holds (and a position where & holds must exist).
We can extend LTL with unary numerical predicates in the same way we did it for FO. Formally, we define (Mo(Mon) as the extension of LTL with every formula of the form θ for O a unary numerical predicate. We write (w, i) } θ to denote that (i) 1, where is the length of w. If ő is an LTL.(Moo (Mon) formula over Σ, we write [(ő) for the set words w E Σ+ with (w. 0) } Φ.
Kamp's 's Theorem establishes that for every FO sentence & there exists LTL formula v such that I(Ø) = T.(b),, and vice-versa. It is straightforward to see that this property extends to the logics FO(Mon) and (Mon).
Proposition 2. KKmp 1968) For every FO(Mo)) sentence @ there exists an (ML) eb such that [()) L(1), and vice-versa.
5

---

Published as a conference paper at ICLR 2024
Our proof of Theorem T then derived directly from Proposition and the following result. Proposition 3. Let Σ be finite alphabet and & an LTL(MMn)) formula defined over words from the alphabet E. There is an UHAT T that accepts L(().
Before proving this result, we make the following important remark regarding the positional encod- ing used by T to accept [()). On a pair (i, E N x N with i < n, we have that p(i, n) is composed of elements i, 1/(+1), (-1)', , cos (s(1-27)/10). sin (=(1-27)/10). and on (i), for every unary numerical predicate @ mentioned in Φ.
Proof of Proposition Let Φ be formula of (.TT.(Mon). We say that UHAT realizes & position- wise if, given a word w ag ... an-1 E Σt, the UHAT outputs a sequence:
I( 0) = Φ). [( 1) + o). ..... I((w,
that is, binary word indicating for which positions & is true w and for which is false. We show by structural induction that every LTT.(Mon) formula realizable position-wise by some UHAT.
Let us consider first the base cases. If a, for some E Σ, our goal is obtain sequence:
T(ao = a), I(a = a),
T(am-1 = a).
This can easily be achieved by using a one-hot encoding as the embedding function. In turn, if o = O, for unary numerical predicate, then & can be realized position -wiee using the corresponding positional encoding p(i, n) = (1).
We continue with Boolean combinations. They can be implemented position wise by compositions of affine transformation and max as follows: - = 1 - x² and x V y (2x-1221..2-- 11++1
For the cases when our formula is of the form X or @Ub, need the following lemma.
Lemma 1. There is an UHAT' that transforms each To, .o.....,n-nn. E (0. 1) as follows:
Fo, In- In-1 + 20: 22 0.
Let assume now that our formula is of the form XΦ. It is enough to design unique hard attention layer in which attention is always maximized at the next position. More precisely, we construct UHAT that outputs a sequence of vectors Vi...., V, R., and linear transformation A: R + R.3 such that arg maxjeN (Av, v,) {i+ 1}. for i O.....
2. This will allow us ) to the éth position, for i = 0, O...., 2. It only remains then to apply Lemma to obtain 0 = I[ n - 1) F XØ} at the last position.
to "send" If i + 1) + o} (w. i) + XØ)
Using our positional encoding and an affine position-wis wise transformation, we can obtain:
2 2
[T(1 2
(-1)
V
=
Cos
sin
10
10
Let A be linear transformation that inverts the sign of the third coordinate. Observe that:
(Avi, Vz) = cos (2 (2--2) + (-1)++5+1
10. .10.
10
We claim that, for a fixed i, this quantity is maximized at i 1. First, those js that have the same parity as i (in particular, j = i) cannot achieve the maximum because the second term is -10. For js with a different parity, we have (Av,, = cos (5(2 22220010)//0) + 10. Since all angles are in |-x/10, x /10), this quantity is maximized when |2- 2- is minimized. For j < i, the last quantity is at least 2 and for j the minimum of this quantity is 2 achieved at
11/10)
1.
Let us finally assume that our formula is of the form ΦUv. Observe that the value of ΦUv at position i can be computed as follows: we go to the right, starting from the ith position, until we see a position je where either ò is false, or 1p is true, or this is the last position. Then @Uv holds at i and only if holds j.. That is, (10 i) } if and only if (w, - vb, where ji fi....,
is the minimal position with r(j) = 1, where, in turn, the sequence 7 is defined by r(1) = [[ i) 1}. for i O,..., n 1. To compute the sequence t, we first compute @ -
me v vb v Vii

---

Published as a conference paper at ICLR 2024
position-wist wise (we can do that because we already have & and s our disposal), then we add the conjunction with I[ + n n-11 by Lemma and then we take the negation of the resulting sequence.
To show the lemma, it is enough to create unique hard attention layer, where for every position i the attention maximized at j:. Using our positional encoding and the induction hypothesis, we can obtain sequence of vectors Vi,..., Vn E R.d such that:
T 2
(11 )
1, -(i).
Vi cos
sin
10
10
Consider a linear transformation
B: R + R such that
<<1 - 2
T - - (1)))),))
Bv; = cos
sin
10
10
+ (0), We claim that this expression is maximized at j = Jr. First, because of the last term it, it cannot be maximized at j with T(j) = 0. remains to show that among the js with (w.j) +fr Φ, this quantity is minimized on the minimal which is at least i. In fact, in this case we have (vi, Bv2) = cos -(2-'-2-1) + 10. All the angles in question are in |-x/10, π 7/10], so the cosine is maximized when |2 2- is minimized. Now, this absolute value is at least 2 when < i. In turn, this absolute value is smaller than 2 for j 2 i, and it is the smaller the smaller is j. as required.
Observe that (v,, Bvj) cos
1-2
10
3.4 APPLICATIONS OF OUR MAIN RESULT
We show two applications of our main result. First, UHAT' accept all regular languages in AC Second, UHAT's are strictly more expressive than regular and context-free languages in terms of the acceptance of languages up to letter-permutann
Regular languages in AC There is an important fragment of FO(Mon) which is interesting in its own right. This is the logic FO i.e., the extension of FO with unary numerical predicates of the form Mod for p > and 0 S S p 1. We have that Mod = if and only if i = r (mod p)- In fact, by using a characterization given in Barrington al. 1992,. , one show that the languages definable in FO(Mod) are precisely the regular languages within AC Then: Corollary 1. Let L. C E be a regular language in AC There is an UHAT that accepts L.
Although not all regular languages are accepted by UHATs (e.g. parity), we can use Theorem to show that, up to letter setterpermutation, UHAT is in fact strictly more powerful than regular and context-free languages.
Recognizing regular languages up letter-permutation
To formalize our result, we recall the notion of semilinear sets and the Parikh image of a language. linear set S a subset of Nd (for some positive integer d, called dimension) of the form vo + Ex v.N := E k; ki....,k, ky E N} for some vectors Vo E Nd. A semilinear sei S over Nd is finite union of linear sets over Nd. Semilinear sets have very tight connection to formal languages through the notion of the Parikh image a language (Parikh) 1966). which intuitively corresponds to the set of "letter-counts" of L. More precisely, consider the alphabet E = {a1,..., aa) and a language I. over Σ. For a word w E Σ, let |w]a,, denotes the number of occurrences of a, in w. The Parikh image P(L) of L is defined (Jwlai... ( E Nd for some word w E L. For example, if L = {a"t" n 2 0} and L' (ab)*, then P(L) P(L'). In this case, we say that L and L' are Parikh-equivalent. Note that L' is regular, while L is context-free but not regular. This is not coincidence based on the celebrated Parikh's Theorem (cf. |Parikh| (1966), also see Kozen (197p).
be the set of tuples
Proposition 4 (Parikh (1966)). The Parikh images of both regular and context-free languages coin- cide with semilinear sets.
In other words, although context-free languages are strict superset of regular languages, they are in fact equally powerful up to letter seterrpermutatton. What about UHATs? We have that they are strictly more powerful than regular and context free languages up to letter permutatonnn..onn Proposition 5. Each regular language has a Parikh- equivalee language accepted by an UHAT. In turn, there is an UHAT language with Parikh- Parikh-equivalent regular language.
7

---

Published as a conference paper at ICLR 2024
4 LANGUAGES BEYOND AC
Transformer encoders with unique hard attention can only recognize languages in AC but a slight extension of the attention mechanism allows recognize languages lying outside such class (Hao al. 2022). this section, we show that in fact such an extended model can recognize all languages definable in a powerful logic that extends LTL with counting features. This logic can express inter- esting languages outside AC", such as majority and parity.
4.1 AVERAGE HARD ATTENTION
For the results in this section, we consider an extended version of transformer encoders that utilize an average hard attention mechanism (Pérez al. 2021 Hao al. 2022). Following the literature, we call these AHAT.
Encoder layer with average hard attention. As before, these layers are defined by two affine transformations, A, B: Rd + Rd and one feed-forward neural network W: g2d + R with ReLU activation function. For every E {O...., n-11, we define S; the set of positions {O..... 1} that maximize (Av,, Bvy). We then set
ΣΣ v2 /15 JES,
a;
After that, we set v/ t (V,,, ax), for each 0, .......7 n That is, attention scores under average hard attention return the uniform average value among all positions that maximize attention.
We also use future positional masking that allows us take into account only positions up to If the future positional masking is used, the sets S; are defined sets of positions E {0, 1, ..... i} that maximize (Av,, Bv,)- Positional masks have been employed on several occasions theoretical papers (Yao et al., 2021 [Bhattmishra et al.] 22000; Hao et al.) 2022) as well as in practice, for example, for training GPT-2 (Radford et al. 2019).
4.2 LTL EXTENDED WITH COUNTING TERMS
We present here LTL((C, (C, an extension of (.TT.(MM)) that allows us to define counting properties over words in simple manner. This requires the introduction of counting terms defined next.
Counting terms. Suppose & is a unary formula. Then #6 and #6 are counting terms. The interpretation of these terms in position of a word w of length is defined as follows:
#6(0, i) Kij {O....,.)
{}
(w, )) F Φ)1, #o(Ø, i) Hj (i...., n 1) (w.j) o1
That is, #o(w, i) is the number of positions to the left of i (including i) that satisfy á. while # (w; i) the number of positions to the right of (including i) that satisfy Φ. Notice that, for words of length n, counting terms take values in {0, 1, nR..
Counting formulas. With counting terms and unary numerical predicates we can create new for- mulas in the following way. Let ø be unary formula and @ unary numerical predicate. We define new formulas O #6) and (##)). The interpretation of such formulas on position of word of length n is as follows:
(w, i) + O (##) + (+ i)) =
(w, - O + 0, 0,(#o(0, i)) =.
That is, the number of positions to the left (resp., right) of i (including i) that satisfy satisfies the predicate O As counting terms can take value n. the value of 0, on becomes useful.
We also incorporate into our logic the possibility of checking linear inequalities with inte- coefficients over counting terms. More specifically, for any finite set of unary formulas dI...., 2k, 11 thx, and for any coefficients cI,... Ck, di...., ......., dl we can create a formula:
Σ Cj #Ø; Ej=1d
dj #bb 2 0, which is interpreted as follows:
(w, = Σ
Cj #のズ
Σ dj
#b 2
Σ oj (0, + Σ dj ( 0.
==1
==1
f=1
8

---

Published as a conference paper at ICLR 2024
The logic LTL(CC +). We denote by LTL(C, +) the logic that is recursively defined follows:
Every formula (Mon) is also an LTL(C,+) +) formula.
Boolean combinations of LTL(C,++) formulas LTL(CC+)) formulas.
If Φ and va are LTT(CC,++ +) formulas, then so are X and @Uv.
If o is an LTL(CC +) formula and è is a unary numerical predicate, then ( and @ LTL(C,++ +) formulas.
If .i.... 62. Vi...., th are formulas of LTL(C,+), then Σj #0J + Eド= 13
#0 2 O, is formula of LT)
4.3 LTL(C)) DEFINABLE LANGUAGES ARE ACCEPTED BY ENCODERS
Next, we state the main result this section: languages definable by LTL(C,+ +) formulas are accepted by transformer encoders with average hard attention.
Theorem 2. Let E be a finite alphabet and & an LTL(C, formula defined over words from the alphabet E. There is an AHAT T that accepts L(Ø).
As a corollary to Theorem 2 we show that AHATs are rather powerful in counting. To make this claim more formal, we study pwwmutation-
languages, i.e., languages L such that iff any detter-permutation of is in L. For a language L, we write perm(L) ()) to be the permutation-closure cloosur of L, i.e., perm(e)mm))))))) (w P(w)) P(O), for some E L). Observe that perm((abe) consists of all strings with the same number of occurrences of a, b, and c; this is not even context-free. Owing to Parikh's Theorem, to recognize perm([)) LL), where T. is a regular language, an ability to perform letter-counting and linear arithmetic reasoning (i.e. semilinear set reasoning) is necessary. AHATs possess such an ability, as shown by the following corollary.
The permutation closure perm L.) of any regular language T. is accepted by AHAT: Moreover, any permutation-clant language over a binary alphabet is accepted by an AHAT.
Corollary 2.
Both majority and parity are permutation-closed and are binary alphabet. Hence, by the previous result, they are both accepted by AHATs. While for majority this was known (Hao et al., 2022], the result for parity is new.
CONCLUSIONS AND FUTURE WORK
We have conducted investigation of the problem of which languages can be accepted by trans- former encoders with hard attention. For UHATs, we have demonstrated that while they cannot accept all languages AC", they can still accept all languages by the logic FMoM).). Crucial to the proof of this result is the equivalence between FO and LTL, as provided by Kamp's Theorem. turn, we have shown that AHATs are capable of expressing any language definable in powerful counting logic, LTL +), that can express properties beyond AC This implies, among other things, that the parity language be accepted by an AHAT.
'monadic' version of it defined
In a work of Angluin et al. 2003), contemporaneous to ours, it was shown that the logic FO exactly captures languages, accepted by UHATs with positional masking and finite-valute positional encoding. At the same time, with our technique, it can be shown that there are languages beyond FO(Mon) that can be accepted by UHAT's with infinite-valued positional encoding, for instance, the language of palindromes. The idea is that since we do not use positional masking, we can use arbitrary order on positions, in particular, one that puts the language of palindromes into FO(Mon).
Due to the space constraints, we omit a more detailed discussion of this.
ACKNOWLEDGMENTS
Barceló and Kozachinskiy are funded by Millennnennium Science Initiative Program ICN17002 and by the National Center for Artificial Intelligence CENIA FB210017, Basal ANID. Anthony Lin was supported by European Research Council under European Union's Horizon research and innovation programme (grant agreement no 101089343).

---

Published as a conference paper at ICLR 2024
REFERENCES
Miklós Ajtai. -formuulae on finite structures. Ann. Pure Appl. Log., 24(1):1-48, 1983.
Dana Angluin, David Chiang, and Andy Yang. Masked hard-attention transformers and boolean rasp recognize exactly the star-free languages, 2023.
Pablo Barceló, Alexander Kozachinskiy, Anthony Widjaja Lin, and Vladimir Podolskii, Logical lan- guages accepted by transformer encoders with hard attention. arXiv preprint arXhv:2310.03817, 2023.
David A. Mix Barrington, Kevin J. Compton, Howard Straubing, and Denis Thérien. Regular lan- guages ne" J. Comput. Syst. Sci., 44(3):478 499, 1992.
David A. Mix Barrington, Neil Immerman, Clemens Lautemann, Nicole Schweikardt, and Denis Thérien. First-order expressibility of languages with neutral letters The crane beach conjec- ture. Comput. Syst. Sci., 70(2)101-127, 2005.
Satwik Bhattamishra, Kabir Ahuja, and Navin Goyal. On the ability and limitations of transformers to recognize formal languages. In EMNLP, pp. 7096-7116, 2020.
David Chiang and Peter Cholak. Overcoming theoretical limitation of self-attention. ACL, pp. 7654-7664, 2022.
David Chiang, Peter Cholak, and Anand Pillay. Tighter bounds on the expressivity of transformer encoders. ICML, volume 202, pp. 5544-5562. PMLR, 2023.
Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron A. Peled, and Helmut Veith. Model checking, 2nd Edition. MIT Press, 2018.
Merrick L. Furst, James B. Saxe, and Michael Sipser. Parity, cireuits, and the polynomial-time hierarchy. In FOCS, pp. 260-270. IEEE Computer Society, 1981.
Michael Hahn. Theoretical limitations of self-attention in neural sequence models. Trans. Assoc. Comput. Linguistics, 8:156-171, 2020.
Yiding Hao, Dana Angluin, and Robert Frank. Formal language recognition by hard attention trans- formers: Perspectives from circuit complexity. Trans. Assoc. Comput. Linguisties, 10:800-810, 2022.
Neil Immerman. Descriptive complexity. Graduate texts in computer science. Springer, 1999.
H. W. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, 1968.
Dexter C. Kozen. Automata and Computability. Springer, 1997.
William Merrill and Ashish Sabharwal. The parallelism tradeoff:: Limitations of log-precision trans- formers, 2023.
William Merrill, Ashish Sabharwal, and Noah A. Smith. Saturated transformers are constant-
depth threshold circuits. Trans. Assoc. Comput. Linguistics, 10:843-856 2022. URL https:
Rohit Parikh. On context-free languages. ACM, 13(4):57--881, 1966. doi: 10.1145/321356. 321364.
321364
Jorge Pérez, Pablo Barceló, and Javier Marinkovic, Attention is turing-complete. J. Mach. Learn. Res., 22:75:1-75:35,, 2021.
Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, Ilya Sutskever, et al. Language models are unsupervised multitask learners. OpenAl blog, 1(8)99 2019.
Lena Strobl. Average-hard attention transformers are constant-depth uniform threshold circuits, 2023.
10

---

Published as a conference paper at ICLR 2024
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In NeurIPS, pp. 5998 80880008, 2017.
Emanuele Viola. On approximate majority and probabilistic time. Computational Complexity, 18: 337-375, 2009.
Gail Weiss, Yoav Goldberg, and Eran Yahav. Thinking like transformers. In ICML, volume 139, pp- 11080-1 11900, 2021.
Shunyu Yao, Binghui Peng, Christos H. Papadimitriou, and Karthik Narasimhan. Self-attention networks process bounded hierarchical languages. In ACL/MCNLL, pp. 3770-3785, 2021.


Reviews:
[{"review_id": "4gymZUSaOq", "reviewer": "Reviewer_ceMz", "summary": "Review\n======\n\nAs a non-IA specialist but a circuit-complexity and automata specialist,\nI found those connection amusing but slightly artificial.\nI will not express myself on the pertinence of analizing the expressivity\nof those models from IA-perspective but provides a bit of insight about\nthe automata/circuit complexity side.\n\nFirst I found some claim dubious:\n\nIn a footnote you claim that only rational numbers where used in Hao (2022)\nbut generalize it real numbers.  It is known in complexity theory  that going from rational to real number is always complicated. Even\ncalculability theory can become weird when considering real numbers.\n\nWhile it is rather clear that computation performed by UHAT can be computed\nin AC0 when restricted to rational numbers, it is much less clear when going\nwithin rational numbers. If it holds, it by the sake of some continuity and\napproximation by real numbers arguments, but it deserves some details...\nI believe it should be explained.\n\nBecause I don't really get that, I have assumed that the remaining where\ndone on rational numbers;\n\nAbout the question about \"what fragment of AC0, UHAT can belongs to\", since it\ncontains all regular languages in AC0, it is improbable that you can find\na sound answer for that since it is already wide open for regular languages.\nIndeed:\n- regular language are complete for each level of the depth hierarchy AC0, \n- regular language are in quasilinear AC0 and proving that they are linear AC0\nis a long standing open problems (see the survey of Koucky on the topic).\n\nAbout Proposition 1. I believe a much simpler argument can be used using\na simple padding argument: \n\n>AC^0 recognized all languages up to exponential padding. \n>That is, Pad(L) = { u #^{2^|u|} \\mid u in L } is always in AC^0 whatever is L. \n>Your UHAT shouldn't be able to capture all Pad(L) as it only can remember a small\n>piece of information and convolute it. Basic information theory/pigeon hole might\n>help to conclude without a hammer of sensitivy of circuits within AC0.\n\nAbout proposition 5: I don't really understand why the Parikh\nclosure/permutation closure of languages is meaningful here. Sounds like an\narbitrary property to me.\n\n\nLogic with counting operators has been introduced in the past (Majority logic)\nand a study of its expressivity with respect to circuit classes.\nSee for instance (https://link.springer.com/chapter/10.1007/978-3-642-02737-6_7)\nIs there a connection?", "questions": "Comments \n========\n- The last sentence of the second paragraph of section 2.2 makes no sense.\nf is a function from Sig -> R^d, T: Sig^+ -> R et the last sentence\nsays that T get an input sequence that type as a sequence of vectors of R\"e.\nThe value of T(w) = (t, v0) only depending of t and v0 which is plain weird\nas it gives the impression it depends of a constant (t) and v0 which is f(a_0) + p(0, n).\nThe whole paragraph is thus buggy.\n\n- You can have some feelings on what is going on with logic extended with monadic\npredicates through this paper.\n\nhttps://dl.acm.org/doi/10.1145/3091124\n\n- About your open question: \nAdditionally, does there exist a language in the circuit complexity class TC0, the\nextension of AC0 with majority gates, that cannot be recognized by AHATs\n\nI would go for Dyck language. Sounds hard for a AHATs.", "limitations": "", "rating": 6, "confidence": 2, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "The paper contribute to a fun connection between formal language theory in order to analyze the expressivity of transformers. This line of research sounds more like research performed in TCS than in IA tracks but since it is apply to IA-defined model it makes some sense. Understanding the expressivity of those model might be enlightening to people actually playing with them.", "weaknesses": "Some of the contribution sounds really artificial to me. In particular, why should we study the commutative closure of language defined by transformers? While it makes sense in TCS, I fail to grasp the importance in this context.", "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": "", "extra_scores": {}}, {"review_id": "AKDtHrK1lL", "reviewer": "Reviewer_wdZx", "summary": "This paper investigates whether circuit language can be accepted by existing transformer encoders with hard attention. Specifically, this work concludes that UHATs cannot accept all languages in $AC^0$, but they can still accept all languages in a ’monadic’ version. Besides, \nthis work finds out that AHATs, other transformer encoders, can express any language definable in a powerful counting logic. Moreover, this work provides sufficient theoretical justifications to support their findings and conclusions.", "questions": "Please refer to the weakness of the questions that I proposed.", "limitations": "", "rating": 3, "confidence": 3, "soundness": 2, "presentation": 2, "contribution": 2, "strengths": "1. The study about whether circuit language can be accepted by existing transformer encoders is interesting and impressive. \n2. The paper offers comprehensive theoretical justification to demonstrate and validate their findings.", "weaknesses": "1. The structure of this paper is very messy, which is very hard to follow. Let me take the Section Introduction as an instance:\n\n1.a In Section 1 Introduction, the paper claims that \"the expressive power of transformer encoders\nhas not been fully elucidated to date.\". I am curious about that. What do you mean they are not fully elucidated?\n\n1.b I am very confused about the challenges of studying the circuit language. I could not find any information to discuss the existing challenges and related works, which makes it hard to understand the motivation for this work.\n\n1.c What are your contributions to this work? I could not find any conclusions about contributions after reading this section, or even the whole manuscript.\n\n\n2. The paper has a very weak introduction to related works, making this work hard to understand and compare.\n\n3. I would suggest that an illustration figure be provided to clearly show the main idea of this work.", "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": "", "extra_scores": {}}, {"review_id": "5eUXqQmF27", "reviewer": "Reviewer_maoo", "summary": "This paper studies the expressiveness of Transformer encoders by establishing their relation with a class of formal languages called circuits. Based on prior work, the main theoretical claims of the paper are:\n\nPrevious works have demonstrated that UHAT transformers (similar to Transformers with hard attention) cannot recognize languages beyond AC^0 (informally: circuits of polynomial size and constant depth). This paper further finds an example problem class within AC^0 that cannot be recognized by UHAT, which demonstrates that AC^0 is not a “lower bound” of UHAT.\n\nThe paper further establishes a class of problems that can be recognized by UHAT.\n\nResults are then extended to AHAT (Transformers with averaged head attention).", "questions": "Some important assumptions seem to be missing.\n\nIt would be nice to discuss the relation between this paper and the missed related work mentioned in the weaknesses section.", "limitations": "", "rating": 3, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "Justifying the expressiveness of Transformers through the length of formal language is a very important topic and could lead to better understanding of the working mechanisms of Transformers. This paper strengthens prior theoretical results and better bounds the expressivness of UHAT and AHAT.", "weaknesses": "Although the theoretical results themselves sounds interesting, I found some definitions and assumptions are not approprately stated, which potentially leads to incorrect results. While it is possible that the theoretical results still hold after fixing all the problems, I think the paper needs a major revision to ensure its validity.\n\nMissing important restrictions when defining the transformer model. \n\n- Precision of the number processed by the transformer. The paper does not include any restriction on the precision of the numbers processed by the transformer. This could make the model unrealistically expressive as discussed in many related work (e.g., proving Turing completeness of RNNs require relaxations on the numerical precision). In related works, a realistic assumption could be log-precision transformers, i.e., the number of floating/fixed-point bits scale logarithmically with the sequence length.\n\n- No assumptions have been made about the number of transformer layers. Prior work usually assume constant depth or logarithm depth (w.r.t. sequence length). Related to this assumption, it seems that the proof of Proposition 2 constructs a Transformer whose number of layers depends on the form of input LTL. This makes it particularly important to make the correct assumption.\n\n- Structure of the model. The model does not include residual connections and only uses single-head attention. Also the ReLU layer only applies ReLU to a single element of the input vector. Although these might be able to adapt in the proof, it would still be nice to make these assumptions as practical as possible.\n\nMany related works are missing. The paper states that “there has been very little research on identifying logical languages that can be accepted by transformers”. However, with a quick google scholar search, I found the following highly-related papers not cited in the paper. It would be nice to discuss the relation of this paper’s results with these prior works.\n\n[1] Merrill, William, Ashish Sabharwal, and Noah A. Smith. \"Saturated transformers are constant-depth threshold circuits.\" Transactions of the Association for Computational Linguistics 10 (2022): 843-856.\n\n[2] Merrill, William, and Ashish Sabharwal. \"The parallelism tradeoff: Limitations of log-precision transformers.\" Transactions of the Association for Computational Linguistics 11 (2023): 531-545.\n\n[3] Strobl, Lena. \"Average-Hard Attention Transformers are Constant-Depth Uniform Threshold Circuits.\" arXiv preprint arXiv:2308.03212 (2023).", "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": "", "extra_scores": {}}, {"review_id": "sJ9CfhkWyt", "reviewer": "Reviewer_auhY", "summary": "The papers is a contribution to the exciting and challenging domain of characterizing expressivity of transformers. The authors focus on the  Unique Hard Attention Transformers (UHAT). Previous results have shown that $UHAT \\subseteq AC^{0}$, where $AC^{0}$ is the circuit complexity class of circuits with constant depth, with unlimited fan-in  $AND$, and $OR$ gates. The author's first result is to show that  $UHAT \\subset AC^{0}$. The key contribution of the paper is that First Order Logic on words with unary numerical predicates (i.e. unary boolean functions on positions of the symbols in a word, and the length of the word) is readable by UHAT. They denote this fragment with FO(Mon), the proof strategy used by authors relies on a classic result in logic known as the Kamp's theorem, which says that FO(Mon) is equivalent to another type of logic, known as the Linear Temporal Logic (Mon) i.e. the extension of LTL with unary numerical predicates. The authors then design vector encodings and positional encodings that allow evaluation of any LTL (Mon) formula using a UHAT. Finally, they show the applications of their results by comparing them to other types of formal languages.", "questions": "- In my understanding, in section 2.2 paragraph 2, it is unclear to me why you set $T(\\bar{w})$ to $\\langle \\mathbf{t},\\mathbf{v}_{0}\\rangle$. \n- [Minor Comment] Page 6, \"reverses the third coordinate\" is not a very precise statement. \n- When is the notion of $T(\\bar{w}) > 0$ (as introduced in section 2.2), used as the criterion in proof on page 6 and page 7. From this proof, I just see that you can perform LTL operations on input strings, but I am not sure how this shows that a string in the language will never be mapped to a string outside the language?\n- Does Kamp's theorem give any bounds on the length of equivalent FO(Mon) equivalent formula in LTL(Mon)?", "limitations": "", "rating": 8, "confidence": 3, "soundness": 2, "presentation": 2, "contribution": 4, "strengths": "Formal properties of transformers are not very well-understood, and analyzing them w.r.t. the formal languages they accept is a very exciting and challenging direction. The author's provide significant contributions in this direction, and the paper contributes many new results and ideas that can contribute to theoretical investigation of transformers. Writing is quite clear, the proof though hard, seems to consist of clear arguments (I mention my confusions in the questions).", "weaknesses": "The proof on Page 6 and Page 7 could be further clarified. Although, the structural induction arguments are clear, but I am not sure how this is consistent with the meaning of accepting a word as part of the language --- which authors define earlier (See questions)", "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": "", "extra_scores": {}}, {"review_id": "FAgUIzTQOy", "reviewer": "Reviewer_yxZd", "summary": "This paper theoretically analyses the formal languages that transformer encoders can recognize. \nThe paper analyses two classes of transformers depending on the attention mechanism. The first class is \nunique hard attention transformers (UHAT), and the second class is average hard attention transformers (AHAT). \nIt is known that UHAT encoders can only recognize languages inside the circuit complexity class $AC^0$. AHAT\ncan recognize languages outside $AC^0$, but its expressive power still lies in the circuit complexity class $TC^0$.\n\nThis paper gives new theoretical results on the topic. The main findings of the paper are:\n- There is a language in $AC^0$ that UHAT cannot recognize.\n- UHAT can recognize all languages definable in first-order logic with arbitrary unary numerical predicates. The class includes all regular languages in $AC^0$.\n- AHAT can recognize all languages definable by LTL(C, +), which is an extension of the logical language acceptable by UHAT with counting terms.", "questions": "On p.6, the paper says, \"Observe that $(\\bar{w}, i) \\models \\phi U \\psi $ if and only if $(\\bar{w}, j_i) \\models \\psi$.\" I wonder what happens if there exists $i \\leq j^\\prime < j_i$ such that $(\\bar{w}, j^\\prime) \\models \\psi$\"? Following the definition on page 5, I think $(\\bar{w}, i) \\models \\phi U \\psi$ holds if there exists such $j^\\prime$.\n\n\n**Minor comments:**\n- **Abstract:** outside AC^0) -> AC^0 ?\n- **page2, before related work:** it have been shown before that parity can be accepted by an AHAT -> it has not been shown before that parity can be accepted by an AHAT?\n- **p.5, first paragraph:** at at least 2n/3 -> at least 2n/3\n- **Appendix, proof of lemma1:** max{0, x_i + i - (n+1)} -> max{0, x_i + 1 - (n-1)}?", "limitations": "", "rating": 8, "confidence": 3, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "**Important topic, impressive results:**\n Since the transformer is one of the most important neural architectures, understanding its expressiveness in a formal way seems an important topic. This paper brings progress on this topic by relating the expressive power of transformers with logical languages.\nThis connection results in identifying some important language classes that can be acceptable by UHAT, e.g.,  all regular languages in $AC^0$.\n\n**A clearly written paper:** The paper is very clearly written. I feel no difficulty in reading the paper. \nThe background needed to understand the contribution is concisely explained in the paper. \nProofs of important theorems are shown in the main body of the paper, and they are easy to follow.\n\n**New approaches for proofs.**\nThe paper uses the relationship between first-order logic and linear-time logic to prove the main results. This technique seems not\nused in the previous papers analyzing the expressive powers of transformer encoders.", "weaknesses": "Currently, I have no clear reason to reject the paper.", "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": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (poster)