CoT out了！新加坡国立让符号逻辑在大模型推理中换发新春

夕小瑶科技说 原创
作者 | Richard
近年来，人工智能领域涌现出一系列引人注目的大语言模型。这些模型展现出了惊人的语言理解和生成能力，在许多任务上甚至超越了人类的表现。然而，它们在逻辑推理方面仍然存在局限性。最近一种名为"思维链"(Chain of Thought)的提示方法为这一问题带来了曙光。通过鼓励模型按步骤进行推理，思维链显著提升了语言模型的推理能力。

在最新的一项研究中，研究者提出了一种创新的方法——符号化思维链(SymbCoT)，将符号表示和逻辑规则引入到思维链中，以增强语言模型在逻辑推理任务上的表现。SymbCoT采用了一种全新的"计划-求解"架构，将复杂的推理问题分解成一系列更小的子问题，并通过严格的逻辑规则逐步求解。同时SymbCoT引入了一种回溯验证机制，以保证推理过程的可靠性。在多个基准测试中，SymbCoT都取得了优于现有方法的出色表现，展现出其在逻辑推理领域的巨大潜力。

这项突破性的研究工作为语言模型的逻辑推理能力带来了新的希望。通过巧妙地结合符号表示和自然语言，SymbCoT在保证严谨推理的同时，最大限度地利用了语言模型的语义理解优势。这一新颖的方法有望成为未来语言模型逻辑推理的重要范式，助力大模型在语言和符号领域两开花。

论文标题：
Faithful Logical Reasoning via Symbolic Chain-of-Thought

论文链接：
https://arxiv.org/pdf/2405.18357

大语言模型的逻辑推理之困

近年来，大语言模型如ChatGPT、GPT-4等在各种任务上表现出色，展现出了惊人的语言理解和生成能力。它们能够流畅地回答问题、生成文本、进行对话，甚至在一些推理任务上超越人类。这些成就让人们对语言模型在逻辑推理领域的潜力充满期待。

然而，尽管思维链(Chain of Thought)提示方法在一定程度上提升了语言模型的推理能力，但它们在处理复杂逻辑推理任务时仍然存在局限性。这些任务通常需要严谨的符号表示和严格的推理规则，而单纯依赖自然语言表达往往难以满足这一要求。

以一阶逻辑(First-Order Logic)为例，它是一种常用的符号表示，能够刻画对象之间的复杂关系和性质。但是，仅凭自然语言很难准确表达一阶逻辑的语法和语义。类似地，在约束优化(Constraint Optimization)问题中，需要用符号形式描述变量、域和约束条件，并运用特定的推理规则进行求解。这些都不是自然语言所擅长的。

此外，逻辑推理任务对推理过程的可解释性和可验证性有很高的要求。每一步推理都需要有严格的逻辑依据，并且能够被验证正确性。而思维链方法生成的自然语言解释，往往难以满足这种严谨性的要求。

种种困难表明，尽管语言模型在许多任务上表现出色，但在逻辑推理领域仍面临巨大挑战。如何赋予语言模型强大的逻辑推理能力，成为亟待解决的问题。本文提出的SymbCoT方法,正是对这一问题的有益探索。它巧妙地将符号表示和逻辑规则引入到思维链中，开创了一种全新的逻辑推理范式。那么，SymbCoT究竟是如何实现的呢?让我们在下一节中一探究竟。

SymbCoT：符号化思维链新范式

针对上述问题，研究者提出了一种创新的方法——符号化思维链(SymbCoT)。SymbCoT巧妙地将符号表示和逻辑规则引入到思维链中，以增强语言模型在逻辑推理任务上的表现。

为了更好地理解SymbCoT的工作原理，让我们来看一个具体的任务示例。假设给定以下前提:

• P1：鹰从不降落。(A hawk never lands.)
• P2：有些鸟是鹰。(Some birds are hawks.)

我们需要判断以下结论的真假:

• 所有的鸟都会降落。(All birds land.)

传统的思维链方法可能会给出这样的推理过程：根据P2，有些鸟是鹰。根据P1，鹰从不降落。因此，有些鸟(即鹰)不会降落。由此可知，并非所有的鸟都会降落。

虽然这个推理过程看似合理，但它缺乏严谨的逻辑依据。相比之下，SymbCoT会将其转化为更加严谨的符号表示:

