Can Transformers Reason Logically? A Study in SAT Solving

We have adjusted our paper accordingly (modified Definition 4.2 to explicitly state that the procedure must halt and remove the statement of as a decision procedure in Definition 4.3.) to explicitly state that a decision procedure must always halt and we’re very grateful to the reviewer for the observation.

Am I right that you so far did not revise it?

This is done by proving trace equivalence of our theoretical construction with the abstract DPLL algorithm [8], which is proved to always terminate in the referred paper (Theorem 5).

While I did not check the details again, this makes sense. Thanks!

We mainly formulated Transformers with probability distribution as output to align with the modus operandi of commercial LLMs [...] We have adjusted the definitions in our paper so that the model directly outputs the next token.

That is an important difference, you are right! Its probably best to make this clear at some point. Given this LLM view, the "probability distribution view" is clearly the right one. Again, you did not revise anything yet, right?

---

You did not respond to my question regarding PARAT so far, right?

---

So far, I believe my initial rating to be correct. I want to highlight that I very much appreciate the theoretical contributions that the paper makes. The answers in the rebuttal make clear that the authors have a very clear understanding of their contributions and the mathematical details are sufficiently supported in the appendix, although I did not check them carefully. However, I still feel the current form of presentation in the paper does not do this justice and strongly obscures the actual contributions.

If the authors are interested in my opinion beyond this review: Give this paper another iteration, remove PARAT completely, use the newly gained space to strengthen, especially the clarity of, the theoretical parts in the main paper + a convincing proof sketch for 4.5. If you feel like PARAT needs to be included, it needs to be clearer why, as this was also a concern in other reviews.

Given such improvements, which I feel go beyond the reasonable adjustments of a rebuttal phase, I clearly see this paper a worthy contribution!

Thanks for getting back to me, I do my best to address all you responses adequately, since the rebuttal phase is ending soon.

---

"We theoretically construct non-uniform decoder-only Transformers that can solve SAT using backtracking and deduction via Chain-of-Thought (CoT)."

What do you mean by "non-uniform" here? Am I right to assume what you want to say is " ... construct a class of decoder-only Transformers that can solve...."?

"decoder-only Transformers can solve 3-SAT”

Sorry, but I think that this short, informal statement oversells.

which is significantly more powerful than “given an arbitrary 3-SAT formula, there exists a decoder-only Transformer that can reason whether it is satisfiable.”

Ah, of course, sorry. That was wrongly stated by me, meaning that I switched the quantification. What I meant was "there is a Transformer T that given a 3-SAT formula ...".

I appreciate your extensive explanations regarding the three "levels of computation", but as stated above I never intended to suggest such a weak form of statement to be stronger. Sorry again for the typo!

Thank you for your careful review of the paper and for pointing out the important distinction between different interpretations of our theorems. We will answer your three questions and address your concerns separately in the following sections.

Q1: Concern Can Be Fixed via a Minor Revision

We fully agree that our theorem does not demonstrate the existence of a decoder-only Transformer that solves SAT, and our current expression in the abstract is flawed. Our theorem implies that different Transformer models are required for different input sizes of 3-SAT instances. The accurate statement would be: “We theoretically construct non-uniform decoder-only Transformers that can solve SAT using backtracking and deduction via Chain-of-Thought (CoT).”

However, after this minor revision, we believe that our claim that “decoder-only Transformers can solve 3-SAT” is well-founded, non-trivial, and follows the expression conventions of seminal works on Transformer expressiveness. In particular, our theorem considers the setting of non-uniform computation, which is significantly more powerful than “given an arbitrary 3-SAT formula, there exists a decoder-only Transformer that can reason whether it is satisfiable.” The non-uniform computation setting is also implicitly assumed throughout the relevant literature.

To support this claim, we will divide our arguments as follows:

1.1 Clarification of Our Theorem as a Non-Uniform Computational Model and Why It Is Non-Trivial

The dependence of the construction on the number of clauses $c$ demonstrates that a single Transformer model can achieve logical reasoning within bounded input length. However, this capability is already highly non-trivial. To demonstrate this, we first differentiate between different kinds of computation models:

1. Uniform Computation: There exists a single Transformer model that can solve all 3-SAT instances regardless of input size.

