LINC：一种结合语言模型与一阶逻辑证明器的逻辑推理神经符号方法

逻辑推理，即从一组前提中演绎推断结论的真值，是人工智能的一项重要任务，对科学、数学和社会具有广泛潜在影响。虽然已有许多基于提示(prompting)的策略被提出以使大语言模型(LLMs)更有效地进行此类推理，但它们仍不尽如人意，常以微妙且不可预测的方式失败。在这项工作中，我们研究将此类任务重新表述为模块化神经符号编程的有效性，我们称之为LINC：基于神经符号计算的逻辑推断(Logical Inference via Neurosymbolic Computation)。在LINC中，LLM充当语义解析器，将前提和结论从自然语言翻译为一阶逻辑中的表达式。这些表达式随后被移交给外部定理证明器，由其对演绎推断进行符号化执行。利用该方法，我们观察到在FOLIO和ProofWriter的一个平衡子集上，对三个不同模型在几乎所有实验条件下均取得显著性能提升。在ProofWriter上，将相对较小的开源StarCoder+ (15.5B参数)与LINC结合，甚至分别以绝对38%和10%的优势超越采用思维链(Chain-of-Thought, CoT)提示的GPT-3.5和GPT-4。当与GPT-4一起使用时，LINC在ProofWriter上的得分比CoT高26%，同时在FOLIO上表现相当。进一步分析表明，尽管两种方法在该数据集上平均成功频率大致相同，但它们表现出不同且互补的失败模式。因此我们提供了有前景的证据，说明如何通过联合利用LLM与符号证明器来处理自然语言上的逻辑推理。所有相应代码已在 https://github.com/benlipkin/linc 公开。