Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning

## Abstract

Abstract We analyse the complexity of the satisfiability problem (SAT) for transformer encoders (TE), naturally occurring in formal verification or interpretation tasks. We find that SAT is undecidable when considering TE as they are commonly studied in the expressiveness community. Furthermore, we identify practical scenarios where SAT 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 SAT due to their limited attention capabilities. However, the problem remains difficult, as we establish scenarios where SAT 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.

## 1 Introduction

Natural language processing (NLP) models, processing and computing human language,
are gateways for modern applications aiming to interact with human users in a natural way.
Although NLP is a traditional field of research, the use of deep learning techniques has
undoubtedly revolutionised the field in recent years Otter et al. ().
In this revolution, models such as Recurrent Neural Networks (RNN) or more specific Long
Short-term Memory Networks (LSTM) Yu et al. ()
have long been the driving force, but for a few years
now NLP has a new figurehead: *transformers* Vaswani et al. ().

Transformers are a deep learning model using (multiple) self-attention mechanisms to
process sequential input data, usually natural language. The efficient trainability
of transformers, for example in contrast to LSTM, while achieving top-tier performance
led to numerous heavy-impact implementations such as BERT Devlin et al. (), GPT-3
Brown et al. () or GPT-4 OpenAI (), 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 of learning-based models:
first, certifying specific, application-dependent safety properties, called
*verification*, and second, interpreting the behaviour of 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 $T$ and (verification or interpretation) specification $\varphi$ outputs
true if $T$ satisfies $\varphi$ (soundness) and for every given pair $T,\varphi$ where $T$ satisfies
$\varphi$ algorithm $A$ outputs true (completeness).
We refer to such sound and complete methods and tasks for verification and interpretation collectively using the term *formal reasoning*.

We lay out a 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 *satisfiability (Sat) problem* of
sequence-classifying transformers:
given a transformer $T$, decide whether there is some input word $w$ such that $T(w)=1$, which
can be interpreted as *$T$ accepts $w$*.
Although this may seem like an artificial problem at first glance, it is a natural abstraction of
problems that commonly occur in almost all non-trivial formal reasoning tasks. Additionally,
since it is detached from the specifics of particular reasoning specifications like safety
properties for instance, uncomputability results and complexity-theoretic hardness results immediately
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),
mainly due to the fact that the known high expressive power of encoder-decoder transformers Pérez et al. () makes formal reasoning trivially impossible.

Our work is structured as follows. We define necessary preliminaries in Section 2.
In Section 3, we give an overview on our complexity results and take a
comprehensive look at their implications for formal reasoning for transformers.
In Section 4 and Section 5 we present our theoretical results:
we show that Sat is undecidable for classes of TE commonly considered
in research on transformer expressiveness, we show that a bounded version bSat of the satisfiability problem
is decidable, for any class of (computable) TE, and give corresponding complexity bounds
and we show that considering quantized TE, meaning TE
whose parameters and internal computations are limited by some fixed-width arithmetic,
leads to decidability of Sat 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 transformers*
and *transformer expressiveness*.

There is a limited amount of work concerned with methods for the verification of safety properties of transformers
Hsieh et al. (); Shi et al. (); Bonaert et al. (); Dong et al. ().
However, 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 applied 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 encoder-decoder models
and showed that such models are Turing-complete Pérez et al. (); Bhattamishra et al. (). Encoder-only models have
so far been analysed in connection with circuit complexity Hahn (); Hao et al. (); Merrill et al. (); Merrill & Sabharwal (),
logics Chiang et al. (); Merrill & Sabharwal () and programming languages Weiss et al. (). A recently published survey Strobl et al. ()
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 proofs are similar.

## 2 Fundamentals

#### Mathematical basics.

Let $\Sigma$ be a finite set of symbols, called *alphabet*. A *(finite) word $w$ over $\Sigma$* is a finite sequence
$a_{1}\dotsb a_{k}$ where $a_{i}\in\Sigma$. We define $|w|=k$.
As usual, we denote the set of all non-empty words by $\Sigma^{+}$. A *language* is a set of words.
We also extend the notion of an alphabet to vectors $\bm{x}_{i}\in\mathbb{R}^{d}$, meaning that a sequence $\bm{x}_{1}\dotsb\bm{x}_{k}$
is a word over some subset of $\mathbb{R}^{d}$.
Usually, we denote vectors using bold symbols like $\bm{x},\bm{y}$ or $\bm{z}$.

#### Transformer encoders (TE).

We consider the transformer encoders (TE), based on the transformer architecture originally introduced in Vaswani et al. ().
We take a look at TE from a computability and complexity perspective, making a formal definition of the considered architecture necessary.
Thereby, we follow the lines of works concerned with formal aspects of transformers like Hahn (); Pérez et al. (); Hao et al. (). From a syntax point of view,
our definition is most near to Hao et al. ().(^1^11As 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. () for an overview of different notions of TE). The definition we use here is sufficiently general and provides a parameterized template for the classes of TE considered in our main results.)

An *TE $T$ with $L$ layers and $h_{i}$ attention heads in layer $i$* is a tuple
$(\mathit{emb},\{\mathit{att}_{i,j}\mid 1\leq i\leq L,1\leq j\leq h_{i}\},\{
\mathit{comb}_{i}\mid 1\leq i\leq L\},\mathit{out})$ where

- •
$\mathit{emb}\colon\Sigma\times\mathbb{N}\rightarrow\mathbb{R}^{d_{0}}$ for some $d_{0}\in\mathbb{N}$ is the *positional embedding*,
- •
each *attention head* is a tuple $\mathit{att}_{i,j}=(\mathit{score}_{i,j},\mathit{pool}_{i,j})$ where
$\mathit{score}_{i,j}\colon\mathbb{R}^{d_{i-1}}\times\mathbb{R}^{d_{i-1}}
\rightarrow\mathbb{R}$ is a function called *scoring* and
$\mathit{pool}_{i,j}\colon(\mathbb{R}^{d_{i-1}})^{+}\times\mathbb{R}^{+}
\rightarrow\mathbb{R}^{d_{i}}$ is a function called *pooling*,
computing $(\bm{x}_{1},\dotsc,\bm{x}_{n},s_{1},\dotsc,s_{n})\mapsto\sum_{i^{\prime}=1}^{n
}\mathit{norm}(i^{\prime},s_{1},\dotsc,s_{n})(W\bm{x}_{i^{\prime}})$
where $W$ is a linear map represented by a matrix and $\mathit{norm}\colon\mathbb{N}\times\mathbb{R}^{+}\rightarrow\mathbb{R}$
is a *normalisation*,
- •
each $\mathit{comb}_{i}\colon\mathbb{R}^{d_{i,1}}\times\dotsb\times\mathbb{R}^{d_{i,
h_{1}+1}}\rightarrow\mathbb{R}^{d_{i}}$ is called a *combination*
and $\mathit{out}\colon\mathbb{R}^{d_{L}}\rightarrow\mathbb{R}$ is called the *output*.

For given $i\leq k$ we call the tuple $(\mathit{att}_{i,1},\dotsc,\mathit{att}_{i,h_{i}},\mathit{comb}_{i})$ the *$i$-th layer* of $T$. The TE
$T$ computes a function $\Sigma^{+}\rightarrow\mathbb{R}$ as follows, also schematically depicted in Figure 1.
Let $w=a_{1},\dotsc,a_{n}\in\Sigma^{+}$ be a word. First, $T$ computes an embedding of $w$ by
$\mathit{emb}(w)=\bm{x}_{1}^{0}\dotsb\bm{x}_{n}^{0}$ where $\bm{x}^{0}_{i}=\mathit{emb}(a_{i},i)$.
Next, each layer $1\leq i\leq L$ computes a sequence $\bm{x}_{1}^{i}\dotsb\bm{x}_{n}^{i}$ as follows:
for each input $\bm{x}_{m}^{i-1}$ and attention head $\mathit{att}_{i,j}$,
layer $i$ computes $\bm{y}_{m,j}^{i}=\mathit{pool}_{i,j}(\bm{x}_{1}^{i-1},\dotsc,\bm{x}_{n}^{i-1},
\mathit{score}_{i,j}(\bm{x}_{m}^{i-1},\bm{x}_{1}^{i-1}),\dotsc,\mathit{score}_
{i,j}(\bm{x}_{m}^{i-1},\bm{x}_{n}^{i-1}))$.
Then, $\bm{x}^{i}_{m}$ is given by $\mathit{comb}_{i}(\bm{x}^{i-1}_{m},\bm{y}_{m,1}^{i},\dotsc,\bm{y}_{m,h_{i}}^{i})$. In the end, the output
$T(w)$ is computed by $\mathit{out}(\bm{x}^{k}_{n})$, 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$ if $T(w)=1$, and we say that $T$ *rejects* $w$ otherwise.
We call $L$ the *depth* of $T$ and the maximal $h_{i}$ the *(maximum) width* of $T$. Furthermore,
we call the maximal $d_{i}$ the *(maximum) dimensionality* of $T$.
Let $\mathcal{T},\mathcal{T}^{\prime}$ be some classes of TE. We sometimes say that *$\mathcal{T}^{\prime}$ is at least as expressive as
$\mathcal{T}$* or *$\mathcal{T}$ is at most as expressive as
$\mathcal{T}^{\prime}$*, meaning that for each $T\in\mathcal{T}$ there is $T^{\prime}\in\mathcal{T}^{\prime}$ such that $T$ and $T^{\prime}$ compute
the same function.
The decision problem $\textsc{Sat}[\mathcal{T}]$ is given $T\in\mathcal{T}$ over alphabet $\Sigma$, decide whether there is $w\in\Sigma^{+}$ such that $T(w)=1$. We refer to this as the *satisfiability problem* of $\mathcal{T}$.

Figure: Figure 1: Schematic depiction of an TE $T$ with embedding $\mathit{emb}$ and $k$ (encoder) layers $l_{i}$. Each layer $l_{i}$ consists of some $h_{i}$ attention heads $\mathit{att}_{i,j}$, whose output is combined by $\mathit{comb}_{i}$. Additionally, for some layer $l_{i}$, the computational flow of $T$ regarding input position $m$ is schematically depicted in detail.

#### Fixed-width arithmetics.

