LeanReasoner: 用 Lean 增强复杂逻辑推理
Logic-LM 是一种将大型语言模型与符号推理相结合的框架,通过首先使用大型语言模型将自然语言问题转化为符号形式,然后进行确定性符号求解,以及自我精炼阶段来修正符号形式,在 ProofWriter、PrOntoQA、FOLIO 和 LogicalDeduction 等四个逻辑推理数据集上的结果表明,与仅使用大型语言模型相比,我们的方法可以显著提高逻辑推理的性能。
May, 2023
通过强化学习与逻辑反馈,加强语言模型在逻辑推理方面的能力,为处理复杂法律推理任务的大型语言模型的发展提供新的研究途径,并承认了语言与逻辑之间的基本联系。
Nov, 2023
通过提出一种新的流程,我们利用合成数据来将自然语言数学问题转化为 Lean 4 语句,并相应地进行过滤,从而为解决 LLMs 在理解复杂数学问题和证明上的性能提供有用的训练数据。最终数据集包含约 57K 个正式 - 非正式问题对以及来自数学竞赛论坛的搜索证明和 21 个新的 IMO 问题。
Jun, 2024
最近发展的大型语言模型 (LLMs) 在各种语言理解任务上表现出色,但它们真正能够对自然语言进行 “推理” 吗?本文综合评估了 LLMS 在涵盖命题逻辑、一阶逻辑和非单调逻辑的 25 种不同推理模式上的逻辑推理能力,并引入了 LogicBench,一个关注单个推理规则使用的自然语言问答数据集,通过使用一系列的连贯思维提示与 GPT-4、ChatGPT、Gemini、Llama-2 和 Mistral 等多个 LLMS 进行详细分析。实验结果表明,现有的 LLMS 在 LogicBench 上表现不佳,尤其在涉及复杂推理和否定的情况下遇到困难,并有时忽视推理所需的上下文信息以得出正确结论。我们认为我们的工作和发现将有助于未来评估和提升 LLMS 的逻辑推理能力。
Apr, 2024
通过对大型语言模型的研究,我们发现它们在逻辑推理方面存在缺陷,导致其在任务解决中产生反事实的答案。为了解决这个问题,我们提出了多种策略,赋予大型语言模型逻辑推理能力,从而使其能够在不同场景中生成更符合逻辑的答案。我们还通过构建一个综合数据集 (LMM-LR) 对该方法进行了评估和预训练。在不同任务上进行了广泛的定量和定性分析,验证了通过逻辑训练大型语言模型的有效性和必要性,并为将来的工作提供了启示。
Oct, 2023
本文介绍了 LeanDojo:一个开源、可交互的证明环境,它从 Lean 中提取了证明中的数据及注释,提供了有价值的前提数据,以便于选取前提。 我们使用此数据,开发了 ReProver:第一个增加检索功能的基于 LLM 的证明程序。其成本低廉,只需要一台 GPU 进行一周的训练,并且可以有效地选择定理中的前提。我们构建了一个包含 96962 个定理和证明的新基准,并将其用于培训和评估。实验结果表明,相对于非检索基线和 GPT-4,ReProver 非常有效。我们发布了代码和数据集,以促进进一步的研究。
Jun, 2023
基于大规模合成数据,使用 Lean 4 proof 数据生成方法,我们的模型在定理生成和解决题目方面取得了卓越的成果,证明了合成数据对提高 LLMs 中的定理证明能力的潜力。
May, 2024
通过对归纳逻辑编程基准测试的深入评估,本研究表明与模型规模较小的神经程序归纳系统相比,最新的大型语言模型在推理能力方面表现较差,无论是使用自然语言提示还是真值矩阵提示,它们在性能和泛化方面都表现较低。
Jan, 2024
通过将大型语言模型 (LLMs) 与各种符号求解器相结合,我们对 Z3、Pyke 和 Prover9 三个符号求解器的性能进行实验证明,其中与 LLMs 相结合时,Pyke 的性能明显低于 Prover9 和 Z3,Z3 的总体准确性略高于 Prover9,但 Prover9 能够处理更多问题。
Jun, 2024