Can Transformers Reason Logically? A Study in SAT Solving

We thank the reviewer for their detailed feedback. We’re grateful for your acknowledgment of the soundness of our construction and the relevance of the experiments. We would like to focus on your primary concern regarding novelty compared to Turing Completeness (TC) results.

While we agree that TC of Transformers with CoT implies that, in principle, simulating algorithms like DPLL is possible, we believe this perspective overlooks the core contributions and significance of our work. Allow us to elaborate:

Beyond Turing Completeness: The "How" Matters

Our work, like previous works on Transformer expressiveness, aims at advancing our understanding of the capabilities and mechanisms of Transformer models in reasoning. Previous TC results rely on step-by-step simulations of single-tape Turing Machines (TM), which are theoretically foundational but don't well-explain how logical reasoning is performed internally in Transformers. I.e., Many reasoning phenomena of LLMs remain poorly explained by TC alone.

Consider an analogy: Mathematical theorem proving (e.g., solving IMO problems) can be framed as search problems over LEAN proofs. If LLMs are TC, does this make their success on math benchmarks unsurprising or non-novel? We argue no. The interest lies in how LLMs solve these problems – potentially using more efficient, structured reasoning mechanisms than TM simulation. Our work moves beyond TC by asking how a Transformer can efficiently simulate a specific, non-trivial logical reasoning procedure (DPLL for 3-SAT) using its inherent architectural features. We provide an explicit construction and demonstrate a concrete CoT mechanism.

Novelty in Parallelism via Attention

As highlighted in your review, a key novelty is demonstrating how Transformers use parallelism effectively. We provide the first theoretical evidence that the attention mechanisms in Transformers can support parallelism for logical reasoning. This suggests that the Transformer models can be particularly suitable for deductive logical reasoning in large contexts. In particular, Lemma 4.8 shows that a single Transformer head can perform satisfiability checking, conflict detection, and unit propagation, respectively overall all clauses in parallel.

Novelty in CoT Efficiency and Structure

While the reduction in CoT tokens compared to TM simulations might seem “reasonably expected”, anticipated theoretical results still significantly benefit from formal proofs—analogous to widely believed mathematical conjectures (e.g., P ≠ NP).

Our CoT simulates DPLL at an abstraction level higher than TM emulation, explicitly representing logical reasoning steps of assumption, deduction, and backtracking.

Furthermore, we formally provide an explicit upper bound (p·2^(p+1)) on CoT length (Theorem 4.5), a contribution extending beyond mere TC results. In particular, such upper bounds for TC results are unknow for 3-SAT.

Preliminary Section Clarity

Regarding your suggestion on swapping the preliminaries section for background on 3-SAT and DPLL, this is indeed a greatly helpful suggestion for readability, and we will certainly do that during revision. In particular, we will swap the preliminary section on transformers with Appendix C.1 on 3-SAT after rewriting for brevity.

Questions

The main connection between the experimental results is the shared Chain-of-Thought design. Our theoretical construction provides a specific CoT structure. The experiments then investigate whether Transformers can learn this structure from data. The strong intra-length OOD generalization (Table 1) suggests that training on this theoretically-grounded CoT does allow the model to learn a robust reasoning procedure applicable across different data distributions, overcoming limitations seen in prior work where models trained with CoT relied on statistical shortcuts [1].

We agree that additionally investigating the accuracy of models of different sizes trained on 3-SAT problems with Chain-of-Thought is an interesting and insightful direction of experimental investigation according to the $O(p^2)$ scaling of our theorems and aligns with the “scaling law” line of research. However, such experiments are computationally beyond our theoretical focus and available resources.

As you mentioned in the review, Transformer models would introduce significant overheads compared to modern SAT-solvers. Having that said, it may be possible to develop efficient parallelized SAT-solver operations such as unit propagation, satisfiability checking, and conflict detection on GPU architectures using the insights from Lemmas 4.7 and 4.8. Our construction may also be used as a differentiable SAT-solving component that allows LLMs to formulate the underlying logic within natural language reasoning traces as SAT formulas and use traditional SAT solvers to perform more reliable reasoning.

[1] Zhang, et al. On the paradox of learning to reason from data. IJCAI '23

Thank you for your devoted time in reviewing the paper. We're glad that you found the writing and experimental results of our work satisfactory.

To verify the logical reasoning capabilities of decoder-only Transformers, It would be good to add research on other types of SAT problems.

The suggestion is highly insightful! Including more complicated SAT instance structures beyond CNF formulas may reveal further insights into more complicated Transformer reasoning, especially when processing hierarchical data. This is currently beyond the scope of this work, and we would certainly look into these directions in future work. For the present work, since it’s well known that all SAT formulas can be converted into 3-SAT in polynomial time, and we are the first theoretical work investigating the capacity of Transformers in formal logical reasoning, we believe that our current contributions are sufficient for the current manuscript.

