Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning
Authors: Marco Sälzer
Eric Alsmann
Martin Lange
Venue: ICLR 2025 Poster (2025)
Keywords: transformer
formal reasoning
complexity
Primary area: interpretability and explainable AI

Abstract: We analyse the complexity of the satisfiability problem, or similarly feasibility problem, (trSAT) for transformer encoders (TE), which naturally occurs in formal verification or interpretation, collectively referred to as formal reasoning. We find that trSAT is undecidable when considering TE as they are commonly studied in the expressiveness community. Furthermore, we identify practical scenarios where trSAT is decidable and establish corresponding complexity bounds. Beyond trivial cases, we find that quantized TE, those restricted by fixed-width arithmetic, lead to the decidability of trSAT due to their limited attention capabilities. However, the problem remains difficult, as we establish scenarios where trSAT is NEXPTIME-hard and others where it is solvable in NEXPTIME for quantized TE. To complement our complexity results, we place our findings and their implications in the broader context of formal reasoning.

Published as a conference paper at ICLR 2025
TRANSFORMER ENCODER SATISFIABILITY: COM- PLEXITY AND IMPACT ON FORMAL REASONING
Marco Sälzer
Eric Alsmann
University of Kaiserslautern-LLnndd RPTU
Theoretical Computer Science / Formal Methods University of Kassel, Germany
Kaiserslautern, Germany
marco sael wew.zerrrt.ruruuu.....
eric a smann @nn -wasskaaslllcee.
Martin Lange
Theoretical Computer Science Formal Methods University of Kassel, Germany
ma artiin -kanini--ssses
ABSTRACT
We analyse the complexity of the satisfiability problem, or similarly feasibility problem, (trSAT) for transformer encoders (TE), which naturally occurs in formal verification or interpretation, collectively referred to as formal reasoning. We find that trSAT is undecidable when considering TE as they are commonly studied in the expressiveness community. Furthermore, we identify practical scenarios where trSAT is decidable and establish corresponding complexity bounds. Be- yond trivial cases, find that quantized TE, those restricted by fixed-width arith- metic, lead to the decidability of trSAT due to their limited attention capabilities. However, the problem remains difficult, is NEXPTIME-haad and others where it is solvable NEXPTIME for quantized TE. To complement complexity results, place our findings and their impli- cations in the broader context of formal reasoning.
establish scenarios where trSAT
INTRODUCTION
Natural language processing (NLP) models, processing and computing human language, are gate- ways for modern applications aiming interact with human users in natural way. Although NLP a traditional field research, the use of deep learning techniques has undoubtedly revolutionised the field in recent years (Otter al.] (2021)). In this revolution, models such Recurrent Neural Networks (RNN) or more specific Long Short-term Memory Networks (LSTM) (Yu et al. (2019) have long been the driving force, but for few years now NLP has figurehead: transformers Vaswani et al. )
Transformers are deep learning model using (multiple) self-attention mechanisms process se- quential input data, usually natural language. The efficient trainability of transformers, for example in contrast LSTM, while achieving top-tier performance led numerous heavy-impact implemen- tations such as BERT (Devlin et al. (2019)), GPT-3 (Brown et al. (2020) or GPT-4 (OpenAll (203)), ) sparking widespread use of the transformer architecture. However, the foreseeable omnipresence of transformer-based applications leads to serious security concerns.
In general, there are two approaches to establishing trustworthiness learning-based models: first, safety properties, called verification, and second, inter-
certifying specific, application-depencel preting the behaviour such models and giving explanations for it, called interpretation. In both approaches, the holy grail is to develop automatic methods that are sound and complete: algorithm A given some model and (verification or interpretation) specification outputs t rue if satisfies y (soundness) and for every given pair T, ip where T satisfies &o algorithm A outputs rue (complete- ness). We refer to such sound and complete methods and tasks for verification and interpretation collectively using the term formal reasoning.

---

