Can Transformers Reason Logically? A Study in SAT-Solving

Transformer-based LLMs have apparently demonstrated capabilities that resembles human reasoning. In our recent work, we investigated the Boolean reasoning abilities of decoder-only Transformers equipped with Chain-of-Thought, establishing that a Transformer model can decide all 3-SAT instances up to a bounded size (i.e., number of variables and clauses). In this talk, I will first review recent studies that formally examine the expressiveness of Transformer models. Next, I will explain how we establish an equivalence between Chain-of-Thought reasoning and algorithm, in our case, the DPLL SAT-solving algorithm. I will then discuss how to encode 3-SAT formulas and partial assignments as vectors so that the high-level operations in DPLL can be represented as vector operations and implemented using attention mechanisms within Transformers. Finally, I will present experimental results that support our theoretical predictions. I will also address why standard Transformers can only solve reasoning problems of bounded length, leading to failures in length-generalization, and discuss potential solutions to overcome this limitation.

In person or on Zoom:

https://harvard.zoom.us/j/92220006185?pwd=V3mrb4cNSbgRXtNJtRJkTvWFVhmbI5.1
Password: cmsa