摘要

本文探讨了大型语言模型（LLMs）在复杂推理任务中的局限性，特别是在生成和细化符号形式化表示方面的挑战。为了解决这些问题，作者提出了Logic-LM++，这是对Logic-LM的改进版本，利用LLMs的成对比较能力来评估和改进符号形式化表示。实验结果表明，Logic-LM++在自然语言推理任务上优于Logic-LM和其他基于LLM的技术，特别是在FOLIO和AR-LSAT数据集上显示出显著的性能提升。

原理

Logic-LM++的核心创新在于其利用LLMs的成对比较能力来评估和细化符号形式化表示。具体来说，Logic-LM++通过以下两个主要改进来增强符号形式化表示的语义准确性：

1. 成对比较能力：Logic-LM++利用LLMs的成对比较能力，允许模型评估LLM提出的细化建议，并进行语义检查，确保符号形式化表示的编辑在语义上改进了解决方案。
2. 细化过程中的问题上下文：在细化过程中，Logic-LM++为LLM提供更多关于问题陈述的上下文，从而减少推荐编辑中出现的错误，确保细化后的符号形式化表示更加准确。

流程

Logic-LM++的工作流程包括以下几个关键步骤：

1. 问题形式化：LLM根据任务描述和问题陈述生成符号形式化表示。
2. 符号推理：使用符号求解器（如Prover9和Z3定理证明器）解决生成的符号形式化表示。
3. 结果解释：将生成的输出映射到正确的答案，使用正则表达式解析。
4. 细化循环：在形式化和推理阶段，Logic-LM++使用细化循环来修复符号形式化表示中的错误，并通过成对比较和问题上下文细化来提高语义准确性。

应用

Logic-LM++的应用前景广泛，特别是在需要复杂推理的自然语言处理任务中。例如，在法律、教育和技术领域，Logic-LM++可以用于自动化解析和推理复杂的逻辑问题。此外，随着模型的进一步优化和扩展，Logic-LM++有望在更多领域实现自动化推理和决策支持。