Published as a conference paper at ICLR 2025
We lay out framework for the possibilities and challenges of formal reasoning for transformers by establishing fundamental complexity (and computability) results in this work. Thereby, we focus on the so-called satisfiabillity (TRSAT) problem of requence-classifying former T, decide whether there is some input word w such that ((w) = 1, which can be interpreted as T accepts w. Although this may seem like artificial problem at first glance, it is natural abstraction of problems that commonly occur in almost all non-trivial formal reasoning tasks. Ad- ditionally, since it is detached from the specifics of particular reasoning specifications like safety properties for instance, uncomputability results and cmpplexit-thhoreete hardness results immedi- ately transfer to more complex formal reasoning tasks. This also keeps the focus on the transformer architecture under consideration. Here, we exclusively consider transformer encoders (TE), which are encoder-only. This is mainly due to the fact that the known high expressive power of encoder- decoder transformers (Pérez et al. (202T)) makes formal reasoning trivially impossible.
transformers: given trans-
Our work is structured as follows. We define necessary preliminaries in Section 2 In Section 3 we give an overview on complexity results and take comprehensive look at their implications for formal reasoning for transformers, In Section 4 and Section 5 we present our theoretical results: we show that TRSAT is undecidable for classes of TE commonly considered in research on transformer expressiveness, we show that a bounded version BTRSAT of the satisfiability problem is decidable, for any class of (computable) TE, and give corresponding complexity bounds and show that considering quantized TE, meaning TE whose parameters and computations are carried out a fixed-width arithmetic, leads to decidability of TRSAT and give corresponding complexity bounds. Finally, we discuss limitations, open problems and future research in Section 6
Related work. We establish basic computability and complexity results about transformer-related formal reasoning problems, like formal verification or interpretation. This places our work in the intersection between research on verification and interpretation of trunsformers and transformer expressiveness.
There is a limited amount of work concerned with methods for the verification of safety properties of transformers (Hsieh et al. (2019); Shi et al. (2020); [onaert et al. (2021); Dong et al. (2021) )) How- ever, all those methods do not fall in the category of formal reasoning, as they are non-complete. This means, the rigorous computability and complexity bound established in this work cannot be ap- plied without further considerations. The same applies for so far considered interpretability methods Zhao et al. ). We remark that a lot of these approaches are not sound methods either.
In contrast, there is an uprise in theoretical investigations of transformer expressiveness. Initial work dealt with -eecoder-decoder models and showed that such models are Turing-complete (Pérez et al. (2021); Bhattammaaaii et al. (2020)). Note that these are different models than the ones we consider, which are encoder-only. Encoder-only models have so far been analysed in connection with circuit complexity (Hahn (2020; Hao et al. (2022) Merrill et al. (2022): [Merrll Sabharwal (202bb), logics (Chiang et al. (2023); Merrill & Sabharwal (2023a) and programming languages (Weiss) al. (2021)) A recently published survey (Strobl et al. (2024)) provides an overview of these results. This work is adjacent as some of the here considered classes of TE, mainly those considered in Section 4 are motivated by these results and some of the constructions we use in corresponding proof's similar.
FUNDAMENTALS
Mathematical basics. Let Σ be finite set of symbols, called alphabet. A (finite) word over Σ is finite sequence a1...au ag where a; E Σ. We define |w| w k. As usual, we denote the set of all non-empty words by Σt language is a set of words. We also extend the notion of an alphahet to vectors a; E Rdd, meaning that sequence æ Rt is word over some subset of IRd Usually, we denote vectors using bold symbols like x. y or z.
Transformer encoders (TE). We consider the transformer encoders (TE), based on the trans- former architecture originally introduced in (Vaswani et al. (2017)). We take a look at TE from computability and complexity perspective, making a formal definition of the considered architecture necessary. Thereby, follow the lines of works concerned with formal aspects of transformers like
2

---

Published as a conference paper at ICLR 2025
Hahn 2020): Pérez et al. (202] Hao al. (022)) ) From syntax point of view, our definition is most near to (aa et al. (2022)
An TE T with L layers and h; attention heads in layer i is tuple (emb, {attis 1 s1sis L,
j S h;), { comb;
1 S < L}. out) where
emb: Σ x N -> de for some de E N is the positional embedding.
each attention head is tuple att = (scores.j) pool where s.: Rd. x xR
IR is a function called scoring and pool,,; (IR xxxxE R + Rdd is function called pool- ing, computing (z1....,, En, $1,....,sn. + Ex= norm (i', .1.....,8.)) s,) where W is linear map represented by a matrix and norm: N R + - IR is normalisation,
each comb;; g4.. x ... x 11 + Rd is called combination and out: RR + R is called the output.
For given S L we call the tuple (att;,1,... atti,h,, combe) the i-th layer of T. The TE T computes a function Σ+ + IR as follows, also schematically depicted in Figure [ Let w aj....,a, an E E+ be a word. First, T computes an embedding of w by emb(w) aT- sy where x.
emb(as, i). Next, each layer S S L computes sequence o ................................ vy as follows: for each input xi and attention head alla,g, layer computes ymn. poot, (x) ..... o 1 scores (3) .i "f""")...,, scorei, (1rt)
" 1))) Then, st is given by somb((a)) (x ymm...... k. In the end, the output T(w) is computed by out().)) thus the value of the output function for the last symbol of w after being transformed by the embedding and L layers of T. We say that T accepts w ((w) = 1, and we say that T rejects w otherwise. We call L the depth of T and the maximal h2 the (maximum) width of T. Furthermore, we call the maximal d, the (maximum) dimensionality of T. Let T, T' be some classes of TE. We sometimes say that T' least as expressive as T or is at most as expressive as T', meaning that for each T T there is T' E 'I' such that T and T' compute the same function. The decision problem TRSAT[ is given T E T over alphabet Σ, decide whether there is w Σ such that T (ww) 1. We refer to this as the satisfiability problem of T.
Fixth-width arithmetics. We consider commonly used fixed-width arithmetics (FA) that repre- sent numbers using a fixed amount of bits, like floating- or fixed-poin arithmetic in this work. See (Baranowski et al. (2020)) (fixed-point) or (Constantinides et al. (202T) (floating-poinl for rigor- ous mathematical detinitions of such FA. In this work, however, we only make use of a high-level view on different FA. Namely, given some FA F' we assume that all values are represented in binary using b E N bits for representing its numbers. Thus, there are 2a different rational numbers repre- sentable in F. Furthermore, we assume that the considered FA can handle overflow situations using either saturation or wrap-around and rounding situations by rounding up or off. We consider TE in the context of F. We say that T works over F, assuming that all computations as well as values occurring in a computation T(w) are carried out in the arithmetic defined by F.
3 OVERVIEW OF COMPLEXITY RESULTS AND CONNECTION TO FORMAL REASONING
We address elementary problems arising in formal reasoning for transformers in this work. In doing so, we pursue the goal of establishing basic computability and complexity results for corresponding problems in order to frame possibilities and challenges.
We want our results to be detached from any intricacies of specific transformer architectures: first, we focus on transformer encoders (TE), so leaving any decoder mechanism unconsidered. The primary reason for this is that encoder-decoder architectures are of such high expressive power
As of now, no single definition of Transformer encoders (TE) has been universally adopted in research on their formal aspects, particularly concerning syntax (see the recent survey (Strobl et al. (2024)) for overview of different notions of TE). The definition use here is sufficiently general and provides parameterized template for the classes TE considered in our main results.
We observe that we can equivalently define TRSAT as requiring T(w) 2 c for arbitrary E Q without changing any of the results detailed in this work.
3

---

Published as a conference paper at ICLR 2025
out
X
comb
ott
ott
11
emb
Figure I: Schematic depiction of TE T' with embedding emb and k (encoder) layers Each layer 4 consists of some h; attention heads all,, whose output is combined by comb; Additionally, for some layer 4, the computational flow of regarding input position m schematically depicted in detail.
(éérez et al. 2021 1)) that almost all formal reasoning problems are easily seen to be undecidable. The secondary reason for this that encoder-decoder architectures subsume encoder-only architectures. So any lower complexity bound, established in this work, is also a lower bound for encoder-decoder
transformers.
SATISFIABILITY AS A BASELINE FORMAL RESONING PROBLEM
To achieve widespread implications of our results, we focus our considerations on fundamental problem arising in formal verification and interpretation tasks: given a TE T, decide whether there is some input w leading to some specific output 7 Tww). as defined formally terms of the satisfiability problem [T]] for class T of specific TE, see Section 2
To see that this captures the essence of formal reasoning problems occurring in practice, consider the following formal verification task: Given TE T, verify that T only accepts inputs where every occurrence of a specific key from a set K is accompanied by a particular pattern- for example, a key from K must be immediately followed by value from ensure syntactic correctness or adherence to some protocol specification. Formally, this is called a robustness property (Shi al. (2000) Huang al. (2023)). We can phrase this example task satisfiability problem by considering the property's 's negation, namely, to verify that there exists some properly followed by a value from V. yet we have T(w) 1.
V. Such tasks important
input w in which key from K
Similarly, consider a formal interpretation task where we aim to find the minimal subset E' C E of some of eтror symbols E such that all inputs containing all errors in E' are rejected by T. For instance, in a spam detection system powered by transformer encoder, E' could represent set of spam indicators or malicious keywords. We might want to determine the minimal combination of these indicators that will cause the system to classify an input spam. This is understood as an abductive explanation
formal explainable AI (Marques-Sill Silva & Ignatiev (2022)). Given candidate subset E', we can certify this by checking that there is some which contains all errors E', but accepted by T. This scenario a special case of the satisfiability problem TRS for some transformer class T.
OVERVIEW OF RESULTS THE COMPLEXITY TRANSFORMER ENCODER SATISFIABILITY
We start by considering the class Tudec of TE, motivated by commonly considered architectures in the theoretical expressiveness community (Pérez et al. (202I); Hao et al. (2022); Hahn (2020)): T dodes consists of those TE that use positional embedding, expressive enough compute sum,
4

---

Published as a conference paper at ICLR 2025
modecidable
Tudel
decidable
(Theore 2TTRSAT(T
udoe.
NEXPTIME
ITRS [7]
(Theurem 3)
[T
(Theorem 1aSAr(T
TRSAT(7
(Theorem
Figure 2: Schematic overview of the computability and complexity results, established in this work. The classes of TE are described the pretext of the respective theorem. Note that T refers to an arbitrary class of (computable) TE. The small subset the classes NP and NEXPTIME refers the complete problems. The NEXPTIME-hardness result of TRSAT is not visualized
hardmax hardmax as normalisation functions and a scalar- based scoring, enriched with a nonlinear map represented by an FNN.
Theorem (Section 4). The satisfiability problem TRSAT (TSAee(Tuee)) is undecidable.
Essentially, this result implies that even for TE the combination of hardmax normalizations and expressive scoring is enough to make satisfiability undecidable. Generally, this makes formal rea- soning, like verifying robustness properties or giving formal explanations, impossible for classes of TE that subsume Tadec- Specifically, no such methods exist that are fully automatic, sound and complete. Theorem does not preclude the existence of incomplete methods for instance.
Recently, so-called log-precision transformers have been studied (Merrill & Sabharwal (023a These transformers are defined as usual, but given a word length is assumed that a log-precision transformer 7' uses most (log(n)) bits in its internal computations. To complement these the- oretical considerations, we consider the class Tuye of TE from Tudee that work with log- fog-precision. Unfortunately, this restriction is not enough to circumvent general undecidability.
Theorem (Section 4 The satisfiability problem TRSAT adec. is undecidable.
Given such impossibility results, turn attention to the search for decidable cases. We make the reasonable assumption that all considered TE are computable, meaning that their components like scoring, normalisation, pooling, combination and output functions computable functions. Moreover, we assume that each TE I'' computes its output T(w) for given input w within polyno- mial time relative to the size of T' and the length w. This reasonable. as the output is computed layer-wise where each layer involves quadratic amount of calculations per attention head. There- fore, the computation depends polynomially on the depth and width of T and the length of w.
First, we consider natural restriction of the satisfiability problem by bounding the length of valid inputs. Then satisfiability becomes decidable, regardless of the respective class of TE, but it difficult from complexity-theored perspective. To formalize this, we introduce the bounded sat- isfiability problem (T(] for class T: given an TE 7 T and bound n E on its input length, decide whether there is word with [/ < s.t. T(w)= =
Theorem 3 (Section informal restatement). The bounded satisfiability problem BTRSAT[T] is decidable for all classes T of (computable) TE. Depending on whether n given in binary or unary coding, BTRSATITT is NEXPTIME- resp. NP-complete assuming T 2 Tudoc-
5

---

Published as a conference paper at ICLR 2025
Informally, this result implies that bounding the word length is method to enable formal reasoning. However, it does not change the fact that satisfiability is an essentially hard problem. As hardness is lower bound, this also translates to subsuming formal reasoning tasks.
Imposing a bound on the input length may not be a viable restriction for various formal reasoning tasks. We therefore study other ways of obtaining decidability. We address the unbounded satisfia- bility problem for practically motivated classes of TE. We consider the class Thax of TE that use a positional embedding with some periodicity in their positional encoding, commonly seen in practice (Vaswani et al. (2017); Dufter et al. ). use softmax or hardmax as normalisation and which work over some
arithmetic (FA). This last restriction is motivated by recent popular ways to handle ever increasing TE sizes, for example via quantization or using low-bit arithmetics (Bondarenko et al. (202T). From a complexity-thene -theortcc perspective, the use of Exed-width arith- metic has a similar effect to bounding the input length.
Theorem (Section5) 5
The satisfiabiiity problem TRSAT [T!IX] is in NEXPTIME.
So automatic, sound and complete formal reasoning for periodical TE in a fixed-width arithmetic environment is generally possible with potentially high complexity. Note that formal reasoning tasks with more complex safety or interpretabilityy specifications than simple satisfiability may even lead to higher complexities.
We then aim to show that this is optimal by providing a matching lower bound. However, we need to relax these restrictions again, namely considering the class 7 allowing for TE that use arbitrary embeddings and work over some fixed-width arithmetic. However, due to the fixed-witdth arith- metic assumption, which consequently applies to positional informations as well, every embedding must necessarily witness a periodic behaviour. Thus, decidability is implied by the same arguments as used in Theorem 4. Additionally, we show that high complexity is unavoidable, making sound and complete automatic formal reasoning for fixed-width arithmetic transformers with arbitrary po- sitional embeddings practically intractable.
Theorem 5 (Section
5). The satisfiability problem (RSAT(TTM) is decidable and NEXPTIME-hane
Figure 2 provides a schematic illustration of the computability and complexity results summarized in this section. This figure is intended purely for technical clarity, summarizing our findings without delving into the formal reasoning implications discussed earlier.
4 TRANSFORMER ENCODER SATISFIABILITY IS GENERALLY UNDECIDABLE
We consider a class of TE, denoted by Tudees which we design with the aim of minimising its expressive power, but having an undecidable satisfiability problem. We define Tudec by giving min- imum requirements: positional-embeedingg can be of the form emb(as, 0) = (1, 0, 0, and emb(ax, a) = (0, 1, Ej=o j. k) where we assume some order on the alphabet symbols @1, .2..... For scoring functions we allow for N((2x, K Ky)) where N is classical Feedforward Neural Net- work (FNN) with relu activations, Q and K are linear maps and (---> denotes the usual scalar product, for normalisations we allow for hardmax hardmax(i, (i. ha all j S n and there are m distinct 2y such that x; = xy otherwise hardmax(i, Rn) = O. Combinations as well as output functions can be classical FNN with relu activation. Aside from technical reasons, we motivate the choice of Tudec in Section 3 To ease our notation, we exploit the fact that using hardmax as normalisation implies a clearly defined subset of positions M that are effective in the computation of some attention head att given some position i, namely those that are weighted non-zero. In this case, we say that att attends to M given position i.
= if x; 2 xj for
We prove that TRSAT(Tuace) is undecidable by establishing a reduction from the (unbounded) octant tiling-word problem (OTWP*). For details on tiling problems, see Appendix A The OTWP" is defined as follows: given a tiling system S = (S, H, tt) where 5 is some fi- nite set of tiles, V.V C S² and tr E S we have to decide whether there is a word (a) to.o, t1,0, 41,1, 12,0, f2,1, 2,,,,,,,,, la.0............. tR E St such that (b) to,o = t,, lR. = tr. (c) for all < k and 0 & j < holds (tz,, +1) E H and (d) for all i S k 1 and j S i holds (tr,,. f.+ E V. We call word which satisfies (a) encoded riling and if (b)-(d) are satisfied well then we call w a valid encoded tiling. Our proof strategy is easily described: given a tiling system S. we build an TE Ts E T Tedee which accepts word if it fulfils conditions (a) to (d) and otherwise Ts rejects w.

---

Published as a conference paper at ICLR 2025
d
a a
d
Lemma
a
2
Figure 3: Schematic depiction of the expressive capabilities of TE from Tuder in context of the OTWP" proven in Lemma 1 and Lemma 2
We derive most technical proofs the following lemmas and theorems to Appendix and instead provide intuitions and proof sketches in this section.
We start with the first observation: the expressiveness of TE in Tuder is sufficient decode the octant tiling potentially represented by given word w. as depicted by the arrows in Figure 3 In detail, two encoder layers combination with positional embedding definable Tudec are expressive enough to compute for given symbol t in to which position in octant tiling corresponds, if we interpret w as an encoded tiling.
oxt. There is an embed- ding function emb and there are encoder layers l and la definable in Tuder: such that for each word w = 10.00,.01,,12200.... .mmm E S+ holds that 12(1 (e(((()()))
Lemma 1. Let be a tiling system with tiles S
x?...
where x; (1,i, c(i), ki) such that as; is equal to the symbol at position in w and (r(1), (r()), ..... (r([ur)) ((wl)))(()))) is equal (0, 0), (1, O,.)..., (m,n).
Assume that S+ Lemma I iimplies that TE T Tudo: is generally able recognize whether w is an encoded tiling as soon as T is able to check whether r( ((wl) and c([wl) of the last symbol of w processed by (2(41( (emb(-..)) (---))))))))))) })) are equal. Therefore, property (a) and also (b) can be checked by TE in Tudee using the residual connection and FNN.
Property (c) can be ensured if it possible build attention head that is able attend to position k k+1 1 given position k. Let w fo.ofi.of1,112..0 ... fm,m with fa.j S. To verify whether property (d) holds, a TE must be able to attend position &e + + 1) given position corresponding to symbol fz.j. This is depicted in Figure 3 by the bold lines between horizontal and vertical tiles. In summary, to check properties (a) - (d) it is left argue that there are attention heads Tudec that can attend to positions depending linearly the values of the currently considered position.
Lemma 2. Let f((1,..., 2R) = +4. + with a;, b E IR be some linear function. There attention head att , in Tudec such that for all sequences I1. Im where all x; (1, y: for some y; E = attention head att, attends {æ; Fj+13 } given position if f(x;) j j with j S m - 1 and otherwise to {æ;} where is the value nearest to f(x:).
combination, the previous lemmas indicate that TE from Tadeo are able to verify whether a given word is valid encoded tiling. This expressive power is enough, to lead to undecidable satisfia- bility problem for TE from Tudec-
Theorem 1. The decision problem TRSAT [uudec] is undecidable.
Proof Sketch. We establish reduction from OTWP" to TRSAT[Tuded] by constructing for each instance S (S, H, V,t, tF) of OTWP" an TE T's accepting exactly those w corresponding to a valid encoded-tiling for S.
Ts uses the positional embedding described in the beginning of Section and has four layers. Layers I and ly are given by Lemma and used to decode the and column indexes corresponding to a potential octant tiling for each symbol in a given word w. Layer lą uses the informations encoded by the embedding and the decoded row and column indexes to check whether properties (a) (d)

---

Published as a conference paper at ICLR 2025
described above hold for w. The necessary informations are aggregated using three attention heads att prev. aft and step. each built according to Lemma 2 Thereby, att att attends each position to its predecessor, but the first position attends to itself. This allows to clearly identify the vector corresponding to the first position in w and check whether this is equal to tile iy- Attention head att nezt attends each position its successor, but the last position attends to itself. This allows to clearly identify the vector corresponding to the last position in w, in order to check whether this is equal f and to check conditions given by H. Attention head aft step attends each position the position with the same column index but the successive row index. If there is no such successive row attends the last position. This allows to check whether conditions given by V holds. Each of these conditions is checked in the combination function of lg. using specifically built feed-forward neural networks outputting to some predefined vector dimension and only if the condition met. Finally, layer 4 aggregates the information of all positions in the vector corresponding to the last position using attention head att again given by Lemma The correctness of this reduction follows from the detailed construction of Ts. given in Appendix B
Next, we consider the class Tudee which is defined exactly like Tudee but for all T E Tudee working over alphabet Σ and all words w with [w] we assume that T(w) is carried out in some fixed- width arithmetic F' using (log(maxx n))) bits.
Theorem 2. The decision problem TRS adeel is undecidable.
Proof sketch. This proof follows the exact same line as the proof of Theorem | Additionally, we need to argue that Ts works as intended, despite the fact that it is limited by some log- log-precision F.
Looking at the proof of Theorem 1 used and produced in the computation Ts(w depend polynomially on n and, thus, we can choose the representation of F to be linear in log(n), which avoids any overflow or rounding situations and ensures that Ts works as intended. A formal proof is given in Appendix B
imminent that the magnitude and precision of all values
L
5 HOW TO MAKE TRANSFORMER ENCODER SATISFIABILITY DECIDABLE
In this section we investigate classes of TE leading to decidable TRSAT problems or decidable re- strictions of it. Additionally, we establish corresponding complexity bounds.
In order to establish clearly delineated upper complexity bounds, we need to bound the represen- tation size of TE T. Instead of tediously analyzing the space needed to represent embedding, scoring, pooling, combination and normalisation functions, we note that it suffices to estimate the size up to polynomials only. The complexity of a TE with I. layers and h2 attention heads in layer i, working on inputs over alphabet Σ, is [T] [ L + H + D where H max(h; and D is the maximal dimensionality of vectors occurring in a computation of T'. Note that one can reasonably assume the size of syntactic representation of T to be polynomial in [T), and that TE have the polynomial evaluation property: given a word w E Σt, ((w) can be computed in time that polynomial in [T' |w]. Section 3 discusses why this assumption is reasonable.
S i S L}
We start with a natural restriction: bounding the word length. Let T be a class of TE. The bounded satisfiability problem, denoted by [TRSAT[T] is: given T T and some n. E N, decide whether there a word w with |w| < n such that T(w) = 1. It is not hard to see that BTRSAT(T] is decidable. However, its complexity depends on the value of n, and we therefore distinguish whether n is rep- resented in binary or unary encoding. We denote the problems as BTRSAT [7] and BTRSAT,.. [7].
Theorem 3. Let T be a class of TE. Then
1. BTRSATT [T] is in NP; Tudec TT then BTRSAT [T] NP-complete,
2. BTRSATT [T] is in NEXPTIME; Tudee C T then BTRSATBin [T] is NEXXPIIME-compeeee
Proof Sketch The decidability result of statement I can be shown using a simple guess-and-check argument: given E N, guess word w E E with |w| n, compute T(w) and check that the result is This is possible in time polynomial in [T] + n using the polynomial evaluation property. Note that [T] depends on [S), thus this also respects the actual representation size of w.
8

---

Published as a conference paper at ICLR 2025
Moreover, the value of [T] + n is polynomial in the size needed to represent n in unary encoding. The decidability result of statement (2) is shown along the same lines. However, if the value n is encoded binarily then this part of the imput is of size log n. and [T] + n becomes exponential in this. Hence, the guess-and-check procedure only proves that BTRSAT [T] E NEXPTIME.
For the completeness result in ① it suffices argue that the problem is NP-hard. We use that TE in Tadoo are expressive enough to accept a given word w if and only if is a valid encoded tiling, cf. Section for details. is possible establish NP-hardness of a restriction of the octant word-tiling problem, namely the bounded octant word-tiling problem (for unarily encoded input values). See Appendix [A for details on tiling problems. It remains to observe that the construction in Theorem is in fact polynomial-tin the bounded satisfiability problem. The argument for NEXPTIME- hardnesss in statement ( works the same with, again, the bounded octant-word tiling problem shown to be NEXPTIME-hare when
reduction, and that it reduces the bounded octant word-tiling problem to
the input parameter n is encoded binary. full proof for Theorem 3 is in Appendix
L
We turn our attention to classes of TE that naturally arise in practical contexts. We consider TE that work over some fixed-width arithmetic, like fixed- or floating- numbers, and which have an em- bedding relying on periodical encoding of positions. We start with establishing a scenario where TRSAT is decidable in NEXPTIME. Regardless of the underlying TE class T, our proof strategy always relies on a certifier- based understanding of NEXPTIME: given T E T. we nondeterministi- cally guess a word w, followed by a deterministic certification whether T(w) = 1 holds. For this to show ATS) E NEXPTIME, we need to argue that the overall running time of such a procedure is at most exponential, in particular that whenever there is word w with T(w) = then there is also some w' with T(w") = 1 and |w'l S 2 Again, we rely on the polynomial evaluation property of TE in i.e. the fact that (w'' can be computed in time polynomial in [T'] + (wo).
We consider the class of TE T.EN, defined by placing restrictions on the positional embedding of an TE T to be perriive which means that emb (a, i) = emb' (a) + pos(t) where pos is periodical, i.e. there is p 2 1 such that pos(i) pos(i + p) for all normalisation functions are realised by either the softmax function softmax or the hardmax func- tion hardmax. Moreover, we assume that all computations occurring in T are carried out in some fixed-width arithmetic, encoding values in binary using a fixed number b E N of bits. Aside from technical reasons, we motivate the choice of FIX in Section 3 Given these restrictions, we ad- just the definition of the complexity of T E T as a measure of the size (up to polynomials) as [T|== = |Σ| + L + + D + p b.
N. Additionally, all
Lemma 3. There is a polynomial function poly: N - N such that for all T E TTex and all words with T(w)= 1 there is word w' with T(w') 1 and |w'] (Pooy((TT)
Proof Sketch. The polynomial poly can be chosen uniformly for all T E Thux because for all po- sitional embeddings of TE in T there is an upper bound on the period and on the bit-width in the underlying arithmetic. The small- word property stated by the lemma is then shown by arguing, given polynomial poly, TE T and |w| > 2T0ly((T)), that w contains unnecessary subwords u that can be cut out without changing the output in T. Here, we exploit the fact T has some periodicity p and only consider those u whose length is multitude of This ensures that the resulting word w', given by w without u, is embedded the same way as w by the positional embedding of T', The existence of such subwords follows from I"s limited distinguishing capabilities, especially in its normalisations, due to the bounded representation size of numerical values possible in the underlying fixed-widte arithmetic. A formal proof relies on basic combinatorial arguments and given in Appendix C O
Theorem 4. [T..A( for additive
TE over fixed- arithmetic is in NEXPTIME.
Proof. Let T E T.ux working over alphabet Σ. We use a certifier-based understanding of a nonde- terministic exponential-time algorithm follows: We (a) guess an input w E Σ+ and (b) compute T(w) to check whether T(w)= = 1. For correctness, we need to argue that the length of w is at most exponential in (T'. This argument is given by Lemma 3 Note that via assumption we have that T(w) can be computed in polynomial time regarding T and |w]]
Next, we address the goal of obtaining a matching lower bound, i.c. TEXPTIME-hhrrdees An obvious way do so would be to follow Theorem 3 and form reduction from the bounded

---

Published as a conference paper at ICLR 2025
octant word-tiling problem. Hence. given tiling system S and N encoded binarily, we would have to construct - in time polynomial in |S] + +oggn - an TE Ts.n E Te such that T = f1,1, 12 22,2, ts.1....... .,,, representing valid S-tiling.
for some w E Σ* iff there is word In particular, Ts.n would have to be able to recognise the correct word length and reject input that is longer than |w| m(x+1), This poses a problem for TE with periodical embeddings. To recognize whether a word is too long, an TE T must ultimately rely on its positional embedding, which seems to make periodicity of p > m(n++)
necessary. Since the size of periodical TE is linear in p. we get an exponential blow-up in a potential reduction of OTWP bin to TRSAT[T,"*], given that the values of n(x+1) and already are exponential in the size of a binary representation of n. This problem vanishes when the requirement of the underyling positional embedding to be periodical is lifted: allowing for arbitrary TE, working over some fixed-widhs width arithmetic, leads to an NEXPTIME-HE satisfiability problem. Let T be defined similar to T.Pk, but we allow for arbitrary embeddings. Furthermore, we assume that the considered fixed- arithmetics can handle overflow situations using saturation.
Theorem 5. TRSAT[TRIM] for TE over fixedwwitthh arithmetic is decidable and NEXPTIME-hard.
Proof sketch. The decidability follows from the same arguments as in Theorem with the insight that even though T' E T uses an arbitrary embedding, a Exit-width setting with b bits enforces periodicity of size most 2", assuming overllow is handled by wrap-around, or periodicity of size 1 after a finite prefix of length up to 2b, assuming overflow is handled by saturation, in the embedding. For the hardness, we establish reduction from OTP bin TRS [T by constructing, for each instance (S, n) of P an TE Ts.n. working over some width arithmetic F. which
accepts exactly those with |w| m(n+1) corresponding to valid word-encoded tiling for S. See Appendix /foo for details on tiling problems. The construction is similar to the one given for Ts in the proof of Theorem but we need to enable Ts.n. to reject words that are too long corresponding polynomial bound dependent on n. This implies that Ts... based on the positional embedding emb specified in Section [4] is able check for all symbols their respective position less than or equal to predefined bound. This can be achieved with similar tools as used in Lemma Furthermore, we need to ensure that Ts.n works as intended, despite the fact that is limited by F. The arguments follow the same line as the proof of Theorem 2
A formal proof is given in Appendix C
6 SUMMARY, LIMITATIONS AND OUTLOOK
We investigated the satisfiability problem of transformer encoders (TE). In particular, we consid- ered the computational complexity of the satisfiability problem TRSAT of TE in context of different classes of TE, forming a baseline for understanding possibilities and challenges of formal reasoning of transformers. We showed that TRSAT is undecidable for classes of TE recently considered in research on the expressiveness of different transformer models (Theorem and Theorem 2 This implies that formal reasoning is impossible as soon as we consider classes of TE that are at least as expressive as the classes considered in these results. Additionally, we identified two ways to enable formal reasoning for TE: by bounding the length of inputs (Theorem or by considering quantized TE, where computations and parameters are limited by fixed-width arithmetic (Thcorem 4). These imply that formal reasoning is possible for TE classes that are at most as expressive as those in our results. Thereby, we assume that TE expressiveness is the primary factor influencing computability or complexity bounds, rather than specific safety or interpretability assumptions. However, in both cases, AT remains computationally difficult (Theorems 3 5). Again, these results apply only to TE classes at least as expressive as those we considered. While our results provide an initial framework for understanding the possibilities and challenges of formal reasoning for transformers, there is room for more detailed investigations. Our undecidability and hardness results rely on nor- malizations realized by the hardmax function, and it's unclear whether similar results hold when using the commonly employed softmax function. Additionally, further exploration of the interplay between the embedding function and the internal structure of the TE is of interest. We expect that less expressive embeddings require a richer attention mechanism, but it's unclear where the limits lie regarding the undecidability of the satisfiability problem. Regarding our decidability and upper complexity bounds, examining the specifics of particular fixed-width arithmetics could be practically beneficial. While this wouldn't 't change our overall results, could provide tighter tome-compy estimates valuable for certain formal reasoning applications.
10

---

Published as a conference paper at ICLR 2025
REFERENCES
Marek S. Baranowski, Shaobo He, Mathias Lechner, Thanh Son Nguyen, and Zvonimir Rakamaric. An SMT theory of fixed-point arithmetic. In Nicolas Peltier and Viorica Oofronie-Stokkerman (eds.). Automated Reasoning 10th International Joint Conference, IJCAR 2020, Paris, France, July 144, 2020, Proceedings, Part I, volume 12166 of Lecture Notes in Computer Science, pp. 13-31. Springer, 2020. doi: 10.
Robert Berger. The undecidability of the domino problem. Mem. Amer. Math. Soc., 66:72, 1966.
Satwik Bhattamishra, Arkil Patel, and Navin Goyal. On the computational power of transformers and its implications in sequence modeling. In Raquel Fernández and Tal Linzen (eds.). Pro- ceedings of the 24th Conference on Computational Natural Language Learning, CoNLL 2020, Online, November 19-20, 2020, pp. 455-475, Association for Computational Linguistics, 2020. 10033//1/220.CONIO
doi:
Gregory Bonaert, Dimitar I. Dimitrov, Maximilian Baader, and Martin Vechev. Fast and precise cer- tification of transformers. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pp. 466-481. Association for Computing Machinery, 2021. ISBN 978-1-4503-8391-2 doi: 10. (0.1145/3553433.4455558
Yelysei Bondarenko, Markus Nagel, and Tijmen Blankevoort. Understanding and overcoming the challenges of efficient transformer quantization. In Maric-Francine Moens, Xuanjing Huang, Lucia Specia, and Scott Wen-tau Yih (eds.), Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing. EMNLP 2021, Virtual Event / Punta Cana, Domini- can Republic, 7-11 November, 2021, pp. 7947-7969, Association for Computational Linguistics. 2021. doi: 10. 18653/V1/22221 11L.E/VV2222..EENNPMMMAAA. J.NNN---MN.M.....
Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared 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 M. Ziegler. Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam Mc- Candlish, Alec Radford, Ilya Sutskever, and Dario Amodei. Language models are few- shot learners. In Advances Neural Information Processing Systems 33: Annual Con- ference on Neural Information Processing Systems 2020, NeurlPS 2020, December 6-12, 2020, virtual, 2020. URL httpttttss:::psseeeeessss 1457c0d6bf cb 446 www.seoewaacceee.co Abstract html
neur ips hoc.//aper/222////
David Chiang. Peter Cholak, and Anand Pillay. Tighter bounds on the expressivity of transformer encoders. In Andreas Krause, Emma Brunskill, Kyunghyun Cho, Barbara Engelhardt, Sivan Sabato, and Jonathan Scarlett (eds.), International Conference on Machine Learning, ICML 2023, 23-29 July 2023, Honolulu, Hawaii, USA, volume 202 of Proceedings of Machine Learning Re- search, pp. 5544-5562. PMLR, 2023. URL chiang23a, html
/ttsstss:///rooeed.co http://pooceeee//eee/eeeeeeeesee mll..
vr2ss/v202/
George A. Constantinides, Fredrik Dahlqvist, Zvonimir Rakamaric, and Rocco Salvia. Rigorous roundoff error analysis of probabilistic floating-point computations. In Alexandra Silva and K. Rustan M. Leino (eds.), Computer Aided Verification 33rd International Conference, CAV 2021, Virtual Event. July 20-23, 2021, Proceedings, Part II, volume 12760 of Lecture Notes in Computer Science, pp. 626 650. Springer. 2021. doi: 1000000797-3-0000 1830-81688-99 29.
S. Demri, V. Goranko, and M. Lange. Temporal Logics in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. ISBN 9781 107028364. URL http: /ttt::/wwwrr cambridgeeeeeeee org/ core www.:tttttttteeeeeeeeeeeeee
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 of the Association for Computational Linguistics: Human Language Technologies. NAACL-HLT 2019, Minneapolis, MN, USA, June 2-7, 2019, Volume I (Long and Short Papers), pp. 4171 -1186. Association for Computational Linguistics, 2019. doi: 10.18653/ N1N119-143..
11

---

Published as a conference paper at ICLR 2025
Xinshuai Dong. Anh Tuan Luu, Rongrong Ji, and Hong Liu. Towards robustness against natu- ral language word substitutions. In 9th International Conference on Learning Representations,
ICLR 2021. Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL https:
//peereview. wwt//foroutaa d=
Philipp Dufter, Martin Schmitt, and Hinrich Schüitze Position information in transformers: An overview. Comput. Linguistics, 48(3))333-763, 2022. doi: (0.1162/COLI,
Michael Hahn. Theoretical limitations of self self-attention in neural sequence models. Trans. Assoc. Comput. Linguistics, 1:15 2020. doi: 10.1162/TACI) A 00306.
Yiding Hao, Dana Angluin, and Robert Frank. Formal language recognition by hard attention transformers: Perspectives from circuit complexity. Trans. Assoc. Comput. Linguistics, 10:800- 810. 2022. URL 3765
htt.:/aaaaa....ooss////oaoaaaaa inddxxxxxxxixxxxx.xoooixxxxxxxx. phpptacll/atiicl////
Yu-Lun Hsieh, Minhao Cheng, Da-Cheng Juan, Wei Wei, Wen-Lian Hsu, and Cho-Jui Hsieh. On the robustness of self-attentive models. In Anna Korhonen, David R. Traum, and Lluís Mårquez (eds.), Proceedings of the 57th Conference of the Association for Computational Linguistics, ACL 2019, Florence, Italy, July 28- August 2, 2019, Volume 1: Long Papers, pp. 1520-1529. Associa- tion for Computational Linguistics, 2019. doi: 10. 10.1865/V1/119--1477
Xiaowei Huang, Wenjie Ruan, Wei Huang, Gaojie Jin, Yi Dong, Changshun Wu, Saddek Bensalem, Ronghui Mu, Yi Qi, Xingyu Zhao, Kaiwen Cai, Yanghao Zhang, Sihao Wu, Peipei Xu, Dengyu Wu, André Freitas, and Mustafa A. Mustafa. A survey of safety and trustworthiness of large language models through the lens of verification and validation. CoRR, abs/2305.1139) 2023. doi: 10.48550/ARXIV.3055.11
João Marques-Sike -Slva and Alexey Ignatiev. Delivering trustworthy Al through formal XAI. In Thirty- Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Inno- vative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 Marrch 1, 2022, pp- AAAI Press, 2022. doi: 10.1609/AAAL, V3611 1 1.21499.
William Merrill and Ashish Sabharwal. A logic for expressing rog-precision transformers. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine (eds.), Advances in Neural Information Processing Systems 36: Annual Conference on Neural Infor- mation Processing Systems 2023, NewrIPS 2023, New Orleans, LA, USA, December 10 16, 2023, 2023a. URL http: /ttpt:::/ppppeeee nips -ate:s88-bbsttaccc Con.rtt--Coooeeeoeceocooooooneee html
William Merrill and Ashish Sabharwal. The parallelism tradeoff:: Limitations of log-precision trans- formers. Transactions of the Association for Computational Linguistics, 11:531-545, 2023b. doi: 10.1162/tacl_a 00056...
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: 7 //transacl..org///tt/ wwtps//inxxxeecm http://wwwwpppp/aaaaaaatat//////
OpenAl. Gpt-4 technical report, 2023.
Daniel W. Otter, Julian R. Medina, and Jugal K. Kalita, A survey of the usages of deep learning for natural language processing. IEEE Trans. Neural Networks Learn. Syst., 32(2):604 624, 2021. doi: 10.1119/TNLL 2020..9977200
Jorge Pérez, Pablo Barceló, and Javier Marinkovic, Attention is turing-complete. J. Mach. Learn. html
Res., 22:75:1-75:35, 2021. URL htctp:://mmmr..org/ppprrrrs
Marco Sälzer and Martin Lange. Fundamental limits in formal verification of message-passing paassing neural networks. In The Eleventh International Conference Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023, WRLhttps:: /ttp:////pee/eee/// net/pdf?id=h 1GG21lG822322
12

---

Published as a conference paper at ICLR 2025
Zhouxing Shi, Huan Zhang, Kai- Wei Chang, Minlie Huang, and Cho-Jui Hsich. Robustness verification for transformers. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020. URL https: //openreview. wwt.//ftooroo d=BJxwPPPPP JHF.
Lena Strobl, William Merrill, Gail Weiss, David Chiang, and Dana Angluin. What Formal Lan- guages Can Transformers Express? A Survey. Transactions of the Association for Computational Linguistics, 12:543-561, 05 2024. ISSN 2307-387X. doi: 10.1162/tacl a 00663.
van Emde Boas. The convenience of tilings. In A. Sorbi (ed.), Complexity, Logic, and Recursion Theory, volume 187 of Lecture notes in pure and applied mathematics, pp. 331-363, Marcel Dekker, Inc., 1997.
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett (eds.), Advances in Neural Information Processing Systems 30: Annual Conference Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pp. 5998 6008, 2017. URL httph: httppp/:/ppoccce.gggg.... nww.........pp.... ips pc/ppappe//11//aaa/// wwteraa-bbbttttttt.
Gail Weiss, Yoav Goldberg, and Eran Yahav. Thinking like transformers. In Marina Meila and Tong Zhang (eds.), Proceedings of the 38th International Conference Machine Learning, ICML 2021, 18-24 July 2021, Virtual Event, volume 139 of Proceedings of Machine Learning Re- search, pp. 11080-110 11090. PMLR, 2021. URL UtL.tttp://proceedd.ng mlr. wtt.pptsss/.../////// we 85 a. 1
Yong Yu, Xiaosheng Si, Changhua Hu, and Jianxun Zhang. A review of recurrent neural networks: 2019. doi: 10.1162/
LSTM cells and network architectures. Neural Comput.,
Haiyan Zhao, Hanjie Chen, Fan Yang, Ninghao Liu, Huiqi Deng, Hengyi Cai, Shuaiqiang Wang, Dawei Yin, and Mengnan Du Explainability for large language models: A survey, ACM Trans. Intell. Syst. Technol., 15(2):20:1-20:3 2024. doi: 10.1645/3639372.
A TILING PROBLEMS
We make use of particular tiling problems in order to prove lower bounds on the complexity and decidability of TT) for different classes T.
A siling system is an S = (S. H, tr) where is a finite set; its elements are called riles. H. S x S define horizontal, resp. vertical matching relation between tiles, and t,,tp to are two designated initial, resp.finat tiles in S.
Problems associated with tiling systems typically of the following form: given discrete convex plain consisting of cells with horizontal and vertical neighbors, is it possible to cover the plane with tiles from S in way that horizontally adjacent tiles respect the relation H and vertically adjacent tiles respect the relation V. together with some additional constraints about where to put the initial and final tile f,, tr. Such tiling problems, in particular for rectangular planes, have proved to be extremely useful in computational complexity, cf. (Berger (1966); van Emde Boas (1997), since they can seen as abstract versions of halting problems.
We need variant in which the plane to be tiled is of triangular shape. The n-th triangle is On ((i.)) E N N i iii n) for n > 0. An (S)-tiling of O, is function On - s.t.
(i.. +1) E H for all (1,5) E O with < i <
(7(1.)), 7(i + 1,5)) e V for all (i.j) E O with j < i < n.
Such tiling successful, if additionally r(0, f, and T(i, i) tr for some (i, E O,,-
The unbounded octant tiling problem (OTP") is: given tiling system S. decide whether a success- ful S-tiling of O,, exists for some N. The bounded octant tiling problem (OTP) is: given
13

---

Published as a conference paper at ICLR 2025
tiling system S and n 2 1, decide whether successful S-tiling of On exists. Note that here, n is part of the input, and that it can be represented differently, for example in binary or in unary encoding. We distinguish these two cases by referring to OTP bin and OTP.n. un
It is well-known that OTP" is undecidable (van Emde Boas (997)). It is also not hard to imagine that OTPun un is NP-complete while OTP un is NEXPTIME-compleet In fact, this is well-known for the variants in which the underlying plane is not a triangle of height n but a square of height n (van) Emde Boas (1977). The exponential difference incurred by the more compact binary representation of the input parameter v. is best seen when regarding the upper complexity bound for these problems: given n, a nondeterministic algorithm can simply guess all the n² many tiles of the underlying square and verify the horizontal and vertical matchings in time (n²)) If is encoded unarily. i.c. the space needed to write it down is == n, then the time needed for this is polynomial in the input size s; is encoded binarily with space == [log n. then the time needed for this is exponential in s.
then remains to argue that the tiling problems based on triangular planes are also NP- resp. NEXPTIME-Complett Clearly, the upper bounds can be established with the same guess-and-check procedure. For the lower bounds suffices to observe that hardness of the tiling problems for the squares is established by a reduction from the halting problem for Turing machines (TM) such that a square of size n X n represents a run of the TM of length n as a sequence of rows, and each row represents a configuration of the TM using at most n tape cells. This makes use of the observation that the space consumption of a TM can never exceed the time consumption. Likewise, assuming that a TM always starts a computation with its head on the very left end of a tape, one can easily observe that after i time steps, it can change at most the leftmost tape cells. Hence, a run of a TM can therefore also be represented as a triangle with its first configuration of length I in row 1, the second of length 2 in row 2 etc.
At last, we consider two slight modifications of these two problems which are easily seen to preserve undecidability resp. NP- and SEXPTIMEE-compltenne word problem (OTWP*) is: given some S (S, H, V tr), decide whether there is a word to,o. t1,0, 12.0, 12,1, 12.2,..., In,n E S* for some n E N. s.t. the tiling 7 defined by r(i, == 44 comprises a successful tiling of On. The two variants of the bounded octant tiling-word problem are both: given some S as above and n, decide whether such a word exists. Note that, again, here is an input parameter, and so its representation may affect the complexity of the problem, leading to the distinction between OTWPbin bin with binary encoding and OTWP un with unary encoding.
The unbounded octant tiling-
Theorem 6.
a) OTWP" is undecidable (E) -cooolple)
b) PT bin is NEXPTIME-complete.
c) OTWP un is NP-complete.
Proof. (a) It should be clear that a tiling problem and its tiling-word variant (like OTP" and OTWP") are interreducible since they only differ in the formulation of how the witness for suc- cessful tiling should be presented. So they are essentially the same problems. Undecidability of OTP" and, thus, OTWP" is known from (van Emde Boas (1997)) the Σ Uppuppe bound can be ob- tained through a semi-decision procedure that searches through the infinite space of O,,tiling for any > 1. This justifies the statement in part (a) Thm. 6
(b) With the same argument as in (a) suffices to consider OTP instead of OTWP pin. The upper bound is easy to see: nondeterministic procedure can easily guess tiling for O, and verify the horizontal and vertical matching conditions, as well as the use of the initial and final tile in appropriate places. This is possible in time O(?²), resp. (222logm) which is therefore exponential in the input size [log ni] for binarily encoded parameters n. This shows inclusion in NEXPTIME.
For the lower bound we argue that the halting problem for nondeterministic, exponentially-ting bounded TM can be reduced to O'P given a nondeterministic TM M over input alphabet Σ and tape alphabet that halts after at most time 2*(*) steps on input words of length n for some polynomial n, and word w E Σ*, we first construct TM M,, that is started in on the empty tape and begins by writing w onto the tape and then simulates M on it. This is a standard construction in complexity theory, and it is easy to see that the running time of M., is bounded by a function
14

---

Published as a conference paper at ICLR 2025
2 (er) for some polynomial p'. With the observation made above, computation of MM can be seen as a sequence of configurations Ci...., Cy((n))) with |C,] = i. This does not directly define tiling system, instead and again by standard trick, cf. (van Emde Boas (197)) or (Demni et al.) 2016 Chp. 11), one compresses three adjacent tape cells into one tile in order to naturally derive horizontal matching relation from overlaps between such triples and vertical matching relation from the TM's transition function. At last, let n' := p' /((ww). It is then a simple exercise to verify that a valid tiling of the triangle An' corresponds an accepting run of M on and vice-versa, HEAPTIME-hardness
which establishes
(c) This is down exactly along the same lines as part (b), but instead making use of the fact that, when n is given in unary encoding, p(n) is polynomial in the size of the representation of n. and hence, the time needed for the guess-and-check procedure in the upper bound is only polynomial, and for the lower bound we need to assume that the running time of the TM is polynomially bounded. Thus, we get NP-completeness instead of NEXPTIMEE-cmppleenees..
B PROOFS OF SECTION
In the following, we give formal proof for the undecidability results of Section 4 To do so, we make use of classical Feed-Forward Neural Networks.
Feed-Forward Neural Network A neuron v is a computational unit computing a function RR - R by - )..) (b E w;ar:)) where is function called activation and b, w; parameters called bias resp. weight. A layer I a tuple of nodes (UI,..., Un) where we assume that all nodes have the same input dimensionality m. Therefore, computes function 1² R". We call n the size of layer I. Let | be a layer with input dimensionality m and l layer of size n. A Feed-Forward Neural Network (FNN) N is tuple (4,,... .4) of layers where we assume that for all i < k- 16-1 holds that the size of L, equals the input dimensionality of 4++1 Therefore, N computes a function RT 1 by processing an input layer by layer.
In particular, we use specific FNN with refu(z) (r) = max(0, x) activations, called gadgets, to derive lower bounds in connection with the expressibility of transformers. We denote the class of all FNN with relu activations by (relu).
Lemma 4. Let & E R²0. There are basic gadgets
1. MH E (relu) computing [11(x)= = |z=].
2. Nr E ((rel) computing a function TR2 TR such that NN x2) 0f) (11 S
0, 2 x22) = (I1 + - 22 if (x1 + 1) - x2 E (0; and N (21, [22) = otherwise,
3. N= E (relu) computing a functio I22 + R such that N N= 22) 0 if x2 = 0,
N (2) [x2 =1| if |2/ 21 (0; 1) and N= x2) otherwise.
4. N_, E (relu) computing a function R.2 -> IR such for all imputs 22 with 2n (0. 13
and E [0; k) holds N (=1(11,2)) = 0 if x = x2 or xn 1 and N N=,
relu(12) otherwise.
Proof. Let Ny. be the minimal FNN computing (elu(relu(=z) relu(z)), let N₂ be the minimal
FNN computing relu (f 2222 - (x1, (21, where (= 12) relu (31 - y2 +1) and let N_ be the minimal FNN computing relu redu(f=(z)) (ffff((11100 (122-4 f=(11 + 11, + f= (1), - f= + 1, 1,)1) where f= [=(11, (
relu(y22 - y1 The claims of the lemma regarding these gadgets are straight- forward given their functional form. Let N_, be the minimal FNN computing relu( relu(x2) - k
relu(x))) )). As stated in the lemma, we assume that x E (0, 1} and x2 [0; k). Then, -k relu(x))
is -k if _1 = and 0 if æ = O. Thus, N_, is guaranteed to be 0 if # = 1 and otherwise it depends on T2. This gives the claim regarding gadget N...
We will combine gadgets in different ways. Let N₁ and N2 be FNN with the same input di- mensionality m and output dimensionality nı respectively 72. We extend the computation of Nj to functions Rm' + R with m < m' by weighting additional dimensions with in the input layer. Given a set of input dimensions 31,-.., we denote the effective dimensions
15

---

Published as a conference paper at ICLR 2025
Fays Fim with pairwise different i, E {l....,m) m') by Ni" Ni Formally, this means that N1 ( Fi... for all inputs. We denote the FNN consisting of N1 and N₂ placed next to each other by Nil Formally, this is done by combining N1 and N₂2 layer by layer using 0 weights in intersecting connections. Then, Ni ll-V2 computes I + R t given by N1 (2 = (N1 (x), (x)). We generalize this operation to k FNN N1 IN in the obvious sense. Let N₂ be an FNN with imput dimensionality nı and output dimensionality nt. We denote the FNN consisting of N1 and N3 placed sequentially by N3 Ni. Formally, this is done by connecting the output layer of N1 with the input layer of Ng. Then, N3 o N1 computes I - I8as given by N3 N₁ (z:) =
Nit Wii "f1....-Tm''
We also consider specific gadgets needed in the context of tiling problems.
Lemma 5. Let S _ NN be a finite set and R C S There is FNN NR (rrll) computing IR? + R such that N NR(01,2) N= E (rrlu) for each E S computing R - R such that N=((z) E {0. 1} for each x E N and (x) = 0 iff t.
E {0, 1} if (æ1, E S and N NR(T1, x2) = 0 iff (II, x2) E R and there is
Proof. Let S S N be finite, R S S and & E S. First, consider N=.. Let N₂ be the minimal FNN computing relu(0 x + t) and Naa be the minimal FNN computing (rela(z), (rell(-el)))) Obviously, N₂ computes the constant function and Nis computes the identity in the form of two dimensional vectors. Let N= be given by the minimal FNN computing N= (NaallNe) with the slight alteration that the two output dimensions of Nia are connected to the first dimension of N= Then, the claim of the lemma regarding N= follows from Lemma and the operations on FNN described in Appendix B
Now, consider Nn- Given some 8 E S let R(s] = (r I (s.r) E R). Let N be the mini- mal FNN computing relu(11 .... + rx). Furthermore, let NeT for some set T C S be the minimal FNN such that Ner(z) = 0 if x E T and NET(z)
if x E S \ T. A con- struction for NeT is given in Theorem 4 in (Sälzer & Lange 2023 ). According to this con- struction, Ner consists of three layers and is polynomial in T. In the case that T = 0 we as- sume that Nep is the constant function represented by suitable FNN. Then, Na is given by ( o |.N (e i))Il ... IN [ for some arbitrary order on S with the slight alteration that NR has two input dimensions, meaning that each subnet (N=., (NeRte)) is connected the same two input dimensions. Again, the claim of the lemma regarding Nn follows
from Lemma 4 and the operations on FNN described in Appendix B
Given these understandings of gadgets, we are set to formally prove the results of Section 4
... fm E St as stated in the lemma and assume some order 0; on S. Furthermore, let emb(a;, 1) = 1,, and emb(a,, j) = (0, 1, E h, i) if > 1. Let emb(w) = xf ...... In the following, we build two layers I and l2 using com- ponents allowed in Tadee, satisfying the statement of the lemma. Layer l consists of single attention head att,,1 = =scoore,,1, pool,,1). The scoring function is given by score,, (x. x²)
Proof of Lemma 7 Let w =
(1Q, K k(,=²))) where Q1,1 = [[0, 0, -1, 0, 0), 1,, 1,, 0), (0. 1, O. 0), (0, 0, 1,0) and Nxx) -relu((E h) - (i - 1)) and it follows that score ( x = 0 if Ei h < i - 1 and otherwise we have that sco xf) < 0. The pooling function is specified by the matrix W1,1 = [[1, 0, 0, 0, 0)] and uses hardmax normalisation function. The combination comb; func- tion is given by the FNN N₂ (x)..... Fs. 8) = relu(z2)l -.- (eeeu(()))(rel((()) Given position z?, the attention head att attends to all positions æ5. satisfying Ei=o h S 1- This is due the way score1,1 is build. Then, all computes 1 using pool,,1 where is the number of positions allı, attends to. Here, we exploit the fact that only the first position æf has a non-zero entry in the its first dimension and that for all head att,,1 attends to 2². Finally, comb, simply stacks the old vector æc onto the value t. but leaves out the first dimension of ae.. Let i (emb(w)) 2| a/. Layer l2 consists of a single attention head all2,1 = (score2,1, poolg,1) The scoring function score2,1 is given by N2,1 ((Q2,1)) !! k2)zz))) where Q2.1 = [ 0, 0, 0, 1)), K2,1 = [(0, 1, 0, 0, 0)0)] and
0, 0). (0, 1, 1,0,0,000000 0,0 and K1,1 = re). We have that score (2. x9)
1 = -relu(relu( (x: 1) + relu(1 - x)). We have that score2, 1 ( (a!,ar)) a?)) if } +-j = 1 where
16

---

Published as a conference paper at ICLR 2025
is the fifth dimension of z! and otherwise scoreg, (a) x < 0. The pooling function pool2, 2,1 is specified by W2,1 [(0, 1, O, O. 0), (0,0, 0, 0)] and uses hardmax normalisation. The combi- nation comby is given by the FNN (Z T5. U1, 92) = relu(z1) [relu(12) (relu())) 1/2 relau((xa)) Given position x... the attention head att2,1 attends to the position j. where 1. = Relying on our arguments regarding the computation of (1, this is the position j satisfying max, max,(Ei h < i - 1). However, this j is equal to the row index r(t) of the decomposition of i
based on the inversion of Cantor's pairing function. Thus, have that r(i) = j. Furthermore,
have that c(i) = (i - 1) - Eh=n h),, which is computed by relu(x2 - //2 1) in the combination function comb2. Overall, we see that (21 (emb(w)) gives the desired result.
L
Proof of Lemma 2 Let I be stated in the lemma. By definition of Tudecs the scoring func-
tion of f is of the form N((2x, Kmy)) and the normalisation is hardmax. Let Q =
(aa,.....0 0x). : (b, O,. .......,),, (1, O, ..... 0)], K [[1, ((., 0), (1, 0, ..... 0), (0, -,,0,.... 0)] and N be the minimal FNN computing (xx) = -relu(Ny,
= ||x] where Mμ1 is given by Lemma
Overall, this ensures that the scoring is given by score Zz) = (1) -jl- Then, the statement
of the lemma follows from the fact that hardmax attends the maximum, which is 0 given this scoring, and that j E N is unique for each z.j.
Lemma 6. There is atlention head all- in Tudes such that for all sequences æ1.... Em where all x; = (1, i, ys) the head a attends to {z1...., xi} given i.
Proof. By definition of Tudors the scoring function of ally is of the form N((Qu,, Kæ₂)) and the normalisation is hardmax. Let Q 1,0,,,..... 0). O1,0.....
..... 0) and let K be equal to [[1.0 0. ...,............................ 0), (0,-1,0, 0, .... O)]. Furthermore, let Nxx) = -relu(z). We observe that N outputs 0 if j S and otherwise (xx) < O. In combination with hardmax, this ensures that att& behaves as stated by the lemma.
Proof of Theorem 7 We prove the statement via reduction from OTWP". S (S, be an instance of OTWP" with |S| = k. W.L.o.g we assume that S S N. Let Ts E Tudec be built the following way. Ts uses the embedding emb of transformer in Tuiee specified in the beginning of Section Furthermore, it has four layers. Layers 4, 12 are as in Lemma T Layer l is given
by la - ( pall; all all atts combs) where all allnext and allstep are of Lemma 2 whereby
prev ............................. .x,))..,,,))))))) = x2 1, (x), (5) x22 + and slep(I), ..5) = 22 + 23g + 1. We
assume that all three attention heads use the identity matrix as linear maps in their respective pooling
function. comby is given by an FNN Ns computing IR + R. Let the input dimensions of Ng be
F1,1, ,1,,,,,,,1111--......... 22,1, T4455- Then, Ng is equal to
relu(z1,1) M relu(11, 2) IN6 IN.IN
where N₂ = No (N N 1.14. No, = N o (N IN 1 No, = N o (N 2 (1 No N_, o (N (N |N .3..55 and Na = N_ o (N 3...3 I (2..) us- ing the gadgets and constructions described in Appendix B Layer 4 is given by 4 where atflee attends to (æ1..... ..;) given i and comb4 is given by the minimal FNN Na com- puting relu(x3 +... ....... + 27). formal proof for the existence of atfeeg Tuder is given in Lemma 6 Furthermore, the output function out of T's is given by the minimal FNN Nout com- puting [(11) = velu(1-x1)
(attleg comb,)
Let w 4 ...4 S* be some word over alphabet S. As defined above, we have that emb(l,, i) (1, Ej where k; E {l....,|S]] Consider .. 2m after propagating w through the embedding emb and layers 4, la of Ts. As stated by Lemma [ we have that x² = (1, i, r(i), c(i), k;) where r(i) and c(i) are the row respectively column of tile I, if we interpret w as an encoded tiling. Note that all vectors æxf are non-negative due to the way N₂ is built. In the following, we argue that all x;- = 0 if and only if w is valid encoded tiling. Given this equivalence, the statement of the lemma follows immediately as 44 simply sums up all vectors and dimensions (except for the first and second) of ......, 2² in at and the output of N₂ indicates whether there was some non-zero value. We fix some arbitrary 2 = (1, r(), c(1), kz). Then, æi =Na(= Na 2 _ "²",,, where ineat = i ++1 1 if < m and m otherwise, iprew i 1f i and otherwise and istep = i + r(i) if < m r(i) and m otherwise.
namely the sequence of vectors
17

---

Published as a conference paper at ICLR 2025
Consider property (a) and subnetwork Na. With the understanding gained in Appendix B N 2 outputs iff 11,2 = 23 These dimensions correspond to positions and Enezt. which are only equal if i = m (Lemma 2 Furthermore, the property of NN,, stated by Lemma is given as the output of N= is guaranteed to be in [0; 1] and the values of 21,2 and I3,2 are guaranteed to be in N. In summary, this ensures that the third dimension of xy, is iff r(m) = c(m). For other positions the third dimension is always 0 since N+, outputs 0 in these cases due to the fact that 2 equals 1. Analogously, No, and No, ensure that 1 = tt and Im = ty and, thus, property (b) iff the fourth and fifth dimensions in all positions are equal to O. Consider properties (c) and (d) described above and assume that property (a) holds. These two properties are non-local in the sense that they depend at least two positions in of ......... x Consider the subnet No- By construction and the gadgets described in Appendix B we have that N. outputs O if c(i) < r(i) and (t,, (++1) E H or c(i) = r(i), which means that tile t, is rightmost in its corresponding row. Otherwise the value computed by N₂ is greater than O. Analogously, subnet Na checks whether vertically stacked tiles do match. In summary, this ensures that the sixth and seventh dimension of each x is equal to and only if properties (c) and (d) hold.
Proof of Theorem 2 In the same manner as in the proof of Theorem I we prove the statement via reduction from OTWP". The reduction is exactly the same, namely given an OTWP" instance = (S. H. V, t1, te) we build TE Tss which recognizes exactly those words w representing valid encoded tiling of S. For details, see the proof of Theorem
Given the correctness arguments for T's in Theorem I left to argue that Is works as intended, despite the fact that it works over some FA F using at most (log (llo((max((5) n))) bits where n is the length of an input word. We choose F such that overflow situations do not occur in any computation (w) and rounding is handled such that T's works as intended. Throughout this proof, we use log(n) Namely, given a word w with |w] = n assume that F uses m = [4 log (og(maa((51) n))J + bits and rounds values off to the nearest representable number. We denote the value resulting from rounding x off in arithmetic F by |-|p- We assume that there is an extra bit that is used as a sign bit and that least [3 log(n)] + 1 bits can be used to represent integer and at least [log(n) bits can be used to represent fractional parts. Note that this is a reasonable assumption for all common FA, like fixed-point or floating-point arithmetic. Furthermore, it is clearly the case that m E (log max()S), n))). To case our arguments and notation from here on, we assume w.l.o.g. that we represent n using log(n) instead of [log(n)] +1.
Per definition, Ts uses the embedding function emb(ax, 0) = (1, and emb(ap, i) (0, L, o. First, we assume that each k, namely the value representing a specific tile from S, is unique, positive value. This is possible as F uses m log([S]) bits. Furthermore, that emb, especially the sum Σ Σj=o- = ((++1) S ? works as intended up to i = n due to the fact that F uses more than m > 2 log) bits to represent integer parts. Next, consider layer l and la of Lemma [ Layer l consists of a single attention head all,,1. 1. Here, the only crucial parts are the computation of value 1 in pool,, for position i. Per definition, I corresponds to the number of positions j such that Ei_o h <i- 1. As i is bounded by n, this inequality can only be satisfied by positions j for which j S vn holds. As Ts uses hardmax to count the positions for which this
2
inequality holds, is bounded by Vn. Next, we observe that L F 2log(m) = _ namely the general understanding of rounding off where we use log(n) bits to represent fractions. However, this
21og(()
gives that for all 1 < 1,- < la S v that [+ F # [ F ] o 1 holds for all < l2 S vn.
This means, that it is ensured by F' that & is uniquely representable.
Next, the only crucial part in La is the computation of the product } j. which is used to determine the position j for which + - = in score2, which is obviously given by position 7. This equality is no longer guaranteed to exist if we consider [7.r | .j. However, due to the monotonicity of [iJr for I I vni and that the maximum round of error is given by ạoon. we have that the j = I produces the value closest to in the product & .j. Taking a look at score2,1, this ensures that is still the position that attz,1 1 attends to. Therefore, the statement of Lemma [ is still valid for T's working over F. We observe that all values of some vector 2² after layer l2 are positive integers whose magnitude is bounded by n
18

---

Published as a conference paper at ICLR 2025
Now, consider layer is and 4. From the proof of Theorem
1 we see that the gadgets at most sum up two values or compute fraction of the form 1 and (in gadgets NH or Ny). Both can 2
safely be done with at least 3 (og(n) bits for integer and log(n) for fractional parts, as all previously computed values, up to layer 12. in a computation of (s(w) are representable using 2 log(n) bits. We observe that the values of the third to seventh dimension of some æ) are either 0 or 1. This is due to the fact that all values after layer l2 guaranteed to be integers. Next, consider layer 44- The computation done by allg is safe (see Lemma 6 and the crucial step here is the computation of combs given by relu(x3 + ............................... + z7). The values I; are all of the form ; where i is guaranteed to be 0 or 1 and j is the normalisation induced by attg from perspective of position j. However, this means j is bounded by n and, thus, [ > 0 if and only if i = 1 for all j due to the fact that F allows for log(n) bits to represent fractional parts. Finally, out is trivially computable in F, which finishes the proof.
C PROOFS OF SECTION 5
Proof of Theorrm 3 The decidability and membership results of statements ciently argued in the proof sketch given in Section
T and 2
Dare suffi-
To prove the hardness results of statements ( and we establish a reduction from OTWP Pun re- spectively OTWPbin: given some bounded word-tiling instance (2, we build an instance (T's n) of BTRSAT, respectively BTRSAT where Ts is build as described in Theorem The only miss- ing argument is that these reductions polynomial. In particular, this means that Tss must be built in polynomial time regarding the size of nS. Therefore, we recall the proof of Theorem [
First, we see that the embedding function emb and the amount of layers of Ts is independent of S and n. The first two layers l and l2 of Tss are specified in Lemma Recalling the proof of Lemma see that l and l2 each consist of a single attention head, whose internal parameters like scoring, pooling or combination are independent of (S, n) as well. Next, consider layer (3. This layer consists of three attention heads att pree. attnext and step each given by the template described in Lemma 2 which again is independent of (S.n). Additionally, 1s contains the combination function comby. This combination function is represented by a FNN Na, using smaller FNN N.. No., No.. N. and N₂ as building blocks. These are dependent on S, as they are built using gadgets s N=ty, Nи and Ny where I,, Lr, H and V are components of S. However, the proof of I Lemma that these gadgets are at most polynomial in their respective parameter. Layer L and the output function, specified by FNN N out, are again independent of (S, nz). In summary, the TE T's is polynomial in (S, n2,, which makes the reductions from OTWpesp und OTW OPoyy polynomial. 0
Next, we address the proof of Lemma 3 We need some preliminary, rather technical result first. Let be an TE and w Σ be a word and consider the computation T(w). Let T(w) = emb(w) and X (w) be the sequence of vectors occurring after the computation of layer 4 of T. Let and æ' be two vectors matching the dimensionality of scores, of T. Overloading some notation, x)),, scooee,, (x, (x.,)) where score, (x, Xiru) is the vector of all scorings of æ with sequence T(w). We remark that it is not necessary that x or xx must occur in T(w) for this to be well defined. Again overloading some notation, let Pa (a, i, pool, (Xr(u): s (x,
let Nw (i,j) = p
Lemma 7. Let T be auditive-periodican TE of depth L, maximum width H and periodicity p with norma,j E {softmax, hardmax] for all i I L.j S H, let w = U1 u.- U2 e Ex where u1 E Σt, all uj, E EP and all Uj. also occur in ui or w2 and let X be the set of all vectors occurring in any of the sequences X; Xi If there are indexes h <
h2 I h such that for all x, x' E X,i S L.j S H holds that Nuang (x, x' (i,
Nurun masnnn (x, x', (i,j) and Purua "ai,, (x,i,j) = Purny uMsnn (x,i,j) then it holds that Na Mij mannn Mintt uu (x, (i,j) = Nu was (2, x', i,5) and Purasy Wan, "inges u i, = Pa ug (x0, i.
19

---

Published as a conference paper at ICLR 2025
Proof. Let T. w, X, h1 and h2 be as stated above. We prove the statement via induction on the layers 4-- First, consider layer I and fix some tuple (x, x', 1.5). We first show that Naiu, ""Mnn "Magt1" "uug (2, x', 1.5)
Was (1))). Assume that normi, is given by (
softmax. Then, normi, computes Evare, y(m. T(wl e'v for all words w', Obviously, the
numerator in Nuy Magtiiing (z, x'; 1.3) and N Nay (x. 1, is equal. By definition, we have that scoreij is local in the sense that it compares vectors pairwise, producing the different scoring values sy independent of the overall word. Furthermore, due to the fact that emb is
additive-periodiaal, we have XT ( "",,, "1ag+1 mi)))) and XT (w)--))) are equal in the sense that the vectors corresponding to Mjng u2 are equal. We refer to this property (*) later on. Using these observations and that Naius, -,sh, (æz, a,,,,,,,,,,, 1,5) = Narus, maasing (æz, x², 1,5), we have that the denominator is equal as well. Now, assume that normi, is given by hardmax. Then, [sccoes, ((a,,a" (a,, ((w0)))
nor computes 2 (x, "(ww)) Seoye, (t. ((we)))) where (s) = 1 if is maximal in
S and 0 otherwise for any word w'. In contrast softmax, we have that the values of f(...) are dependent of the overall context, namely the vector of all scorings p X ((w))) Compare Xu
T(urs 4 m,y,, "na+1 (')a)) and X -()) both given by the additive-periodiees embedding emb. Via assumption, we have that each Uj block also occurs in in u2. In particular, this means every vector that occurs in emb(u)... u2) does also occur in emb(u145, ... ".iing Wingi1 u2) and vice-versa. This implies that [(score1, (ar,aa) æ'), score1, X T(wiss "ss, Whati ) mm)))) fscorre, (xx, æ²), score1,, (x))))))))) for any scoring value scorei, (x, x'). In com- bination with the assumption that Noru, "Minn (e,x',1,1) = Nuung "aasn (0, de,,',1,) 1,5) and the observations above, we also get Nuuu ""ii,, "inges "mu (20, x 1,
Na (x,x', .1.) in the hardmax case. tions. By definition, we have that pX ((rr) sconer, (xx, X xxp(r)))) computes X norm1, (1, Dee scorei, ( )) (War)) for any word w'. Our previous ar-
Next, consider the pooling func-
Exp P(wo))
guments give that Numn "raiin Monat1 uu (x, 115) tion with P Puguy,-nn (ar, (, = Puru,,""in "iing (x,, () and (*), we immediately get that Pu Put (2, i, holds as well. Next, consider layer 4. The arguments are exactly the same as in the base case. However, we need to rely on the induction hypothesis. Namely, we assume that all pool,_1.j produce the same output in computation T(uu,, U.,,,, Ujnzta u.)) and computation T(u ..2)). This implies that all vectors present in x--1 T(uaa "iin "ingei (2))) are also present in (()) and vice-versa and that the vectors corresponding to Ujngzi ... U2 are equal in both computations.
(x, xx, 1.j). In combina-
P Paras "'uss, "ing=i nmug i,5)
Proof of Lemma 3 Let T FIX be an additive perttive-eeiodicall TE working over alphabet E, having periodicity p. depth L, maximum width H. maximum dimensionality D and working over an FA F using bits for binary encoding. We use V to denote the set of values representable in the fixed arithmetic that 7 works over. Note that [V| < 2 Let w E Σ+ be word such that T(w) = 1. We observe that there is m E N such that w u1 ... Us where u; E Σ" are blocks of symbols of length p and u E ySS, Our goal is to prove that not necessarily connected subsequence of at most 2(ID many p-blocks u; from in ...... Um is sufficient ensure the same computation of T. In the case that pm + p S 2(TT)) we are done. Therefore, assume that m > 2(T")
Let U be the set of all unique u; We observe that |U| S EEP. Next, we fix some not necessarily connected but ordered subsequence = Uujo ... Uy Ujn+1 with Ujo = U1 js E {2.... m) and "jn11 u of w such that each u' E U occurs exactly once. For the case that #1 = we allow this specific block to occur twice in S. The assumption > 2Poly((T)) implies that S # w. This means that there are pairs (Mjr ")n..) in S with some non-empty sequence of p-blocks us ".. Uy in between. W.loog. assume Ujo and u, is such a pair. Our goal is to argue that there are at most 2(1 blocks from uyy ... dz needed to ensure the same computation of T. Given that this argument works for all E adjacent pairs in S, we are done.
20

---

Published as a conference paper at ICLR 2025
Consider the computation T(w). The periiiiee embedding emb of T impliee that emb(w) includes at most Ep different vectors. Furthermore, from layer to layer equal vectors are mapped equally, which means that each X X_....,................... .. contains at most Ep different vectors as well. This implies that the computation T(w) induces at most (LEp)² x I. X H I (E < (EpI. different tuples (a, x', i.j) where æ, xr' vectors induced by T(w) and < L,J < H. Additionally, we have that for each value Nu,la x', i. and Pu(x,i,)) as defined in the beginning of this section, there are most [VP] I 26D possibilities. Simple combinatorics, namely the pigeon hole principle, states that in the increasing sequence Uj[, Ugg.... there must be points h1 and h2 with hn &2DD(EoLH) < 2(IT))* such that for all tuples (x, (2, ,i,5) induced by T(w) we have that Nuso "s ,t,5))
Nayo "i "r",,, (a), a', (i,5) and Pupo "1 "o,,, (x, i.j) = Pajo u "ash (x),, Now, Lemma states that this implies Nuso " """,, "shzti "on wn (z. (2,,d',,,, 2,5) = (z, and
Pa Paso P350"'1 "31 "1,",,,,, "/,, "shuti "" ...((; (. = Pul However, this implies that the subsequence "hht1 "", has no influence in the computation of 7 on and, thus, can be left out. As we can argue this for every such cycle occurring in uz u.g, we get the desired bound of 20/).
Proof of Theorem 5 First, argue the decidability of [ Assume that T T with an arbitrary embedding emb is given that operates in a fixed-width arithmetic using b bits for rep- resenting numbers and wrap-around
handle overflow. Then, emb is periodic with periodicity p S. 2b, simply due to the fact that positions é in some word w can only be exactly represented up to magnitude 2h. Therefore, the same arguments used in Theorem 4 apply here. Note that this does not imply DEXPPIMEE-memberssip of TRSAT(7 due to the fact that the period is exponential in b. Analogously, in a saturating scenario, we have that emb has finite prefix of length at most 2 and is periodic with periodicity afterwards. Here, the small-word property used in Theorem 4 follows the same line of reasoning, with the difference that either the finite prefix sufficient as a witness, or the finite prefix followed by an exponentially bounded suffix, whose existence follows from the same arguments as Lemma 3 with periodicity p 1 1.
Second, we argue the NEXPTIME-hardness Let S = (S, H, V, (tp) and n 2 1 be an instance of Pin We construct an TE Ts. E T working over some FA F with (w) 1 if and only if w E S+ witnesses the validity of the OTWP instance (S, n).
We prove the statement via reduction from OTWP Piinin-
Next, let Ts.n be built exactly like T's in the proof of Theorem 4 but with the following structural adjustments. In layer La we adjust comb3 to be comb3 = N3 N. N where N3 is specified as in the proof of Theorem 4 No = N (N (N212.23. | and N2 2 int where Ngt
is analogous to the construction of N= given in Lemma 5 Furthermore, we adjust comb, in layer la to be represented by the FNN retu(xs + + F3g + 2gg). We refer to the gadgets described in Lemma and Lemma 5 as well as the proof of Theorem [ for further details.
Consider the adjustment in I3. FNN N₂ in comby ensures that (w)
only if the row index corresponding to the last symbol is equal to n. Note that N₂ checks whether row and column index corresponding to the last symbol are equal. Additionally, N, checks if there is no id equal to
(x+ (++1)(((+)++1] + 1. This corresponds to the position id of the successor of the vector representing tile (n. Furthermore, the adjustment of combA considers the output of Ne and N2 in addition to the outputs of N3. In summary. we have that Ts,n only outputs 1 given wr if the word length is such that the row index corresponding to the position of the last symbol of w in a respective octant tiling is equal to n (ensured by Ne). that w is at most of length [n+1)((++1++1) (ensured by Ny) and if w represents a valid encoded tiling (the remaining parts of Ts....
2
2
Additionally, we need to argue that Ts,,, works as intended, despite the fact that is limited by some FA F using a representation size that is at most logarithmic in These arguments follow the exact same line as in the proof of Theorem 2 but using FA F that uses m = |6 log(mmxx (max( ( n)) + 2 bits
and handles overflow using saturation. The reason for the larger representation size is that words w representing a valid encoded tiling ending at position (n, n) are of length |w]| = (n+1)((++)+))) <
2 a((2)
n². Thus, we use [4 log(n)) + integer bits to be able to represent sum Σ/ -
< 2
21

---

Published as a conference paper at ICLR 2025
for all i S n² and [2 log(n)] fractional bits to uniquely represent fraction for / Σ For detail see the proof of Theorem 2 Furthermore, the fact that we use [n]o + bits to encode integers and that F handles overflow using saturation ensures that Ny works intended: that (m+1((x++++1) + < n² and, thus, we have that the id (=+I((x++++1) + occurs at most 2 once, independent of the length of it is the point where I enforces saturation the positional embedding. Thus, allzetr works for this position as intended and then Ny checks the property described above correctly.
have
The argument that Ts., can be built in polynomial time is a straightforward implication from the arguments for Theorem and the fact that N, and N are small gadgets with maximum parameter quadratic in n, which can be represented using a logarithmic amount of bits.
22


Reviews:
[{"review_id": "BF9FqbdhT8", "reviewer": "Reviewer_1Qh5", "summary": "The paper proves several hardness results on the satisfiability of encoder-only Transformers. These results demonstrates the hardness of preforming formal verification of satisfiability over Transformers Encoders, which is undecidable for unbounded-length, log-precision Transformer Encoders, NEXPTIME-Hard for bounded-length inputs and bounded precision.", "questions": "Please address the concerns raised in the Weaknesses section.", "limitations": "", "rating": 6, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "Overall, the theoretical contributions of this work can be impactful as formalizations of impossibility results of general formal verification over Transformers. The theoretical contribution of implementing a tiling system within Transformer Encoders can also be useful for further theoretical work, whereas prior works on expressiveness on Transformer Encoders mostly focused on upper bounds with circuit complexity. As such, I recommend for Acceptance (assuming the authors make appropriate clarifications as mentioned below).", "weaknesses": "The paper tries to make arguments that connects the satisfiability theorems proven in the paper to “formal reasoning” (i.e, model verification and interpretation), which I believe is not sufficiently justified. In the section 3.1 “Satisfiability as a baseline formal reasoning problem” the author makes 2 examples: robustness verification and formal interpretation. However, both examples require the input to satisfy certain properties and decides satisfiability on the set of inputs with the given properties. It is unclear whether the how hardness results still hold when input space is constrained as in the given examples. As such, this connection between the theorems proven in the paper and “formal reasoning” should be accurately characterized.\n \nThe naming in the paper can cause much confusion. SAT typically refers to the Boolean Satisfiability problem in computational complexity, and using SAT to also refer to Transformer Encoder Satisfiability can be confusing to many readers, especially the claim that “SAT is undecidable” in the abstract. It is recommended to use a different acronym for the specific problem. Similarly, “Formal Reasoning” also has specific meanings referring to reasoning over formal systems with well-defined inference rules and axioms. The “formal reasoning” in this paper can be directly stated as “verification and interpretation”.\n \nAt the current state, the paper’s conclusions are not fundamentally surprising given the recent line on work on the expressiveness of Transformers (although, as mentioned, formalizing such statements and providing a concrete construction is a sufficient contribution). From a practicality perspective, both NP-Hard and NEXPTIME-hard are both infeasible, and it would be more impactful if the work shows interesting classes of Transformers/properties that can be verified in polynomial time.", "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": "qMlaRUIdQn", "reviewer": "Reviewer_RHMx", "summary": "The paper studies the decidability of the emptiness problem of the language recognized by a transformer encoder classifier,  that is, whether there exists a string w in the input domain for which the given transformer will return true. It also studies the complexity of such problem in contexts where it is found to be decidable.", "questions": "Pg. 2. L 54-54. I disagree with this comment. Programming languages are Turing Complete, still formal reasoning and verification has been a very active, productive and necessary field of computer science. Nevertheless, it is worth knowing\tthe boundaries of decidability and complexity to figure out methods to cope with that.  Please comment.\n\nPg. 2. L 66-69. What do you mean by “formal interpretation”? The term is not common in the field of formal verification and you do not define it here nor provide references to definitions or related work. An example is provided later in Pg. 4, Sec. 3, which reduces to a verification problem. There is missing related work regarding formal methods and tools for extracting automata-based models from different kinds of neural classifiers (including transformers) and language models that should be cited here. Such methods can accomplish verification and generate explanations. Good sources of references for this matter are the Proceedings of the International Conference on Grammatical Inference 2023 and the last two LearnAut workshops. That line of relevant work is not referenced by the cited papers.\n\nPg. 3. L 169-174. What part of the TC proof of Pérez et al made you believe that languages recognized by the class T_udec could possibly be decidable?\n\nPg. 4. Could it be possible that softmax rather than hardmax change the decidability result?\n\nPg. 5. L 251. The 3. Clearly, bounded satisfiability is decidable if T(w) is computable because you can enumerate all words up to length n. The important result here is the complexity bound. Also, the way this theorem is written  here is different from Sec. 5. You should rewrite this.\n\nPg. 5. L. 265. In what sense fixed-width arithmetic has a similar effect to bounding the input length? Besides, why not considering then T^FIX only?\n\nPg. 6. L. 302. Why is it the case that T_udec is the weakest class in terms of expressivity? \n\nPg. 6. L. 306. The name “octant” tiling problem does not seem to be standard. It is not mentioned as is in the provided reference. Also it is not clear why it is necessary to distinguish between “tiling” problem and “tiling word” problem. The definitions in the appendix do not make this clear. Could you explain it?\n\nPg. 8. L. 401. It reads “one can reasonably assume the size of a syntactic representation of T to be polynomial on |T|”. It is not clear to me that this assumption is reasonable. Please provide arguments.\n\nPg. 8. L. 402. The so-called polynomial evaluation property is not discussed in Section 3 nor elsewhere in the paper. Why is it reasonable?\n\nPg. 8. It seems that the proof sketch of The 3 does not take into account the representation of w. Please comment on this.\n\nOther comments\n\nPg. 3. L. 138. k should be L since i is a layer, and layers go from 1 to L.\n\nPg. 3. L. 157. different rational number”s”", "limitations": "", "rating": 3, "confidence": 4, "soundness": 2, "presentation": 1, "contribution": 2, "strengths": "The main interest of the paper is to try to define bounds on the complexity of decidable classes of problems related to languages recognized by transformes.", "weaknesses": "The paper itself is quite a high-level description of a list of results. The necessary definitions, such as the tiling problem, and other key aspects of the proofs are in the appendix or completely missing. The absence of important definitions makes the paper difficult to follow.\n\nBesides, the structure of the paper with a preview of the results does not enhance readability but quite the contrary. It would be much readable if the results were shown, proved and explained once, providing reasonably detailed proofs that put forward the important issues (while the much technical details are put in the appendix).", "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": "tLs8ZMWDr7", "reviewer": "Reviewer_UiUG", "summary": "This technical paper tackles the decidability of satisfiability for Transform encoders (TE), namely, does there exists an input such that the output of the TE is a given constant, say 1. This problem is a generic problem which can encode pattern recognition, etc. The results by the authors are as follows:\n\n1) in general, the satisfiability problem is undecidable. The proof is by reduction to a tilling system, or equivalently to halting problem - a correct input of the TE leading to output 1 corresponds one to one to a (correct) halting unfolding of a run of the machine. The encoding requires a number of bits for each neuron computation logarithmic in the size of the input, and also that the embeddings are *not* periodic.\n\n2) If the input is bounded by size n, then the problem is NP-complete(n) (leading to a usual NExptime-complete complexity if n is written in binary), the upper bound being trivial and the lower bound being the same reduction than for undecidability.\n\n3) Alternatively, if the input is unbounded but the number of bits for each neuron computation is bounded by a number of bits part of the input, then the problem is also NEXPTIME-hard using the exact same encoding, although no upper bound, is provided in this case, not even decidability.\n\n4) The most interesting decidability result is that if the number of bits for each neuron computation is bounded and the embedding periodic, with both the period and number of bits are part of the input (in unary), then the problem is decidable in NEXPTIME (but no lower bound is provided).", "questions": "1. Where is the fix-precision used in the proof of lemma 3? Is it necessary?\n \n2. Do you have proof of decidability for fix-precision (*without* periodic embeddings)?\n\nIn all cases, you cannot draw Sat[T^fix] on the Nexptime ball (in figure 2), as there is no proof it is *in* Nexptime. (edit: fixed)", "limitations": "", "rating": 5, "confidence": 5, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "1. The paper explores the complexity of Transform encoders. Understanding the theoretical complexity of this hot topic is very timely.\n\n2. The proofs seem solid. 2 constructions are non-trivial (one lower bound encoding (1) and one decidability & (upper bound) complexity proof (4), the other being direct application of the first construction).", "weaknesses": "1. The paper could be written in a more reader-friendly way, it is very technical. Statements of the theorems are unnecessarily complicated. The number of Theorems is also inflatted. E.g. theorem 2 should just be a note at the end of theorem 1: \"undecidable in general, even when restricted to log-precision transformers.\" At the end of the day, there are 2 main results in this paper (1 and 4 listed above).\n\n2. (edit: partially improved, but the solution does not fundamentally change the usability landscape, which is in practice somehow still restricted to bounded input) The biggest weakness is that the complexity landscape has a serious gap. The authors need 2 restrictions together to get decidability (see 4.), and the proof of undecidability needs both restriction lifted. So what happens if only one of this restriction? Even more problematic, the authors focus heavily on one of these restrictions (bounded-precision, which is arguably a very reasonable restriction to consider), leaving the other (periodicity, a much stronger restriction) as a technical factor that can be easily overlooked by an inattentive reader (for instance, the notation is using a small '_o'). The proof in appendix C reveals that its actually periodicity that is the main driver for decidability, and fix-precision only seems to be accessory to simplify the proof, and may be useful for the Nexptime upper bound complexity.", "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": "bbkK5lYvhO", "reviewer": "Reviewer_1jYG", "summary": "The paper studies the complexity of deciding whether a transformer accepts a given input sequence. This problem of satisfiability (SAT) is studied on encoder-only transformers. Encoder-decoder transformers are not considered, as they are Turing complete and hence the SAT problem is immediately undecidable. Firstly, the SAT problem is proven to be undecidable for hardmax encoder-only transformers using a reduction to tiling problems, even when the transformer has log precision. Secondly, decidable restrictions are achieved using bounded length sequences or fixed precision in combination with periodic embedding results. However, in these cases, the SAT problem still remains NEXPTIME.", "questions": "- Do any of the proven results change if satisfiability is defined as exceeding a given threshold instead of just being equal to 1? This could be a more realistic condition for acceptance.\n\n- Do the authors have an intuition on to what extent their results could generalize to soft-attention?\n\n- It was not clear to me if the definition of SAT on transformers is new, or has been proposed before.\n\n- This perhaps a bit of a broad/vague question, but seeing the many undecidability and hardness results proven in the paper, do the authors think that there is hope for formal verification techniques on transformers? Or should the verification efforts focus on more tractable and less expressive classes of models than the transformer?\n\n*Some small nitpicks*\n\n- Brackets for citations are not used properly. The paper consistently cites transformers Vaswani et al. (2018) instead of transformers (Vaswani et al., 2018).\n\n- The font in Figure 2 is too small for me to be readable without zooming.", "limitations": "", "rating": 8, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "Although the content is very theoretical, the authors take care to first give a general overview of the results (Section 3), after which proof sketches are given (Sections 4 and 5) and more detailed proofs follow in the appendices. This presentation kept the paper relatively digestible, despite the fact I’m not very familiar with this subject matter. From a theoretic viewpoint, I found the results interesting. The practical usefulness seems somewhat limited to me, but as the authors note the presented SAT problem is foundational in relation to safety and verification of model properties and this work provides a useful start in its study.", "weaknesses": "As I am not really familiar with the computational complexity study of neural networks, I do not feel very confident to judge the significance of the findings. However, some of the assumptions seem to limit the practical usefulness of the results.\n-  As the authors mention themselves, the distinctions between the considered transformer models fall away when a bounded word length is assumed. Given that transformers almost always have a (fixed) context window, such a bounded length assumption seems quite reasonable to me, and the results for unbounded length seem less relevant.\n- The $\\mathcal{T}_{udec}$ class for transformers (and its further restrictions) uses hard-attention instead of soft-attention. Previous works have indicated that soft-attention can achieve significantly different results compared to hard-attention (Strobl et al. 2024).\n- The decidability results of e.g. Theorem 3 are based on naive enumeration, which is not realistic except for very short word lengths.", "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)