ACL 2024 | 让纯LLM实现类人的符号逻辑推理能力，开源框架SymbCoT来了

论文题目：

Faithful Logical Reasoning via Symbolic Chain-of-Thought

论文作者：

徐俊东1，费豪1，潘亮铭2，刘茜3，Mong-Li Lee1，Wynne Hsu1

新加坡国立大学1，加州大学圣芭芭拉分校2，奥克兰大学3

收录会议：

ACL 2024

论文链接：

https://arxiv.org/pdf/2405.18357.pdf

代码链接：

https://github.com/Aiden0526/SymbCoT

极简概括：这篇工作提出了一种名为 SymbCoT（Symbolic Chain-of-Thought）的新型逻辑推理框架，它通过将符号表达和逻辑规则与思维链提示相结合，增强了纯 LLMs 的逻辑推理能力。SymbCoT 首先将自然语言上下文翻译成符号格式，然后使用符号逻辑规则逐步推导出解决问题的方案，并通过验证器检查翻译和推理链的正确性。

在五个标准数据集上的广泛评估表明，SymbCoT 在逻辑推理方面显著提高了传统 CoT 方法的性能，同时刷新了最新性能水平。

动机和背景

实现类似人类的逻辑推理能力对于发展通用人工智能至关重要，它使智能系统能够参与到问题解决、决策制定和批判性思维中。最近的大型语言模型（LLMs）在语义理解方面取得了显著进展，为实现 AGI 带来了希望。然而，要进一步提升 LLMs 的逻辑推理能力，尤其是达到人类水平，仍然至关重要且具有挑战性。逻辑推理是一种需要严格证据评估、论点构建和逻辑演绎的认知过程。

目前的趋势是将 LLMs 与符号求解器集成以提升性能，但这些尝试通常仅限于将 LLMs 作为文本到符号的翻译器，核心推理过程仍然依赖于传统的外部推理器。这种方法并没有增强 LLMs 在逻辑推理方面的能力，而且过度依赖外部符号求解器可能导致缺乏灵活性、信息遗漏和不可解释性。

为了克服这些限制，研究者们引入了链式思考（CoT）的概念，以模仿人类的思考过程，鼓励 LLMs 在解决问题时明确考虑中间步骤，并为决策提供理由，从而提高推理过程的可靠性。CoT 已经成功地集成到了多种任务中，显著提升了 LLMs 的推理能力，有时甚至能在特定场景下与人类表现相匹敌。

然而，直接将基本 CoT 应用于逻辑推理存在固有的局限性，因为语言表达的抽象性无法充分支持所需的精确逻辑。逻辑推理要求严格的逻辑计算，依赖于符号表达和严格的推理规则来表示问题的结构。因此，研究者们提出了一种新颖的符号链式思考（SymbCoT）框架，专门用于逻辑推理。

SymbCoT 是一个完全基于 LLMs 的框架，不依赖于任何外部推理器或工具，包括初始翻译和随后的推理阶段。SymbCoT 由四个主要模块组成：翻译器、规划器、求解器和验证器。它通过以下三个核心方面来增强逻辑推理能力：

1. 将符号表达集成到 CoT 中，以更精确地描述中间推理过程。同时，结合自然语言和符号表达的优势，以充分利用两者的长处。
2. 采用“计划然后解决”的架构，将复杂问题分解为更小、更易于管理的子问题，使整个推理过程更加清晰和有结构。
3. 设计了回顾性验证机制，在翻译和问题解决阶段验证每一步结果的正确性，确保推理过程的准确性和可靠性。

在实验中，SymbCoT 在五个逻辑推理数据集上进行了测试，使用了 GPT-3.5 和 GPT-4，并在符号表达方面展示了显著的性能提升，超越了现有的最先进解决方案。

结果表明，SymbCoT 在处理更复杂的逻辑推理任务时，相较于传统 CoT 方法有更明显的改进，并且通过验证机制确保了推理过程的忠实性。深入分析表明，完全基于 LLMs 的逻辑推理能够提供更好的符号语法鲁棒性、人类可读的解释和更充分的信息利用。

