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

Yuliang Ji; Fuchen Shen; Jian Wu; Qiujie Xie; Yue Zhang

cs.CLFeb 24, 2026

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

Authors: Yuliang Ji, Fuchen Shen, Jian Wu, Qiujie Xie, Yue Zhang

Organizations: Nanjing University of Science and Technology · Westlake University · Zhejiang University

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.

Figures & tables

Panel of Table 2 — Table 2: Examples of linear-reasoning problem and proof-by-cases problem. The left side presents an example of linear-reasoning FOL question with a step-by-step proof sketch. The right side presents an example of proof-by-cases FOL question with a proof sketch.

Dataset Name	$\#$ Linear Reasoning	$\#$ Proof-by -Cases	$\#$ Total
PC-FOL	511	511	1022
PC-FOL-Replace	511	511	1022
PC-FOL Total	1022	1022	2044

Table 3: Basic statistics of PC-FOL.

\#

Linear-Reasoning represents the number of linear-reasoning type instances,

\#

Proof-by-Cases represents the number of the proof-by-cases type instances.

Figure 1: Abstracted reasoning chain for the left side example of Table 2 .

$\#$ Shot	Linear R-1	Linear R-2	Linear R-L	Linear Acc	Case R-1	Case R-2	Case R-L	Case Acc
0-shot	43.56	29.24	31.67	85.13	59.05	36.73	34.37	51.66
5-shot	54.88	37.60	42.42	85.77	62.00	39.99	37.97	53.95
10-shot	55.98	38.50	43.23	86.36	62.16	40.36	38.57	55.73
20-shot	55.77	38.58	43.02	87.15	62.86	40.96	39.27	55.53
40-shot	55.96	38.74	43.11	87.94	63.38	41.20	39.76	57.91

Table 6: Result of ROUGE metrics for few-shot prompting with GPT-4o on PC-FOL dataset.

Model	k	PC-FOL Linear-Reasoning	PC-FOL Proof-by-Cases
GPT-4o	1	82.58	46.38
	2	96.67	71.82
	3	99.41	85.13
	4	100.0	92.95
	5	100.0	95.50

Table 7: Pass

@

k results for GPT-4o model on the PC-FOL dataset.

Category	PC-FOL Linear-Reasoning	PC-FOL Proof-by-Cases
Wrong Label Wrong Proof	15.07 $\%$	45.79 $\%$
Correct Label Wrong Proof	4.31 $\%$	28.18 $\%$
Correct Label Correct Proof	80.63 $\%$	26.03 $\%$

Table 8: Proportions of the three answer categories (round to two decimal places) of GPT-4o (web interactive) on our PC-FOL dataset.

Panel of Figure 2 — Figure 2: Upper : The abstracted reasoning chain for right side example of Table 2 . Lower : The abstracted reasoning chain for a typical example that existing a contradiction in a subcase. The dotted line represents a possible case inferred from a certain premise and the previous steps, and the red double-headed arrow denotes the existence of a contradiction.

Appendix figures & tables9 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 3: The distribution of the number of premises in each instance of the PC-FOL dataset. Blue color represents the distribution of the proof-by-case type problems, and the yellow color represents the distribution of the linear reasoning type problems.

Model	PC-FOL Linear reasoning	PC-FOL proof-by-case	PC-FOL-Replace Linear reasoning	PC-FOL-Replace proof-by-case
GPT-4o 0-shot	85.13	51.08	84.34	51.66
GPT-4o 3-shot	83.17	55.58	82.39	52.64
GPT-4.1 0-shot	89.24	69.86	88.45	63.80
GPT-4.1 3-shot	86.30	71.23	84.34	68.69
o4-mini 0-shot	90.80	79.84	88.26	77.89
o4-mini 3-shot	90.02	80.43	88.45	79.45

Appendix

Table 9: Logical reasoning accuracy results of zero-shot and few-shot prompting on English PC-FOL dataset.

	PC-FOL Linear-Reasoning Accuracy	PC-FOL Proof-by-Cases Accuracy	PC-FOL Acc. Gap
Temperature 0	82.39	54.99	27.40 ↓
Temperature 0.5	83.17	55.58	27.59 ↓
Temperature 1	82.39	52.45	29.94 ↓
Average	82.65	54.34	28.31 ↓
Standard Deviation	0.4503	1.6632	-

Appendix

Table 10: Evaluating the GPT-4o model on PC-FOL dataset. Random seeds of the model are fixed as 1.

	PC-FOL Linear-Reasoning Accuracy	PC-FOL Proof-by-Cases Accuracy	PC-FOL Acc. Gap
Random seed 1	82.39	52.45	29.94 ↓
Random seed 11	84.15	52.25	31.90 ↓
Random seed 22	82.19	48.73	33.46 ↓
Average	82.91	51.14	31.77 ↓
Standard Deviation	1.0785	2.0924	-

Appendix

Table 11: Evaluating the GPT-4o model on PC-FOL dataset. Temperatures of the model are fixed as 1.

