新数据集揭示大模型在分情况证明上表现远差于线性推理。
Linear Reasoning vs. Proof by Cases: Obstacles for Large Language Models in FOL Problem Solving
- 构建专业标注的分情况推理FOL数据集PC-FOL。
- 主流大模型在分情况题上准确率显著低于线性推理题。
- 理论分析指出图模型结构差异是核心障碍，适合推理研究者参考。
为全面评估大语言模型（LLMs）的数学推理能力，现有数据集多聚焦线性推理，忽视了反证法和分情况证明等关键类型。为此，本文引入由专业数学家标注的首阶逻辑（FOL）新数据集PC-FOL，专攻分情况推理问题。所有题目均配有手工编写的自然语言证明，与传统线性数据集明显区分。对主流LLMs的实验显示，模型在分情况推理任务上的表现远低于线性推理。进一步基于图模型的理论分析揭示了两类推理之间的根本差异。本工作旨在揭示自动化自然语言数学证明生成的核心挑战，推动后续研究。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。