Linear Reasoning vs. Proof by Cases: Obstacles for Large Language Models in FOL Problem Solving

TL;DR

This paper introduces a new FOL dataset focusing on case-based reasoning, revealing significant performance gaps in LLMs between linear and proof by cases, supported by theoretical analysis.

Contribution

The paper presents a novel FOL dataset with case-based reasoning problems and provides a theoretical explanation for LLMs' difficulties with non-linear reasoning.

Findings

LLMs perform significantly worse on case-based reasoning tasks

A new dataset (PC-FOL) for evaluating proof by cases in FOL

Theoretical analysis explains the disparity in reasoning performance

Abstract

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.