2. Non-Uniform Computation: Given any input size $n$, there exists a Transformer model that can decide all 3-SAT instances with input size up to $n$.

3. Given any input 3-SAT instance $x$, there exists a Transformer model that can decide $x$.

Option 3 best resembles your description of “given an arbitrary 3-SAT formula, there exists a decoder-only Transformer that can reason whether it is satisfiable.” This interpretation has a trivial proof of existence since we can simply construct a Transformer that outputs the constant string of the correct reasoning for that particular instance by encoding the exact string in the weights of the model. However, our theorem is strictly more powerful than this claim.

Option 1 is the strongest claim but, as we will elaborate in section 1.3, is very likely impossible for Transformer models.

Option 2 is a more realistic setting that is adopted by most works investigating Transformer expressiveness. In our case, the Transformer is only dependent on the maximum number of variables $p$ and the maximum number of clauses $c$, and is not dependent on the actual input instance itself, as in Option 3. Even if we only consider formulas with exactly $p$ variables and $c$ clauses (rather than “at most”), there are more than $p^{3c}$ possible 3-SAT instances that can be solved by a single Transformer model.

To illustrate this quantity and how it compares with the number of parameters in the construction, for the 20 max variable and 88 max clause Transformer we compiled for evaluation, our theorem implies that the single Transformer model is able to correctly reason about the satisfiability of more than $10^{343}$ possible SAT instances. However, the model only contains 5,011,862 parameters, which shows that it is impossible to trivially encode all reasoning paths for all possible samples as parameters of the Transformer. Therefore, our theorem implies that Transformers are capable of performing logical reasoning in the context of 3-SAT solving.

Our theoretical construction also depends on the maximum number of variables $p$. This is due to each variable requiring a unique token in the vocabulary. Therefore, the number of token embeddings and the embedding size have to be increased to account for a larger vocabulary size. Thus, having a different Transformer to account for larger vocabulary sizes is inevitable by design. However, in any given LLM with a fixed vocabulary, the actual number of variables involved in the formulas does not matter for our theoretical construction. Since all Transformers have predefined fixed-size vocabularies, the dependence of our Transformer on the number of variables $p$ is not a significant limitation in reasoning capability. Rather, the dependence on $p$ is due to the token-based processing design of Transformer models and can be ignored with a pre-defined fixed vocabulary.

Thank you for your timely response and acknowledging the contributions of our paper! It is true that we haven’t fully completed our response or updated the paper at the time of posting the previous replies. We wanted to post our partial written responses ASAP to facilitate timely discussion. We have updated the paper implementing the above mentioned changes now and attached our response to your final question in this response.

Regarding the first part of your response "What do you mean by "non-uniform" here", in section 1.1 of our response, we explained the concept of non-uniform as having different circuits for different input lengths. This is also a well-defined term in circuit complexity [9]. Regarding the claim that the short statement of “Transformers can solve 3-SAT” oversells, in the previous response 1.2 we explained how this form of expression is used in the expressions of many precious seminar works in Transformer expressiveness, but we agree that this may cause misunderstandings for readers regarding the exact contributions. Correspondingly, we have adjusted to expression to “construct a non-uniform class of decoder-only Transformers that can solve 3-SAT using….”

Again, we’re very grateful for pointing out important suggestions for our paper. Regarding your suggestions to remove PARAT completely, we fully agree that the engineering-focused PARAT compiler may not fully fit the theory-focused contributions of this paper and could instead be included in further work focusing on empirical contributions. However, the required structural changes may be too significant for the discussion period in the review phase. Instead, we will reduce the proportion focused on details of the compiler and add lemmas describing core theoretical contributions from the proof. Please see our updated manuscript for our efforts in this regard.

Please let us know if our responses have addressed your concerns and if you have any further questions. If possible, we would be very glad if you can update the score reflecting any updated evaluation regarding the contributions of our paper.

Q3 Definition of PARAT

We directly answer your question with the following definition:

PARAT Language

The syntax of the PARAT language is a restricted subset of Python with the NumPy library. Every variable $v$ in PARAT is an 2-D Numpy array of shape $n\times d_v$, where $n$ denotes the input number of tokens and $d_v$ is the dimension of PARAT variable $v$ that can be different for every variable $v$.

