Can Transformers Reason Logically? A Study in SAT Solving

Authors: Leyan Pan, Vijay Ganesh, Jacob Abernethy, Chris Esposo, Wenke Lee
Primary area: foundation or frontier models, including LLMs
Keywords: Transformer LLMs, Logical Reasoning, Chain-of-Thought, SAT Solving, Backtracking

Abstract:
We theoretically and empirically study the logical reasoning capabilities of LLMs in the context of the Boolean satisfiability (SAT) problem. 
First, we construct a non-uniform class of decoder-only Transformers that can solve 3-SAT using backtracking and deduction via Chain-of-Thought (CoT). We prove its correctness by showing trace equivalence to the well-known DPLL SAT-solving algorithm. Second, to support the implementation of this abstract construction, we design a compiler PARAT that takes a procedural specification as input and outputs a transformer model to implement this specification. Third, rather than programming a transformer to reason, we evaluate empirically whether it can be trained to do so by learning directly from algorithmic traces (``reasoning paths'') of the DPLL algorithm.

Decision: reject
Reviewer scores: 8, 3, 5, 5, 5

Reviews and discussion:
<thread>
creation date:
1730219474556

thread_type:
official_review

<thread_object>
creator: reviewer_6fmx

<content>
summary:
The paper contributes to research on understanding the reasoning capabilities of transformers when using the chain of thought. Its contributions are threefold:
- It asserts that a decoder-only transformer can, in principle, solve Boolean SAT using the chain-of-thought to reason similar to the DPLL algorithm.
- It introduces PARAT, described as a "compiler that takes procedural specifications as input and outputs a transformer model that implements these specifications."
- It empirically explores whether a transformer can be trained to solve SAT problems.

strengths:
- Investigating the reasoning capabilities of transformers, particularly concerning formal 
problems, is highly valuable.
- Boolean satisfiability serves as an appropriate baseline candidate.
- Supporting the initial contribution of theoretical expressiveness with experiments that 
provide a practical perspective is a sound approach.

weaknesses:
My main concerns regard the first two contributions. I categorize the weaknesses based on the contributions of this paper and order them from most important to least important in each category. 

### Transformers with CoT solve SAT
- The claim of the paper may be perceived as somewhat misleading. While it states, 
  "we construct a decoder-only Transformer that can solve SAT," the actual result 
  (Theorem 1) is that "for any $p,c \in \mathbb{N}^+$ there exists a decoder-only Transformer 
  with [...] that can decide all 3SAT instances of at most $p$ variables and $c$ clauses using CoT." 
  This is correctly described as the construction of a decoder-only Transformer for 
  a bounded version of 3SAT. Alternatively, Theorem 1 implies that the class of all 
  decoder-only Transformers solves the general 3SAT problem: given an arbitrary 
  3SAT formula, there exists a decoder-only Transformer that can reason whether it is satisfiable. 
  The distinction is significant, as this contribution of the paper is directed towards proving 
  that a single decoder-only Transformer exists for solving SAT. In fact this is not implied by Theorem 1.
- Definition 4.3 could benefit from clarification. While the intended meaning might be inferred, 
  there remains uncertainty due to the probabilistic nature of the map computed by a decoder-only 
  transformer. The pivotal question is ensuring the decision procedure always 
  terminates. It appears that a parameter may be absent in this definition, one that would 
  guarantee termination after a predetermined length if an end-of-sequence token does not 
  appear.
- The intuition behind the Transformer template constructed for Theorem 1 needs improvement.
  While Figure 1 is comprehensive, despite being oddly distant in placement within the paper, 
  the explanations from line 277 to 300 are overly abstract. Specifically, lines 288 to 294 
  lack clarity, making it difficult for the reader to grasp their meaning. This may confuse 
  the reader more than it helps.