Model	w/ SFT	PC-FOL w/ proof		PC-FOL w/o proof
Model	w/ SFT	Linear reasoning	proof-by-case	Linear reasoning	proof-by-case
Flan-T5-large	Yes	47.37 ↑	35.53 ↑	57.89 ↑	47.37 ↑
Flan-T5-large	No	46.05	30.26	43.42	36.84
Llama-3.1-8B-Instruct	Yes	73.68 ↑	48.68 ↓	59.21 ↑	46.05 ↑
Llama-3.1-8B-Instruct	No	64.47	50.00	57.89	40.79
Qwen3-0.6B	Yes	61.84 ↑	32.89 ↓	40.79 -	36.84 ↑

Appendix

Table 12: Fine-tuning results (Label Accuracy in %) of LLMs trained on the full set of PC-FOL dataset and tested on the test set of Case/Linear.

Model	SFT Data	PC-FOL w/ proof		PC-FOL w/o proof
Model	SFT Data	Linear reasoning	proof-by-case	Linear reasoning	proof-by-case
Qwen3-0.6B	Linear	-	36.84	-	47.37
	Case	72.37	-	51.32	-
	Null	57.89	39.47	40.79	32.89

Appendix

Table 13: Fine-tuning results of Qwen3 trained on the Linear/Case of PC-FOL dadaset and tested on the test set of Case/Linear.

Figure 4: Comparison between the ground truth of the correct proof ratio and the estimated correctness ration over the PC-FOL Linear-Reasoning dataset.

Panel of Figure 5 — Figure 5: Left : The abstracted reasoning chain for right side example of Table 2 . Right : The abstracted reasoning chain for a typical example that existing a contradiction in a subcase.

Figure 6: The distribution of the number of proof steps over the PC-FOL dataset (linear-reasoning part).

Logical Reasoning

Logical reasoning studies how formal rules support valid inference, knowledge representation, and reliable decisions.

See all 161 papers

Mathematical Reasoning in Large Language Models: Benchmarks, Architectures, Evaluation, and Open Challenges
May 19, 2026Husnain Amjad, Raja Khurram Shahzad, Aamir Shahzad +1Mathematical Reasoning Benchmarks LLM Evaluation
School of Electrical Engineering and Computer Science, National University of Sciences and Technology, Islamabad, Pakistan · Department of Communication, Quality Management and Information Systems, Mid Sweden University, Östersund Campus, Sweden · School of Computing, Data, and Mathematical Sciences, Western Sydney University, Indonesia
Improving Mathematical Reasoning Capabilities in Large Language Models via Reasoning Process Error Classification
Sep 14, 2026Runa Yoshida, Kosuke Nishida, Kyosuke NishidaLLM Prompting LLM Mathematical Reasoning
Human Informatics Labs., NTT, Inc.
Failure Modes of Large Language Models on Research-Level Mathematics: A Taxonomy and an Empirical Characterisation
Jun 12, 2026Arnesh Banerjee, Ayushi BhattacharjeeMathematical Reasoning Benchmarks LLM Auditing
Dept. of CSE (Data Science) Heritage Institute of Technology Kolkata, India

May 19, 2026J/K move · Enter open · S save

Mathematical Reasoning in Large Language Models: Benchmarks, Architectures, Evaluation, and Open Challenges

Husnain Amjad, Raja Khurram Shahzad, Aamir Shahzad, Mehwish Fatima

School of Electrical Engineering and Computer Science, National University of Sciences and Technology, Islamabad, Pakistan · Department of Communication, Quality Management and Information Systems, Mid Sweden University, Östersund Campus, Sweden · School of Computing, Data, and Mathematical Sciences, Western Sydney University, Indonesia

Mathematical Reasoning Benchmarks LLM Evaluation Process Supervision LLM Mathematical Reasoning

Open paper AskPDF arXiv

Mathematical reasoning is essential for problem-solving in education, science, and industry, serving as a crucial benchmark for evaluating artificial intelligence systems. As Large Language Models (LLMs) improve their reasoning capabilities, understanding how well they perform mathematical reasoning has become increasingly important. This survey synthesizes recent advancements in mathematical reasoning with LLMs through a structured analysis of datasets, architectures, training strategies, and evaluation protocols. Our systematic review encompasses approximately 120 peer-reviewed studies and preprints, examining the evolution of this research area and providing a unified analytical framework to understand current progress and limitations. Our study particularly introduces a unified taxonomy of mathematical datasets, distinguishing between pretraining corpora, supervised fine-tuning resources, and evaluation benchmarks across varying levels of reasoning complexity. A systematic analysis of reasoning architectures and training strategies, including tool integration, verifier-guided reasoning, and parameter-efficient adaptation, is presented to assess their effects on reasoning robustness and generalization. Moreover, a comparative evaluation of existing metrics highlights the gap between final-answer accuracy and process-level reasoning verification. By synthesizing insights across these areas, our analysis identifies recurring failure modes, such as reasoning faithfulness issues, benchmark biases, and generalization limitations, and outlines key research directions toward improving symbolic grounding, evaluation reliability, and the development of more robust and trustworthy LLM-based reasoning systems.

Abstract

Logical Reasoning

Explore similar work

Mathematical Reasoning in Large Language Models: Benchmarks, Architectures, Evaluation, and Open Challenges

Improving Mathematical Reasoning Capabilities in Large Language Models via Reasoning Process Error Classification

Failure Modes of Large Language Models on Research-Level Mathematics: A Taxonomy and an Empirical Characterisation