A pragram in the PARAT language is composed of a linear sequence of statements (i.e. no control flow allowed such as loops and branching), where each statement assign the value of an expression to a variable. Let v_1, v_2, … denote PARAT variable names, then each statement involving PARAT variables must be one of the following:

• Binary operations: v_1 + v_2 , v_1 * v_2, v_1 - v_2
• Index operations: v_1[v_2, :] , v_1[:, start:end] for non-negative integers start and end
• A function in our predefined library that takes as input PARAT variables

The input variables of a PARAT program for vocabulary size $V$ are tokens and indices , where tokens is a $V$ dimension PARAT variable including one-hot token embeddings of the input tokens and indices is a 1 dimension PARAT variable s-op including the numerical index of each input token (i.e. the array [[1], [2], …, [n]])

ParametricTransformer Compiler

The ParametricTransformer compiler takes in a program written in the PARAT language and a PARAT variable out of dimension $V$ and outputs a PyTorch Module object that implements a Transformer model as defined in Section 2 such that the following is satisfied: For any possible input sequence of tokens $s$ in the vocabulary, the token predicted by the Transformer model is the same as the token corresponding to out[-1, :].argmax() (i.e., the token prediction at the last position) when interpreting the PARAT program with the Python interpreter with the NumPy library

[9]https://en.wikipedia.org/wiki/Circuit_complexity#:~:text=Boolean circuits are one of,for all possible input lengths.

Thank you for your detailed review of the paper and insightful suggestions.

Include lemmas in the main paper

Thank you so much for pointing out the importance of including important lemmas in the main paper to emphasize our theoretical contribution. We fully agree with this statement and, after careful consideration of your and other reviewers’ feedback, decide that the details of the PARAT compiler are less important for this theory-focused work and instead should include more details on our theoretical contribution. In this regard, we included multiple definitions and lemmas that were extracted from our main proof and included in the main text. Please see our updated PDF for related changes. We’ll be very grateful if you can provide further comments and feedback on this updated section.

Fundamental question about whether LLMs can perform propositional reasoning

Thank you for pointing out that our statement of “propositional reasoning” is not exactly the same term as 3-SAT. However, we are slightly confused by the statement since SAT-Solving is equivalent to formal propositional reasoning. In the paper“Propositional Reasoning by Model”, which introduced the concept, propositional reasoning is defined as “deduction depending on if, or, and, and not”, which is encompassed by SAT. SAT-Solving is also linearly equivalent to 3-SAT, as demonstrated by the Tseitin Transformation, which shows that and SAT formula can be efficiently converted to an equivalent 3-SAT formula that’s linear in the original size. Therefore, our claim that our paper answers “a fundamental question about whether Transformers can perform propositional reasoning” is well-justified under the above equivalences. However, the sentences may indeed be unclear in meaning without further explanation of the concepts, and we have changed the statement to “a fundamental question about whether Transformers can perform propositional reasoning with the 3-SAT problem.”

Advantages compared to the Tracr Compiler

Thanks for pointing out that we haven’t explicitly stated the advantages of our compiler compared with the Tracr Compiler. The advantage of our compiler lies in increase expressiveness and reduced parameter complexity, which makes our compiler much more suitable for implementing complex algorithms with large input size.

In particular:

• Expressiveness: The PARAT language supports operations on 2-D arrays of size $n\times d_v$ where $d_v$ is a dimension specific to variable $v$ and $n$ is the input length. The RASP language for which Tracr is based on only supports operations on 1-D arrays of size $n$. Therefore, PARAT supports a more diverse set of operations than RASP. For example, the operation for checking satisfaction and detecting conflict can both be implemented with a single PARAT statement but have no simple implementation in RASP that we know of.
• Parameter Complexity w.r.t. Context Length: The ParametricTransformer Compiler generates Transformers uses a single embedding dimension to embed the position of each token, and the dependence of parameter number (excluding positional encodings) on the context length is $O(1)$. In contrast, the Tracr compiler uses $O(l)$ embedding size to create a one-hot encoding of each position for context length $l$ and results on $O(l^2)$ number of Parameters.
• Parameter Complexity for Arithmetic Operations: For basic binary arithmetic operations such as addition, subtraction, and multiplication of 1-D variables, a ParametricTransformer compiled model requires only $O(1)$ additional parameters. However, the Tracr compiler enumerates every possible value combination of the 2 operands, and as such requires $O(v^2)$ parameters for parameters that can take up $v$ possible values.

