Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning
transformer;formal reasoning;complexity
> Pg. 8. It seems that the proof sketch of The 3 does not take into account the representation of w. Please comment on this.

We believe you are referring to the fact that $|w|$ measures only the length of a word, as opposed to its representation size, which should also account 
for $|\Sigma|$. You are indeed correct in this observation. However, the size of a TE $|T|$ does depend on $|\Sigma|$, hence this poses no issue for the 
lower bounds demonstrated in Theorem 3. 
Nevertheless, we agree with your point and have included a clarifying sentence in the revised version in the first paragraph of the proof sketch of Theorem 
3 (page 8).

> Other comments

Thank you for pointing out these typos. We fixed them in the revised version!


### Weaknesses

Regarding the structure and presentation of the paper: we see the point. But other reviewers have commented on the presentation in an opposite way. We 
will write a short reply on this issue to all reviews as a general comment.
answer to questions  - part 3 + weaknesses pointed out
> 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?

Octant tiling is a variant of the well-known quadrant-tiling (named in [Rob71]) instance in the class of domino tiling problems, where the tiling is 
restricted to a certain octant of the plane, also known as a quadrangle. It is true that there does not seem to be one citable reference for 
the undecidability of the octant tiling problem, but this is also due to the fact that it is easily seen to be undecidable by observing that the 
standard reduction from the halting problem for Turing Machines to the quadrant tiling problem yields an octant tiling (because after n steps a TM can 
have modified or visited at most the first n tape cells). The octant tiling problem is often used in the literature for undecidability proofs, for 
instance in [BGD+10,BDG+14,B22,B24,HMS08]. 

In our undecidability proofs, the "octant tiling word problem" serves as an intermediate problem between octant tiling and the satisfiability problem for 
transformer encoders. The "octant word tiling problem" is used to translate the source problem in the reduction, formulated as a constraint problem 
over a two-dimensional geometry, into a constraint problem over a one-dimensional geometry, i.e. as a problem of finding a linear word structure. This is
all there is to 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.

To ensure that Theorems 3 and 4 are still broadly applicable, we have defined classes of transformer encoders (TE) without rigidly fixing every 
single parameter such as the precise combinations of scorings and similar aspects. However, for obtaining complexity bounds it is essential to establish the 
measure of representation size for transformers. The size measure |T| used in the paper takes only the most significant parts of an encoder transformer into 
account, namely alphabet size, depth, width, and dimensionality. This ensures that Theorems 3 and 4 are applicable to transformer models that may vary in 
certain aspects, for as long as the other parameters do not exceed this polynomial bound. It is, of course, possible to devise transformers that do not meet 
the assumption in question, for example by use of non-standard normalisation functions that require large programs or very large constants for their 
computation or representation. To the best of our knowledge, the transformers that are widely considered in the literature and in practice do all meet this 
property of being representable in space that is polynomial in the measure |T|. This is why we call this assumption reasonable.

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

Thank you for pointing this out; it appears to be an oversight on our part. The polynomial evaluation property is deemed reasonable as it aligns with how 
encoders process their output. The outlined procedure is as follows: for each layer $l_i \leq L$, the output sequence $w^i = x_1^i \dotsb x_{|w|}^i$ is 
derived from $w^{i-1}$ by pairing each $x_h^{i-1}$ and $x_k^{i-1}$ with $h, k \leq |w|$. This pairing occurs within each attention head 
$\mathit{att}_{i,j}$ where $j \leq H$. Given that $|T|$ is dependent on both $L$ and $H$, this computation is polynomial in terms of $|T| + |w|$.
We added a clarifying paragraph after Theorem 2 in Section 3!

---
[Rob71] R. Robinson. "Undecidability and Nonperiodicity for Tilings of the Plane", Inventiones Mathematicae, 12(3), 1971 pp. 177–209

[B22] L. Bartholdi, "Monadic second-order logic and the domino problem on self-similar graphs", Groups Geom. Dyn. 16 (2022), pages 1423–1459

[B24] B. Bednarczyk, "Exploring Non-Regular Extensions of Propositional Dynamic Logic with Description-Logics Features", Log. Methods Comput. Sci. 20(2) (2024)

[BDG+10] D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, G. Sciavicco, "Undecidability of the Logic of Overlap Relation over Discrete Linear 
Orderings", Electronic Notes in Theoretical Computer Science, vol. 262, 2010, pages 65-81

[BDG+14] D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, G. Sciavicco, "The dark side of interval temporal logic: marking the undecidability 
border", Ann. Math. Artif. Intell. 71(1-3): 41-83 (2014)

[HMS08] I. M. Hodkinson, A. Montanari, G. Sciavicco, "Non-finite Axiomatizability and Undecidability of Interval Temporal Logics with C, D, and T", CSL 
2008:308-322
answer to questions - part 2
Firstly, we would like to express our gratitude for your comprehensive review! We appreciate the considerable time you devoted to raising those questions. 

We are looking forward to an engaging discussion. To make it efficient, we have paraphrased the main questions below.
However, the numerous questions you stated make it necessary to spread our answer across several comments.

--- 

### Questions 

> Pg. 2. L 54-54.  "I disagree with this comment. Programming languages are Turing Complete, still [...]. Please comment."

