通过自然语言可满足性突破 Transformer 中规则推理的极限

研究 Transformer 模型的推理能力并为其发现新的挑战性任务，一直是一个备受关注的话题。最近的研究发现，这些模型在执行以自然语言表达的形式逻辑理论上的演绎推理方面表现出惊人的强大能力。然而，这些研究的不足之处在于，它们没有考虑到在随机均匀采样时，逻辑理论不一定能产生困难实例。我们提出了一种新的方法学，用于创建专注于自然语言可满足性 (NLSat) 问题的具有挑战性的算法推理数据集。其核心思想是从困难命题 SAT 问题的经验采样以及语言的复杂度理论研究中汲取见解。该方法学使我们能够区分简单与困难实例，并系统地增加现有推理基准（如 RuleTaker）的复杂度。我们发现，当前的 Transformer 在给定充足训练数据的情况下，对于难度大幅增加的 NLSat 问题表现出惊人的鲁棒求解能力。它们还展现出一定程度的尺度不变性——即泛化到更大规模和范围问题的能力。然而，我们的结果也揭示了重要的局限性：精心采样训练数据对于构建能够泛化到更大问题的模型至关重要，而 Transformer 模型有限的尺度不变性表明，它们远未学习到鲁棒的演绎推理算法。