We consider commonly used *fixed-width arithmetics (FA)* that represent
numbers using a fixed amount of bits, like floating- or fixed-point arithmetic in this work. See
Baranowski et al. () (fixed-point) or Constantinides et al. () (floating-point) for
rigorous mathematical definitions 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\in\mathbb{N}$ bits for representing its numbers.
Thus, there are
$2^{b}$ different rational number representable 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 Pérez et al. ()
that almost all formal reasoning problems are easily seen to be undecidable. The secondary reason for this is 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 a 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 $T(w)$, as defined formally in terms
of the *satisfiability problem $\textsc{Sat}[\mathcal{T}]$* for a class $\mathcal{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 a 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 a value from a set $V$. Such tasks are important to ensure syntactic
correctness or adherence to some protocol specification. Formally, this is called a robustness property Shi et al. (); Huang et al. (). We can phrase this example task as a
satisfiability problem by considering the property’s negation, namely, to verify that there exists some input $w$
in which a key from $K$ is not properly followed by a value from $V$, yet we have $T(w)=1$.

Similarly, consider a formal interpretation task where we aim to find the minimal subset $E^{\prime}\subseteq E$
of some set of error symbols $E$ such that all inputs $w$ containing all errors in $E^{\prime}$ are rejected by $T$. For
instance, in a spam detection system powered by a transformer encoder, $E$ could represent a 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 as spam. This is understood as an abductive
explanation in formal explainable AI Marques-Silva & Ignatiev (). Given a candidate subset $E^{\prime}$, we can certify this by checking that there is some $w$
which contains all errors $E^{\prime}$, but is accepted by $T$. This scenario is a special case of the satisfiability
problem $\textsc{Sat}[\mathcal{T}]$ for some transformer class $\mathcal{T}$.

### Overview of results on the complexity of transformer encoder satisfiability

We start by considering the class $\mathcal{T}_{\mathit{udec}}$ of TE, motivated by commonly considered
architectures in the theoretical expressiveness community Pérez et al. (); Hao et al. (); Hahn (): $\mathcal{T}_{\mathit{udec}}$ consists of
those TE that use a positional embedding, expressive enough to compute a sum, hardmax $\mathrm{hardmax}$ as normalisation functions
and a scalar-product based scoring, enriched with a nonlinear map represented by an FNN.

###### Theorem 1 (Section 4 ) .

The satisfiability problem $\textsc{Sat}[\mathcal{T}_{\mathit{udec}}]$ is undecidable.

Figure: Figure 2: Schematic overview of the computability and complexity results, established in this work. The classes of TE are described in the pretext of the respective theorem. Note that $\mathcal{T}$ refers to an arbitrary class of (computable) TE. The small subset in the classes NP and NEXPTIME refers to the complete problems. The NEXPTIME-hardness result of $\textsc{Sat}[\mathcal{T}^{\textsc{fix}}]$ is visualized by putting it exactly on the upper border between NEXPTIME and all decidable problems.
Refer to caption: extracted/5922055/assets/overview.png

Essentially, this result implies that even for TE the combination of $\mathrm{hardmax}$ normalizations and
expressive scoring is enough to make satisfiability undecidable. Generally, this makes formal reasoning,
like verifying robustness properties or giving formal explanations, impossible for classes of TE that subsume $\mathcal{T}_{\mathit{udec}}$.
Specifically, no such methods exist that are fully automatic, sound and complete. Theorem 1
does not preclude the existence of incomplete methods for instance.

Recently, so-called *log-precision transformers* have been studied Merrill & Sabharwal ().
These transformers are defined as usual, but given a word length $n$ it is assumed that
a log-precision transformer $T$ uses at most $\mathcal{O}(\log(n))$ bits in its internal
computations. To complement these theoretical considerations, we consider the class
$\mathcal{T}^{\textsc{log}}_{\mathit{udec}}$ of TE from $\mathcal{T}_{\mathit{udec}}$ that work with log-precision. Unfortunately,
this restriction is not enough to circumvent general undecidability.

###### Theorem 2 (Section 4 ) .

The satisfiability problem $\textsc{Sat}[\mathcal{T}^{\textsc{log}}_{\mathit{udec}}]$ is undecidable.

Given such impossibility results, we turn our 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 are computable functions.

First, we consider a 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 is difficult from a
complexity-theoretic perspective. To formalize this, we introduce the *bounded satisfiability problem*
$\textsc{bSat}[\mathcal{T}]$ for a class $\mathcal{T}$: given an TE $T\in\mathcal{T}$ and a bound $n\in\mathbb{N}$
on its input length, decide whether there is word $w$ with $|w|\leq n$ s.t. $T(w)=1$.

###### Theorem 3 (Section 5 , informal) .

The bounded satisfiability problem $\textsc{bSat}[\mathcal{T}]$ is decidable for all classes $\mathcal{T}$ of (computable) TE.
Depending on whether $n$ is given in binary or unary coding, $\textsc{bSat}[\mathcal{T}]$ is NEXPTIME-, resp. NP-hard whenever
$\mathcal{T}\supseteq\mathcal{T}_{\mathit{udec}}$.

Informally, this result implies that bounding the word length is a method to enable formal reasoning. However, it does not
change the fact that satisfiability is an essentially hard problem. As hardness
is a 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 satisfiability
problem for practically motivated classes of TE. We consider the class $\mathcal{T}^{\textsc{fix}}_{\circ}$ of TE that use a positional
embedding with some periodicity in their positional encoding,
commonly seen in practice Vaswani et al. (); Dufter et al. (), use softmax or hardmax as normalisation
and which work over some fixed-width 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. (). From a complexity-theoretic perspective, the use of fixed-width arithmetic
has a similar effect to bounding the input length.

###### Theorem 4 (Section 5 ) .

The satisfiability problem $\textsc{Sat}[\mathcal{T}^{\textsc{fix}}_{\circ}]$ 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 interpretability
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 $\mathcal{T}^{\textsc{fix}}$ allowing for TE that use non-periodical embeddings and
work over some fixed-width arithmetic that can use saturation to handle overflow situations. We show that this high
complexity is unavoidable, making sound and complete automatic formal reasoning for fixed-width arithmetic transformers
with general positional embeddings practically intractable.

###### Theorem 5 (Section 5 ) .

The satisfiability problem $\textsc{Sat}[\mathcal{T}^{\textsc{fix}}]$ is NEXPTIME-hard.

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.

###### Theorem 1 (Section 4 ) .

###### Theorem 2 (Section 4 ) .

###### Theorem 3 (Section 5 , informal) .

###### Theorem 4 (Section 5 ) .

###### Theorem 5 (Section 5 ) .

## 4 Transformer encoder satisfiability is generally undecidable

We consider a class of TE $\mathcal{T}_{\mathit{udec}}$, which is
as weak as possible regarding the expressiveness of included TE. We define $\mathcal{T}_{\mathit{udec}}$ by giving minimum requirements:
positional-embeddings can be of the form $\mathit{emb}(a_{k},0)=(1,1,0,0,k)$ and
$\mathit{emb}(a_{k},i)=(0,1,i,\sum_{j=0}^{i}j,k)$ where we assume some order on the alphabet symbols
$a_{1},a_{2},\dotsc$. For scoring functions we allow for $N(\langle Q\bm{x},K\bm{y}\rangle)$ where $N$ is a classical Feedforward Neural Network
(FNN) with $\mathit{relu}$ activations, $Q$ and $K$ are linear maps and $\langle\dotsb\rangle$ denotes the usual scalar product,
for normalisations we allow for hardmax $\mathrm{hardmax}(i,x_{1},\dotsc,x_{n})=\frac{1}{m}$ if
$x_{i}\geq x_{j}$ for all $j\leq n$ and there are $m$ distinct $x_{j}$ such that $x_{i}=x_{j}$ otherwise $\mathrm{hardmax}(i,x_{1},\dotsc,x_{n})=0$.
Combinations as well as output functions can be classical FNN with $\mathit{relu}$ activation. Aside from technical reasons,
we motivate the choice of $\mathcal{T}_{\mathit{udec}}$ in Section 3.
To ease our notation, we exploit the fact that using $\mathrm{hardmax}$ as normalisation implies a clearly
defined subset of positions $M$ that are effective in the computation of some attention head $\mathit{att}$
given some position $i$, namely those that are weighted non-zero. In this case, we say that $\mathit{att}$ *attends to $M$ given position $i$*.

Figure: Figure 3: Schematic depiction of the expressive capabilities of TE from $\mathcal{T}_{\mathit{udec}}$ in context of the $\textsc{OTWP}^{*}$ proven in Lemma 1 and Lemma 2.

We prove that $\textsc{Sat}[\mathcal{T}_{\mathit{udec}}]$ is undecidable by establishing a reduction from the *(unbounded) octant tiling-word problem ($\textsc{OTWP}^{*}$)*.
For details on tiling problems, see Appendix A. The $\textsc{OTWP}^{*}$ is defined as follows: given a tiling system $\mathcal{S}=(S,H,V,t_{I},t_{F})$
where $S$ is some finite set of tiles, $H,V\subseteq S^{2}$ and $t_{I},t_{F}\in S$ we have to decide whether there is a word (a)
$t_{0,0},t_{1,0},t_{1,1},t_{2,0},t_{2,1},t_{2,2},t_{3,0},\ldots,$ $t_{k,k}\in S^{+}$ such
that (b) $t_{0,0}=t_{I}$, $t_{k,k}=t_{F}$, (c) for all $i\leq k$ and $0\leq j<i$ holds $(t_{i,j},t_{i,j+1})\in H$ and (d) for all $i\leq k-1$ and $j\leq i$ holds
$(t_{i,j},t_{i+1,j})\in V$. We call a word $w$ which satisfies (a) an *encoded tiling* and if (b)-(d) are satisfied as well then
we call $w$ a *valid* encoded tiling.
Our proof strategy is easily described: given a tiling system $\mathcal{S}$, we build an TE
$T_{\mathcal{S}}\in\mathcal{T}_{\mathit{udec}}$ which accepts a word $w$ if it fulfils conditions (a) to (d) and otherwise $T_{\mathcal{S}}$ rejects $w$.
We derive most technical proofs of the following lemmas and theorems to Appendix B and instead provide intuitions
and proof sketches in this section.

We start with the first observation: the expressiveness of TE in $\mathcal{T}_{\mathit{udec}}$ is sufficient to decode the octant tiling potentially represented by a given word $w$, as depicted by the arrows in Figure 3.
In detail, two encoder layers in combination with a positional embedding definable in $\mathcal{T}_{\mathit{udec}}$ are expressive enough to compute for a given symbol $t$ in $w$ to which position in an octant tiling it corresponds, if we interpret $w$ as an encoded tiling.

###### Lemma 1 .

Let $\mathcal{S}$ be a tiling system with tiles $S=\{a_{1},\dotsc,a_{k}\}$.
There is an embedding function $\mathit{emb}$ and there are encoder layers
$l_{1}$ and $l_{2}$ definable in $\mathcal{T}_{\mathit{udec}}$ such that for each
word $w=t_{0,0}t_{1,0}t_{1,1}t_{2,0}\dotsb t_{m,n}\in S^{+}$ holds that
$l_{2}(l_{1}(\mathit{emb}(w)))=\bm{x}^{2}_{1}\dotsc\bm{x}^{2}_{|w|}$ where $\bm{x}^{2}_{i}=(1,i,r(i),c(i),k_{i})$ such that
$a_{k_{i}}$ is equal to the symbol at position $i$ in $w$ and
$(r(1),c(1)),(r(2),c(2)),\dotsc,(r(|w|),c(|w|))$ is equal to $(0,0),(1,0)\dotsc,(m,n)$.

Assume that $w\in S^{+}$. Lemma 1 implies that a
TE $T\in\mathcal{T}_{\mathit{udec}}$ is generally able to recognize whether $w$ is an encoded tiling
as soon as $T$ is able to check whether $r(|w|)$ and $c(|w|)$ of the last symbol of $w$ processed by $l_{2}(l_{1}(\mathit{emb}(\dotsb)))$ are equal.
Therefore, property (a) and also (b) can be checked by TE in $\mathcal{T}_{\mathit{udec}}$ using the residual connection in the combination
functions together with the expressive power of FNN.

Property (c) can be ensured if it is possible to build an attention head that is able to attend to position $k+1$ given
position $k$. Let $w=t_{0,0}t_{1,0}t_{1,1}t_{2,0}\dotsb t_{m,m}$
with $t_{i,j}\in S$. To verify whether property (d) holds, a TE must be able to attend
to position $k+(i+1)$ given position $k$ corresponding to symbol $t_{i,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 to argue that there are attention heads in $\mathcal{T}_{\mathit{udec}}$ that can attend to positions
depending linearly on the values of the currently considered position.

###### Lemma 2 .

Let $f(x_{1},\dotsc,x_{k})=a_{1}x_{1}+\dotsb+a_{k}x_{k}+b$ with $a_{i},b\in\mathbb{R}$ be some linear function.
There is attention head $\mathit{att}_{f}$ in $\mathcal{T}_{\mathit{udec}}$
such that for all sequences $\bm{x}_{1},\dotsc,\bm{x}_{m}$ where all $\bm{x}_{i}=(1,i,\bm{y}_{i})$ for some $\bm{y}_{i}\in\mathbb{R}^{k-2}$
attention head $\mathit{att}_{f}$ attends to $\{\bm{x}_{j},\bm{x}_{j+1}\}$ given position $i$ if $f(\bm{x}_{i})=j+\frac{1}{2}$ with $j\leq m-1$
and otherwise to $\{\bm{x}_{j}\}$ where $j$ is the value nearest to $f(\bm{x}_{i})$.

In combination, the previous lemmas indicate that TE from $\mathcal{T}_{\mathit{udec}}$ are able to verify whether a given word is a valid encoded tiling.
This expressive power is enough, to lead to an undecidable satisfiability problem for TE from $\mathcal{T}_{\mathit{udec}}$.

###### Theorem 1 .

The decision problem $\textsc{Sat}[\mathcal{T}_{\mathit{udec}}]$ is undecidable.

###### Proof Sketch.

We establish a reduction from $\textsc{OTWP}^{*}$ to $\textsc{Sat}[\mathcal{T}_{\mathit{udec}}]$ by constructing
for each instance $\mathcal{S}=(S,H,V,t_{I},t_{F})$ of $\textsc{OTWP}^{*}$ an TE $T_{\mathcal{S}}$ accepting
exactly those $w$ corresponding to a valid encoded-tiling for $\mathcal{S}$.

$T_{\mathcal{S}}$ uses the positional embedding described in the beginning of Section 4 and has four layers. Layers $l_{1}$ and $l_{2}$ are given by Lemma 1 and are used to decode the row and column
indexes corresponding to a potential octant tiling for each symbol in a given word $w$.
Layer $l_{3}$ uses the informations encoded by the embedding and the decoded
row and column indexes to check whether properties (a) to (d) described above hold
for $w$. The necessary informations are aggregated using three attention heads
$\mathit{att}_{\mathit{prev}}$, $\mathit{att}_{\mathit{next}}$ and $\mathit{att}_{\mathit{step}}$, each built
according to Lemma 2.Thereby, $\mathit{att}_{\mathit{prev}}$ 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 $t_{I}$.
Attention head $\mathit{att}_{\mathit{next}}$ attends each position to 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 to $t_{F}$, and to check conditions
given by $H$. Attention head $\mathit{att}_{\mathit{step}}$ attends each position to the position
with the same column index but the successive row index. If there is no such successive row it attends to the last position. This allows to check whether conditions given by $V$
holds. Each of these conditions is checked in the combination function of $l_{3}$, using
specifically built feed-forward neural networks outputting 0 0 to some predefined vector dimension if and only if the condition is met. Finally, layer $l_{4}$ aggregates the information
of all positions in the vector corresponding to the last position using attention head $\mathit{att}_{\text{leq}}$, again given by Lemma 2.

The correctness of this reduction follows from the detailed construction of $T_{\mathcal{S}}$, which is technically extensive and given in Appendix B.
∎

Next, we consider the class $\mathcal{T}^{\textsc{log}}_{\mathit{udec}}$ which is defined exactly like $\mathcal{T}_{\mathit{udec}}$
but for all $T\in\mathcal{T}^{\textsc{log}}_{\mathit{udec}}$ working over alphabet $\Sigma$ and all words
$w$ with $|w|=n$ we assume that $T(w)$ is carried out in some fixed-width arithmetic
$F$ using $\mathcal{O}(\log(\max(|\Sigma|,n)))$ bits.

###### Theorem 2 .

The decision problem $\textsc{Sat}[\mathcal{T}^{\textsc{log}}_{\mathit{udec}}]$ is undecidable.

###### Proof sketch.

This proof follows the exact same line as the proof of Theorem 1.
Additionally, we need to argue that $T_{\mathcal{S}}$ works as intended, despite
the fact that it is limited by some log-precision $F$.

Looking at the proof of Theorem 1, it is imminent
that the magnitude and precision of all values used and produced in the computation $T_{\mathcal{S}}(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 $T_{\mathcal{S}}$ works as intended. A formal proof is given in Appendix B.
∎

###### Lemma 1 .

###### Lemma 2 .

###### Theorem 1 .

###### Proof Sketch.

###### Theorem 2 .

###### Proof sketch.

## 5 How to make transformer encoder satisfiability decidable

In this section we investigate classes of TE leading to decidable Sat problems or decidable restrictions of it.
Additionally, we establish corresponding complexity bounds.

In order to establish clearly delineated upper complexity bounds, we need to bound the
representation size of a 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 $T$
with $L$ layers and $h_{i}$ attention heads in layer $i$, working on inputs over alphabet $\Sigma$, is $|T|:=|\Sigma|+L+H+D$ where
$H:=\max\{h_{i}\mid 1\leq i\leq L\}$ and $D$ is the maximal dimensionality of vectors occurring in a computation of $T$. Note that one
can reasonably assume the *size* of a syntactic representation of $T$ to be polynomial in $|T|$, and that TE have the
*polynomial evaluation property*: given a word $w\in\Sigma^{+}$, $T(w)$ can be computed in time that is polynomial in $|T|+|w|$.
Section 3 discusses why this assumption is reasonable.

We start with a natural restriction: bounding the word length. Let $\mathcal{T}$ be a class of TE. The *bounded satisfiability problem*, denoted by $\textsc{bSat}[\mathcal{T}]$ is: given $T\in\mathcal{T}$
and some $n\in\mathbb{N}$, decide whether there is a word $w$ with $|w|\leq n$ such that $T(w)=1$. It is not hard
to see that $\textsc{bSat}[\mathcal{T}]$ is decidable. However, its complexity depends on the value of $n$, and we therefore
distinguish whether $n$ is represented in *binary* or *unary* encoding. We denote the corresponding problems as
$\textsc{bSat}_{\mathsf{bin}}[\mathcal{T}]$ and $\textsc{bSat}_{\mathsf{un}}[\mathcal{T}]$.

###### Theorem 3 .

Let $\mathcal{T}$ be a class of TE. Then

- 1.
$\textsc{bSat}_{\mathsf{un}}[\mathcal{T}]$ is decidable in NP and if
$\mathcal{T}_{\mathit{udec}}\subseteq\mathcal{T}$ then $\textsc{bSat}_{\mathsf{un}}[\mathcal{T}]$ is NP-complete,
- 2.
$\textsc{bSat}_{\mathsf{bin}}[\mathcal{T}]$ is decidable in NEXPTIME and
if $\mathcal{T}_{\mathit{udec}}\subseteq\mathcal{T}$ then $\textsc{bSat}_{\mathsf{bin}}[\mathcal{T}]$ is NEXPTIME-complete.

###### Proof Sketch.

The decidability result of statement (1) can be shown using a simple guess-and-check argument: given $n\in\mathbb{N}$,
guess a word $w\in\Sigma^{+}$ with $|w|\leq n$, compute $T(w)$ and check that the result is $1$. This is possible in time polynomial
in $|T|+n$ using the polynomial evaluation property. 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 input is of size $\log n$, and $|T|+n$ becomes exponential in this. Hence, the guess-and-check procedure only proves
that $\textsc{bSat}_{\mathsf{bin}}[\mathcal{T}]\in$ NEXPTIME.

For the completeness result in (1)
it suffices to argue that the problem is NP-hard. We make use of the fact that TE in $\mathcal{T}_{\mathit{udec}}$
are expressive enough to accept a given word $w$ if and only if it is a valid encoded tiling, cf. Section 4 for details.
It is possible to establish NP-hardness of a corresponding 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 then only remains to observe that the construction
in Theorem 1 is in fact a polynomial-time reduction, and that it reduces the bounded octant word-tiling
problem to the bounded satisfiability problem. The argument for NEXPTIME-hardness in statement (2)
is done along the same lines with, again, the bounded octant-word tiling problem shown to be NEXPTIME-hard when the input parameter $n$
is given in binary coding.
A formal proof for Theorem 3 is given in Appendix C.
∎

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-point numbers, and which have an embedding relying on a periodical encoding of positions.

We start with establishing a scenario where Sat is decidable in NEXPTIME. Regardless of the underlying TE class $\mathcal{T}$,
our proof strategy always relies on a certifier-based understanding of NEXPTIME: given $T\in\mathcal{T}$, we nondeterministically
guess a word $w$, followed by a deterministic certification whether $T(w)=1$ holds. For this to show $\textsc{Sat}[\mathcal{T}]\in\text{NEXPTIME}$,
we need to argue that the overall running time of such a procedure is at most exponential, in particular that whenever there is a
word $w$ with $T(w)=1$ then there is also some $w^{\prime}$ with $T(w^{\prime})=1$ and $|w^{\prime}|\leq 2^{\mathit{poly}(|T|)}$. Again, we rely on the polynomial
evaluation property of TE in $\mathcal{T}$, i.e. the fact that $T(w^{\prime})$ can be computed in time polynomial in $|T|+|w^{\prime}|$.

We consider the class of TE $\mathcal{T}^{\textsc{fix}}_{\circ}$, defined by placing restrictions on the positional embedding of an TE
$T$ to be *additive-periodical* which means that $\mathit{emb}(a,i)=\mathit{emb}^{\prime}(a)+\mathit{pos}(i)$ where $\mathit{pos}$ is periodical, i.e. there is
$p\geq 1$ such that $\mathit{pos}(i)=\mathit{pos}(i+p)$ for all $i\in\mathbb{N}$. Additionally, all normalisation functions are realised by
either the softmax function $\mathrm{softmax}$ or the hardmax function $\mathrm{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\in\mathbb{N}$ of bits.
Aside from technical reasons, we motivate the choice of $\mathcal{T}^{\textsc{fix}}_{\circ}$ in Section 3. Given these restrictions,
we adjust the definition of the complexity of $T\in\mathcal{T}^{\textsc{fix}}_{\circ}$ as a measure of the size (up to polynomials) as
$|T|:=|\Sigma|+L+H+D+p+b$.

###### Lemma 3 .

There is a polynomial function $\mathit{poly}\colon\mathbb{N}\to\mathbb{N}$ such that for all $T\in\mathcal{T}^{\textsc{fix}}_{\circ}$ and all words $w$ with $T(w)=1$ there
is word $w^{\prime}$ with $T(w^{\prime})=1$ and $|w^{\prime}|\leq 2^{\mathit{poly}(|T|)}$.

###### Proof Sketch.

The polynomial $\mathit{poly}$ can be chosen uniformly for all $T\in\mathcal{T}^{\textsc{fix}}_{\circ}$ because
for all positional embeddings of TE in $\mathcal{T}^{\textsc{fix}}_{\circ}$ 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 $\mathit{poly}$, TE $T$ and $|w|>2^{\mathit{poly}(|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 a multitude of $p$. This ensures that the resulting word
$w^{\prime}$, 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 $T$’s limited distinguishing capabilities,
especially in its normalisations, due to the bounded representation size of numerical values
possible in the underlying fixed-width arithmetic.

A formal proof relies
on basic combinatorial arguments, but is technically extensive, and given in Appendix C.
∎

Based on this preliminary result, we can then immediately derive an upper bound on the complexity of $\textsc{Sat}[\mathcal{T}^{\textsc{fix}}_{\circ}]$.

###### Theorem 4 .

The satisfiability problem $\textsc{Sat}[\mathcal{T}^{\textsc{fix}}_{\circ}]$ for TE over fixed-width arithmetic
using additive-periodical embeddings is in NEXPTIME.

###### Proof.

Let $T\in\mathcal{T}^{\textsc{fix}}_{\circ}$ working over alphabet $\Sigma$.
We use a certifier-based understanding of a nondeterministic exponential-time algorithm as follows:
We (a) guess an input $w\in\Sigma^{+}$ 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|$ and $T(w)=1$ obviously as well.
∎

Next, we address the goal of obtaining a matching lower bound, i.e. NEXPTIME-hardness. An obvious way to do so would be to follow
Theorem 3.2 and form a reduction from the
bounded octant word-tiling problem.
Hence, given a tiling system $\mathcal{S}$ and $n\in\mathbb{N}$ encoded binarily, we would have to construct – in time
polynomial in $|\mathcal{S}|+\log n$ – an TE $T_{\mathcal{S},n}\in\mathcal{T}^{\textsc{fix}}_{\circ}$ such that $T_{\mathcal{S},n}(w)=1$
for some $w\in\Sigma^{+}$ iff there is a word $w=t_{1,1},t_{2,1},t_{2,2},t_{3,1},\ldots,t_{n,n}$ representing a valid
$\mathcal{S}$-tiling. In particular, $T_{\mathcal{S},n}$ would have to be able to recognise the correct word length and
reject input that is longer than $|w|=\frac{n(n+1)}{2}$.
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 a periodicity of $p\geq\frac{n(n+1)}{2}$ necessary.
Since the size of periodical TE is linear in $p$, we get an exponential blow-up in a potential reduction
of $\textsc{OTWP}_{\mathsf{bin}}$ to $\textsc{Sat}[\mathcal{T}^{\textsc{fix}}_{\circ}]$, given that the values of $\frac{n(n+1)}{2}$ and already $n$ 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 non-periodical TE, working over some fixed-width arithmetic, leads
to an NEXPTIME-hard satisfiability problem. Let $\mathcal{T}^{\textsc{fix}}$ be defined similar to $\mathcal{T}^{\textsc{fix}}_{\circ}$, but we allow for
non-periodical embeddings. Furthermore, we assume that the considered fixed-width arithmetics can handle overflow situations
using saturation.

###### Theorem 5 .

The satisfiability problem $\textsc{Sat}[\mathcal{T}^{\textsc{fix}}]$ for TE over fixed-width arithmetic is NEXPTIME-hard.

###### Proof sketch.

We establish a reduction from $\textsc{OTP}_{\mathsf{bin}}$ to $\textsc{Sat}[\mathcal{T}^{\textsc{fix}}]$ by
constructing, for each instance $(\mathcal{S},n)$ of $\textsc{OTP}_{\mathsf{bin}}$, an TE
$T_{\mathcal{S},n}$ working over some fixed-width arithmetic $F$, which accepts exactly those
$w$ with $|w|=\frac{n(n+1)}{2}$ corresponding to a valid word-encoded tiling for $\mathcal{S}$.
See Appendix A for details on tiling problems.

The construction is similar to the one given for $T_{\mathcal{S}}$ in the proof of
Theorem 4, but we need to enable $T_{\mathcal{S},n}$ to reject words
that are too long corresponding a polynomial bound dependent on $n$.
This implies that $T_{\mathcal{S},n}$, based on the positional embedding $\mathit{emb}$
specified in Section 4, is able to check for all symbols if their respective
position is less than or equal to a predefined bound. This can be achieved with similar tools as used in Lemma 2.

Furthermore, we need to ensure that $T_{\mathcal{S},n}$ works as intended, despite the
fact that it is limited by $F$. The arguments follow the same line as the proof of Theorem 2.
A formal proof is given in Appendix C.
∎

###### Theorem 3 .

###### Proof Sketch.

###### Lemma 3 .

###### Proof Sketch.

###### Theorem 4 .

###### Proof.

###### Theorem 5 .

###### Proof sketch.

## 6 Summary, limitations and outlook

We investigated the satisfiability problem of transformer encoders (TE) through the lens of
formal reasoning. In particular, we considered the computability and complexity of the satisfiability problem Sat
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 Sat is undecidable for classes of TE recently considered in research on the expressiveness of different
transformer models (Theorem 1 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. We remark that this result also translates to encoder-decoder architectures, whose
encoder part is as expressive as the here considered TE.

Additionally, we identified two ways to enable formal reasoning for TE: by bounding the length of inputs
(Theorem 3) or by considering quantized TE, where computations and
parameters are limited by fixed-width arithmetic (Theorem 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, Sat remains
computationally difficult (Theorems 3
and 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 normalizations 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 change our
overall results, it could provide tighter time-complexity estimates valuable for certain formal reasoning
applications.

## Appendix A Tiling Problems

We make use of particular tiling problems in order to prove lower bounds on the complexity
and decidability of $\textsc{Sat}[\mathcal{T}]$ for different classes $\mathcal{T}$.

A *tiling system* is an $\mathcal{S}=(S,H,V,t_{I},t_{F})$ where $S$ is a finite set; its elements
are called *tiles*. $H,V\subseteq S\times S$ define a horizontal, resp. vertical
matching relation between tiles, and $t_{I},t_{F}$ are two designated *initial*, resp. *final* tiles in $S$.

Problems associated with tiling systems are typically of the following form: given a discrete convex plain
consisting of cells with horizontal and vertical neighbors, is it possible to cover the plane with tiles
from $S$ in a 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 $t_{I},t_{F}$. Such tiling problems, in particular for rectangular planes, have proved to be
extremely useful in computational complexity, cf. Berger (); van Emde Boas (), since they can be seen as
abstract versions of halting problems.

We need a variant in which the plane to be tiled is of triangular shape. The *$n$-th triangle* is
$\mathcal{O}_{n}=\{(i,j)\in\mathbb{N}\times\mathbb{N}\mid j\leq i\leq n\}$ for $n>0$. An
($\mathcal{S}$)-*tiling* of $\mathcal{O}_{n}$ is a function $\tau:\mathcal{O}_{n}\to S$ s.t.

- •
$(\tau(i,j),\tau(i,j+1))\in H$ for all $(i,j)\in\mathcal{O}$ with $j<i\leq n$,
- •
$(\tau(i,j),\tau(i+1,j))\in V$ for all $(i,j)\in\mathcal{O}$ with $j\leq i<n$.

Such a tiling a *successful*, if additionally $\tau(0,0)=t_{I}$ and $\tau(i,i)=t_{F}$
for some $(i,i)\in\mathcal{O}_{n}$.

The *unbounded octant tiling problem* ($\textsc{OTP}^{*}$) is: given a tiling system $\mathcal{S}$, decide whether a
successful $\mathcal{S}$-tiling of $\mathcal{O}_{n}$ exists for some $n\in\mathbb{N}$.
The *bounded octant tiling problem* (OTP) is: given a tiling system $\mathcal{S}$ and an
$n\geq 1$, decide whether a successful $\mathcal{S}$-tiling of $\mathcal{O}_{n}$
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 $\textsc{OTP}_{\mathsf{bin}}$ and
$\textsc{OTP}_{\mathsf{un}}$.

It is well-known that $\textsc{OTP}^{*}$ is undecidable van Emde Boas (). It is also not hard to imagine
that $\textsc{OTP}_{\mathsf{un}}$ is NP-complete while $\textsc{OTP}_{\mathsf{un}}$ is NEXPTIME-complete. 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 (). The exponential difference incurred by the more compact
binary representation of the input parameter $n$ is best seen when regarding the upper complexity
bound for these problems: given $n$, a nondeterministic algorithm can simply guess all the $n^{2}$ many
tiles of the underlying square and verify the horizontal and vertical matchings in time $\mathcal{O}(n^{2})$.
If $n$ is encoded unarily, i.e. the space needed to write it down is $s:=n$, then the time needed for
this is polynomial in the input size $s$; if $n$ is encoded binarily with space $s:=\lceil\log n\rceil$
then the time needed for this is exponential in $s$.

It then remains to argue that the tiling problems based on triangular planes are also NP- resp. NEXPTIME-complete. Clearly, the upper bounds can be established with the same guess-and-check
procedure. For the lower bounds it 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\times 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 $i$ leftmost tape cells. Hence, a run of a TM
can therefore also be represented as a triangle with its first configuration of length 1 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 NEXPTIME-completeness. The *unbounded octant tiling-word problem*
($\textsc{OTWP}^{*}$) is: given some $\mathcal{S}=(S,H,V,t_{I},t_{F})$, decide whether there is a word
$t_{0,0},t_{1,0},t_{1,1},t_{2,0},t_{2,1},t_{2,2},\ldots,$ $t_{n,n}\in S^{*}$ for some $n\in\mathbb{N}$, s.t. the tiling $\tau$ defined by $\tau(i,j):=t_{i,j}$ comprises a successful tiling of $\mathcal{O}_{n}$.
The two variants of the *bounded octant tiling-word problem* are both: given some
$\mathcal{S}$ as above and $n$, decide whether such a word exists. Note that, again, here $n$ is
an input parameter, and so its representation may affect the complexity of the problem, leading
to the distinction between $\textsc{OTWP}_{\mathsf{bin}}$ with binary encoding and $\textsc{OTWP}_{\mathsf{un}}$
with unary encoding.

###### Theorem 6 .

- a)
$\textsc{OTWP}^{*}$ is undecidable ($\Sigma_{0}^{1}$-complete).
- b)
$\textsc{OTWP}_{\mathsf{bin}}$ is NEXPTIME-complete.
- c)
$\textsc{OTWP}_{\mathsf{un}}$ is NP-complete.

###### Proof.

(a) It should be clear that a tiling problem and its tiling-word variant (like $\textsc{OTP}^{*}$ and $\textsc{OTWP}^{*}$) are
interreducible since they only differ in the formulation of how the witness for a successful tiling
should be presented. So they are essentially the same problems. Undecidability of $\textsc{OTP}^{*}$ and, thus,
$\textsc{OTWP}^{*}$ is known from van Emde Boas (), the $\Sigma^{1}_{0}$-upper bound can be obtained through a
semi-decision procedure that searches through the infinite space of $\mathcal{O}_{n}$-tiling for any
$n>1$. This justifies the statement in part (a) of Thm. 6.

(b) With the same argument as in (a) t suffices to consider $\textsc{OTP}_{\mathsf{bin}}$ instead of
$\textsc{OTWP}_{\mathsf{bin}}$. The upper bound is easy to see: a nondeterministic procedure can easily guess a tiling
for $\mathcal{O}_{n}$ 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 $\mathcal{O}(n^{2})$,
resp. $\mathcal{O}(2^{2\log n})$ which is therefore exponential in the input size $\lceil\log n\rceil$
for binarily encoded parameters $n$. This shows inclusion in NEXPTIME.

For the lower bound we argue that the halting problem for nondeterministic, exponentially-time
bounded TM can be reduced to $\textsc{OTP}_{\mathsf{bin}}$: given a nondeterministic TM $\mathcal{M}$ over
input alphabet $\Sigma$ and tape alphabet $\Gamma$ that halts after at most time $2^{p(n)}$ steps
on input words of length $n$ for some polynomial $n$, and a word $w\in\Sigma^{*}$, we first construct
a TM $\mathcal{M}_{w}$ that is started in on the empty tape and begins by writing $w$ onto the tape
and then simulates $\mathcal{M}$ on it. This is a standard construction in complexity theory, and
it is easy to see that the running time of $\mathcal{M}_{w}$ is bounded by a function $2^{p^{\prime}(|w|)}$
for some polynomial $p^{\prime}$. With the observation made above, a computation of $\mathcal{M}_{w}$ can
be seen as a sequence of configurations $C_{1},\ldots,C_{p^{\prime}(|w|)}$, with $|C_{i}|=i$. This does not
directly define a tiling system, instead and again by a standard trick, cf. van Emde Boas () or
(Demri et al., , Chp. 11), one compresses three adjacent tape cells into one tile in order to
naturally derive a horizontal matching relation from overlaps between such triples and a vertical
matching relation from the TM’s transition function. At last, let $n^{\prime}:=p^{\prime}(|w|)$. It is then a
simple exercise to verify that a valid tiling of the triangle $\Delta_{n^{\prime}}$ corresponds to an
accepting run of $\mathcal{M}$ on $w$ and vice-versa, which establishes NEXPTIME-hardness.

(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 NEXPTIME-completeness.
∎

###### Theorem 6 .

###### Proof.

## Appendix B Proofs of Section 4

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 $\mathbb{R}^{m}\rightarrow\mathbb{R}$ by
$v(x_{1},\dotsc,x_{m})=\sigma(b+\sum_{i=1}^{m}w_{i}x_{i})$ where $\sigma$ is a function called *activation*
and $b,w_{i}$ are parameters called *bias* resp. *weight*. A *layer* $l$ is a tuple of nodes $(v_{1},\dotsc,v_{n})$
where we assume that all nodes have the same input dimensionality $m$. Therefore, $l$ computes a function
$\mathbb{R}^{m}\rightarrow\mathbb{R}^{n}$. We call $n$ the *size of layer $l$*.
Let $l_{1}$ be a layer with input dimensionality $m$ and $l_{k}$ a layer of size $n$.
A *Feed-Forward Neural Network (FNN)* $N$ is a tuple $(l_{1},\dotsc,l_{k})$ of layers where we assume that for all $i\leq k-1$
holds that the size of $l_{i}$ equals the input dimensionality of $l_{i+1}$. Therefore, $N$ computes a function $\mathbb{R}^{m}\rightarrow\mathbb{R}^{n}$
by processing an input layer by layer.

In particular, we use specific FNN with $\mathit{relu}(x)=\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 $\mathit{relu}$ activations by $\mathcal{N}(\mathit{relu})$.

###### Lemma 4 .

Let $k\in\mathbb{R}^{>0}$. There are basic gadgets

- 1.
$N_{|\cdot|}\in\mathcal{N}(\mathit{relu})$ computing $N_{|\cdot|}(x)=|x|$,
- 2.
$N_{<}\in\mathcal{N}(\mathit{relu})$ computing a function $\mathbb{R}^{2}\rightarrow\mathbb{R}$ such that
$N_{<}(x_{1},x_{2})=0$ if $(x_{1}+1)-x_{2}\leq 0$, $N_{<}(x_{1},x_{2})=(x_{1}+1)-x_{2}$ if $(x_{1}+1)-x_{2}\in(0;1)$
and $N_{<}(x_{1},x_{2})=1$ otherwise,
- 3.
$N_{=}\in\mathcal{N}(\mathit{relu})$ computing a function $\mathbb{R}^{2}\rightarrow\mathbb{R}$ such that
$N_{=}(x_{1},x_{2})=0$ if $x_{1}-x_{2}=0$, $N_{=}(x_{1},x_{2})=|x_{2}-x_{1}|$ if $|x_{2}-x_{1}|\in(0;1)$
and $N_{=}(x_{1},x_{2})=1$ otherwise,
- 4.
$N_{\rightarrow}\in\mathcal{N}(\mathit{relu})$ computing a function $\mathbb{R}^{2}\rightarrow\mathbb{R}$
such for all inputs $x_{1},x_{2}$ with $x_{1}\in\{0,1\}$ and $x_{2}\in[0;k]$ holds
$N_{\rightarrow}(x_{1},x_{2})=0$ if $x_{1}=x_{2}=0$ or $x_{1}=1$
and $N_{\rightarrow}(x_{1},x_{2})=\mathit{relu}(x_{2})$ otherwise.

###### Proof.

Let $N_{|\cdot|}$ be the minimal FNN computing $\mathit{relu}(\mathit{relu}(-x)+\mathit{relu}(x))$, let
$N_{<}$ be the minimal FNN computing $\mathit{relu}(f_{<}(x_{1},x_{2})-f_{<}(x_{1},x_{2}+1))$ where $f_{<}(y_{1},y_{2})=\mathit{relu}(y_{1}-y_{2}+1)$
and let $N_{=}$ be the minimal FNN computing $\mathit{relu}(f_{=}(x_{1},x_{2})-f_{=}(x_{1}+1,x_{2})+f_{=}(x_{2},x_{1})-f_{=}
(x_{2}+1,x_{1}))$
where $f_{=}(y_{1},y_{2})=\mathit{relu}(y_{2}-y_{1})$. The claims of the lemma regarding these gadgets are straightforward given their functional form.
Let $N_{\rightarrow}$ be the minimal FNN computing $\mathit{relu}(\mathit{relu}(x_{2})-k\cdot\mathit{relu}(x_{1}))$. As stated in the lemma, we assume that $x_{1}\in\{0,1\}$
and $x_{2}\in[0;k]$. Then, $-k\cdot\mathit{relu}(x_{1})$ is $-k$ if $x_{1}=1$ and 0 0 if $x_{1}=0$. Thus, $N_{\rightarrow}$ is guaranteed to be 0 0 if
$x_{1}=1$ and otherwise it depends on $x_{2}$. This gives the claim regarding gadget $N_{\rightarrow}$.
∎

We will combine gadgets in different ways. Let $N_{1}$ and $N_{2}$ be FNN with the same input dimensionality $m$ and output
dimensionality $n_{1}$ respectively $n_{2}$.
We extend the computation of $N_{1}$ to functions $\mathbb{R}^{m^{\prime}}\rightarrow\mathbb{R}^{n_{1}}$
with $m<m^{\prime}$ by weighting additional dimensions with 0 0 in the input layer. Given a set of input dimensions
$x_{1},\dotsc,x_{m^{\prime}}$, we denote the effective dimensions $x_{i_{1}},\dotsc,x_{i_{m}}$ with pairwise
different $i_{j}\in\{1,\dotsc,m^{\prime}\}$ by $N^{x_{i_{1}},\dotsc,x_{i_{m}}}_{1}$. Formally, this means that
$N^{x_{i_{1}},\dotsc,x_{i_{m}}}_{1}(x_{1},\dotsc,x_{m^{\prime}})=N_{1}(x_{i_{1}
},\dotsc,x_{i_{m}})$ for all inputs.
We denote the FNN consisting of $N_{1}$ and $N_{2}$ placed next to each other
by $N_{1}|\!|N_{2}$. Formally, this is done by combining $N_{1}$ and $N_{2}$ layer by layer using 0 0 weights in intersecting connections.
Then, $N_{1}|\!|N_{2}$ computes $\mathbb{R}^{m}\rightarrow\mathbb{R}^{n_{1}+n_{2}}$ given by $N_{1}|\!|N_{2}(\bm{x})=(N_{1}(\bm{x}),N_{2}(\bm{x}))$.
We generalize this operation to $k$ FNN $N_{1}|\!|\dotsb|\!|N_{k}$ in the obvious sense. Let $N_{3}$ be an FNN with input
dimensionality $n_{1}$ and output dimensionality $n_{3}$. We denote the FNN consisting of $N_{1}$ and $N_{3}$ placed sequentially
by $N_{3}\circ N_{1}$. Formally, this is done by connecting the output layer of $N_{1}$ with the input layer of $N_{3}$. Then, $N_{3}\circ N_{1}$
computes $\mathbb{R}^{m}\rightarrow\mathbb{R}^{n_{3}}$ given by $N_{3}\circ N_{1}(\bm{x})=N_{3}(N_{1}(\bm{x}))$.

We also consider specific gadgets needed in the context of tiling problems.

###### Lemma 5 .

Let $S\subseteq\mathbb{N}$ be a finite set and $R\subseteq S^{2}$. There is
FNN $N_{R}\in\mathcal{N}(\mathit{relu})$ computing $\mathbb{R}^{2}\rightarrow\mathbb{R}$ such that $N_{R}(x_{1},x_{2})\in\{0,1\}$
if $(x_{1},x_{2})\in S^{2}$ and $N_{R}(x_{1},x_{2})=0$ iff $(x_{1},x_{2})\in R$ and there is
$N_{=t}\in\mathcal{N}(\mathit{relu})$ for each $t\in S$ computing $\mathbb{R}\rightarrow\mathbb{R}$ such that
$N_{=t}(x)\in\{0,1\}$ for each $x\in\mathbb{N}$ and $N_{=t}(x)=0$ iff $x=t$.

###### Proof.

Let $S\subseteq\mathbb{N}$ be finite, $R\subseteq S^{2}$ and $t\in S$. First, consider
$N_{=t}$. Let $N_{t}$ be the minimal FNN computing $\mathit{relu}(0\cdot x+t)$ and $N_{\mathit{id}}$
be the minimal FNN computing $(\mathit{relu}(x),-\mathit{relu}(-x))$.
Obviously, $N_{t}$ computes the constant $t$ function and
$N_{\mathit{id}}$ computes the identity in the form of two dimensional vectors. Let $N_{=t}$ be given by the minimal FNN computing
$N_{=}\circ(N_{\mathit{id}}|\!|N_{t})$ with the slight alteration that the two output dimensions of $N_{\mathit{id}}$
are connected to the first dimension of $N_{=}$. Then, the claim of the lemma regarding $N_{=t}$ follows from
Lemma 4 and the operations on FNN described in Appendix B.

Now, consider $N_{R}$. Given some $s\in S$ let $R[s]=\{r\mid(s,r)\in R\}$.
Let $N^{k}_{\land}$ be the minimal FNN computing $\mathit{relu}(x_{1}+\dotsb+x_{k})$.
Furthermore, let $N_{\in T}$ for some set $T\subseteq S$ be the minimal FNN such that
$N_{\in T}(x)=0$ if $x\in T$ and $N_{\in T}(x)=1$ if $x\in S\setminus T$. A construction
for $N_{\in T}$ is given in Theorem 4 in Sälzer & Lange (). According to this construction,
$N_{\in T}$ consists of three layers and is polynomial in $T$. In the case that $T=\emptyset$ we assume that
$N_{\in\emptyset}$ is the constant $1$ function represented by a suitable FNN.
Then, $N_{R}$ is given by $N^{|S|}_{\land}\circ((N_{\rightarrow}\circ(N_{=s_{1}}|\!|N_{\in R[s_{1}]}))|\!
|\dotsb|\!|(N_{\rightarrow}\circ(N_{=s_{|S|}}|\!|N_{\in R[s_{|S|}]})))$
for some arbitrary order on $S$ with the slight alteration that $N_{R}$ has two input dimensions, meaning that each subnet $(N_{=s_{i}}|\!|N_{\in R[s_{i}]})$
is connected to the same two input dimensions. Again, the claim of the lemma regarding $N_{R}$ 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.

###### Proof of Lemma 1 .

Let $w=t_{0,0}t_{1,0}t_{1,1}t_{2,0}\dotsb t_{m,n}\in S^{+}$ as stated in the lemma and assume some order $a_{i}$ on $S$.
Furthermore, let $\mathit{emb}(a_{i},1)=(1,1,1,1,i)$ and $\mathit{emb}(a_{i},j)=(0,1,j,\sum_{h=0}^{j}h,i)$ if $j>1$. Let $\mathit{emb}(w)=\bm{x}^{0}_{1}\dotsb\bm{x}^{0}_{k}$.
In the following, we build two layers $l_{1}$ and $l_{2}$ using components allowed in $\mathcal{T}_{\mathit{udec}}$, satisfying
the statement of the lemma.
Layer $l_{1}$ consists of a single attention head $\mathit{att}_{1,1}=(\mathit{score}_{1,1},\mathit{pool}_{1,1})$. The scoring function is given
by $\mathit{score}_{1,1}(\bm{x}^{0}_{i},\bm{x}^{0}_{j})=N_{1,1}(\langle Q_{1,1}\bm
{x}^{0}_{i},K_{1,1}\bm{x}^{0}_{j}\rangle)$ where $Q_{1,1}=[(0,0,-1,0,0),(0,1,0,0,0),(0,1,0,0,0)]$
and $K_{1,1}=[(0,1,0,0,0),(0,1,0,0,0),(0,0,0,1,0)]$ and $N(x)=-\mathit{relu}(x)$.
We have that $\mathit{score}_{1,1}(\bm{x}^{0}_{i},\bm{x}^{0}_{j})=-\mathit{relu}((\sum_{h=0}
^{j}h)-(i-1))$ and it follows that $\mathit{score}_{1,1}(\bm{x}^{0}_{i},\bm{x}^{0}_{j})=0$ if $\sum_{h=0}^{j}h\leq i-1$ and otherwise we have that $\mathit{score}_{1,1}(\bm{x}^{0}_{i},\bm{x}^{0}_{j})<0$. The pooling function is specified by the matrix $W_{1,1}=[(1,0,0,0,0)]$ and uses $\mathrm{hardmax}$ as normalisation function.
The combination $\mathit{comb}_{1}$ function is given by the FNN
$N_{1}(x_{1},\dotsc,x_{5},y)=\mathit{relu}(x_{2})|\!|\dotsb|\!|\mathit{relu}(x_
{5})|\!|\mathit{relu}(y)$.
Given a position $\bm{x}^{0}_{i}$, the attention head $\mathit{att}_{1,1}$ attends to
all positions $\bm{x}^{0}_{j}$ satisfying
$\sum_{h=0}^{j}h\leq i-1$. This is due to the way $\mathit{score}_{1,1}$ is build. Then, $\mathit{att}_{1,1}$ computes $\frac{1}{l}$ using
$\mathit{pool}_{1,1}$ where $l$ is the number of positions $\mathit{att}_{1,1}$ attends to. Here, we exploit the fact that only the first position
$\bm{x}^{0}_{1}$ has a non-zero entry in the its first dimension and that for all $i$ head $\mathit{att}_{1,1}$ attends to $\bm{x}^{0}_{1}$.
Finally, $\mathit{comb}_{1}$ simply stacks the old vector $\bm{x}^{0}_{i}$ onto the value $\frac{1}{l}$, but leaves out the first dimension of $\bm{x}^{0}_{i}$.
Let $l_{1}(\mathit{emb}(w))=\bm{x}^{1}_{1}\dotsb\bm{x}^{1}_{k}$.
Layer $l_{2}$ consists of a single attention head $\mathit{att}_{2,1}=(\mathit{score}_{2,1},\mathit{pool}_{2,1})$. The scoring function
$\mathit{score}_{2,1}$ is given by $N_{2,1}(\langle Q_{2,1}\bm{x}^{1}_{i},K_{2,1}\bm{x}^{1}_{j}\rangle)$ where $Q_{2,1}=[(0,0,0,0,1)]$,
$K_{2,1}=[(0,1,0,0,0)]$ and $N_{2,1}(x)=-\mathit{relu}(\mathit{relu}(x-1)+\mathit{relu}(1-x))$. We have that $\mathit{score}_{2,1}(\bm{x}^{1}_{i},\bm{x}^{1}_{j})=0$ if
$\frac{1}{l}\cdot j=1$ where $\frac{1}{l}$ is the fifth dimension of $\bm{x}^{1}_{i}$ and otherwise $\mathit{score}_{2,1}(\bm{x}^{1}_{i},\bm{x}^{1}_{j})<0$.
The pooling function $\mathit{pool}_{2,1}$ is specified by
$W_{2,1}=[(0,1,0,0,0),(0,0,1,0,0)]$ and
uses $\mathrm{hardmax}$ as normalisation. The combination $\mathit{comb}_{2}$ is given by
the FNN $N_{2}(x_{1},\dotsc,x_{5},y_{1},y_{2})=\mathit{relu}(x_{1})|\!|\mathit{relu}(x_
{2})|\!|\mathit{relu}(y_{1})|\!|\mathit{relu}(x_{2}-y_{2}-1)|\!|\mathit{relu}(
x_{4})$.
Given a position $\bm{x}^{1}_{i}$, the attention head $\mathit{att}_{2,1}$ attends to the position $j$, where $\frac{1}{l}\cdot j=1$. Relying on
our arguments regarding the computation of $l_{1}$, this is the position $j$ satisfying $\max_{j}(\sum_{h=0}^{j}h\leq i-1)$. However, this
$j$ is equal to the row index $r(i)$ of the decomposition of $i$ based on the inversion of Cantor’s pairing function. Thus, we have that $r(i)=j$.
Furthermore, we have that $c(i)=(i-1)-(\sum_{h=0}^{j}h)$, which is computed by $\mathit{relu}(x_{2}-y_{2}-1)$ in the combination function $\mathit{comb}_{2}$.
Overall, we see that $l_{2}(l_{1}(\mathit{emb}(w)))$ gives the desired result.
∎

###### Proof of Lemma 2 .

Let $f$ be as stated in the lemma. By definition of $\mathcal{T}_{\mathit{udec}}$, the scoring function of $\mathit{att}_{f}$ is of the form $N(\langle Q\bm{x}_{i},K\bm{x}_{j}\rangle)$ and the
normalisation is $\mathrm{hardmax}$. Let $Q=[(a_{1},\dotsc,a_{k}),(b,0,\dotsc,0),(1,0,\dotsc,0)]$, $K=[(1,0,\dotsc,0),(1,0,\dotsc,0),(0,-1,0,\dotsc,0)]$ and
$N$ be the minimal FNN computing $N(x)=-\mathit{relu}(N_{|\cdot|}(x))=-|x|$ where $N_{|\cdot|}$ is given by Lemma 4.
Overall, this ensures that the scoring is given by $\mathit{score}(\bm{x}_{i},\bm{x}_{j})=-|f(\bm{x}_{i})-j|$. Then, the statement of the lemma follows from the
fact that $\mathrm{hardmax}$ attends to the maximum, which is 0 0 given this scoring, and that $j\in\mathbb{N}$ is unique for each $\bm{x}_{j}$.
∎

###### Lemma 6 .

There is attention head $\mathit{att}_{\leq}$ in $\mathcal{T}_{\mathit{udec}}$
such that for all sequences $\bm{x}_{1},\dotsc,\bm{x}_{m}$ where all $\bm{x}_{i}=(1,i,\bm{y}_{i})$ the head $\mathit{att}_{\leq}$ attends to $\{\bm{x}_{1},\dotsc,\bm{x}_{i}\}$ given $i$.

###### Proof.

By definition of $\mathcal{T}_{\mathit{udec}}$, the scoring function of $\mathit{att}_{f}$ is of the form $N(\langle Q\bm{x}_{i},K\bm{x}_{j}\rangle)$ and the
normalisation is $\mathrm{hardmax}$. Let $Q=[(0,1,0,\dotsc,0),(1,0,\dotsc,0)]$ and let $K$ be equal to $[(1,0\dotsc,0),(0,-1,0,\dotsc,0)]$.
Furthermore, let
$N(x)=-\mathit{relu}(x)$. We observe that $N$ outputs 0 0 if $j\leq i$ and otherwise $N(x)<0$.
In combination with $\mathrm{hardmax}$, this ensures that $\mathit{att}_{\leq}$ behaves as stated by the lemma.
∎

###### Proof of Theorem 1 .

We prove the statement via reduction from $\textsc{OTWP}^{*}$. Let $\mathcal{S}=(S,H,V,t_{I},t_{F})$
be an instance of $\textsc{OTWP}^{*}$ with $|S|=k$. W.l.o.g we assume that $S\subseteq\mathbb{N}$.
Let $T_{\mathcal{S}}\in\mathcal{T}_{\mathit{udec}}$ be built the following way.
$T_{\mathcal{S}}$ uses the embedding $\mathit{emb}$ of transformer in $\mathcal{T}_{\mathit{udec}}$ specified in the beginning of Section 4.
Furthermore, it has four layers. Layers $l_{1}$, $l_{2}$ are as in Lemma 1. Layer
$l_{3}$ is given by $l_{3}=(\mathit{att}_{\mathit{prev}},\mathit{att}_{\mathit{next}},\mathit{att}_
{\mathit{step}},\mathit{comb}_{3})$
where $\mathit{att}_{\text{prev}}$, $\mathit{att}_{\text{next}}$ and $\mathit{att}_{\text{step}}$ are of
Lemma 2 whereby
$\mathit{prev}(x_{1},\dotsc,x_{5})=x_{2}-1$,
$\mathit{next}(x_{1},\dotsc,x_{5})=x_{2}+1$
and $\mathit{step}(x_{1},\dotsc,x_{5})=x_{2}+x_{3}+1$.
We assume that all three attention heads use the identity matrix as linear maps in their respective pooling function.
$\mathit{comb}_{3}$ is given by an FNN $N_{3}$ computing $\mathbb{R}^{4\cdot 5}\rightarrow\mathbb{R}$. Let the input
dimensions of $N_{3}$ be $x_{1,1},\dotsc,x_{1,5},x_{2,1},\dotsc,x_{4,5}$. Then, $N_{3}$ is equal to

$$ $\mathit{relu}(x_{1,1})|\!|\mathit{relu}(x_{1,2})|\!|N_{a}|\!|N_{b_{1}}|\!|N_{b _{2}}|\!|N_{c}|\!|N_{d}$ $$

where $N_{a}=N_{\rightarrow}\circ(N^{x_{1,2},x_{3,2}}_{=}|\!|N_{=}^{x_{1,3},x_{1,4}})$,
$N_{b_{1}}=N_{\rightarrow}\circ(N^{x_{1,2},x_{2,2}}_{=}|\!|N_{=t_{I}}^{x_{1,5}})$,
$N_{b_{2}}=N_{\rightarrow}\circ(N^{x_{1,2},x_{3,2}}_{=}|\!|N_{=t_{F}}^{x_{1,5}})$,
$N_{c}=N_{\rightarrow}\circ(N^{x_{1,4},x_{1,3}}_{<}|\!|N^{x_{1,5},x_{3,5}}_{H})$
and $N_{d}=N_{\rightarrow}\circ(N_{<}^{x_{1,3},{x_{4,3}}}|\!|N^{x_{1,5},x_{4,5}}_{V})$
using the gadgets and constructions described in Appendix B.
Layer $l_{4}$ is given by $l_{4}=(\mathit{att}_{\text{leq}},\mathit{comb}_{4})$
where $\mathit{att}_{\text{leq}}$ attends to $\{\bm{x}_{1},\dotsc,\bm{x}_{i}\}$ given $i$
and $\mathit{comb}_{4}$ is given by the minimal FNN $N_{4}$ computing $\mathit{relu}(x_{3}+\dotsb+x_{7})$.
A formal proof for the existence of $\mathit{att}_{\text{leq}}$ in $\mathcal{T}_{\mathit{udec}}$ is given in Lemma 6.
Furthermore, the output function $\mathit{out}$ of $T_{\mathcal{S}}$ is given by the minimal FNN $N_{\mathit{out}}$ computing $N(x_{1})=\mathit{relu}(1-x_{1})$.

Let $w=t_{1}\dotsb t_{l}\in S^{*}$ be some word over alphabet $S$. As defined above, we have that
$\mathit{emb}(t_{i},i)=(1,i,\sum_{j=0}^{i}j,k_{i})$ where $k_{i}\in\{1,\dotsc,|S|\}$.
Consider $\bm{x}^{2}_{1}\dotsb\bm{x}^{2}_{m}$, namely the sequence of vectors after propagating $w$
through the embedding $\mathit{emb}$ and layers $l_{1},l_{2}$ of $T_{\mathcal{S}}$. As stated by Lemma  1, we have that
$\bm{x}^{2}_{i}=(1,i,r(i),c(i),k_{i})$ where $r(i)$ and $c(i)$ are the row respectively column of tile $t_{i}$
if we interpret $w$ as an encoded tiling. Note that all vectors $\bm{x}^{3}_{i}$ are non-negative due to the way $N_{3}$ is built.
In the following, we argue that all $\bm{x}^{3}_{i}=\bm{0}$ if and only if $w$ is a valid
encoded tiling. Given this equivalence, the statement of the lemma follows immediately as $l_{4}$ simply sums up
all vectors and dimensions (except for the first and second) of $\bm{x}^{3}_{1},\dotsc,\bm{x}^{3}_{m}$ in $\bm{x}^{4}_{m}$
and the output of $N_{4}$ indicates whether there was some non-zero value.
We fix some arbitrary $\bm{x}^{2}_{i}=(1,i,r(i),c(i),k_{i})$.
Then, $\bm{x}^{3}_{i}=N_{3}(\bm{x}^{2}_{i},\bm{x}^{2}_{i_{\mathit{prev}}},\bm{x}^{2}_
{i_{\mathit{next}}},\bm{x}^{2}_{i_{\mathit{step}}})$ where
$i_{\mathit{next}}=i+1$ if $i<m$ and $m$ otherwise, $i_{\mathit{prev}}=i-1$ if $i>1$ and $1$ otherwise and
$i_{\mathit{step}}=i+r(i)+1$ if $i<m-r(i)-1$ and $m$ otherwise.

Consider property $(a)$ and subnetwork $N_{a}$. With the understanding gained in Appendix B,
$N^{x_{1,2},x_{3,2}}_{=}$ outputs 0 0 iff $x_{1,2}=x_{3,2}$. These dimensions correspond to positions
$i$ and $i_{\mathit{next}}$, which are only equal if $i=m$ (Lemma 2). Furthermore,
the property of $N_{\rightarrow}$ stated by Lemma 4 is given as the output of $N_{=}$ is guaranteed to be in
$[0;1]$ and the values of $x_{1,2}$ and $x_{3,2}$ are guaranteed to be in $\mathbb{N}$. In summary, this ensures that
the third dimension of $\bm{x}^{3}_{m}$ is 0 0 iff $r(m)=c(m)$. For other positions the third dimension is always 0 0 since
$N_{\rightarrow}$ outputs 0 0 in these cases due to the fact that $N^{x_{1,2},x_{3,2}}_{=}$ equals $1$.
Analogously, $N_{b_{1}}$ and $N_{b_{2}}$ ensure that $t_{1}=t_{I}$ and $t_{m}=t_{F}$ and, thus, property (b) iff the fourth
and fifth dimensions in all positions are equal to 0 0.
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 on at least two positions in
$\bm{x}^{2}_{1}\dotsb\bm{x}^{2}_{m}$. Consider the subnet $N_{c}$. By construction and the gadgets described
in Appendix B, we have that $N_{c}$ outputs 0 0 if $c(i)<r(i)$ and $(t_{i},t_{i+1})\in H$
or if $c(i)=r(i)$, which means that tile $t_{i}$ is rightmost in its corresponding row. Otherwise the value computed by $N_{c}$ is greater
than 0 0. Analogously, subnet $N_{d}$ checks whether vertically stacked tiles do match. In summary, this ensures that
the sixth and seventh dimension of each $\bm{x}^{3}_{i}$ is equal to 0 0 if and only if properties (c) and (d) hold.
∎

###### Proof of Theorem 2 .

In the same manner as in the proof of Theorem 1,
we prove the statement via reduction from $\textsc{OTWP}^{*}$. The reduction is exactly the
same, namely given an $\textsc{OTWP}^{*}$ instance $\mathcal{S}=(S,H,V,t_{I},t_{F})$ we build TE
$T_{\mathcal{S}}$ which recognizes exactly those words $w$ representing a valid encoded
tiling of $\mathcal{S}$. For details, see the proof of Theorem 1.

Given the correctness arguments for $T_{\mathcal{S}}$ in Theorem 1, it
is left to argue that $T_{\mathcal{S}}$ works as intended,
despite the fact that it works over some FA $F$ using at most $\mathcal{O}(\log(\max(|S|,n)))$ bits
where $n$ is the length of an input word. We choose $F$ such that overflow
situations do not occur in any computation $T_{\mathcal{S}}(w)$ and rounding
is handled such that $T_{\mathcal{S}}$ works as intended.
Throughout this proof, we use $\log(n)$
Namely, given a word $w$ with $|w|=n$ assume that $F$ uses $m=\lfloor 4\log(\max(|S|,n))\rfloor+2$ bits and rounds values off to the nearest representable number.
We denote the value resulting from rounding $x$ off in arithmetic $F$ by $\lfloor x\rfloor_{F}$.
We assume that there is an extra bit that is used as a sign bit and that at least $\lfloor 3\log(n)\rfloor+1$ bits can be
used to represent integer and at least $\lfloor\log(n)\rfloor+1$ 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\in\mathcal{O}(\log(\max(|S|,n)))$. To ease our arguments and notation from here on, we assume w.l.o.g.  that we represent $n$ using $\log(n)$ instead of $\lfloor log(n)\rfloor+1$.

Per definition, $T_{\mathcal{S}}$ uses the embedding function
$\mathit{emb}(a_{k},0)=(1,1,0,0,k)$ and $\mathit{emb}(a_{k},i)=(0,1,i,\sum_{j=0}^{i}j,k)$. First, we assume that each $k$,
namely the value representing a specific tile from $S$, is a unique, positive value. This is possible as $F$
uses $m>\log(|S|)$ bits. Furthermore, we see that $\mathit{emb}$, especially the sum $\sum_{j=0}^{i}j=\frac{i(i+1)}{2}\leq i^{2}$, works as intended up to $i=n$ due to the fact that $F$ uses more than $m>2\log(n)$ bits to represent integer parts.
Next, consider layer $l_{1}$ and $l_{2}$ of Lemma 1. Layer $l_{1}$
consists of a single attention head $\mathit{att}_{1,1}$. Here, the only crucial parts are the computation of value $\frac{1}{l}$ in $\mathit{pool}_{1,1}$ for a position $i$. Per definition,
$l$ corresponds to the number of positions $j$ such that $\sum_{h=0}^{j}h\leq i-1$.
As $i$ is bounded by $n$, this inequality can only be satisfied by positions $j$ for which
$j\leq\sqrt{n}$ holds. As $T_{\mathcal{S}}$ uses $\mathrm{hardmax}$ to count the positions for which
this inequality holds, $l$ is bounded by $\sqrt{n}$. Next, we
observe that $\lfloor\frac{1}{l}\rfloor_{F}=\frac{\lfloor 2^{\log(n)}\frac{1}{l}\rfloor}{2^{
\log(n)}}=\frac{\lfloor\frac{n}{l}\rfloor}{n}$, namely
the general understanding of rounding off where
we use $\log(n)$ bits to represent fractions. However, this
gives that for all $1\leq l_{1}<l_{2}\leq\sqrt{n}$ that
$\lfloor\frac{1}{l_{1}}\rfloor_{F}\neq\lfloor\frac{1}{l_{2}}\rfloor_{F}$ as
$\lfloor\frac{n}{l_{1}}\rfloor\neq\lfloor\frac{n}{l_{2}}\rfloor$
holds for all $l_{1}<l_{2}\leq\sqrt{n}$. This means, that
it is ensured by $F$ that $\frac{1}{l}$ is uniquely representable.

Next, the only crucial part in $l_{2}$ is the computation of the product $\frac{1}{l}\cdot j$, which is used to determine
the position $j$ for which $\frac{1}{l}\cdot j=1$ in $\mathit{score}_{2,1}$, which is obviously given by position $l$.
This equality is no longer guaranteed to
exist if we consider $\lfloor\frac{1}{l}\rfloor_{F}\cdot j$. However,
due to the monotonicity of $\lfloor\frac{1}{l}\rfloor_{F}$ for
$l\leq\sqrt{n}$ and that the maximum round of error is given
by $\frac{1}{2^{\log(n)}}$, we have that the $j=l$ produces the
value closest to $1$ in the product $\frac{1}{l}\cdot j$.
Taking a look at $\mathit{score}_{2,1}$, this ensures that
$l$ is still the position that $\mathit{att}_{2,1}$ attends to.
Therefore, the statement of Lemma 1 is
still valid for $T_{\mathcal{S}}$ working over $F$.
We observe that all values of some
vector $\bm{x}^{2}_{j}$ after layer $l_{2}$ are positive integers whose magnitude is bounded
by $n^{2}$.

Now, consider layer $l_{3}$ and $l_{4}$. From the proof of
Theorem 1 we see that the gadgets at most sum up
two values or compute a fraction of the form $\frac{i+j}{2}$ and $\frac{i-j}{2}$
(in gadgets $N_{H}$ or $N_{V}$). Both can safely be done with at least $3\log(n)$ bits for
integer and $\log(n)$ for fractional parts, as all previously computed values, up to layer
$l_{2}$, in a computation of $T_{\mathcal{S}}(w)$ are representable using $2\log(n)$ bits.
We observe that the values of the third to seventh dimension of some $\bm{x}^{3}_{j}$ are either 0 0 or $1$. This is due to the fact that all values after layer $l_{2}$
are guaranteed to be integers.
Next, consider layer $l_{4}$. The computation done by $\mathit{att}_{\leq}$ is safe (see Lemma 6) and the crucial step here is the computation of $\mathit{comb}_{4}$ given by $\mathit{relu}(x_{3}+\dotsb+x_{7})$. The values $x_{i}$ are all of the form
$\frac{i}{j}$ where $i$ is guaranteed to be 0 0 or $1$ and $j$ is the normalisation
induced by $\mathit{att}_{\leq}$ from perspective of position $j$. However, this means $j$ is bounded by $n$ and, thus,
$\lfloor\frac{i}{j}\rfloor_{F}>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, $\mathit{out}$ is trivially computable in $F$, which finishes the proof.
∎

###### Lemma 4 .

###### Proof.

###### Lemma 5 .

###### Proof.

###### Proof of Lemma 1 .

###### Proof of Lemma 2 .

###### Lemma 6 .

###### Proof.

###### Proof of Theorem 1 .

###### Proof of Theorem 2 .

## Appendix C Proofs of Section 5

###### Proof of Theorem 3 .

The decidability and membership results of statements (1) and (2 )are sufficiently
argued in the proof sketch given in Section 5.

To prove the hardness results of statements (1) and (2),
we establish a reduction from $\textsc{OTWP}_{\mathsf{un}}$ respectively
$\textsc{OTWP}_{\mathsf{bin}}$: given some bounded word-tiling
instance $(\mathcal{S},n)$ we build an instance $(T_{\mathcal{S}},n)$ of $\textsc{bSat}_{\mathsf{un}}$ respectively $\textsc{bSat}_{\mathsf{bin}}$ where
$T_{\mathcal{S}}$ is build as described in Theorem 1. The only missing argument is that these reductions are polynomial.
In particular, this means that $T_{\mathcal{S}}$ must be built in polynomial time regarding the size of $(\mathcal{S},n)$.
Therefore, we recall the proof of Theorem 1.

First, we see that the embedding function $\mathit{emb}$ and the amount of layers of $T_{\mathcal{S}}$ is independent of $\mathcal{S}$ and $n$.
The first two layers $l_{1}$ and $l_{2}$ of $T_{\mathcal{S}}$ are specified in Lemma 1.
Recalling the proof of Lemma 1, we see that $l_{1}$ and $l_{2}$ each consist of a single attention head,
whose internal parameters like scoring, pooling or combination are independent of $(\mathcal{S},n)$ as well. Next, consider layer $l_{3}$.
This layer consists of three attention heads $\mathit{att}_{\mathit{prev}}$, $\mathit{att}_{\mathit{next}}$ and $\mathit{att}_{\mathit{step}}$ each given by the
template described in Lemma 2, which again is independent of $(\mathcal{S},n)$. Additionally, $l_{3}$ contains
the combination function $\mathit{comb}_{3}$. This combination function is represented by a FNN $N_{3}$, using smaller FNN
$N_{a}$, $N_{b_{1}}$, $N_{b_{2}}$, $N_{c}$ and $N_{d}$ as building blocks. These are dependent on $\mathcal{S}$, as they are built
using gadgets $N_{=t_{I}}$, $N_{=t_{F}}$, $N_{H}$ and $N_{V}$ where $t_{I}$, $t_{F}$, $H$ and $V$ are components of
$\mathcal{S}$. However, in the proof of Lemma 5 we see that these gadgets
are at most polynomial in their respective parameter. Layer $l_{4}$ and the output function, specified by FNN $N_{\mathit{out}}$,
are again independent of $(\mathcal{S},n)$. In summary, the TE $T_{\mathcal{S}}$ is polynomial in $(\mathcal{S},n)$,
which makes the reductions from $\textsc{OTWP}^{\mathsf{exp}}$ und $\textsc{OTWP}^{\mathsf{poly}}$ polynomial.
∎

Next, we address the proof of Lemma 3. We need some preliminary, rather technical result first.
Let $T$ be an TE and $w\in\Sigma^{+}$ be a word and consider the computation $T(w)$.
Let $X_{T(w)}^{0}=\mathit{emb}(w)$ and $X_{T(w)}^{i}$ be the sequence of vectors occurring after the computation of layer $l_{i}$ of $T$.
Let $\bm{x}$ and $\bm{x}^{\prime}$ be two vectors matching the dimensionality of $\mathit{score}_{i,j}$ of $T$.
Overloading some notation, let $N_{w}(\bm{x},\bm{x}^{\prime},i,j)=\mathit{norm}_{i,j}(\mathit{score}_{i,j}(\bm
{x},\bm{x}^{\prime}),\mathit{score}_{i,j}(\bm{x},X_{T(w)}^{i-1}))$ where $\mathit{score}_{i,j}(\bm{x},X_{T(w)}^{i-1})$ is the vector of all scorings of $\bm{x}$ with sequence
$X_{T(w)}^{i-1}$. We remark that it is not necessary that $\bm{x}$ or $\bm{x}^{\prime}$ must occur in $X_{T(w)}^{i-1}$ for this to be well defined.
Again overloading some notation, let $P_{w}(\bm{x},i,j)=\mathit{pool}_{i,j}(X_{T(w)}^{i-1},\mathit{score}_{i,j}(\bm{
x},X_{T(w)}^{i-1}))$.

###### Lemma 7 .

Let $T$ be a additive-periodical TE of depth $L$, maximum width $H$ and periodicity $p$ with $\mathit{norm}_{i,j}\in\{\mathrm{softmax},\mathrm{hardmax}\}$ for all
$i\leq L,j\leq H$, let $w=u_{1}u_{j_{1}}\dotsb u_{j_{h}}u_{2}\in\Sigma^{+}$ where
$u_{1},u_{2}\in\Sigma^{+}$, all $u_{j_{i}}\in\Sigma^{p}$ and all $u_{j_{i}}$ also occur in $u_{1}$ or $u_{2}$ and
let $\mathcal{X}$ be the set of all vectors occurring in any of the sequences $X^{i}_{T(w)}$.
If there are indexes
$h_{1}<h_{2}\leq h$ such that for all $\bm{x},\bm{x}^{\prime}\in\mathcal{X},i\leq L,j\leq H$ holds that
$N_{u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}}(\bm{x},\bm{x}^{\prime},i,j)=N_{u_{1}u_{
j_{1}}\dotsb u_{j_{h_{2}}}}(\bm{x},\bm{x}^{\prime},i,j)$ and $P_{u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}}(\bm{x},i,j)=P_{u_{1}u_{j_{1}}\dotsb u_{
j_{h_{2}}}}(\bm{x},i,j)$
then it holds that $N_{u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}u_{j_{h_{2}+1}}\dotsb u_{2}}(\bm{x},\bm{x
}^{\prime},i,j)=N_{u_{1}\dotsb u_{2}}(\bm{x},\bm{x}^{\prime},i,j)$ and $P_{u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}u_{j_{h_{2}+1}}\dotsb u_{2}}(\bm{x},i,j)=
P_{u_{1}\dotsb u_{2}}(\bm{x},i,j)$.

###### Proof.

Let $T$, $w$, $\mathcal{X}$, $h_{1}$ and $h_{2}$ be as stated above.
We prove the statement via induction on the layers $l_{i}$. First,
consider layer $l_{1}$ and fix some tuple $(\bm{x},\bm{x}^{\prime},1,j)$.
We first show that $N_{u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}u_{j_{h_{2}+1}}\dotsb u_{2}}(\bm{x},\bm{x
}^{\prime},1,j)=N_{u_{1}\dotsb u_{2}}(\bm{x},\bm{x}^{\prime},1,j)$.
Assume that $\mathit{norm}_{1,j}$ is given by $\mathrm{softmax}$. Then, $\mathit{norm}_{1,j}$
computes $\frac{e^{\mathit{score}_{1,j}(\bm{x},\bm{x}^{\prime})}}{\sum_{\mathit{score}_{
1,j}(\bm{x},X_{T(w^{\prime})}^{0})}e^{s_{i^{\prime}}}}$ for all words $w^{\prime}$.
Obviously, the numerator in $N_{u_{1}\dotsb u_{h_{1}}u_{h_{2}+1}\dotsb u_{2}}(\bm{x},\bm{x}^{\prime},1,j)$ and $N_{u_{1}\dotsb u_{2}}(\bm{x},\bm{x}^{\prime},1,j)$ is equal.
By definition, we have that $\mathit{score}_{i,j}$ is local in the sense that it
compares vectors pairwise, producing the different scoring values
$s_{i^{\prime}}$ independent of the overall word. Furthermore, due to the
fact that $\mathit{emb}$ is additive-periodical, we have $X^{0}_{T(u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}u_{j_{h_{2}+1}}\dotsb u_{2})}$ and $X^{0}_{T(u_{1}\dotsb u_{2})}$ are equal in the sense that the vectors corresponding to
$u_{j_{h_{2}+1}}\dotsb u_{2}$ are equal. We refer to this property (*) later on. Using these observations
and that $N_{u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}}(\bm{x},\bm{x}^{\prime},1,j)=N_{u_{1}u_{
j_{1}}\dotsb u_{j_{h_{2}}}}(\bm{x},\bm{x}^{\prime},1,j)$, we have that
the denominator is equal as well. Now, assume that $\mathit{norm}_{1,j}$
is given by $\mathrm{hardmax}$. Then,
$\mathit{norm}_{1,j}$ computes $\frac{f(\mathit{score}_{1,j}(\bm{x},\bm{x}^{\prime}),\mathit{score}_{1,j}(\bm{
x},X^{0}_{T(w^{\prime})}))}{\sum_{\mathit{score}_{1,j}(\bm{x},X^{0}_{T(w^{
\prime})})}f(s_{i^{\prime}},\mathit{score}_{1,j}(\bm{x},X^{0}_{T(w^{\prime})}))}$
where $f(s,S)=1$ if $s$ is maximal in $S$ and 0 0 otherwise for any word $w^{\prime}$.
In contrast to $\mathrm{softmax}$, we have that the values of $f(\dotsb)$ are dependent of the overall context, namely the vector of all scorings
$\mathit{score}_{1,j}(\bm{x},X^{0}_{T(w^{\prime})})$. Compare $X^{0}_{T(u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}u_{j_{h_{2}+1}}\dotsb u_{2})}$ and $X^{0}_{T(u_{1}\dotsb u_{2})}$,
both given by the additive-periodical embedding $\mathit{emb}$. Via assumption,
we have that each $u_{j_{i}}$ block also occurs in $u_{1}$ or $u_{2}$.
In particular, this means every vector that occurs in $\mathit{emb}(u_{1}\dotsb u_{2})$ does also occur in $\mathit{emb}(u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}u_{j_{h_{2}+1}}\dotsb u_{2})$ and vice-versa.
This implies that $f(\mathit{score}_{1,j}(\bm{x},\bm{x}^{\prime}),\mathit{score}_{1,j}(\bm{x},X^{
0}_{T(u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}u_{j_{h_{2}+1}}\dotsb u_{2})}))=f(
\mathit{score}_{1,j}(\bm{x},\bm{x}^{\prime}),\mathit{score}_{1,j}(\bm{x},X^{0}
_{T(u_{1}\dotsb u_{2})}))$ for any scoring value $\mathit{score}_{1,j}(\bm{x},\bm{x}^{\prime})$.
In combination with the assumption that $N_{u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}}(\bm{x},\bm{x}^{\prime},1,j)=N_{u_{1}u_{
j_{1}}\dotsb u_{j_{h_{2}}}}(\bm{x},\bm{x}^{\prime},1,j)$ and the observations above, we also get $N_{u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}u_{j_{h_{2}+1}}\dotsb u_{2}}(\bm{x},\bm{x
}^{\prime},1,j)=N_{u_{1}\dotsb u_{2}}(\bm{x},\bm{x}^{\prime},1,j)$ in the $\mathrm{hardmax}$ case.
Next, consider the pooling functions. By definition, we have that $\mathit{pool}_{1,j}(X^{0}_{T(w^{\prime})},\mathit{score}_{1,j}(\bm{x},X^{0}_{T
(w^{\prime})}))$ computes $\sum_{X^{0}_{T(w^{\prime})}}\mathit{norm}_{1,j}(\bm{x},\bm{x}_{i^{\prime}},
\mathit{score}_{i,j}(\bm{x},X^{0}_{T(w^{\prime})}))(W\bm{x}_{i^{\prime}})$ for any word $w^{\prime}$.
Our previous arguments give that $N_{u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}u_{j_{h_{2}+1}}\dotsb u_{2}}(\bm{x},\bm{x
}^{\prime},1,j)=N_{u_{1}\dotsb u_{2}}(\bm{x},\bm{x}^{\prime},1,j)$. In combination with
$P_{u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}}(\bm{x},i,j)=P_{u_{1}u_{j_{1}}\dotsb u_{
j_{h_{2}}}}(\bm{x},i,j)$ and (*), we immediately get that
$P_{u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}u_{j_{h_{2}+1}}\dotsb u_{2}}(\bm{x},i,j)=
P_{u_{1}\dotsb u_{2}}(\bm{x},i,j)$ holds as well.
Next, consider layer $l_{i}$. 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 $\mathit{pool}_{{i-1},j}$ produce the same output in computation $T(u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}u_{j_{h_{2}+1}}\dotsb u_{2})$ and computation $T(u_{1}\dotsb u_{2})$.
This implies that all vectors present in $X^{i-1}_{T(u_{1}u_{j_{1}}\dotsb u_{j_{h_{1}}}u_{j_{h_{2}+1}}\dotsb u_{2})}$ are also present in $X^{i-1}_{T(u_{1}\dotsb u_{2})}$ and vice-versa
and that the vectors corresponding to $u_{j_{h_{2}+1}}\dotsb u_{2}$ are equal in both computations.
∎

