线性推理与证明中的反证法：大型语言模型在一阶逻辑问题解决中的障碍
Linear Reasoning vs. Proof by Cases: Obstacles for Large Language Models in FOL Problem Solving
AI总结：
本文提出PC-FOL数据集，通过对比线性推理与基于情况的推理，揭示大型语言模型在FOL问题解决中的核心挑战。
摘要：
为了全面评估大型语言模型（LLMs）的数学推理能力，研究者已经引入了大量数学推理数据集。然而，大多数现有数据集主要关注线性推理，忽略了诸如反证法和证明中的情况分析等其他部分，这些部分对于研究LLMs的推理能力至关重要。为了解决这一限制，我们首先引入了一个名为PC-FOL的新的一阶逻辑（FOL）数据集，由专业数学家注释，专注于基于情况的推理问题。该数据集中的所有实例都配备了手动撰写的自然语言证明，明确区别于传统的线性推理数据集。我们的实验结果表明，线性推理与基于情况的推理问题之间存在显著的性能差距。为进一步研究这一现象，我们提供了一种基于图模型的理论分析，为这两种推理问题之间的差异提供了解释。我们希望这项工作能揭示自动自然语言数学证明生成领域中的核心挑战，为未来研究铺平道路。
英文摘要：
To comprehensively evaluate the mathematical reasoning capabilities of Large Language Models (LLMs), researchers have introduced abundant mathematical reasoning datasets. However, most existing datasets primarily focus on linear reasoning, neglecting other parts such as proof by contradiction and proof by cases, which are crucial for investigating LLMs' reasoning abilities. To address this limitation, we first introduce a novel first-order logic (FOL) dataset named PC-FOL, annotated by professional mathematicians, focusing on case-based reasoning problems. All instances in this dataset are equipped with a manually written natural language proof, clearly distinguishing it from conventional linear reasoning datasets. Our experimental results over leading LLMs demonstrate a substantial performance gap between linear reasoning and case-based reasoning problems. To further investigate this phenomenon, we provide a theoretical analysis grounded in graphical model, which provides an explanation for the observed disparity between the two types of reasoning problems. We hope this work can reveal the core challenges in the field of automated natural language mathematical proof generation, paving the way for future research.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