总的来说，SymbCoT 提出了一个基于 CoT 的全新 LLM 逻辑推理框架，展示了 LLMs 在没有外部推理工具的情况下实现强大逻辑推理能力的潜力。与依赖外部解析器的现有解决方案相比，SymbCoT 在翻译错误鲁棒性和提供人类易于理解的解释方面具有优势。

此外，SymbCoT 创新性地整合了符号形式和自然语言表达的优势，实现了精确的推理计算，同时完全解释了隐含信息并捕获了丰富的上下文。通过引入“先计划后解题”的 CoT 推理架构和回顾性验证机制，SymbCoT 增强了推理过程的忠实性。

符号化思维链框架

我们设计了一个四步骤的 SymbCoT 框架，包括了翻译、规划、执行与验证。

2.1 翻译（Translator）

• 将自然语言的前提和问题陈述转换成符号格式。
• 这一步骤的目的是为后续的逻辑推理过程准备结构化的输入，确保问题以有利于逻辑分析的格式表示。

2.2 规划（Planner）

• 将原始问题分解为更小、更易于管理的子问题。
• 制定一个详细的、逐步的计划，将给定的前提联系到问题陈述，形成逻辑推理的蓝图。

2.3 执行（Solver）

• 根据前提、问题陈述和制定的计划，通过一系列逻辑推理步骤来推导答案。
• 该模块强调使用符号推理规则进行逻辑演绎，例如应用一阶逻辑中的规则，如摩根定律（Modus Tollens）

2.4 验证（Verifier）

• 对翻译和推理过程进行验证，确保每一步的输出都正确无误。
• 验证包括检查符号翻译是否与原始自然语言上下文在语义上等价，以及检查推理步骤是否严格遵守形式逻辑的原则。
• 如果发现任何逻辑错误或翻译不一致，验证器将根据正确的逻辑规则进行修正，确保推理过程的准确性和可靠性。

SymbCoT 方法的创新之处在于：

• 它将符号表达式整合到 CoT 中，以更精确地描述推理过程，同时利用LLMs在解释隐含意图和上下文信息方面的优势。
• 它采用了“计划然后解决”的架构，将复杂问题分解为子问题，使得推理过程更加清晰和有结构。
• 它引入了回顾性验证机制，确保推理过程的每一步都经过验证，提高了推理的准确性和可靠性。

实验分析

3.1 SymbCoT在不同数据集与逻辑规则上的表现

我们首先使用 First-order logic 的规则，在三个逻辑推理数据集上进行了测试。实验证明 SymbCoT 在 GPT3.5-turbo 与 GPT-4 上均能大幅超越传统 CoT 的性能，甚至超越了使用外部工具的框架（Logic-LM）。

为了验证该框架的普适性，作者随后使用 Constraint Optimization 符号表达的推理规则在另外两个数据集上进行了测试。实验证明使用不同的逻辑规则也能带来更好的性能。

3.2 复杂推理能力

我们分析了不同方法在不同推理深度上的表现，发现随着推理深度的增加，SymbCoT 相对于 CoT 的改进变得更加明显，表明 SymbCoT 在处理更复杂问题上的优势。

3.3 对符号语法错误的鲁棒性

我们比较了完全基于 LLM 的推理器与依赖外部解析器的方法（如 Logic-LM）在执行符号表达式语法时的成功率，发现 SymbCoT 在语法执行上的成功率显著提高，展示了对语法错误的显著鲁棒性。

3.4 符号与自然语言混合表达的优势

我们分析了 LLM 从自然语言到符号语言的转换过程中可能遗漏的关键信息或引入的不准确性，发现 SymbCoT 通过结合符号和自然语言表达来纠正翻译错误并增强逻辑推理的有效性。

3.5 推理可信度

我们评估了 CoT、SymbCoT 以及不包含验证器的 SymbCoT 在推理忠实度上的表现，定义了“可信”、“不可信”和“错误”的推理实例，并发现 SymbCoT 能够完全消除不忠实的推理，确保了基于有效逻辑的推理过程。

3.6 使用不同LLM的影响