Please let us know if you concerns have been addressed and if you have further questions or comments.

Thank you for your detailed review of the paper and pointing our possible improvements for our current version of the paper. We will discuss your concerns in detail in the following section:

Limited Length Generalization is supportive of our theoretical results and experimental conclusions

We fully agree with the statement that the trained Transformer models demonstrate limited length generalization, and this phenomenon is supportive of our arguments in the paper. First, we would like to clarify that our core contribution is the theoretical result as stated in Theorem 4.5, and our experiments provide supplemental evidence on the capabilities of Transformers trained on the chain of thought used by our theoretical construction. Our theoretical result shows that, for any bounded length, a Transformer can decide all SAT instances within that length. However, the model weights need to be adjusted to account for longer-length inputs. Therefore, the experimental result that trained Transformers perform nearly perfectly within the training lengths but fail to length-generalize exactly fits our theoretical predictions, which is mentioned in lines 537 and 538. The limitation of trained Transformers in length generalization is explicitly stated as one of our experimental conclusions, as demonstrated by section 6.2 titled “limitation in length generalization”. As such, we believe that “Its accuracy declines significantly on SAT instances with up to 20 variables, possibly dropping below 50%” should not be considered a weakness of our work and is instead in support of both our theorems and our experimental conclusions.

Reasoning Process Evaluation

Thank you for pointing out that the reasoning process of the model may be erroneous even though the final SAT vs UNSAT prediction is correct. We fully agree that this is theoretically possible for purely random 3-SAT instances, and models may guess the correct SAT vs UNSAT solution using statistical properties without performing correct reasoning. However, we design our marginal evaluation dataset such as the SAT and UNSAT instances in the evaluation set differently by a single token. Therefore, the statistical properties between SAT vs UNSAT instances are in-differentiable (lines 424-427), and it is impossible for trained Transformers to achieve near-perfect accuracy without the capability for logical reasoning. Therefore, we do not believe that “even when predictions were correct, the reasoning steps might still diverge from the intended algorithm” weakens our experimental arguments on the intra-length out-of-distribution generalization capability of Large Language Models.

Baseline Comparisons and In-depth Error Analysis

Thank you for suggesting further experimental comparisons and analysis to better understand our model capabilities. We agree that these additional experiments may provide further insights into our trained and compiled models. However, we do not see a clear connection between the suggested experiments and our main arguments.

We would like to reiterate that our core contribution is theoretical (theorem 4.5), which demonstrates that Transformers are capable of solving the NP-hard logical reasoning problem 3-SAT, and the experiments provide supplemental evidence to validate our theoretical results. Towards this end, we performed experiments to demonstrate that the theoretical upper bound indeed holds in the implementation of our theoretical construction, and demonstrates that trained Transformer models achieve near-perfect intra-length OOD generalization but have limitations in length generalization.

Therefore, we believe that providing an in-depth error analysis of the trained Transformers does not directly provide additional evidence for our theoretical results and may distract readers following the main argument flow since our theoretical argument does not concern failure modes of Transformer models. We also do not intend to compete with practical SAT-solvers and instead focus on whether Transformers can perform correct propositional reasoning, as stated in the contributions section. Therefore, comparing with a standard DPLL does not seem to contribute to our core argument.

Again, we are very thankful for your insightful and detailed reviews and would like to clarify potential misunderstandings of our paper. Please let us know whether our explanations suffice to address your concerns and if you have further comments and we gladly welcome further discussions.

We greatly appreciate the effort you put into reviewing the paper and thank you for pointing out a potential point of confusion regarding the exact contributions of PARAT. We acknowledge that our current description of PARAT contains informalities that may lead to confusion regarding our contributions. Therefore, we would like to clarify the potential misunderstanding indicated in your review regarding the purpose of the code samples we provided and the PARAT compiler.

