证明Transformer可通过思维链解决3-SAT问题，验证其逻辑推理能力
Can Transformers Reason Logically? A Study in SAT Solving
- 用思维链构造可解3-SAT的Transformer，等价于DPLL算法
- 训练模型在训练规模上表现良好，但长度泛化能力有限
- 为理解大模型逻辑推理提供理论与实证双重支持
我们系统研究了仅解码器架构的Transformer在布尔满足性（SAT）问题中的逻辑推理能力。首先，通过构造证明，在非均匀计算模型下，仅解码器Transformer可通过回溯与思维链（CoT）推导解决3-SAT，并通过追踪等价性证明其正确性，等价于经典的DPLL SAT求解算法。其次，我们基于该构造实现了一个PyTorch模型，并设计工具PARAT，用于实证验证其正确性并分析其性质。第三，不通过编程，而是评估是否可通过直接学习算法轨迹（即“推理路径”）来训练Transformer实现推理。实验表明，训练模型在训练时见过的问题规模上表现出强的分布外泛化能力，但长度泛化能力受限，这与理论结果一致。
原文摘要 · Abstract (English)
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
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。