LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers
作者: Theo X. Olausson, Alex Gu, Benjamin Lipkin, Cedegao E. Zhang, Armando Solar-Lezama, Joshua B. Tenenbaum, Roger Levy
分类: cs.CL, cs.AI
发布日期: 2023-10-23 (更新: 2024-02-14)
备注: EMNLP Main 2023 (Outstanding Paper Award)
期刊: Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pages 5153-5176, Singapore. Association for Computational Linguistics
DOI: 10.18653/v1/2023.emnlp-main.313
🔗 代码/项目: GITHUB
💡 一句话要点
提出LINC以解决逻辑推理中的语言模型局限性问题
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 逻辑推理 神经符号编程 大型语言模型 一阶逻辑 定理证明 模型增强 自然语言处理
📋 核心要点
- 现有的基于提示的策略在逻辑推理任务中表现不佳，常常在细节上出现不可预测的失败。
- 论文提出LINC方法，通过将LLM与外部定理证明器结合，重新定义逻辑推理任务为模块化的神经符号编程。
- 实验结果显示，LINC在多个模型上显著提升了推理性能，尤其是在ProofWriter上超越了更大的GPT模型。
📝 摘要（中文）
逻辑推理，即从一组前提中推导结论的真值，是人工智能中的重要任务，对科学、数学和社会具有广泛影响。尽管已有多种基于提示的策略来增强大型语言模型（LLMs）的推理能力，但这些方法仍显不足，常常在细微和不可预测的情况下失败。本文提出了一种模块化的神经符号编程方法LINC（逻辑推理通过神经符号计算），其中LLM作为语义解析器，将自然语言的前提和结论翻译为一阶逻辑表达式，并将这些表达式交给外部定理证明器进行符号推理。通过这种方法，我们在FOLIO和ProofWriter的平衡子集上观察到显著的性能提升。使用LINC增强的StarCoder+在ProofWriter上超越了GPT-3.5和GPT-4，分别提升38%和10%。
🔬 方法详解
问题定义：本文旨在解决现有大型语言模型在逻辑推理任务中的不足，特别是在细微推理和不可预测失败方面的挑战。
核心思路：LINC方法将逻辑推理任务重构为神经符号编程，利用LLM作为语义解析器，将自然语言转换为一阶逻辑表达式，并通过外部定理证明器进行推理。这样的设计旨在结合LLM的语言理解能力与符号推理的严谨性。
技术框架：LINC的整体架构包括三个主要模块：首先，LLM解析自然语言的前提和结论；其次，生成相应的一阶逻辑表达式；最后，将这些表达式传递给外部定理证明器进行符号推理。
关键创新：LINC的主要创新在于将LLM与符号推理结合，形成了一种新的推理机制，克服了传统方法的局限性，尤其是在处理复杂逻辑推理时的有效性。
关键设计：在实现过程中，LINC对LLM的输出进行了优化，确保生成的逻辑表达式准确无误，并通过精心设计的损失函数来提升推理的准确性和效率。
🖼️ 关键图片
📊 实验亮点
实验结果表明，LINC在ProofWriter上相较于GPT-3.5和GPT-4，分别提升了38%和10%的性能。在与GPT-4结合使用时，LINC在ProofWriter上比Chain-of-Thought方法高出26%的得分，显示出其在逻辑推理任务中的显著优势。
🎯 应用场景
LINC方法在科学研究、数学证明和社会科学等领域具有广泛的应用潜力。通过提高逻辑推理的准确性和效率，LINC可以帮助研究人员更好地处理复杂的推理任务，推动相关领域的进步和创新。
📄 摘要（原文）
Logical reasoning, i.e., deductively inferring the truth value of a conclusion from a set of premises, is an important task for artificial intelligence with wide potential impacts on science, mathematics, and society. While many prompting-based strategies have been proposed to enable Large Language Models (LLMs) to do such reasoning more effectively, they still appear unsatisfactory, often failing in subtle and unpredictable ways. In this work, we investigate the validity of instead reformulating such tasks as modular neurosymbolic programming, which we call LINC: Logical Inference via Neurosymbolic Computation. In LINC, the LLM acts as a semantic parser, translating premises and conclusions from natural language to expressions in first-order logic. These expressions are then offloaded to an external theorem prover, which symbolically performs deductive inference. Leveraging this approach, we observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate. On ProofWriter, augmenting the comparatively small open-source StarCoder+ (15.5B parameters) with LINC even outperforms GPT-3.5 and GPT-4 with Chain-of-Thought (CoT) prompting by an absolute 38% and 10%, respectively. When used with GPT-4, LINC scores 26% higher than CoT on ProofWriter while performing comparatively on FOLIO. Further analysis reveals that although both methods on average succeed roughly equally often on this dataset, they exhibit distinct and complementary failure modes. We thus provide promising evidence for how logical reasoning over natural language can be tackled through jointly leveraging LLMs alongside symbolic provers. All corresponding code is publicly available at https://github.com/benlipkin/linc