### Parat
- The main concern is that the paper struggles to clearly define what PARAT is. The initial description 
between lines 85 to 87 reads, "We design PARAT, a compiler of high-level sequence operations in Numpy-like 
syntax into Transformer model weights, to empirically validate and analyse theoretical constructions of 
Transformer algorithms." However, there is ambiguity surrounding the terms "compiler", "high-level sequence operations", "Transformer model weights", and "Transformer algorithms". Further on line 306, it states, "... a framework for converting theoretical constructions of Transformers into practical models ...". Yet, it remains unclear what is meant by "theoretical constructions of Transformers" and how these relate to "high-level sequence operations". The first detailed exposition of PARAT (commencing with section 5.1) immediately delves into features and operations, leaving a reader, such as myself, completely perplexed as to what it truly encompasses.
- Without addressing the aforementioned ambiguities, it remains unclear why PARAT's contribution is significant for exploring the reasoning capabilities of Transformers, the paper's primary objective. While it appears to be a useful tool, developed with considerable effort, it seems to distract from the main aim of the paper and takes up space that could be used to better elucidate the first contribution.

questions:
Having shared broad and high-level concerns regarding the paper, I encourage the authors to address these directly. 
Here is a summary of the key points:
- Do you agree that your theoretical contributions do not demonstrate the existence of a decoder-only Transformer that solves SAT? Do you believe this could be resolved with minor revisions, and if so, how would you approach this?
- How do you ensure the decision procedure in Definition 4.3 always terminates? What considerations 
lead to defining the "semantics" of a decoder-only transformer as mapping to a probability 
distribution? Is this crucial? If I am not mistaken, this perspective somewhat diverges from research 
addressing the expressiveness of transformers, such as the paper "Attention is Turing-complete", which you cite, or studies focusing on the expressiveness of single-pass or encoder-only transformers.
- Can you provide a clear and concise definition of what Parat is?
</content>
</thread_object>

</thread>
<thread>
creation date:
1730306135487

thread_type:
official_review

<thread_object>
creator: reviewer_pkf5

<content>
summary:
This paper provides a theoretical analysis of the Transformer's ability to solve 3-SAT problems through chain of thoughts, along with a compiler that can output a Transformer model satisfying a given specification. The empirical results demonstrate that the Transformer can achieve high accuracy in solving small-scale 3-SAT problems.

strengths:
The problem tackled in this paper is highly interesting and relevant. I appreciate the effort of theoretical analysis conducted on the reasoning capabilities of transformer models, which is a rapidly evolving and impactful area of AI research.

weaknesses:
This paper has several issues that need to be addressed.

First, the paper's introduction claims to answer a "fundamental question about whether LLMs can perform propositional reasoning." However, after reviewing the paper, it does not appear that the theoretical and empirical analysis provided is sufficient to conclusively answer this broad question. The analysis is focused narrowly on 3-SAT problems, and it is unclear how the results could be generalized to other propositional reasoning problems. Additionally, the model used in the experiments may not be representative of a typical large language model with billions of parameters.

Second, the proofs for the theorems presented in Section 4 are missing. While it is possible the proofs require additional space, it is necessary to at least provide a high-level outline of the proof approach in Section 4. Purely moving numerous lemmas and proofs to an appendix is an unsatisfactory way to present such a crucial part of the paper.

Third, the incremental contribution of the proposed compiler compared to the prior Tracr compiler is unclear. It appears that the primary focus of this work is on addressing implementation issues with Tracr, but the specific novel aspects are not well articulated. The paper should clearly explain what new capabilities or improvements are offered by the proposed compiler over the previous work.

questions:
What is the incremental contribution of the proposed compiler compared to the prior Tracr compiler?
</content>
</thread_object>

</thread>
<thread>
creation date:
1730716254394

thread_type:
official_review

<thread_object>
creator: reviewer_peeh

<content>
summary:
This paper investigates the logical reasoning capabilities of Transformer models in solving SAT problems. The authors designed a decoder Transformer to emulate the DPLL algorithm, tackling SAT through variable selection, conflict detection, and backtracking. The PARAT compiler translates high-level procedural logic into model weights, enabling practical implementation.