###### Proof of Lemma 3 .

Let $T\in\mathcal{T}^{\textsc{fix}}_{\circ}$ be an additive-periodical TE working over alphabet
$\Sigma$, having periodicity $p$, depth $L$, maximum width $H$, maximum dimensionality
$D$ and working over an FA $F$ using $b$ bits for binary encoding.
We use $V$ to denote the set of values representable in the fixed arithmetic that $T$ works over.
Note that $|V|\leq 2^{b}$.
Let $w\in\Sigma^{+}$ be a word such that $T(w)=1$. We observe that there is $m\in\mathbb{N}$ such
that $w=u_{1}\dotsb u_{m}u$ where $u_{i}\in\Sigma^{p}$ are blocks of symbols of length $p$ and $u\in\Sigma^{\leq p}$.
Our goal is to prove that a not necessarily connected subsequence of at most $2^{(|T|)^{6}}$ many
$p$-blocks $u_{i}$ from $u_{1}\dotsb u_{m}$ is sufficient to ensure the same computation of $T$.
In the case that $pm+p\leq 2^{(|T|)^{6}}$ we are done. Therefore, assume that $m>2^{(|T|)^{6}}$.

Let $U$ be the set of all unique $u_{i}$. We observe that $|U|\leq|\Sigma|^{p}$.
Next, we fix some not necessarily connected but ordered subsequence $S=u_{j_{0}}u_{j_{1}}\dotsb u_{j_{n}}u_{j_{n+1}}$
with $u_{j_{0}}=u_{1}$, $j_{i}\in\{2,\dotsc,m\}$ and $u_{j_{n+1}}=u$ of $w$ such that each $u^{\prime}\in U$ occurs exactly once.
For the case that $u_{1}=u$ we allow this specific block to occur twice in $S$.
The assumption $m>2^{\mathit{poly}(|T|)}$ implies that $S\neq w$. This means that there are pairs
$(u_{j_{h}},u_{j_{h+1}})$ in $S$ with some non-empty sequence of $p$-blocks $u_{j^{\prime}_{1}}\dotsb u_{j^{\prime}_{l}}$ in between.
W.lo.g. assume $u_{j_{0}}$ and $u_{j_{1}}$ is such a pair. Our goal is to argue that there are at most $2^{(|T|)^{5}}$
blocks from $u_{j^{\prime}_{1}}\dotsb u_{j^{\prime}_{l}}$ needed to ensure the same computation of $T$. Given that this argument works for all $|\Sigma|^{p}$ adjacent pairs in $S$, we are done.

