Can Transformers Reason Logically? A Study in SAT Solving

TL;DR

This paper investigates the logical reasoning capabilities of decoder-only Transformers for SAT problems, proving their theoretical ability to decide 3-SAT and empirically evaluating their training and generalization properties.

Contribution

It provides a formal proof that Transformers can decide 3-SAT using backtracking and Chain-of-Thought, and introduces a tool to empirically verify and analyze this reasoning ability.

Findings

Transformers can decide 3-SAT in a non-uniform model.

Trained models generalize well to seen problem sizes.

Limited length generalization observed in trained models.

Abstract

We formally study the logical reasoning capabilities of decoder-only Transformers in the context of the boolean satisfiability (SAT) problem. First, we prove by construction that decoder-only Transformers can decide 3-SAT, in a non-uniform model of computation, 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, we implement our construction as a PyTorch model with a tool (PARAT) that we designed to empirically demonstrate its correctness and investigate its properties. Third, rather than \textit{programming} a transformer to reason, we evaluate empirically whether it can be \textit{trained} to do so by learning directly from algorithmic traces (``reasoning paths'') from our theoretical construction. The trained models demonstrate strong out-of-distribution generalization on problem sizes seen during training but has limited length generalization, which is consistent with the implications of our theoretical result