Our main contribution in the PARAT section is the compilation process of array operations expressed in PARAT into Transformer model weights. Therefore, the resemblance of PARAT code with NumPy operations does not render our contributions trivial. PARAT is designed to resemble a “NumPy-like array manipulation syntax”; therefore, many code statements we provide in the paper and appendix are also valid NumPy operations on arrays. However, the purpose of the compiler ParametricTransformer is not to execute the code on given inputs. Instead, the provided PARAT code serves as the input to the compiler, and the compiler produces a Transformer model in PyTorch as output. This output model implements the same computations as those described in the input code when the model takes in a sequence of tokens as input.

Therefore, we respectfully disagree with the claim that our contribution of PARAT is “akin to deception” and would like to clarify our intent. While the implementation of the PARAT language and compiler is based on Python, we believe this was implicitly clear given the context and the references to PyTorch and NumPy. Python has been the de facto programming language for most code associated with deep learning. Furthermore, we explicitly stated that our compiler “outputs a PyTorch model” and that the syntax of PARAT is designed “akin to NumPy,” both of which are well-known Python libraries.

Additionally, the main contribution of the paper is the theoretical result that Transformers can solve SAT. Both the compiler and the experiments provide supplemental evidence to verify several predictions of our theorems. We hope that the reviewer finds the major conclusions of our work compelling, as they represent the primary contributions of our paper.

Thank you again for your review. We are happy to address any further questions you may have.

We’re greatly thankful for your acknowledgement of the strengths and contributions of the paper. Also, thanks for pointing our the description inconsistencies between the figure and section 6.2. The Figure description is accurate (i.e. Trained on different distributions and evaluated on marginal only), and we have fixed section 6.2 accordingly.

For the 2 questions you posted, both of them are insightful and important questions regarding our paper. However, we find them difficult to answer directly due to several technical details. Therefore, we will first explain the technical context related to these questions and provide the closest answer to your question according to our understanding.

Finally, we would greatly appreciate if you could provide some comments on the discussion threads of other reviewers.

1. DPLL CoT Length

Technical context:

• The number of steps of the DPLL algorithm is not a well-defined concept, even though this can be easily defined as the number of Chain-of-Thought tokens for a decoder Transformer model. Our theoretical construction uses Chain-of-Thought to simulate various high-level operators performed by the DPLL algorithm, as summarized by abstract DPLL state transition system, but even so each transition may be simulated by more than one token in the Chain-of-Thought
  • We believe what you’re referring to in the question is the number of tokens of a Chain-of-Thought that trace-simulates a concrete run of the DPLL algorithm they way illustrated in Figure 1 in the paper
• Dependency on branching heuristic The performance of the DPLL algorithm is heavily dependent on a branching heuristic function, which selects decision literal (i.e., the variable picked to assume a truth value) from all unassigned variables when no deduction is possible. Therefore, there is no exact number of steps for the general DPLL algorithm without a specific heuristic. Our theorem proves that our theoretical construction’s CoT is trace equivalent to an DPLL algorithm with a particular heuristic (approximation of the Maximum Occurrences on clauses of Minimum size (MOM’s) heuristic).
  • Therefore, to answer the first part of your question

With the above assumption, here we present the maximum number of tokens for a DPLL algorithm with the Jeroslow-Wang (JW) Heuristic vs our compiled model:

Marginal:

Random:

Skewed

While not always the case, the DPLL with JW heuristic generally uses less corresponding CoT steps than our theoretical construction. This shows that the branching heuristic in our Theoretical Construction is still less efficient than the JW heuristic.

2. Accuracy on more than 20 variables

• Our compiled model for 20 variables only includes token embeddings for the 20 variable tokens. Therefore, if we were to attempt to solve a 21-variable formula, then it will not have the corresponding token embedding for variable 21 and will result in an error.

Instead, we can investigate models with a sufficient number of variable tokens but designed for a smaller number of clauses(i.e., smaller $c$ value in Theorem 4.5). Different $c$ values correspond to different scaling factors for the attention weights, which is represented by $\beta$ and explained in the “Soft vs Hard Attention” paragraph in section 5.2. As such, we can investigate your proposed question by adjusting smaller $\beta$ values of a model designed for a larger number of variables and clauses. We have indeed investigated our compiled model from this aspect in Figure 4. In this figure, you may observe how models without sufficient $\beta$ parameter perform on formulas with different lengths.