Consider the computation $T(w)$. The additive-periodical embedding $\mathit{emb}$ of $T$ implies that $\mathit{emb}(w)$ includes
at most $\Sigma p$ different vectors. Furthermore, from layer to layer equal vectors are mapped equally, which means
that each $X_{w}^{1},\dotsc,X_{w}^{L}$ contains at most $\Sigma p$ different vectors as well. This implies that the
computation $T(w)$ induces at most $(L\Sigma p)^{2}\times L\times H\leq(\Sigma pL^{2}H)^{2}\leq(\Sigma pLH)^{4}$
different tuples $(\bm{x},\bm{x}^{\prime},i,j)$ where $\bm{x},\bm{x}^{\prime}$
are vectors induced by $T(w)$ and $i\leq L,j\leq H$.
Additionally, we have that for each value $N_{w}(\bm{x},\bm{x}^{\prime},i,j)$ and $P_{w}(\bm{x},i,j)$, as defined in the beginning of this section, there are at most
$|V^{D}|\leq 2^{bD}$ possibilities. Simple combinatorics, namely the pigeon hole principle, states that in the
increasing sequence $u_{j^{\prime}_{1}},u_{j^{\prime}_{2}},\dots$ there must be points $h_{1}$ and $h_{2}$ with
$h_{1}\leq 2^{bD(\Sigma pLH)^{4}}\leq 2^{(|T|)^{5}}$ such that for all tuples
$(\bm{x},\bm{x}^{\prime},i,j)$ induced by $T(w)$ we have that $N_{u_{j_{0}}u_{j^{\prime}_{1}}\dotsb u_{j^{\prime}_{h_{1}}}}(\bm{x},\bm{x}^{
\prime},i,j)=N_{u_{j_{0}}u_{j^{\prime}_{1}}\dotsb u_{j^{\prime}_{h_{2}}}}(\bm{
x},\bm{x}^{\prime},i,j)$ and $P_{u_{j_{0}}u_{j^{\prime}_{1}}\dotsb u_{j^{\prime}_{h_{1}}}}(\bm{x},i,j)=P_{u_
{j_{0}}u_{j^{\prime}_{1}}\dotsb u_{j^{\prime}_{h_{2}}}}(\bm{x},i,j)$.
Now, Lemma 7 states that this implies
$N_{u_{j_{0}}u_{j^{\prime}_{1}}\dotsb u_{j^{\prime}_{h_{1}}}u_{j^{\prime}_{h_{2
}+1}}\dotsb u_{j_{1}}\dotsb u}(\bm{x},\bm{x}^{\prime},i,j)=N_{w}(\bm{x},\bm{x}
^{\prime},i,j)$
and $P_{u_{j_{0}}u_{j^{\prime}_{1}}\dotsb u_{j^{\prime}_{h_{1}}}u_{j^{\prime}_{h_{2
}+1}}\dotsb u_{j_{1}}\dotsb u}(\bm{x},i,j)=P_{w}(\bm{x},i,j)$.
However, this implies that the subsequence
$u_{j^{\prime}_{h_{1}+1}}\dotsb u_{j^{\prime}_{h_{2}}}$ has no influence in the computation of $T$ on $w$ and, thus, can be left out.
As we can argue this for every such cycle occurring in
$u_{j^{\prime}_{1}}\dotsb u_{j^{\prime}_{l}}$, we get the desired bound of
$2^{(|T|)^{5}}$.
∎