我们比较了 GPT-3.5 和 GPT-4 在三个 FOL 数据集上的表现，发现在升级模型后，SymbCoT 方法的性能提升最为显著，强调了 SymbCoT 方法与更先进模型之间的协同效应。

3.7 错误分析

我们在错误分析（Error analysis）部分讨论了大型语言模型（LLMs）在准确完成推理任务时所需的两个关键能力：

1. 基本规划能力：这是指识别正确推理路径的能力。在解决问题时，能够正确规划推理步骤是至关重要的。
2. 逻辑步骤的有效性：在识别了推理路径之后，确保每个推理步骤都基于有效的逻辑。这意味着在推理过程中，每一步都必须遵循逻辑规则，以避免逻辑错误。

SymbCoT 的开发主要增强了第二个能力，即确保每个推理步骤都基于有效的逻辑。然而，第一个能力，即规划能力，同样重要，因为它直接关系到问题解决的过程。如果模型无法识别正确的路径，那么甚至都不会有机会去犯逻辑错误，这是SymbCoT 旨在解决的问题。但是，SymbCoT 的方法并没有增强模型的规划能力，因为这本质上依赖于 LLM 本身。因此，为了使 SymbCoT 有效，LLM 需要满足这一推理的基线。

简而言之，错误分析强调了为了使 LLMs 在逻辑推理任务中表现良好，它们需要具备两个关键技能：能够规划出正确的推理路径，以及在确定路径后，确保每个推理步骤都遵循有效的逻辑规则。SymbCoT 框架通过增强 LLMs 遵循逻辑规则的能力来提高其推理性能，但它并不直接改善模型的规划能力，这需要 LLM 自身具备相应的推理基础。

3.8 个案研究分析

为了直观地看到 SymbCoT 对于传统 CoT 和使用外部工具的方法的优势，我们使用了两个典型的案例来展示：

3.8.1 针对CoT的案例研究

• 场景：有一个逻辑推理问题，涉及到比利时选手 Descampe 在 1992 年 du Maurier Classic 比赛排行榜上的位置。
• CoT 的错误：CoT 错误地推断，因为比利时有一人与排行榜上的六人并列，而 Descampe 是比利时人并且出现在排行榜上，所以 Descampe 一定是六人并列中的一员。
• SymbCoT 的正确处理：SymbCoT 正确地指出，由于没有直接说明 Descampe 参与六人并列的前提，例如 “Tie（Descampe, sixWay）”，我们无法确定 “Tie（Descampe, sixWay）”这一陈述的真实性。因此，该陈述的真实性仍然未知。

3.8.2 针对 Prover9 的案例研究

• 场景：Harry 阅读了《瓦尔登湖》这本书，询问这是否使他变得更聪明。
• Prover9 的失败：使用 Prover9 这样的外部推理工具，由于翻译过程中可能丢失一些隐式，但对于人类来说容易理解的假设信息，即 “Harry is a person”（因为 Harry 是一个很明显的人名），导致无法确定 Harry 是否因为阅读《瓦尔登湖》而变得更聪明，Prover9 给出了不确定的结果。
• SymbCoT 的正确处理：SymbCoT 利用其自然语言理解能力，更好地捕捉了上下文的细节，并能够正确推断出由于《瓦尔登湖》是一本书，Harry 阅读了这本书，根据给定的前提，Harry 获得了知识，任何获得知识的人都被认为是更聪明的。并且，SymbCoT 使用其语言理解能力推断出了一个隐藏的假设即 “Harry is a person”，因此得出 Harry 变得更聪明的结论是正确的。

总结

总的来说，这篇论文提出了一种名为 SymbCoT（Symbolic Chain-of-Thought）的新型逻辑推理框架，旨在提升大型语言模型（LLMs）在逻辑推理方面的能力。SymbCoT 通过四个关键步骤——翻译、规划、执行和验证——将自然语言转换为符号表示，并运用符号逻辑规则进行严密的推理。通过大量的实验证明，SymbCoT 相比现有方法具有更好的推理准确度、可信度与鲁棒性等优势。