Large Language Models (LLMs) have shown human-like reasoning abilities but still struggle with complex logical problems. This paper introduces a novel framework, Logic-LM, which integrates LLMs with symbolic reasoning to improve logical problem-solving. Our method first utilizes LLMs to translate a natural language problem into a symbolic formulation. Afterward, a deterministic symbolic solver performs inference on the formulated problem. We also introduce a self-refinement stage, which utilizes the symbolic solver's error messages to revise symbolic formalizations. We demonstrate Logic-LM's effectiveness on four logical reasoning datasets: ProofWriter, PrOntoQA, FOLIO, and LogicalDeduction. Our results show significant improvement compared to LLMs alone, with an average performance boost of 62.6% over standard prompting and 23.5% over chain-of-thought prompting. Our findings suggest that Logic-LM, by combining LLMs with symbolic logic, offers a promising avenue for faithful logical reasoning. Code and data are publicly available at https://github.com/teacherpeterpan/Logic-LLM.

Logic-LM是一种将大型语言模型与符号推理相结合的框架，通过首先使用大型语言模型将自然语言问题转化为符号形式，然后进行确定性符号求解，以及自我精炼阶段来修正符号形式，在ProofWriter、PrOntoQA、FOLIO和LogicalDeduction等四个逻辑推理数据集上的结果表明，与仅使用大型语言模型相比，我们的方法可以显著提高逻辑推理的性能。

Logic-LM: 使用符号求解器增强大型语言模型进行可靠的逻辑推理