###### Proof of Theorem 5 .

We prove the statement via reduction from $\textsc{OTWP}_{\mathsf{bin}}$.
Let $\mathcal{S}=(S,H,V,t_{I},t_{F})$ and $n\geq 1$ be an instance of $\textsc{OTWP}_{\mathsf{bin}}$.
We construct an TE $T_{\mathcal{S},n}\in\mathcal{T}^{\textsc{fix}}$ working over some FA $F$ with
$T_{\mathcal{S},n}(w)=1$ if and only if $w\in S^{+}$ witnesses the validity of the $\textsc{OTWP}_{\mathsf{bin}}$
instance $(\mathcal{S},n)$.

Next, let $T_{\mathcal{S},n}$ be built exactly like $T_{\mathcal{S}}$ in the proof of
Theorem 4, but with the following structural adjustments.
In layer $l_{3}$ we adjust $\mathit{comb}_{3}$ to be
$\mathit{comb}_{3}=N_{3}|\!|N_{e}|\!|N_{f}$ where $N_{3}$ is specified
as in the proof of Theorem 4, $N_{e}=N_{\rightarrow}\circ(N^{x_{1,2},x_{3,2}}_{=}|\!|N^{x_{1,3}}_{=n})$ and $N_{f}=N^{x_{1,2}}_{\neq\frac{(n+1)((n+1)+1)}{2}+1}$ where
$N_{\neq t}$ is analogous to the construction of
$N_{=t}$ given in
Lemma 5.
Furthermore, we adjust $\mathit{comb}_{4}$ in layer $l_{4}$ to be represented by the FNN $\mathit{relu}(x_{3}+\dotsb+x_{8}+x_{9})$.
We refer to the gadgets described in Lemma 4 and Lemma 5 as well as the proof of Theorem 1
for further details.

