arXiv:2410.07432v2 Announce Type: replace-cross 摘要：我们正式研究了仅解码器Transformers在布尔可满足性（SAT）问题中的逻辑推理能力。首先，我们通过构造证明，在非均匀计算模型中，仅解码器Transformers可以使用回溯和通过Chain-of-Thought（CoT）进行的演绎决定3-SAT。我们通过显示与著名的DPLL SAT求解算法的跟踪等价性来证明其正确性。其次，我们使用我们设计的工具（PARAT）实现了这种构造，并通过实验证明其正确性，并探讨其性质。第三，而不是编程Transformer去推理，我们通过直接学习我们理论构造中的算法跟踪（“推理路径”）来评估它是否可以被训练去进行推理。训练后的模型在训练时遇到的问题大小上展示了强大的分布外泛化能力，但在长度泛化上有限，这与我们的理论结果的一致性相符。