strengths:
1. Leveraging a Transformer to simulate the entire DPLL SAT-solving process, rather than focusing on optimizing specific heuristics such as variable selection, represents a novel approach.
2. The paper presents the PARAT compiler, which translates the procedural logic of the DPLL solving process into a Transformer model, achieving perfect accuracy on SAT problems with up to 20 variables and 88 clauses.
3. The trained model sustains high accuracy on SAT test instances with variable counts comparable to those in the training dataset.

weaknesses:
1. The evaluation assessed only the accuracy of satisfiability predictions, without examining the correctness of the reasoning process itself. Thus, even when predictions were correct, the reasoning steps might still diverge from the intended algorithm. Additionally, there was no in-depth analysis of the accuracy drop on larger SAT instances to identify if errors arose from issues in conflict analysis, backtracking, or other specific areas.
2. The experiments compared the Chain-of-Thought (CoT) length solely with theoretical upper bounds, without including baseline comparisons. Evaluating against the reasoning steps of a standard DPLL solver or other baselines could offer a clearer perspective on the model’s reasoning capabilities.
3. The trained model shows limited generalization, performing well only on test instances with variable counts similar to those in the training data. Its accuracy declines significantly on SAT instances with up to 20 variables, possibly dropping below 50%.

questions:
The model demonstrates poor generalization, achieving high accuracy only on SAT instances with variable counts similar to those in the training data. Performance significantly declines on larger instances, indicating that it may be learning patterns specific to the training data rather than pure logical reasoning, thus failing to fully substantiate the claim that Transformers are capable of logical reasoning.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730721639115

thread_type:
official_review

<thread_object>
creator: reviewer_faul

<content>
summary:
This work investigates the application of the Transformer architecture for SAT solving. 
To this end, the authors present theoretical boundaries on decoder-only Transformers' size and solving capabilities in 3-SAT problems.
Furthermore, they introduce "Parametric Transformer" (PARAT) to create and evaluate the SAT-solving model.
The evaluation itself consists of a simulation study where 3-SAT problems with varying numbers of variables have been generated as a benchmark.
The authors show how their compiled model is able to solve all problems with perfect accuracy, while models that were trained instead fail when challenged with problems of previously unseen numbers of variables.

strengths:
The authors present how a 3-SAT solving algorithm can be expressed within the confinements of the building blocks of the Transformer architecture and demonstrate that it remains accurate across varying numbers of involved variables and clauses.

weaknesses:
The contribution and significance of PARAT remained unclear to me after considering both the main text and appendices. 
The authors claim that PARAT "is designed to provide an intuitive syntax resembling standard numerical array manipulation, akin to NumPy, [...]" (page 6, line 311). 
Considering the referenced "ParametricTransformer Code" in Appendix D, it becomes evident that the language in question is pure Python using the numpy library. 
The language "Python" is named not once in the paper, and the formulation of contributing a "compiler" with the notation "akin to" numpy and PARAT's "NumPy-like Array Syntax" (page 6, line 314) seems completely unjustified and bordering on deception.

questions:
I have no questions for the authors.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730840515322

thread_type:
official_review

<thread_object>
creator: reviewer_dcji

<content>
summary:
This paper investigates the capabilities of LLMs to solve an NP-complete problem, the 3-SAT problem. The authors first prove by construction that LLMs can simulate the DPLL algorithm to solve the 3-SAT problem with a bounded number of variables. To support this theoretical argument, they also compiled a Transformer implementation from the construction, which perfectly solved the bounded 3-SAT problems in their evaluation. A further empirical investigation demonstrated that, instead of by construction, LLMs could learn to solve the bounded 3-SAT problems whereas they are unable to generalize to problems with more variables. This observation matches the limitation of the theoretical construction requiring a bounded number of variables for 3-SAT problems.