Consider the adjustment in $l_{3}$. FNN $N_{e}$ in $\mathit{comb}_{3}$ ensures that
$T_{\mathcal{S},n}(w)=1$ only if the row index corresponding to
the last symbol is equal to $n$. Note that $N_{3}$ checks whether
row and column index corresponding to the last symbol are equal.
Additionally, $N_{f}$ checks if there is no id
equal to $\frac{(n+1)((n+1)+1)}{2}+1$. This corresponds
to the position id of the successor of the vector representing tile $(n,n)$.
Furthermore, the adjustment of $\mathit{comb}_{4}$ considers the output of $N_{e}$ and $N_{f}$ in addition to the outputs of
$N_{3}$. In summary, we have that $T_{\mathcal{S},n}$ only outputs $1$ given $w$ 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 $N_{e}$), that $w$ is at most of length $\frac{(n+1)((n+1)+1)}{2}$ (ensured by $N_{f}$) and if $w$ represents a valid encoded tiling (the remaining parts of $T_{\mathcal{S},n})$.

Additionally, we need to argue that $T_{\mathcal{S},n}$ works as intended,
despite the fact that it is limited by some FA $F$ using a representation size that is at most logarithmic in $n$.
These arguments follow the exact same line as in the proof of Theorem 2, but using FA $F$ that uses
$m=\lfloor 6\log(\max(|S|,n))\rfloor+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|=\frac{(n+1)((n+1)+1)}{2}\leq n^{2}$.
Thus, we use $\lfloor 4\log(n)\rfloor+1$ integer bits to be able to represent a sum $\sum_{j=0}^{i}j=\frac{i(i+1)}{2}\leq i^{2}$ for all
$i\leq n^{2}$ and $\lfloor 2\log(n)\rfloor+1$ fractional bits to uniquely represent fraction $\frac{1}{l}$ for $l\leq n$. For detail see the proof
of Theorem 2. Furthermore, the fact that we use $\lfloor 4\log(n)\rfloor+1$ bits to encode integers and
that $F$ handles overflow using saturation ensures that $N_{f}$ works as intended: we have that $\frac{(n+1)((n+1)+1)}{2}+1<n^{4}$
and, thus, we have that the id $\frac{(n+1)((n+1)+1)}{2}+1$ occurs at most once, independent of the length of $w$ as it is not
the point where $F$ enforces saturation on the positional embedding.
Thus, $\mathit{att}_{\text{self}}$ works for this position as intended and then $N_{f}$ checks the property described above correctly.