We agree. It is certainly worth delving into research on formal reasoning for encoder-decoder transformers. The comment to which you refer was intended to 
clarify our decision to focus on encoder-only models, as this is the first work of its kind. We aim to establish fundamental results without imposing 
unnecessary restrictions. Commencing with full encoder-decoder capabilities could potentially require artificial constraints on models and settings to 
achieve decidability, due to their already known high expressive power (Peréz et al. 2021). Thus, we selected encoder-only models for this study, but never 
intended to suggest that encoder-decoder transformers lack interest.

>Pg. 2. L 66-69. "What do you mean by “formal interpretation”?"

The term "formal" indicates our focus on methods that are both sound and complete. We elaborated on this in the paragraph beginning on line 38. "Formal 
interpretation" refers to problems, procedures, and related topics concerning interpretability properties of neural network-based models. For a reference, 
please see Marques-Silva & Ignatiev (2022), where the authors employ the term "formal XAI". We discussed this in the paragraph beginning on line 190.

> Pg. 3. L 169-174. "What part of the TC proof of Peréz et al. [..] T_udec could possibly be decidable?

We view the principal contribution of this work as establishing a foundational framework for comprehending the computational complexity of formal reasoning 
within transformers. The class T_udec under consideration should be regarded as the so far tightest "threshold" concerning expressive power, above which 
formal reasoning of transformer encoders is impossible/undecidable. 
In the study by Peréz et al. (2021), the authors concentrated on encoder-decoder transformers, whereas our research is dedicated solely to encoder-only 
transformers. While some of our architectural choices for T_udec were inspired by their work, primarily to establish the aforementioned threshold, the 
models we investigate are of a different type.

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

We understand this question as you referring to the class $T_\circ^{\text{fix}}$ or the result of Theorem 4. The class 
$T_\circ^{\text{fix}}$ encompasses transformer encoders (TE) that can incorporate either softmax or hardmax normalisations. Consequently, the 
upper bound on decidability also applies to classes of TE analogous to $T_\circ^{\text{fix}}$ that exclusively employ hardmax, which means that 
the presence of softmax is not the reason.

> Pg. 5. L 251. The 3. "Clearly, bounded satisfiability is decidable [...] The important result here is the complexity bound."

We agree with your suggestion. This informal restatement of Theorem 3 would indeed benefit from the inclusion of the upper bounds specified in the formal 
theorem. We have addressed this in the revised version by stating NEXPTIME- and NP-completeness.

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

The sentence you are referring to was meant to convey that both, bounding the input length or considering fixed-width arithmetic, lead to decidability with 
an NEXPTIME upper bound.
The relevance of the bounded input length setting lies in its practicality as a natural constraint, such as when context sizes are limited.

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

While much remains unknown, providing a comprehensive hierarchy of classes for transformer encoders is challenging. This difficulty arises from the 
numerous parameters involved, such as variations in encoding, normalisations, and scorings, among others.
The statement you are referring to was meant to introduce T_udec as the class for which we currently know, based on the results of our paper, that it is 
the weakest leading to the undecidability of SAT. However, you are correct: the way that that sentence is currently phrased could suggest a stronger claim 
than intended. We have addressed this in the revised version.
answer to questions - part 1
Yes
No ethics review needed.
Please address the concerns raised in the Weaknesses section.
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).
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.
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.
Yes
No ethics review needed.
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”
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.
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.
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).
Yes
No ethics review needed.
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.
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).
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).
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. 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.
Yes
No ethics review needed.
- 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.
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.
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.
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.
@inproceedings{
anonymous2024transformer,
title={Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning},
author={Anonymous},
booktitle={Submitted to The Thirteenth International Conference on Learning Representations},
year={2024},
url={https://openreview.net/forum?id=VVO3ApdMUE},
note={under review}
}
We analyse the complexity of the satisfiability problem, or similarly feasibility problem, (trSAT) for transformer encoders (TE), which naturally occurs in formal verification or interpretation, collectively referred to as formal reasoning. We find that trSAT is undecidable when considering TE as they are commonly studied in the expressiveness community. Furthermore, we identify practical scenarios where trSAT is decidable and establish corresponding complexity bounds. Beyond trivial cases, we find that quantized TE, those restricted by fixed-width arithmetic, lead to the decidability of trSAT due to their limited attention capabilities. However, the problem remains difficult, as we establish scenarios where trSAT is NEXPTIME-hard and others where it is solvable in NEXPTIME for quantized TE. To complement our complexity results, we place our findings and their implications in the broader context of formal reasoning.
I certify that there is no URL (e.g., github page) that could be used to find authors’ identity.
I acknowledge that I and all co-authors of this work have read and commit to adhering to the ICLR Code of Ethics.
transformer formal reasoning complexity
I certify that there is no acknowledgement section in this submission for double blind review.
/pdf/27baf43c0a865485a399026e2f4c488e5b9c1760.pdf
interpretability and explainable AI
I understand the reciprocal reviewing requirement as described on https://iclr.cc/Conferences/2025/CallForPapers. If none of the authors are registered as a reviewer, it may result in a desk rejection at the discretion of the program chairs. To request an exception, please complete this form at https://forms.gle/Huojr6VjkFxiQsUp6.
I certify that this submission complies with the submission instructions as described on https://iclr.cc/Conferences/2025/AuthorGuide.
Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning
ICLR 2025 Conference Submission
ICLR.cc/2025/Conference/Submission