strengths:
1. This is the first work to study the capabilities of LLMs to solve NP-complete problems.
2. This paper proves by construction that LLMs can simulate the DPLL algorithm to solve the 3-SAT problem with, though, a bounded number of variables. It demonstrates that Transformers can perform unit propagation and backtracking, which are the core operations of the DPLL algorithm.
3. To support the theoretical argument, the authors also developed a compiler to compile the theoretical construction into a Transformer implementation and verified its practical capability to perfectly solve bounded 3-SAT problems.
4. The evaluation results match the theoretical statement. The main theorem implies that Transformers can perfectly solve 3-SAT problems with a bounded number of variables. In the evaluation, they also observed near-100% accuracy over problems with a bounded number of variables whereas the accuracy dropped significantly as the variable number further increased.

weaknesses:
1. The main theorem implies that an arbitrarily large LLM is required to simulate a general DPLL algorithm for solving all 3-SAT problems. Considering a bounded program (a program of a specific size) can implement the general DPLL algorithm, it is still unclear how to approach the general DPLL algorithm using a bounded LLM.
2. The experiment setting in Sec 6.2 contradicts the description of Figure 2. Sec 6.2 states that the model is trained on the Marginal dataset and evaluated on the three generated datasets while Figure 2 describes the other way.

questions:
1. What is the maximum number of steps, w.r.t. the variable number, for running DPLL over the generated 3-SAT problems? How does it compare to the empirical maximum CoT length?
2. What is the accuracy of the compiled model on instances with more than 20 variables, i.e. beyond the guaranteed upper bound? Does the accuracy drop drastically?
</content>
</thread_object>

</thread>


Metareview:
metareview:
This paper investigates how well LLMs can solve the 3-SAT problem. In particular, it constructs a decoder-only Transformer to solve SAT using backtracking and deduction via Chain-of-Thought (CoT). The reviews agree that this is overall an important question. Unfortunately, there is also much confusion here that should be clarified before publication. First, it is not true that this is the "first work to study the capabilities of LLMs to solve NP-complete problems," as one reviewer argued, as the following selected pointers to SAT works show:

https://github.com/casmlab/NPHardEval

Zhengyuan Shi, Min Li, Yi Liu, Sadaf Khan, Junhua Huang, Hui-Ling Zhen, Mingxuan Yuan, Qiang Xu: SATformer: Transformer-Based UNSAT Core Learning. ICCAD 2023: 1-4
https://arxiv.org/abs/2209.00953

Minyu Chen, Guoqiang Li, Ling-I Wu, Ruibang Liu, Yuxin Su, Xi Chang, Jianxin Xue:
Can Language Models Pretend Solvers? Logic Code Simulation with LLMs. SETTA 2024: 102-121
https://arxiv.org/html/2403.16097v1

Jundong Xu, Hao Fei, Liangming Pan, Qian Liu, Mong-Li Lee, Wynne Hsu:
Faithful Logical Reasoning via Symbolic Chain-of-Thought. ACL (1) 2024: 13326-13365

Second, in the feedback to one of the reviewers, the author argue that there is a potential misunderstanding that the paper  <<“investigates the application of the Transformer architecture for SAT solving,” whereas our primary focus is to “answer a fundamental question about whether LLMs can perform propositional reasoning,” which is a different>> To be honest, I do not see how this is different. 3SAT is NP-complete, and SAT solvers are equal to "propositional reasoning". That is also, I guess, why the abstract refers to 3SAT and SAT solvers. Finally, one reviewer points out that the "evaluation assessed only the accuracy of satisfiability predictions, without examining the correctness of the reasoning process itself." While I see the general argument of the authors provided in the rebuttal, adding such an experiment would improve the papers. Overall, this is a borderline case, and due to many open issues and missing related work, I recommend pushing for one of the next venues. Please note that this decision should not be taken as a statement regarding the usefulness of your research.