The argument that $T_{\mathcal{S},n}$ can be built in polynomial time is a straightforward implication from the arguments for Theorem 3 and the fact that $N_{e}$ and $N_{f}$ are a small gadgets with maximum parameter quadratic in $n$, which can be represented using a logarithmic amount of bits.
∎

###### Proof of Theorem 3 .

###### Lemma 7 .

###### Proof.

###### Proof of Lemma 3 .

###### Proof of Theorem 5 .

## Peer Reviews

confidence: 5
contribution: 2
initial_rating: 6
presentation: 3
questions: Please address the concerns raised in the Weaknesses section.
soundness: 3
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).
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.
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.
 
The 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”.
 
At 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.

---

confidence: 4
contribution: 2
initial_rating: 3
presentation: 1
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	the boundaries of decidability and complexity to figure out methods to cope with that.  Please comment.

Pg. 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.

Pg. 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?

Pg. 4. Could it be possible that softmax rather than hardmax change the decidability result?

Pg. 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.

Pg. 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?

Pg. 6. L. 302. Why is it the case that T_udec is the weakest class in terms of expressivity? 

Pg. 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?

Pg. 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.

Pg. 8. L. 402. The so-called polynomial evaluation property is not discussed in Section 3 nor elsewhere in the paper. Why is it reasonable?