Beides random instances, how does the method perform on industrial instances (e.g., those instances from SAT Competitions)?

Regarding your question, we fully acknowledge the importance and impact of practical SAT solving, but we would like to clarify that our goal is to advance our theoretical understanding of the reasoning capability of Transformer models. Practical SAT solving is orthogonal to this work and our goal. We chose 3-SAT as the theoretical basis for our study because it’s a fundamental NP-complete problem in complexity theory that represents deductive logical reasoning. It is unlikely that our model will have any practical advantage over traditional SAT solvers. The DIMACS encoding and CoT of practical instances are significantly longer than the context lengths of our models. Therefore, we did not use any practical SAT benchmarks for evaluation.

We’re happy to answer any additional questions you may have regarding our work. We also sincerely hope that you can evaluate the theoretical aspects of contributions in more detail if possible.

We greatly thank you for the detailed comments and feedback. We appreciate the reviewer’s careful reading and insightful concerns. We seek to clarify certain potential logical misunderstandings, hoping to address your identified concerns regarding the theoretical results. Most importantly, the correctness of Theorem 4.5 is justified by the proof in Appendix C, rather than the experimental results.

Theorem 4.5 and Theorem 1.1 cannot hold based on the experimental results, where the Transformer models fail to generalize to instances with more than 12 variables.

Mismatch between theorem and empirical results. Theorem 4.5 claims …

We fully appreciate the reviewer’s detailed review. However, we kindly clarify that Theorem 4.5, which shows the existence of a Transformer model that solves SAT, refers explicitly to the Transformer weight configuration rigorously defined in Appendix C. The empirical models, which showed limited generalization beyond 12 variables, were trained from data and thus had fundamentally different weight configurations. The configuration corresponding to Theorem 4.5 and described in Appendix C.6 is also implemented and corresponds to the "Compiled" results presented in Figure 3 and Section 5, achieving perfect accuracy on all tested instances. Again, we note that while such perfect accuracy is implied by Theorem 4.5, no amount of empirical tests can justify the correctness of Theorem 4.5. The experiment results for the compiled model only serve as a “sanity check” on smaller instances. Instead, the correctness depends on the Proof presented in Appendix C. Thus, the empirical limitations in generalization of the trained models and the number of variables in the tested formulas do not contradict our theoretical claims.

Lack of formal justification for model hyperparameters (L=7, H=5). It seems that Appendix C.6 is the corresponding proof…

We would like to clarify that these hyperparameters are indeed rigorously justified through the theoretical construction explicitly presented in Appendix C.6. Specifically, the configuration of the theoretical construction is provided between lines 1363 and 1469, detailing how each of the 7 layers explicitly contributes to achieving the theoretical result. The 5 heads stem from the fact that the operations in layer 5 require 5 attention heads to complete, and the number of attention heads must be the same across all layers by definition of the Transformer architecture. The operations are described at a high-level, and each individual operations have a corresponding lemma in previous sections on how the operations can be represented as attention or MLP layers. Also, we do not claim that the 7 layers and 5 heads are minimal for SAT solving, but rather an upper bound on the number of layers and heads required to solve 3-SAT.

Line 1358 mentioned in your review describes the “embedding layer” of the construction, which converts each token to input vectors before layer 1.

On the possibilities of ablation studies, while ablation studies are typically valuable in empirical research contexts for determining the influence of each component of a machine learning model, they are not applicable to theoretical proofs.

while Appendix C.6 appears to provide a detailed analysis of Theorem 4.5, this link is not explicitly stated in the main text.

In lines 238-239 of the main text, we mentioned that the proof of Theorem 4.5 is in Appendix C, and Appendix C.6 is not only a “detailed analysis” of Theorem 4.5 but a part of its proof that describes the construction.

The additional experiments in Appendix B are not clear.

Thank you for pointing out the missing references to the Figures from the main paper! For the experimental result in the appendix, Figure 5 corresponds to question 3, “How does error induced by soft attention affect reasoning accuracy?” on lines 322-323 (right), while Figure 6 adds the experimental results on the 2 remaining evaluation datasets, Random and Skewed, compared to Figure 3 in the main text. Thank you for pointing out the missing references to these figures in the main text. We will update the paper to clarify and add references to the additional experiment results.

Does it suggest that self-attention-based models are inherently limited in practical scenarios?

