Linear Reasoning vs. Proof by Cases: Obstacles for Large Language Models in FOL Problem Solving
This work addresses a gap in evaluating LLMs' mathematical reasoning for researchers, though it is incremental as it focuses on a specific dataset and analysis.
The authors tackled the lack of datasets for case-based reasoning in first-order logic (FOL) by introducing PC-FOL, a dataset annotated by mathematicians, and found a substantial performance gap between linear and case-based reasoning in leading LLMs.
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.