Pg. 8. It seems that the proof sketch of The 3 does not take into account the representation of w. Please comment on this.

Other comments

Pg. 3. L. 138. k should be L since i is a layer, and layers go from 1 to L.

Pg. 3. L. 157. different rational number”s”
soundness: 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.
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.
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.

Besides, 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).

---

confidence: 5
contribution: 3
initial_rating: 5
presentation: 2
questions: 1. Where is the fix-precision used in the proof of lemma 3? Is it necessary?
 
2. Do you have proof of decidability for fix-precision (*without* periodic embeddings)?

In 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)
soundness: 3
strengths: 1. The paper explores the complexity of Transform encoders. Understanding the theoretical complexity of this hot topic is very timely.

2. 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).
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:

1) 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.

2) 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.

3) 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.

4) 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).
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).

2. (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.

---

confidence: 2
contribution: 2
initial_rating: 8
presentation: 3
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.

- Do the authors have an intuition on to what extent their results could generalize to soft-attention?

- It was not clear to me if the definition of SAT on transformers is new, or has been proposed before.

- 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?

*Some small nitpicks*

- Brackets for citations are not used properly. The paper consistently cites transformers Vaswani et al. (2018) instead of transformers (Vaswani et al., 2018).

- The font in Figure 2 is too small for me to be readable without zooming.
soundness: 3
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.
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.
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.
-  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.
- 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).
- The decidability results of e.g. Theorem 3 are based on naive enumeration, which is not realistic except for very short word lengths.

Meta-review: This paper provides complexity results for transformers, in particular, the authors identify the TRSAT problem and show its general undecidability. Practical cases are identified that can actually be decided. 

The reviewers agree that the topic is important and timely and that the paper provides a solid, albeit not too strong, contribution to the ICLR community. Moreover, the authors are encouraged to reorganize and improve the paper according to the suggestions.

Decision: Accept (Poster)