Our work focuses on advancing our theoretical understanding of the capabilities of Transformers in logical reasoning rather than how Transformers can be used for practical SAT solving. Our results show that given the number of variables and clauses, it’s possible to construct a Transformer model that solves 3-SAT. These models indeed have efficiency limitations compared to traditional SAT-solvers like CDCL and DPLL. Having that said, it might be possible to design for efficient SAT-solving mechanisms by exploiting the parallelism introduced in Lemma 4.8 and GPU architectures.

We’re very grateful for your devoted time and careful review of both the main paper and the appendix. We’re also very glad that you liked the contributions of our paper and consider the proof and description in the appendix rigorous and helpful. We would like to address your comments regarding the difficulty of understanding the proof sketch and your opinion of possible improvements to its clarity, suggested below:

Clarity Improvements to the Proof Sketch

Swapping Preliminary Section on Transformers with Appendix C.1 on 3-SAT (also suggested by reviewer sNWz): From your reviews as well as suggestions from reviewer sNWz, we believe that the most unclear part in the main paper is likely regarding 3-SAT operations and DPLL. As such, we will swap out the detailed mathematical definitions of the Transformer architecture in section 2 with descriptions of 3-SAT in Appendix C.1

Organize Proof Sketch around Major Steps in the Construction: For Section 4, we would like to organize the sketch around the multiple major steps of the Transformer model? i.e., we organize into the following paragraphs:

Step 1: Summarize Clauses and Assignments as Binary Vectors: where we introduce definition 4.6 and explain how the binary encodings can be computed by summing up one-hot encodings in each clause using the attention mechanism of the Transformer

Step 2: Perform Parallel Logical Operations over Clauses: where we introduce Lemmas 4.7 and 4.8 and explain how to determine Satisfiability, Conflict, and Unit Propagation

Step 3: Next Token Prediction: where we have a description on how the final token is decided based on the results calculated in the previous layers

Example on line 1355

Thank you for your careful reading of the appendix. After careful checking, the example is indeed wrong. The correct solution should be: [SEP] D 2 D 1 -4 3 [BT] D 2 -1 -4 [BT] -2 D 3 D 4 1 SAT We will also update this in the paper.

Questions

Can the authors provide insights into the characteristics of SAT instances where the model’s CoT length approaches this worst-case behaviour and how often such instances can occur realistically?

We expect all instances to be lower than this bound, but we do not know of tighter upper bounds that are strictly proven. The number of CoT steps required is dependent on many factors, including the heuristic used to select the next decision (assumption) at each iteration, etc. Providing tighter theoretical upper bounds on solving different types of SAT formulas is an active direction of research in the SAT solving community (e.g., see [1] Section 1.5). We instead used a large upper bound that is guaranteed to be true on all instances and heuristics.

Can it be assumed that having more compute during test-time would allow the models better generalization w.r..t. the number of variables?

We do believe this to be true according to relevant literature on practical LLMs, where longer CoT leads to better reasoning performance. However, it’s difficult to empirically test this hypothesis in our setting since there isn’t a reliable way to increase test-time computation for custom-trained 3-SAT models. In particular, our models are deterministic and do not support additional prompts to elicit longer reasoning chains. Your suggestion is indeed an insightful and promising direction for future work.

What happens as the CoT gets longer? Do the models collapse and start repeating explored patterns? Do they hallucinate?

Yes. We can investigate this phenomenon by observing how models trained on large (11-15) instances behave on smaller instances. For example, on a 3-SAT problem with 5 variables, the model outputs: (recall that D represents “Assume” and [BT] represents “BackTrack” according to Appendix C.1)

D -4 D -1 -5 2 3 D [BT] D -4 D -1 -5 2 3 D -4 D [BT] D -4 D -1 -5 2 3 D -4 D -5 SAT

The model can be considered to be hallucinating since the final D at the end of the first attempt should never occur. Similarly, at the final assignment before SAT, both -4 ($x_4=F$) and -5 ($x_5=F$) occurred 2 times, which shows that the model starts repeating explored patterns. Both of these phenomena are quite common when the CoT is longer than normal.

In another test sample of 5 variables, the model outputs:

D -4 D -3 1 2 -5 -4 -18 17 -26 SAT

Which hallucinates variables that do not exist in the formula (and also outputs -4 twice).

What’s more interesting is that the models still have high SAT vs UNSAT accuracy even when these hallucinations/repetitions occur and our test data explicitly removes statistical evidence on SAT vs UNSAT. This can be seen from Figure 3 (right) where the SAT vs UNSAT accuracy remains high even when the Full Trace Correct accuracy falls off significantly. It seems that the trained model still has ways to “guess” the correct SAT vs UNSAT even with a CoT that’s not fully correct and longer than normal.

[1] On The Unreasonable Effectiveness of SAT Solvers