Automated Theorem Provers Help Improve Large Language Model Reasoning

本文是LLM系列文章，针对《Automated Theorem Provers Help Improve Large Language Model Reasoning》的翻译。

摘要

在本文中，我们演示了逻辑编程系统和自动一阶逻辑定理证明器 (ATP) 如何提高逻辑推理任务的大型语言模型 (LLM) 的准确性，其中基线性能由直接 LLM 解决方案给出。我们首先使用 PRONTOQA 基准评估压路机问题上的 LLM 推理。我们展示了如何通过神经符号架构来提高准确性，其中LLM仅充当将给定问题转换为形式逻辑语言的前端，并调用自动推理引擎来解决它。然而，这种方法关键取决于LLM翻译的正确性。为了评估翻译的正确性，我们其次定义了句法和语义错误类别的框架。我们实现了该框架，并用它来识别LLM在基准领域所犯的错误。基于这些发现，我们第三次扩展了我们的方法，具有自动纠正语法和语义错误的功能。对于语义错误校正，我们集成了一阶逻辑 ATP，这是我们的主要且新颖的贡献。我们证明这种方法显着减少了语义错误，并进一步提高了 LLM 逻辑推理的准确性。

1 引言，背景和相关工作

2 我们的方法

3 结果

4 讨论

5 结论