本文研究了自动形式化的过程，并发现大型语言模型可用于将自然语言的数学问题翻译为Isabelle/HOL的形式化说明，证明了这种方法的实用性，并通过训练预先介绍的神经定理证明器使改进了MiniF2F定理证明基准的证明率从29.6%提高到35.2%。

May, 2022

本文提出 DSR-LM 框架，通过符号编程实现不同iable 符号推理框架，其中预训练的语言模型控制事实知识的感知，符号模块执行演绎推理，并改进了LMs的逻辑推理能力，结果表明其在推理基准测试中的精度提高了20%以上。

May, 2023

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

May, 2023

通过使用神经符号计算来全面利用LLMs和符号化证明器，本文探索了以逻辑推理任务，特别是符合自然语言的任务为基础的解决方案。

Oct, 2023

这篇论文研究了大型语言模型在逻辑推理中的自我验证能力，主要关注其准确识别逻辑谬误的能力。通过对包含232种谬误的数据集进行实验，发现现有的大型语言模型在准确识别谬误的过程中可能存在困难，并可能不能保证自我验证方法的有效性。论文提出了对未来研究和实际应用自我验证方法的建议。

Nov, 2023

我们引入了LogicAsker，它是一种自动方法，全面评估和改进基于命题和谓词逻辑的大型语言模型的逻辑推理能力，并揭示了LLM未能学好的逻辑规则。我们评估了LogicAsker在GPT-3、ChatGPT、GPT-4、Bard、Vicuna和Guanaco等主要的大型语言模型上，并展示了LogicAsker的测试用例在不同LLM中发现逻辑推理错误的比率从25%到94%不等。此外，LogicAsker的测试用例可以进一步用于设计上下文学习的演示例子，有效提高LLM的逻辑推理能力，如GPT-4提高了10%。据我们所知，我们的工作是首次基于测试结果创建提示来有效提高LLM的形式推理能力。所有的代码、数据和结果都将被公开以供复制和未来研究。

Jan, 2024

通过对归纳逻辑编程基准测试的深入评估，本研究表明与模型规模较小的神经程序归纳系统相比，最新的大型语言模型在推理能力方面表现较差，无论是使用自然语言提示还是真值矩阵提示，它们在性能和泛化方面都表现较低。

Jan, 2024

最近发展的大型语言模型 (LLMs) 在各种语言理解任务上表现出色，但它们真正能够对自然语言进行“推理”吗？本文综合评估了 LLMS 在涵盖命题逻辑、一阶逻辑和非单调逻辑的 25 种不同推理模式上的逻辑推理能力，并引入了 LogicBench，一个关注单个推理规则使用的自然语言问答数据集，通过使用一系列的连贯思维提示与 GPT-4、ChatGPT、Gemini、Llama-2 和 Mistral 等多个 LLMS 进行详细分析。实验结果表明，现有的 LLMS 在 LogicBench 上表现不佳，尤其在涉及复杂推理和否定的情况下遇到困难，并有时忽视推理所需的上下文信息以得出正确结论。我们认为我们的工作和发现将有助于未来评估和提升 LLMS 的逻辑推理能力。

Apr, 2024

通过将大型语言模型 (LLMs) 与各种符号求解器相结合，我们对 Z3、Pyke 和 Prover9 三个符号求解器的性能进行实验证明，其中与 LLMs 相结合时，Pyke 的性能明显低于 Prover9 和 Z3，Z3 的总体准确性略高于 Prover9，但 Prover9 能够处理更多问题。

Jun, 2024

我们提出了一种神经符号化方法，该方法通过提示大型语言模型从问题陈述中提取和编码所有相关信息作为逻辑代码语句，并使用逻辑编程语言（Prolog）进行明确的演绎推理的迭代计算，从而显著提高了大型语言模型在标准数学推理基准测试GSM8k和BIG-bench数据集的Navigate数据集上的性能。此外，我们引入了一个新的数据集，Non-Linear Reasoning（NLR）数据集，包含55个唯一的单词问题，针对大型语言模型的下一个令牌预测范式的缺点，并要求使用基本算术技能解决复杂的非线性推理。我们的研究结果表明，Prolog的集成使得大型语言模型能够在NLR数据集上实现高性能，在此任务上，甚至包括GPT4在内的最先进语言模型都无法通过纯文本解决。

Jul, 2024