然后，SymbCoT会应用一阶逻辑的推理规则，例如全称量化(Universal Quantification)、存在量化(Existential Quantification)等，进行严格的推导：

这个符号表达的意思是，"并非所有的鸟都会降落"。可以看到，SymbCoT通过引入严谨的符号表示和推理规则，得出了一个逻辑上正确的结论。

SymbCoT主要包含以下几个关键模块:

1. 翻译器：将自然语言上下文转化为符号表示。
2. 规划器：将原问题分解为一系列子问题,制定符号化的步骤计划。
3. 求解器：根据计划逐步进行符号化的逻辑推理。
4. 验证器：回溯验证翻译和推理过程的正确性。

SymbCoT的一大亮点是采用了"计划-求解"的架构。规划器首先将复杂的推理问题分解成更小的子问题，并制定详细的求解计划。求解器则严格按照逻辑规则，逐步推理求解每个子问题。这种分而治之的策略使得整个推理过程更加清晰和可控。

此外，SymbCoT巧妙地结合了符号表示和自然语言。通过符号化，它能进行严谨精确的逻辑运算；而利用语言模型强大的语义理解能力，它又能充分挖掘蕴含在自然语言中的隐性信息和丰富语境。二者的完美结合，使SymbCoT在逻辑推理任务上大放异彩。

SymbCoT vs. 思维链：全面超越

为了全面评估SymbCoT的性能，研究者在5个逻辑推理基准测试上进行了大量实验，并与现有的方法进行了对比。

下表展示了SymbCoT在三个数据集(ProntoQA、ProofWriter和FOLIO)上的性能对比。在这些任务中，所用的符号表示均为一阶逻辑(First-Order Logic)。可以看到，无论是在GPT-3.5还是GPT-4上，SymbCoT都显著优于朴素的提示方法(Naive)、思维链方法(CoT)以及先进的Logic-LM方法。特别是在GPT-4上，SymbCoT的平均提升幅度高达7.88%，展现出了优秀的推理能力。

然后作者在另外两个数据集(LogicalDeduction和AR-LSAT)上测试SymbCoT的表现，这两个数据集采用了约束优化(Constraint Optimization)的符号表示。同样地，SymbCoT在这些任务上也明显优于思维链和Logic-LM方法，平均提升了3.12%。这表明SymbCoT能够适应不同类型的符号表示，具有很强的泛化能力。

除此之外，作者通过消融实验揭示了SymbCoT各个模块的贡献。可以看出，规划器(Planner)和求解器(Solver)发挥了最关键的作用，平均带来10.4%的性能提升。这证实了"规划-求解"架构的有效性。其次是翻译器(Translator)，也带来了6.3%的提升。验证器(Verifier)虽然贡献相对较小，但能够进一步保证推理过程的可靠性。

下图进一步分析了SymbCoT在不同推理深度(即问题复杂度)下的表现。随着推理深度的增加，SymbCoT相对于思维链的优势愈发明显。这表明SymbCoT在处理复杂逻辑推理问题时，具有更强的鲁棒性和泛化能力。即使在5跳的超长推理任务中，SymbCoT仍然保持了最佳的性能。

在推理可信度验证方面，通过人工评估，研究者发现原始的思维链方法存在6%的"不可信"推理，即得出了正确答案，但推理过程不正确。引入验证器后，SymbCoT将这一比例降至0%，实现了100%可信的推理。这彰显了SymbCoT在推理可解释性和可验证性方面的重要改进。

以上实验结果证明了SymbCoT在各类逻辑推理任务上的卓越表现。它不仅在推理准确性上全面超越了现有方法，而且在推理的鲁棒性、可解释性和可验证性等方面也取得了重要进展。

未来可期：迈向认知智能新高度

SymbCoT通过将符号表示和逻辑规则引入思维链，它在保证推理严谨性的同时，充分利用了语言模型强大的语义理解能力。这一创新范式有望成为未来语言模型逻辑推理的重要发展方向。

当然，SymbCoT仍有进一步优化的空间。未来的工作可以探索将SymbCoT与外部求解器相结合，发挥二者的互补优势；也可以尝试将SymbCoT拓展到更多类型的符号表示和推理任务中。

随着语言模型逻辑推理能力的不断增强，人工智能有望迈向更高层次的认知智能。SymbCoT等创新方法的出现，为实现这一目标注入了新的活力。在不远的将来，语言模型能够胜任更加复杂和抽象的推理任务，成为我们解决复杂问题的得力助手。