# Beyond Correctness: Exposing LLM-generated Logical Flaws in Reasoning via Multi-step Automated Theorem Proving
**Authors**: Xinyi Zheng, Ningke Li, Xiaokun Luan, Kailong Wang, Ling Shi, Meng Sun, Haoyu Wang
> Huazhong University of Science and TechnologyWuhanChinaxinyi˙zheng@hust.edu.cn
> National University of SingaporeSingaporeningke˙li@u.nus.edu
> Peking UniversityBeijingChinaluanxiaokun@pku.edu.cn
> Huazhong University of Science and TechnologyWuhanChinawangkl@hust.edu.cn
> Nanyang Technological UniversitySingaporeling.shi@ntu.edu.sg
> Peking UniversityBeijingChinasunm@pku.edu.cn
> Huazhong University of Science and TechnologyWuhanChinahaoyuwang@hust.edu.cn
(2026)
Abstract.
Large Language Models (LLMs) have demonstrated impressive reasoning capabilities, leading to their adoption in high-stakes domains such as healthcare, law, and scientific research. However, their reasoning often contains subtle logical errors masked by fluent language, posing significant risks for critical applications. While existing approaches like fact-checking, self-consistency methods, and rule-based validation provide partial solutions, they fail to detect complex logical flaws in multi-step reasoning.
To overcome these challenges, we present MATP, an evaluation framework for systematically verifying LLM reasoning via Multi-step Automatic Theorem Proving. MATP translates natural language reasoning into First-Order Logic (FOL) and applies automated theorem provers to assess step-by-step logical validity. This approach identifies hidden logical errors and provides fine-grained classifications of reasoning correctness. Evaluations on a benchmark comprising 10,830 reasoning instances generated by 10 LLMs across tasks from PrOntoQA-OOD, ProofWriter, and FOLIO show that MATP surpasses prompting-based baselines by over 42 percentage points in reasoning step verification. It further reveals model-level disparities, with reasoning models generating more logically coherent outputs than general models. These results demonstrate MATP ’s potential to enhance the trustworthiness of LLM-generated reasoning. journalyear: 2026 copyright: acmlicensed conference: 48th IEEE/ACM International Conference on Software Engineering; April 12-18, 2026; Rio de Janeiro, Brazil booktitle: 48th IEEE/ACM International Conference on Software Engineering (ICSE ’26), April 12-18, 2026, Rio de Janeiro, Brazil
1. Introduction
Large Language Models (LLMs) have achieved remarkable progress in natural language understanding and generation, demonstrating strong capabilities in reasoning (qiao-etal-2023-reasoning; huang-chang-2023-towards; ahn-etal-2024-large), inference (wan2024efficient), and decision-making (Yang2023FoundationMF; Eigner2024DeterminantsOL). Their success has driven their adoption in high-stakes domains including healthcare (Clusmann2023), law (LAI2024181), finance (10.1145/3604237.3626869), and scientific research (zhang-etal-2024-comprehensive-survey; 10.1145/3581784.3613215), where reliable reasoning is essential. However, safe deployment remains challenging: despite producing fluent and seemingly coherent outputs, LLMs often exhibit subtle logical errors, contradictions, or unsupported inferences (li-etal-2024-reason; payandeh-etal-2024-susceptible; mndler2024selfcontradictory) that could lead to serious consequences like misdiagnoses, flawed legal judgments, or erroneous research conclusions. Recent efforts to address these limitations include Large Reasoning Models (LRMs) that augment LLMs with neuro-symbolic AI, reinforcement learning, and causal inference. Yet Apple’s recent analysis (illusion-of-thinking) reveals that even LRMs struggle with complex tasks, often relying on shallow heuristics rather than robust reasoning. Moreover, LLM reasoning remains vulnerable to adversarial attacks, where minor input perturbations can systematically corrupt reasoning chains (gan-etal-2024-reasoning; wu-etal-2024-decot).
Existing research has largely focused on detecting flawed reasoning in LLM outputs, but existing methods face key limitations. Fact-checking approaches (tam-etal-2023-evaluating; chen2023felm; Augenstein2024) verify factual accuracy using external knowledge bases but often miss logical errors, especially when reasoning involves novel or implicit fact combinations. Self-consistency methods (wang2023selfconsistency) reduce random mistakes via majority voting across outputs, yet fail to catch systematic errors repeated across generations. Rule-based and post-hoc validation (Xie2025LogicRLUL; krishna2023post; servantez-etal-2024-chain) can flag simple contradictions but struggle with complex, multi-step logic, offering only limited coverage of reasoning flaws.
Prior works (NEURIPS2023_8e9c7d4a; olausson-etal-2023-linc; pan2023logiclm), using formal methods to enhance LLM reasoning, provide valuable insights. We consider applying formal methods to evaluate, rather than enhance, LLM reasoning quality as a promising direction for rigorous analysis. Despite their theoretical appeal, several intertwined challenges remain. Challenge#1: absence of explicit logical structure in LLM-generated reasoning. Unlike formal reasoning systems, LLMs generate reasoning via probabilistic pattern matching rather than structured inference, resulting in verbose and implicit reasoning chains. Formalizing such unstructured reasoning into precise logical representations is highly challenging, especially compared with Logic-LM (pan2023logiclm), which only formalizes predefined reasoning tasks. Challenge#2: subtle and silent reasoning errors within LLMs. A single incorrect or unsupported inference step can silently contaminate subsequent reasoning, producing conclusions that appear plausible yet are fundamentally unsound. Identifying and isolating such errors is difficult because it requires precise tracking and validation of logical dependencies throughout an entire reasoning chain.
<details>
<summary>x1.png Details</summary>
### Visual Description
\n
## Diagram: Logical Reasoning Challenge - Premises & Conclusion
### Overview
This image presents a logical reasoning challenge. It lists a set of premises (numbered 1-24) and a conclusion ("The mouse is green"). The diagram then shows the reasoning processes of two Large Language Models (LLMs), GPT-3.5-Turbo and GPT-4, in determining whether the conclusion is true or false based on the given premises. Both models arrive at the conclusion that the statement is False.
### Components/Axes
The diagram is divided into three main sections:
1. **Premises (Left):** A numbered list of 24 statements.
2. **LLM Reasoning (Center & Right):** Two columns, one for GPT-3.5-Turbo and one for GPT-4, each detailing their reasoning process as a numbered list.
3. **Header (Top):** Contains the title "Based on the known premises, answer whether the conclusion is True or False, and give the corresponding reasoning process." and a smiling face emoji.
4. **Footer (Bottom):** Contains the conclusion statement "The mouse is green" and the results of the LLM evaluations.
### Content Details
**Premises (1-24):**
1. The bear is green.
2. The bear likes the cat.
3. The bear likes the dog.
4. The bear visits the dog.
5. The cat is young.
6. The cat sees the bear.
7. The cat sees the dog.
8. The cat visits the bear.
9. The cat visits the mouse.
10. The dog is round.
11. The dog likes the bear.
12. The dog likes the mouse.
13. The dog visits the mouse.
14. The mouse is big.
15. The mouse is cold.
16. The mouse is round.
17. If something visits the mouse and the mouse visits the dog then it is cold.
18. If something likes the cat then it visits the dog.
19. If something is cold then it likes the cat.
20. If something is green then it sees the dog.
21. If something likes the mouse then it sees the cat.
22. If something is green and something likes the cat then it is round.
23. If something is round then it is green.
24. If something likes the bear then it is green.
**GPT-3.5-Turbo Reasoning:**
1. The cat is young. (Premise 5)
2. The cat sees the bear. (Premise 6)
3. If something sees the bear then it is green. (Unknown)
4. The bear is green. (Premise 1)
5. If something likes the cat then it visits the dog. (Premise 18)
6. The bear visits the dog. (Premise 4)
7. If something visits the dog and the dog likes the bear then it is cold. (Unknown)
8. If something is cold then it likes the cat. (Premise 19)
9. The bear likes the cat. (Premise 2)
10. The dog likes the bear. (Premise 11)
11. The dog visits the mouse. (Premise 13)
12. If something visits the mouse and the mouse visits the dog then it is cold. (Premise 17)
13. The mouse is cold. (Premise 15)
14. If something is cold then it likes the cat. (Premise 19)
15. The mouse likes the cat. (Premise 15 & Premise 19 & Premise 18)
16. If something likes the mouse then it sees the cat. (Premise 21)
17. The mouse sees the cat. (Premise 16 & Premise 21)
18. If something is green then it sees the dog. (Premise 20)
19. The bear is green. (Premise 1)
20. The bear sees the dog. (Premise 20 & Premise 1)
**GPT-4 Reasoning:**
1. The bear is green. (Premise 1)
2. The cat visits the bear. (Premise 8)
3. The cat visits the mouse. (Premise 9)
4. The mouse visits the dog. (Premise 9)
5. If something visits the mouse and the mouse visits the dog then it is cold. (Premise 17)
6. The cat visits the mouse and the mouse visits the dog. (Reasoning Step 3 & Reasoning Step 4)
7. The cat is cold. (Reasoning Step 5 & Reasoning Step 6)
8. If something is cold then it likes the cat. (Premise 19)
9. The cat likes the cat. (Reasoning Step 7 & Reasoning Step 8)
10. If something likes the mouse then it sees the cat. (Premise 21)
11. The cat sees the cat. (Reasoning Step 9 & Premise 21)
12. If something is green then it sees the dog. (Premise 20)
13. The bear sees the dog. (Premise 1 & Premise 20)
**Results:**
Both GPT-3.5-Turbo and GPT-4 answer: **False**.
### Key Observations
* Both LLMs attempt to derive the conclusion based on the provided premises, but both arrive at the conclusion that the statement "The mouse is green" is false.
* The reasoning processes differ significantly between the two models, demonstrating different approaches to logical deduction.
* The reasoning chains involve multiple steps of applying premises and making inferences.
* The "Unknown" statements in GPT-3.5-Turbo's reasoning indicate that the model encountered premises it could not directly apply.
### Interpretation
This diagram illustrates the challenge of automated logical reasoning. While both LLMs can process the premises and attempt to construct a logical argument, their reasoning processes are not necessarily transparent or consistent. The fact that both models arrive at the same conclusion (False) suggests that the premises do not logically support the statement "The mouse is green." The differences in their reasoning paths highlight the complexities of natural language understanding and the potential for different interpretations of the same information. The diagram serves as a test case for evaluating the capabilities and limitations of LLMs in performing logical inference. The inclusion of "Unknown" steps in GPT-3.5-Turbo's reasoning suggests a limitation in its ability to handle all the premises effectively.
</details>
Figure 1. Motivating Example. Premises used by GPT-3.5-Turbo are marked in Bright Blue; GPT-4o includes these and adds Deep Magenta premises. GPT-3.5-Turbo’s reasoning is invalid, while GPT-4o, leveraging Premises 8, 9, and 15, yields the correct answer with a valid reasoning process.
To address the challenges outlined above, we propose Multi-step Automatic Theorem Proving (MATP), a post-hoc evaluation framework that enables fine-grained analysis of LLM-generated reasoning. MATP leverages the natural language understanding capabilities of LLMs to convert both reasoning tasks and model-generated reasoning chains into unified First-Order Logic (FOL) representations in a single pass (Challenge #1), enabling structured verification via Automated Theorem Prover (ATP). It subsequently verifies the correctness of each reasoning step and searches for a valid proof path within the reasoning chain that logically entails the final conclusion, thereby distinguishing genuine deductive reasoning from mere information regurgitation (Challenge #2). Based on the verification outcomes, MATP performs fine-grained classification of reasoning chains—identifying whether a chain is fully valid, partially flawed, or logically inconsistent. This classification jointly considers answer correctness, step-level validity, and proof-path soundness, moving beyond binary accuracy metrics to provide deeper insights into reasoning quality. Through this design, MATP provides a more interpretable and reliable assessment of LLM reasoning performance in complex deductive tasks.
Results and Findings. We evaluate MATP through extensive experiments on two datasets: (1) a benchmark comprising reasoning tasks from PrOntoQA-OOD (PrOntoQAOOD), ProofWriter (tafjord2021proofwriter), and FOLIO (han2024folio), along with LLM-generated responses from 10 mainstream LLMs, including five general and five reasoning models, totaling 10,830 instances; and (2) a classification dataset based on PrOntoQA-OOD, constructed by applying controlled perturbations to standard reasoning chains. Across the benchmark dataset, MATP converts natural language sentences to FOL representations with over 99% accuracy on syntactically simpler tasks from PrOntoQA-OOD and ProofWriter, while maintaining relatively strong performance on the more linguistically complex tasks from FOLIO. In verifying individual reasoning steps, MATP consistently outperforms prompting-based baselines by more than 42 percentage points in macro F1-score. On the classification dataset, MATP achieves 99% classification accuracy, substantially outperforming all baselines and demonstrating its ability to distinguish fine-grained reasoning types, though occasional misclassifications remain.
Based on MATP ’s evaluation and classification of all LLM-generated responses in the benchmark dataset, we observe that reasoning models—especially DeepSeek-R1—produce more logically coherent reasoning chains than general models, despite similar answer accuracy. Moreover, most evaluation failures originate from errors in the NL2FOL translation stage. We further identify and summarize common failure patterns, providing insights to guide future improvements in LLM-generated reasoning evaluation.
Contributions. The main contributions of this paper are:
- A post-hoc evaluation framework for LLM-generated reasoning. We propose MATP, a framework that integrates formal methods to evaluate LLM-generated reasoning by verifying both step-level correctness and overall logical consistency. MATP is open-sourced at the repository (matp).
- A novel fine-grained reasoning chain classification. We introduce a new classification scheme that distinguishes between sound, partially flawed, and invalid reasoning chains, enabling more nuanced evaluation of LLM-generated reasoning quality.
- Analysis of LLM-generated reasoning behaviors. By large-scale evaluation and classification, we uncover model-specific reasoning patterns and failure modes, and identify common NL2FOL translation errors that inform future improvements.
2. Background and Motivation
2.1. Logic Reasoning in LLMs
Logical reasoning tasks performed by LLMs are generally categorized into inductive, abductive, and deductive reasoning. Among these, deductive reasoning is particularly crucial and forms the core focus of our work. It emphasizes rigorous, consistent, and systematic inference from explicitly stated premises, making it essential in high-assurance domains such as formal verification, legal reasoning, and security-critical decision-making. Recent neuro-symbolic efforts have shown the feasibility of transforming natural language into formal representations and LLM–Prover integration for formal reasoning (pan2023logiclm; olausson-etal-2023-linc; NEURIPS2023_8e9c7d4a). Inspired by these efforts, we propose a lightweight divide-and-conquer framework for assessing logical validity in LLM-generated deductive reasoning chains.
A motivating example. Figure 1 illustrates why systematic verification of LLM reasoning is necessary. When given a deductive reasoning task from ProofWriter, both GPT-3.5-Turbo and GPT-4o reach the correct conclusion but through vastly different reasoning processes. Notably, both models express their reasoning in natural language without an explicit logical structure, making it difficult to verify the correctness of individual steps and their interconnections. This highlights Challenge #1. GPT-3.5-Turbo’s reasoning contains critical flaws: steps 3 and 7 introduce unsupported information while step 13 contradicts the premises—yet these errors are masked by fluent natural language. This illustrates Challenge #2 for identifying subtle yet consequential reasoning errors. Moreover, even when individual steps seem correct, the entire reasoning chain generated by GPT-3.5-Turbo still fails to support the conclusion, indicating that the answer might be coincidental.
2.2. Formal Foundations
We outline the technical foundations for formalizing and verifying logical reasoning using first-order logic (FOL) and automated theorem provers (ATPs).
FOL serves as a formal language for representing and reasoning about logical statements. It extends propositional logic with predicates and quantified variables, enabling the expression of general statements about objects in a domain. The core components of FOL include: constants representing specific objects, predicates representing properties or relations, logical connectives such as negation ( $\neg$ ), conjunction ( $\wedge$ ), disjunction ( $\lor$ ), and implication ( $→$ ), and quantifiers ( $∀$ for “for all”, $∃$ for “there exists”).
The central criterion for evaluating such reasoning is logical validity. A conclusion $C$ is a logical consequence of a set of premises $P=\{P_{1},P_{2},...,P_{n}\}$ , denoted as $P\models C$ , if and only if $C$ is true in every model (i.e., every possible interpretation of the symbols) that satisfies all premises in $P$ . This property of validity ensures that there can be no counterexample where the premises hold true but the conclusion does not, providing a rigorous standard for correctness. In sound and complete logical systems like FOL, this semantic entailment ( $\models$ ) is equivalent to syntactic provability ( $\vdash$ ), meaning a valid conclusion can also be derived from the premises through a finite sequence of formal inference steps. Our work aims to automatically check if the content generated by LLMs satisfy this standard of validity with respect to the given premises.
ATPs are specialized tools designed to automatically determine the validity of logical entailments in formal systems like FOL. State-of-the-art ATPs, including Vampire (kovacs2013vampire) used in our work, primarily operate on the principle of proof by refutation. To verify the logical validity $P\models C$ , the prover mechanistically attempts to find a syntactic proof for the unsatisfiability of $P\cup\{\neg C\}$ , i.e., it searches for a derivation $P\cup\{\neg C\}\vdash\bot$ , where $\bot$ represents a contradiction. Due to the completeness of FOL, finding such a proof provides a definitive confirmation of the original semantic entailment $P\models C$ . For interoperability, our framework translates FOL formulas into the standardized TPTP (Thousands of Problems for Theorem Provers) format (sutcliffe2017tptp). Using a high-performance ATP like Vampire enables the rigorous and automated validation of reasoning steps at scale.
3. Methodology
<details>
<summary>x2.png Details</summary>
### Visual Description
\n
## Diagram: MATP - Multi-hop Automated Theorem Proving
### Overview
The image presents a diagram outlining the Multi-hop Automated Theorem Proving (MATP) framework. It details the process from a reasoning task, through Natural Language to First-Order Logic (NL2FOL) conversion, automated logic verification, and finally, response analysis and classification. The diagram is divided into four main sections, visually separated by distinct backgrounds and titles.
### Components/Axes
The diagram consists of four main sections:
1. **Reasoning Task:** Presents premises and a conclusion, along with a ground truth label.
2. **§3.2 NL2FOL:** Details the process of converting natural language premises and conclusions into First-Order Logic (FOL).
3. **§3.3 Automated Logic Verification:** Illustrates the verification process using ATP (Automated Theorem Provers).
4. **§3.4 Response Analysis and Classification:** Shows the analysis of predicted answers and the identification of valid proof paths.
Each section contains text boxes, flowcharts, and logical statements. The diagram uses color-coding to represent different outcomes (e.g., green for success, red for failure).
### Detailed Analysis or Content Details
**1. Reasoning Task (Leftmost Section):**
* **Title:** Reasoning Task
* **Premises (P1-P6):**
* P1: The cat sees the bear.
* P2: The mouse is cold.
* P3: If something hits the mouse and the mouse vents then it is cold.
* P4: If something hits the cat then it wants the dog.
* P5: If something is cold then it likes the dog.
* P6: Something hits the cat.
* **Conclusion (C):** The cat is not cold.
* **Ground Truth Label (L):** False.
* **Interact with Target LLMs:** Text states "Based on the known premises, answer whether the conclusion is True or False, and give the corresponding reasoning process."
* **Reasoning Steps (S):**
* S1: The cat sees the bear.
* S2: If something hits the cat then it wants the dog.
* S3: Something hits the cat.
* S4: The cat wants the dog.
* S5: If something is cold then it likes the dog.
* **Predicted Answer (A):** The cat is not cold.
* **Predicted Answer Label:** False.
**2. §3.2 NL2FOL (Top-Center Section):**
* **Title:** §3.2 NL2FOL
* **Sub-Title:** Reasoning Steps Filtering
* **Text:** "Parse the premises and the conclusions into first-order logic formulas."
* **Premises/FOL:**
* P1: See(cat, bear)
* P2: Cold(mouse)
* P3: ∃x(Hit(x, mouse) ∧ Vent(x, mouse) → Cold(x))
* P4: ∃x(Hit(x, cat) → Want(x, dog))
* P5: ∃x(Cold(x) → Like(x, dog))
* P6: Hit(x, cat)
* **Conclusions/FOL:**
* C: ¬Cold(cat)
* **LLM Generation:** Text states "Generate the corresponding reasoning path."
**3. §3.3 Automated Logic Verification (Right-Center Section):**
* **Title:** §3.3 Automated Logic Verification
* **Text:** "Single Statement Verification with ATP"
* **Flowchart:**
* FOL to TPTP: FOL → TPTP
* Execution: ATP Tool
* State_Verif(P, S) → {True/False/Unknown}
* Execution Fail → ATP Tool
* **Predicted Answer Correctness:** A = ? → True
* **Reasoning Steps Correctness:** State_Verif(P, S, S) = ? → {S1: True, S2: True, S3: True, S4: False}
* **Valid Proof Path Existence:** State_Verif(S1, S2, S3, S4) → False
* **sk(s)≠north:** S4: True
**4. §3.4 Response Analysis and Classification (Bottom-Right Section):**
* **Title:** §3.4 Response Analysis and Classification
* **Question:** "With Correct Predicted Answer?"
* **Flowchart:**
* Yes → "With Valid Proof Path?"
* Yes → T1
* No → F1
* No → "Without False Step?"
* Yes → T2
* No → F2
* "Without False Step?"
* Yes → T3
* No → F3
* "Without False Step?"
* Yes → T4
* No → F4
The flowchart shows four possible outcomes: T1, F1, T2, F2, T3, F3, T4, and F4, representing different combinations of correct/incorrect predictions and valid/invalid proof paths.
### Key Observations
* The diagram illustrates a pipeline for automated reasoning, starting from natural language input and ending with a classified response.
* The use of First-Order Logic (FOL) as an intermediate representation allows for formal verification using ATP tools.
* The flowchart in the Response Analysis section highlights the importance of both the correctness of the predicted answer and the validity of the reasoning steps.
* The diagram shows that the reasoning steps S1, S2, and S3 are considered correct, but S4 is incorrect, leading to a false conclusion regarding the existence of a valid proof path.
* The color-coding (green for true, red for false) provides a quick visual indication of the success or failure of each step.
### Interpretation
The diagram demonstrates a system designed to evaluate the reasoning capabilities of Large Language Models (LLMs). By translating natural language into formal logic, the system can rigorously verify the correctness of the LLM's conclusions and the validity of its reasoning steps. The classification scheme (T1-F4) provides a nuanced assessment of the LLM's performance, distinguishing between cases where the answer is correct due to a valid proof, incorrect due to a flawed proof, or incorrect despite a seemingly logical reasoning process. The diagram suggests that the system is capable of identifying subtle errors in reasoning, even when the initial premises and conclusions appear plausible. The failure in step S4 indicates a potential weakness in the LLM's ability to correctly apply logical rules or handle conditional statements. This framework is valuable for developing and evaluating LLMs that are capable of complex reasoning tasks. The diagram is a high-level overview of the MATP framework, and further details would be needed to understand the specific algorithms and techniques used in each step.
</details>
Figure 2. The workflow of MATP. Yellow nodes indicate the input, while pink nodes represent intermediate outputs.
We develop a fine-grained evaluation framework for LLM-generated reasoning in deductive tasks, focusing on more than just the final answer’s correctness (§ 3.1). Specifically, MATP uses an LLM to convert both reasoning tasks and model-generated responses into formal representations (§ 3.2), employs an ATP tool and designed algorithms to verify step-level correctness and overall validity of the reasoning chain (§ 3.3), and classifies the reasoning chain into fine-grained categories (§ 3.4). An overview is shown in Figure 2.
3.1. Task Formalization
Given a set of premises and a candidate conclusion, the target LLM is prompted to determine whether the conclusion logically follows from the premises and to generate reasoning to support its judgment. MATP takes the problem statement and the generated reasoning content as input, and performs formal verification to assess both the correctness of individual reasoning steps and the overall sufficiency of the reasoning chain. Formally, the input to MATP is defined as $D=\{P,C,L,S,A\}$ , consisting of five components:
1. Premises ( $P$ ): A set of factual statements $P=\{P_{1},P_{2},...,P_{n}\}$ , where each $P_{i}$ is assumed to be true for subsequent reasoning.
1. Candidate Conclusion ( $C$ ): A statement that is subject to validation based on the given premises $P$ . By design, it is guaranteed to either logically follow from $P$ or contradict it.
1. Ground Truth Label ( $L$ ): A manually annotated label $L∈\{True,False\}$ representing the correctness of the candidate conclusion $C$ under the given premises $P$ . Specifically, $True$ indicates that $P\vdash C$ , i.e., $C$ logically follows from $P$ , and $False$ indicates that $P\vdash\neg C$ , i.e., $C$ contradicts $P$ .
1. Reasoning Steps ( $S$ ): A sequence of intermediate statements $S=(S_{1},S_{2},...,S_{m})$ generated by the target LLM during its reasoning process, where each $S_{i}$ represents a statement produced as part of the model’s reasoning trajectory toward validating or refuting the conclusion.
1. Predicted Answer ( $A$ ): The final judgment $A∈\{True,False\}$ produced by the target LLM regarding the correctness of the candidate conclusion $C$ , representing the model’s decision based on the reasoning steps $S$ .
Based on the input $D$ , MATP translates the premises $P$ , candidate conclusion $C$ , and reasoning steps $S$ into FOL formulas and performs logical verification using an automated theorem prover. It produces three key outputs to facilitate comprehensive evaluation:
1. Reasoning Step Correctness Annotation: For each reasoning step, MATP assigns a correctness label $StepCorrectness(S_{i})\newline
∈\{True,False,Unknown\}$ , indicating whether $S_{i}$ is provable, refutable, or indeterminate based on the premises $P$ .
1. Valid Proof Path Existence: MATP searches for a subset of correct reasoning steps $S_{inProofPath}⊂eq S$ that together entail the conclusion $C$ or its negation $\neg C$ . If such a valid proof path exists, it indicates that the reasoning chain is logically sound.
1. Fine-Grained Classification of the Reasoning Chain: By analyzing the correctness of the final predicted answer, the correctness of individual reasoning steps, and the existence of a valid proof path, MATP categorizes the reasoning output into distinct fine-grained classes.
Through this principled workflow, MATP enables a rigorous and interpretable assessment of LLM reasoning capabilities, going beyond surface-level correctness to reveal potential logical errors and providing insights into the underlying reasoning structure.
3.2. NL2FOL
This module converts the given premises $P$ , candidate conclusion $C$ , and reasoning steps $S$ into FOL representations to enable verification with automated theorem proving.
3.2.1. Preprocessing.
To ensure the accuracy and reliability of translating NL to FOL, we first apply a series of preprocessing measures.
Interacting with LLMs. To generate reasoning chains for subsequent formalization and verification, we employ a structured interaction with LLMs. Given premises $P$ and a candidate conclusion $C$ , the model is prompted to assess whether $C$ logically follows from $P$ through an explicitly generated reasoning process. We use a few-shot prompting strategy, providing annotated examples to guide the model’s behavior. The LLM is instructed to first produce a step-by-step reasoning process based solely on $P$ , followed by a True/False decision on whether $C$ is entailed. This answer-after-reasoning format decouples the reasoning trace from the final verdict, enabling fine-grained evaluation of both components. To ensure faithful reasoning, the prompt explicitly constrains the output to avoid unnecessary complexity, ambiguous language, or reliance on external knowledge. The full prompt design is included in (matp).
Further filtering. After generating the reasoning process, the output is split into individual sentences. Subsequently, uncertain or speculative statements (e.g., “Wren is not necessarily a gorpus”) are filtered out. Inspired by prior work (cui2025practical), which segments reasoning content using reflection-related keywords to identify reflective phases, we extend this approach. We remove uncertain or speculative statements by detecting ambiguity-indicative expressions (e.g., “possible”, “contradict”, or “not necessarily”), without introducing additional filtering models. The remaining reasoning steps are concise and explicit, aiding downstream processing. In particular, repetitive statements are deduplicated after converting sentences into FOL form, as direct comparison in natural language is difficult.
Prompt Template for Translating NL to FOL
Parse the given premises and conclusions into first-order logic formulas. ### Rules 1. Each sentence must be converted into a single FOL formula. 2. Use the following FOL syntax: logical conjunction of expr1 and expr2: $expr1\land expr2$ … 3. Every formula must explicitly include quantifiers ( $∀$ x or $∃$ x) where applicable … 4. When an existential entity reappears with new properties, all properties (both old and new) should be conjoined within the scope of a single existential quantifier into the later formula … … (other more specific rules) ### Output Format Premises / Conclusions: fol-formula ::: (index) reference. … ### Examples Premises: (1) The cow is cold. (2) The cow is not round. … Conclusions: (1) The mouse needs the cow. … (9) The mouse eats the mouse. ### Premises: Cold(cow) ::: (1) The cow is cold. ¬Round(cow) ::: (2) The cow is not round. … Conclusions: Needs(mouse, cow) ::: (1) The mouse needs the cow. … Eats(mouse, mouse) ::: (9) The mouse eats the mouse. ### Your Task Return first-order logic formulas with NO other texts. Premises: {premises} Conclusions: {conclusions}
Figure 3. Prompt Template for Translating NL to FOL.
3.2.2. Translating Natural Language into First-Order Logic.
Inspired by Logic-LM (pan2023logiclm), which successfully leverages prompt engineering with GPT-4 for formalizing long-text reasoning tasks, we follow its prompt design framework to implement NL2FOL. While retaining its core structure, we introduce several modifications tailored to the specific requirements of our task.
Prompt Structure. As illustrated in Figure 3, the prompt structure comprises five components: task definition, translation rules, output format, example demonstrations, and input instance, detailed as follows. Specifically, the “ conclusions ” in the prompt always include both the reasoning steps $S$ and the candidate conclusion $C$ from the actual input.
Task definition establishes the primary goal of converting premises and conclusions into corresponding FOL representations. Translation rules define the fundamental constraints that govern the NL2FOL process. They ensure that each statement is translated in strict accordance with FOL syntax, while following a set of quality assurance strategies. These rules can be flexibly adjusted based on specific scenarios when necessary. Output format requires that each generated output include a formal FOL expression, an index, and the corresponding reference sentence from the input. To ensure completeness and avoid omissions, both premises and conclusions are numerically indexed, accommodating potentially lengthy inputs. Example demonstrations show the expected input-output relationships, enhancing clarity and reinforcing the correct application of conversion principles. Input instance provides the reasoning input, where “ Premises ” corresponds to premises $P$ , and “ Conclusions ” includes both reasoning steps $S$ and the candidate conclusion $C$ . The model is instructed to output only the required FOL formulas, without any extraneous content.
Quality Assurance Strategies. In the Rules component, we implement strategies to minimize common errors and improve translation quality. For quantifier usage, variables must have explicit existential or universal quantifiers. Parentheses are applied to complex statements to define quantifier scopes and avoid ambiguity. For existentially quantified entities, multiple statements can describe different attributes of the same entity, such as introducing property A for an entity Tom and later adding property B. The later translation should integrate both properties to preserve semantic completeness. To ensure cross-step coherence in existential instantiation, we enforce rule constraints to consistently reference entities and their predicate attributes introduced in earlier steps, avoiding logical inconsistencies. As we translate premises, reasoning steps, and candidate conclusions in a single pass, LLMs’ comprehension aids predicate consistency. To further ensure consistent predicate usage, we add the rule that encourages reusing existing predicates before introducing new ones. This reduces redundancy and prevents predicate proliferation. To address LLM’s confusion between “exclusive or” and “inclusive or”, we include targeted conversion examples to clarify their distinction. Detailed implementations of these strategies are provided in the full prompt (matp).
3.2.3. Regeneration
The translation from natural language to FOL by LLMs is not always correct initially. If the generated FOL results in execution errors during verification, or if the verification outcome of the candidate conclusion contradicts the ground-truth label, the NL2FOL process is retried up to a fixed maximum number of attempts. If all retries fail, an error is returned, indicating failure to analyze the input. No feedback is provided during regeneration. Since pinpointing semantic errors in translation is challenging, we cannot provide useful and specific feedback. While using the entire output from the previous generation as feedback is another option, experiments in § 4.5 show its minimal impact.
3.3. Logical Verification
This module aims to perform logical verification on FOL representations of input statements ( $P$ , $C$ , $S$ ) using the automated theorem prover. This process assigns correctness labels to each reasoning step and determines whether a valid proof path exists.
FOL to TPTP. We convert FOL formulas into TPTP format for compatibility with standard ATP tools. This is done via a Python script that enforces a deterministic one-to-one mapping between FOL and TPTP representations. Preprocessing steps are applied to align the FOL formulas with TPTP syntax, including replacing Unicode symbols with ASCII characters, normalizing predicate and constant names, and handling unsupported logical connectives (e.g., exclusive disjunction $A\oplus B$ is rewritten as $(\neg A\land B)\lor(A\land\neg B)$ ). The script also performs lightweight syntax repair—such as correcting missing parentheses or misused connectives—to improve robustness and reduce parsing errors in downstream verification.
Each formula is translated into TPTP’s FOF format: “ fof (name, role, formula)”, where name is a unique identifier for the logical statement, role specifies whether it is an axiom or a conjecture, and formula is the FOL expression rewritten in TPTP syntax. All premises are assigned as axioms, and the candidate conclusion as a conjecture. Unique identifiers follow the pattern “ premise_index ” and “ conclusion ”. We first translate natural language into FOL before TPTP because TPTP syntax is more complex and verbose, making direct NL2TPTP translation more error-prone. Converting FOL to TPTP helps correct syntax errors and ensures compatibility with theorem provers, improving verification reliability.
Provability Verification. A core component of the verification process is to determine whether a statement $S$ is provable from a set of premises $P$ . There are three possible outcomes for $S$ : provable, which means $S$ is logically entailed by $P$ and it holds true whenever $P$ is true; refutable, which means $S$ contradicts $P$ and is always false when $P$ is true; indeterminate, which means $S$ is neither provable nor refutable based on $P$ . To determine this, we invoke the prover to simultaneously check whether $P\vdash S$ or $P\vdash\neg S$ . If either holds, $S$ is classified as True or False accordingly. If neither holds (i.e., both $P\cup{S}$ and $P\cup{\neg S}$ are consistent), $S$ is labeled Unknown. Algorithm 1 summarizes this procedure, with the outputs True, False, and Unknown corresponding to the three provability outcomes. In particular, if both $S$ and $\neg S$ are provable, it indicates a contradiction within $P$ , and we return an Error.
Algorithm 1 Single Statement Verification using ATP
1: Premises $P=\{P_{1},P_{2},...,P_{n}\}$ , candidate statement $S$
2: Check Result (True, False, Unknown, or Error)
3: function VerifySingleStatement ( $P,S$ )
4: $res_{1}←$ ATPRun ( $P,S$ ) and $res_{2}←$ ATPRun ( $P,\neg S$ )
5: if Refutation in $res_{1}$ and Refutation in $res_{2}$ then
6: return Error $\triangleright$ Contradiction exists in $P$
7: if Refutation in $res_{1}$ then
8: return True $\triangleright$ $S$ is verified
9: if Refutation in $res_{2}$ then
10: return False $\triangleright$ $\neg S$ is verified
11: return Unknown
Verification of the Reasoning Steps. We begin by applying VerifySingleStatement to the premises $P$ and the candidate conclusion $C$ to check alignment with the ground-truth label $L$ . A mismatch may arise from: (1) a semantically incorrect but syntactically valid NL2FOL translation that causes the ATP to produce a judgment on $C$ inconsistent with $L$ , or (2) an erroneous ground-truth label annotation. Since these cases cannot be automatically differentiated or corrected, the process reverts to the NL2FOL stage for regeneration. After verifying the conclusion, we assess the correctness of each intermediate reasoning step $S_{i}$ under the same premises $P$ . If a step is refuted or indeterminate, it is recorded as a potential logical error. Algorithm 2 outlines this process. The algorithm returns both the correctness of the predicted answer and the correctness annotation for each reasoning step. Notably, some incorrect steps may not affect the final judgment, while others may compromise the entire reasoning chain. To distinguish these cases, further analysis is conducted to determine whether a valid proof path exists within the reasoning steps.
Algorithm 2 Reasoning Steps Verification
1: Premises $P=\{P_{1},P_{2},...,P_{n}\}$ , candidate conclusion $C$ , ground truth label $L$ , reasoning steps $S=\{S_{1},S_{2},...,S_{m}\}$ , predicted answer $A$
2: Returns $AnswerCorrectness$ , step correctness annotation $S_{correctness}$
3: function VerifyReasoningSteps ( $P,C,L,S,A$ )
4: if VerifySingleStatement ( $P,C$ ) $≠$ $L$ then
5: return Error $\triangleright$ NL2FOL translation error or labeling error
6: $S_{correctness}←[]$ $\triangleright$ Initialize step correctness list
7: for $i← 1$ to $m$ do
8: Append ( $S_{correctness}$ , VerifySingleStatement ( $P,S_{i}$ ))
9: $AnswerCorrectness←(L=A)$ $\triangleright$ Check if the answer matches
10: return $AnswerCorrectness$ , $S_{correctness}$
Verification of the Reasoning Proof Path. Beyond evaluating individual reasoning steps, we also assess whether the reasoning process contains all the necessary steps to logically support the conclusion label. In other words, we determine whether the reasoning chain includes a valid proof path leading to the correct classification of the conclusion. To do this, we iteratively construct a candidate proof path by including only those True -labeled steps that introduce new facts not derivable from previously included steps. Formally, the proof path is a subset $S_{inProofPath}⊂eq S$ , where a step $S_{i}$ is added if and only if it is labeled True and not entailed by $S_{inProofPath}$ . After processing all steps, we check if the truth value of the candidate conclusion $C$ matches the ground truth label $L$ , when evaluated under the proof path $S_{inProofPath}$ . If True, it indicates that reasoning process contains a valid proof path that supports the conclusion label. Otherwise, the proof path is considered invalid. This verification process is detailed in Algorithm 3.
Algorithm 3 Reasoning Proof Path Verification
1: Candidate conclusion $C$ , ground truth label $L$ , reasoning steps $S=\{S_{1},S_{2},...,S_{m}\}$ , step correctness annotation $S_{correctness}$
2: Returns $HasValidProofPath$
3: function VerifyReasoningProofPath ( $C,L,S,S_{correctness}$ )
4: $S_{inProofPath}←[]$
5: for $i← 1$ to $m$ do
6: if $S_{correctness\_i}=\textbf{True}$ then
7: if VerifySingleStatement ( $S_{inProofPath},S_{i}$ ) $=\textbf{Unknown}$ then
8: Append ( $S_{inProofPath},S_{i}$ ) $\triangleright$ Construct the proof path
9: $HasValidProofPath←($ VerifySingleStatement ( $S_{inProofPath},C$ ) $=L)$
10: return $HasValidProofPath$
If the automated theorem prover encounters an execution error indicating syntactic flaws in the generated FOL content, we return to the NL2FOL stage for regeneration.
3.4. Response Analysis and Classification
After the first two stages, inputs exceeding the maximum NL2FOL retries are categorized as Error, indicating that our framework cannot handle them. For successfully processed inputs, this module performs a fine-grained classification of reasoning chains based on logical verification to evaluate the reasoning process comprehensively. Instead of only assessing the final predicted answer, we analyze both individual reasoning steps and the overall reasoning chain to identify potential logical flaws. This allows us to distinguish between responses that are correct by chance and those based on valid reasoning. After logical verification, we obtain three key evaluation dimensions: (1) correctness of the predicted answer, (2) correctness of each reasoning step, and (3) existence of a valid proof path within the reasoning chain. Based on these dimensions, we define six reasoning categories, as illustrated in Figure 2.
For responses with incorrect predicted answer, we classify them into two categories based on whether intermediate reasoning steps contain errors. Any reasoning step labeled as $False$ or $Unknown$ is considered erroneous. F1 represents cases where all reasoning steps are correct but the final answer is incorrect, suggesting that the target model likely fails to construct a valid proof path. F2 covers cases where both the final answer and at least one reasoning step are incorrect, suggesting that intermediate errors may mislead the reasoning process or that the model fails to form a coherent proof.
For responses with correct predicted answers, we assess both the correctness of individual steps and the validity of the reasoning chain. T1 denotes the ideal cases where all steps are correct and a valid proof path exists. T2 includes cases with some erroneous steps, yet the proof path remains valid—indicating partial robustness. T3 represents cases where all reasoning steps are correct, but the reasoning chain does not constitute a valid proof, suggesting that the model correctly infers the answer but fails to provide a logically complete reasoning path. T4 includes responses with step-level errors and no valid proof path, raising concerns that the correct answer may be reached by chance or flawed reasoning.
4. Evaluation
Our evaluation targets the following research questions:
- RQ1 (Effectiveness): Can MATP accurately verify the correctness of reasoning steps generated by LLMs?
- RQ2 (Reasoning Chain Classification): Can MATP effectively classify different types of reasoning chains?
- RQ3 (Model Reasoning Analysis): How do different LLMs perform in terms of reasoning quality, and what are their characteristic behaviors when generating reasoning chains?
Table 1. Evaluation of MATP on the Benchmark: NL2FOL Translation Accuracy and Reasoning Step Correctness Classification Performance. NL2FOL accuracy (§ 4.2.1) is evaluated using four metrics—ER (Execution Rate), EA (Execution Accuracy), FB (FOL BLEU), and LE (Logical Equivalence)—while reasoning step correctness (§ 4.2.2) is measured by Macro F1 score. All values are reported as percentages (%), with higher scores indicating better performance. In the metric rows, GPT-4o and DS-R1 refer to prompt-based baseline methods implemented using GPT-4o and DeepSeek-R1, respectively.
4.1. Experimental Setup
Benchmark Dataset. We construct our benchmark from three reasoning-focused datasets, each designed for natural language inference tasks. PrOntoQA-OOD (PrOntoQAOOD) and ProofWriter (tafjord2021proofwriter) focus on logical reasoning within structured ontologies, emphasizing categories, attributes, and rule-based inference, while FOLIO (han2024folio) centers on realistic semantic reasoning with knowledge about people, locations, quantities, and events. Each test case in these datasets consists of premises, a candidate conclusion, and a ground-truth label ( $True$ , $False$ , or $Unknown$ ). Test cases in PrOntoQA-OOD and ProofWriter use structured natural language, while those in FOLIO use expressions closer to everyday human language.
- PrOntoQA-OOD (PrOntoQAOOD) (384 test cases selected) is a synthetic dataset where all conclusions are labeled $True$ . Tasks are categorized by the minimal number of reasoning steps required; we sample from the 4-hop subset to ensure higher complexity.
- ProofWriter (tafjord2021proofwriter) (344 test cases selected) uses more natural language and complex logic. We sample from its 5-hop test set, excluding tasks with $Unknown$ label due to unclear entailment.
- FOLIO (han2024folio) (355 test cases selected) is a human-authored dataset grounded in real-world facts. We sample from the training set, retaining only $True$ / $False$ cases and discarding instances where the conclusion trivially repeats a premise.
To balance dataset scale and focus on higher-hop instances that elicit richer model responses, we randomly sample test cases from the maximum-hop subset of PrOntoQA-OOD and ProofWriter, rather than using all available data. For FOLIO, which lacks hop-based partitioning, we randomly sample from its training set. For each selected test case, we generate reasoning chains and predicted answers using 10 representative LLMs (detailed in the next section). The prompting template used for generation is provided in (matp). This results in a total of 10830 benchmark instances. Each instance includes the premises, candidate conclusion and ground-truth label provided by the test case, as well as the reasoning chain and predicted answer generated by the target LLM. This benchmark is used to evaluate the effectiveness of MATP (RQ1) and to analyze reasoning chain categories across models (RQ3).
Models Under Test. To ensure a comprehensive evaluation, we test 10 LLMs with MATP, including five general models and five reasoning models. The general models include GPT-3.5-turbo, GPT-4o (achiam2023gpt; hurst2024gpt), LLaMA3.1-8B-chat-hf, LLaMA3.1-70B-chat-hf (grattafiori2024llama) and Qwen2.5-7B-Instruct (qwen2.5). The reasoning models include QwQ-32B (qwen32b), DeepSeek-R1-Distill-Qwen-7B, DeepSeek-R1-Distill-Qwen-32B We use DS-R1-Qwen7B/32B to represent DeepSeek-R1-Distill-Qwen-7B/32B for short., DeepSeek-R1 (guo2025deepseek) and GPT-o4-mini (o4mini).
Model Configuration. We set temperature to 0 for stable and consistent reasoning outputs, with top-p = 1 and top-k = 0 to favor high-probability tokens. An exception is GPT-o4-mini, which uses a fixed temperature of 1 due to model limitations.
Baseline. We compare our method against a prompting-based baseline using GPT-4o and DeepSeek-R1 (RQ1 and RQ2), following (zeng2024mrgsm8kmetareasoningbenchmarklarge). The prompt elicits two outputs: (1) step-by-step judgments on reasoning steps ( $True$ , $False$ , or $Unknown$ ); and (2) a final decision on whether the reasoning supports the predicted answer ( $Yes$ or $No$ ), both with explanations. The full prompt is provided in (matp).
Implementation. Based on MetaGPT (hong2024metagpt), a development framework for multi-agent systems that coordinates tool calls and manages pipeline stages, we integrate existing components to implement the evaluation framework as an automated toolchain. Specifically, we use GPT-4o for the NL2FOL translation, leveraging its strong performance on long and complex natural language tasks, and limit generation attempts to three per input. For automated verification, we adopt the widely used automated theorem prover Vampire (kovacs2013vampire). All implementation details are available at (matp).
Running Environment. All experiments run on a server with Ubuntu 22.04, equipped with two 64-core AMD EPYC 7713 CPUs, 512 GB RAM, and two NVIDIA A100 PCIe 80GB GPUs.
4.2. RQ1: Effectiveness
We conduct evaluations on the benchmark dataset to assess the effectiveness of MATP. The evaluation focuses on two aspects: the accuracy of NL2FOL translation and the ability to identify the correctness of individual reasoning steps.
4.2.1. Accuracy of NL2FOL translation.
We evaluate NL2FOL translation at both the overall and sentence levels.
Overall Level Metrics. Following Logic-LM (pan2023logiclm), we use Execution Rate (ER) and Execution Accuracy (EA) to evaluate NL2FOL translation across the entire benchmark. ER measures the proportion of FOL outputs that can be successfully executed by Vampire, reflecting syntactic correctness. EA measures how often Vampire ’s verdict matches the ground truth label when execution succeeds, indicating semantic preservation.
Sentence Level Metrics. We adopt FOL BLEU (FB) and Logical Equivalence (LE) from LogicLLaMA (yang2023logicllama) to assess sentence-level conversion. FB applies FOL-specific tokenization to compute similarity scores, while LE determines whether the generated and reference FOL formulas are logically equivalent. For datasets with reference FOLs (FOLIO), we compute FB and LE across all premises. For others (PrOntoQA-OOD, ProofWriter), we manually annotate reference FOLs for 300 premises per dataset for metric evaluation, with cross-verification by three authors to ensure consistency.
Results. As shown in Table 1, both ER and EA on PrOntoQA-OOD and ProofWriter are close to 100%, indicating strong syntactic and semantic alignment. In contrast, FOLIO shows high ER (96.06%) but lower EA (70.88%), suggesting challenges in preserving semantics for complex statements. At the sentence level, FB and LE scores on PrOntoQA-OOD and LE on ProofWriter are near 100%. However, ProofWriter ’s FB drops to 84.07%, mainly due to mismatches in forms (e.g., “Like” vs. “Likes”) between model outputs and base-form annotations, highlighting FB’s sensitivity to surface variations. On FOLIO, the FB score drops to 36.91%, while LE remains relatively high (88.30%), reflecting logical equivalence despite low textual similarity. This discrepancy is understandable, as for complex sentences, the choice of predicate or constant names is unlikely to consistently match the expected form.
To better understand the low EA on FOLIO, we conducted a manual review of cases where the MATP ’s labels for candidate conclusion differ from the ground truth labels. The key factors contributing to this issue will be analyzed in detail in § 4.4.3.
4.2.2. Ability to identify the correctness of individual reasoning steps.
This evaluation focuses on whether each reasoning step is correctly labeled by MATP, and how it performs versus the baseline.
Metric. We formulate the task as a three-class classification problem ( $True$ , $False$ , $Unknown$ ), evaluated using macro F1-score. Given the high annotation cost, we sample 20 ER-contributing tasks per dataset for each of the ten models, totaling 600 samples. Each reasoning step correctness within these samples is manually labeled by three authors, and the aggregated annotations are used to compute the final macro F1 score.
Results. The detailed results are shown in Table 1. MATP consistently outperforms both GPT-4o and DeepSeek-R1 baselines in classifying reasoning step correctness. On PrOntoQA-OOD and ProofWriter, MATP achieves 94.26% and 91.24% F1, significantly higher than GPT-4o (47.79%, 49.36%) and DeepSeek-R1 (61.30%, 42.43%). Even on the more informal FOLIO dataset, MATP maintains 84.42% F1, while the baselines drop below 46%. We further analyze the reasons behind the poor performance of the baselines. Specifically, the baselines often mislabel correct steps as $False$ or $Unknown$ when the inference is implicit or requires multi-hop reasoning. They also struggle to distinguish between $False$ and $Unknown$ , resulting in frequent confusion between the two.
ANSWER to RQ1
MATP verifies reasoning steps by accurately translating NL to FOL and identifying correctness, outperforming prompting-based baselines across all datasets. It performs well on PrOntoQA-OOD and ProofWriter, but struggles on FOLIO due to more complex language patterns.
4.3. RQ2: Reasoning Chain Classification
To evaluate whether MATP can accurately classify reasoning chains, we conduct evaluations on a classification dataset and compare its performance with baselines.
Classification Dataset. We construct a classification dataset from 200 PrOntoQA-OOD tasks. Starting from the standard reasoning chains provided by PrOntoQA-OOD (T1-type), we apply targeted mutations to obtain different types of reasoning chains: to generate T2-type chains, we insert a negated premise to introduce false reasoning step; for T3-type chains, we remove key steps and inject irrelevant content to break the logical flow; for T4-type chains, we apply both T2-type and T3-type mutations. Each variant is created for 50 tasks to ensure balanced coverage across the four types.
Results. Figure 4 presents the classification accuracy of MATP versus the baselines. As shown, MATP achieves 100% accuracy on T1–T3 and 96% on T4. A review of the two T4 misclassifications attributes the errors to minor NL2FOL translation deviations, suggesting that with correct translation, MATP can consistently classify reasoning chains accurately. In contrast, the GPT-4o-based baseline achieves lower accuracy—78%, 72%, 84%, and 90% for T1–T4, respectively. Error analysis reveals two main issues: (1) 54 correct steps were misjudged as incorrect, causing 14 T1/T3 cases to be classified as T2/T4; and (2) it struggles to assess whether steps sufficiently support the conclusion, leading to 20 T1/T2 cases misclassified as T3/T4 and 11 T3/T4 cases misclassified as T1/T2. The DeepSeek-R1-based baseline performs better, achieving 96%, 90%, 92%, and 82% accuracy. Most misclassifications arise from failure to assess whether steps sufficiently support conclusions—6 T1/T2 cases were mistaken for T3/T4, and 13 T3/T4 as T1/T2—mainly due to its weaker instruction-following ability, often defaulting to global premise-to-conclusion matching.
While 100% classification accuracy can be guaranteed with perfect translation, we cannot ensure flawless NL2FOL translation in practice. Consequently, MATP cannot ensure absolute correctness in real-world applications. Nevertheless, it achieves significantly higher accuracy than baselines. We also record the average processing time per task for all tools. GPT-4o takes around 6s per task, DeepSeek-R1 is significantly slower at 96s, while MATP maintains a comparable speed of approximately 9s.
ANSWER to RQ2
MATP achieves perfect classification given accurate NL2FOL translation, clearly outperforming the prompting-based baselines.
<details>
<summary>x3.png Details</summary>
### Visual Description
## Heatmap: Model Prediction Confusion Matrices
### Overview
The image presents three confusion matrices, each representing the performance of a different model (MATP, GPT-4o, and DeepSeek-R1) in predicting labels (T1, T2, T3, T4). The matrices visualize the distribution of predicted labels against the ground truth labels. The color intensity represents the number of instances falling into each combination.
### Components/Axes
* **X-axis:** Predicted Label (T1, T2, T3, T4)
* **Y-axis:** Ground Truth Label (T1, T2, T3, T4)
* **Matrices:** Three separate confusion matrices, one for each model:
* MATP Predicted Label
* GPT-4o Predicted Label
* DeepSeek-R1 Predicted Label
* **Color Scale:** The color intensity represents the count of instances. Darker green indicates higher counts, while lighter green indicates lower counts.
* **Correlation Coefficient (ρ):** Displayed for each matrix, indicating the correlation between predicted and ground truth labels.
### Detailed Analysis
**MATP Predicted Label**
* **Trend:** The matrix shows strong diagonal dominance, indicating good performance.
* **Data Points:**
* T1 predicted as T1: 50
* T1 predicted as T2: 0
* T1 predicted as T3: 0
* T1 predicted as T4: 0
* T2 predicted as T1: 0
* T2 predicted as T2: 50
* T2 predicted as T3: 0
* T2 predicted as T4: 0
* T3 predicted as T1: 0
* T3 predicted as T2: 0
* T3 predicted as T3: 50
* T3 predicted as T4: 0
* T4 predicted as T1: 0
* T4 predicted as T2: 2
* T4 predicted as T3: 48
* T4 predicted as T4: 0
* **ρ:** Approximately 1.0
**GPT-4o Predicted Label**
* **Trend:** Also shows diagonal dominance, but with some off-diagonal values.
* **Data Points:**
* T1 predicted as T1: 39
* T1 predicted as T2: 4
* T1 predicted as T3: 0
* T1 predicted as T4: 7
* T2 predicted as T1: 1
* T2 predicted as T2: 36
* T2 predicted as T3: 0
* T2 predicted as T4: 13
* T3 predicted as T1: 5
* T3 predicted as T2: 1
* T3 predicted as T3: 42
* T3 predicted as T4: 2
* T4 predicted as T1: 0
* T4 predicted as T2: 5
* T4 predicted as T3: 0
* T4 predicted as T4: 45
* **ρ:** Approximately 0.9
**DeepSeek-R1 Predicted Label**
* **Trend:** Similar to GPT-4o, with diagonal dominance and some off-diagonal values.
* **Data Points:**
* T1 predicted as T1: 48
* T1 predicted as T2: 1
* T1 predicted as T3: 0
* T1 predicted as T4: 1
* T2 predicted as T1: 0
* T2 predicted as T2: 45
* T2 predicted as T3: 0
* T2 predicted as T4: 5
* T3 predicted as T1: 4
* T3 predicted as T2: 0
* T3 predicted as T3: 46
* T3 predicted as T4: 0
* T4 predicted as T1: 0
* T4 predicted as T2: 9
* T4 predicted as T3: 0
* T4 predicted as T4: 41
* **ρ:** Approximately 0.9
### Key Observations
* All three models demonstrate relatively high accuracy, as indicated by the strong diagonal dominance in their confusion matrices.
* MATP has the highest correlation coefficient (ρ ≈ 1.0), suggesting the strongest agreement between predicted and ground truth labels.
* GPT-4o and DeepSeek-R1 have slightly lower correlation coefficients (ρ ≈ 0.9), indicating some misclassifications.
* The most common misclassifications for GPT-4o and DeepSeek-R1 involve confusing T1 with T2 and T4 with T3.
* MATP has very few misclassifications, with the only notable one being T4 sometimes predicted as T3.
### Interpretation
The confusion matrices provide a comparative assessment of the three models' performance in a four-class classification task. The data suggests that MATP is the most accurate model, closely followed by GPT-4o and DeepSeek-R1. The correlation coefficients quantify the strength of the relationship between the models' predictions and the actual labels.
The off-diagonal values in the matrices reveal the types of errors each model makes. For example, the tendency of GPT-4o and DeepSeek-R1 to confuse T1 with T2 suggests that these labels may have some overlapping features or that the models struggle to distinguish between them.
The consistent diagonal dominance across all three matrices indicates that the classification task is relatively well-defined and that the models are generally able to learn the underlying patterns in the data. The slight differences in performance highlight the trade-offs between different model architectures and training strategies. The values in the matrices are counts, and the sum of each row represents the total number of instances of a particular ground truth label. The sum of each column represents the total number of times a particular label was predicted.
</details>
Figure 4. Heatmap of Reasoning Chain Classification Performance for MATP and Baselines.
4.4. RQ3: Model Reasoning Analysis
Using the reasoning chain classifications produced by MATP, we evaluate how different LLMs perform across tasks, focusing on reasoning quality and model-specific patterns. We first compare model performance across datasets, identifying strengths, limitations, and reasoning tendencies. Next, we analyze structural patterns within each category to uncover common behaviors and failure modes. Lastly, we examine cases where MATP fails to evaluate and summarize typical causes. This analysis reveals key reasoning bottlenecks and guides future improvements in LLM reasoning.
<details>
<summary>x4.png Details</summary>
### Visual Description
## Bar Chart: Performance Comparison of Language Models
### Overview
The image presents a grouped bar chart comparing the performance of several language models (GPT-3.5, GPT-4, LLaMA, Qwen, DeepSeek, and others) across three datasets: ProntoQA-OOD, ProofWriter, and FOLIO. The performance is categorized into five types of responses: T1, T2, T3, T4, F1, and Error. The y-axis represents the "Count" of responses, ranging from 0 to 400.
### Components/Axes
* **Y-axis:** "Count" (Scale: 0 to 400, increments of 50)
* **X-axis:** Language Models (GPT-3.5, GPT-4, LLaMA3.1-8B, LLaMA3.1-70B, Qwen2.5-7B, QwQ-32B, DS-R1-Qwen7B, DS-R1-Qwen32B, DeepSeek-R1, GPT-04-mini)
* **Datasets:** Three rows represent three datasets: ProntoQA-OOD, ProofWriter, and FOLIO.
* **Legend:** Located at the top-left corner, defining the color-coding for response types:
* T1 (Green)
* T2 (Light Green)
* T3 (Yellow)
* T4 (Orange)
* F1 (Red)
* Error (Dark Red)
### Detailed Analysis or Content Details
**1. ProntoQA-OOD Dataset (Top Row)**
* **GPT-3.5:** T1: ~25, T2: ~99, T3: ~115, T4: ~340, F1: ~8, Error: ~3
* **GPT-4:** T1: ~1, T2: ~14, T3: ~12, T4: ~224, F1: ~41, Error: ~1
* **LLaMA3.1-8B:** T1: ~24, T2: ~41, T3: ~27, T4: ~322, F1: ~109, Error: ~1
* **LLaMA3.1-70B:** T1: ~1, T2: ~17, T3: ~15, T4: ~199, F1: ~136, Error: ~26
* **Qwen2.5-7B:** T1: ~4, T2: ~11, T3: ~22, T4: ~72, F1: ~109, Error: ~4
* **QwQ-32B:** T1: ~0, T2: ~8, T3: ~33, T4: ~370, F1: ~128, Error: ~0
* **DS-R1-Qwen7B:** T1: ~0, T2: ~30, T3: ~82, T4: ~320, F1: ~84, Error: ~8
* **DS-R1-Qwen32B:** T1: ~0, T2: ~22, T3: ~44, T4: ~306, F1: ~79, Error: ~2
* **DeepSeek-R1:** T1: ~0, T2: ~4, T3: ~51, T4: ~770, F1: ~38, Error: ~0
* **GPT-04-mini:** T1: ~1, T2: ~13, T3: ~12, T4: ~360, F1: ~82, Error: ~1
**2. ProofWriter Dataset (Middle Row)**
* **GPT-3.5:** T1: ~64, T2: ~52, T3: ~74, T4: ~105, F1: ~224, Error: ~2
* **GPT-4:** T1: ~56, T2: ~39, T3: ~50, T4: ~224, F1: ~24, Error: ~10
* **LLaMA3.1-8B:** T1: ~87, T2: ~70, T3: ~54, T4: ~155, F1: ~87, Error: ~2
* **LLaMA3.1-70B:** T1: ~76, T2: ~65, T3: ~45, T4: ~195, F1: ~151, Error: ~17
* **Qwen2.5-7B:** T1: ~72, T2: ~74, T3: ~69, T4: ~227, F1: ~106, Error: ~8
* **QwQ-32B:** T1: ~71, T2: ~36, T3: ~24, T4: ~265, F1: ~85, Error: ~6
* **DS-R1-Qwen7B:** T1: ~41, T2: ~20, T3: ~11, T4: ~216, F1: ~88, Error: ~24
* **DS-R1-Qwen32B:** T1: ~51, T2: ~22, T3: ~7, T4: ~306, F1: ~79, Error: ~4
* **DeepSeek-R1:** T1: ~44, T2: ~22, T3: ~4, T4: ~770, F1: ~38, Error: ~0
* **GPT-04-mini:** T1: ~17, T2: ~13, T3: ~3, T4: ~309, F1: ~82, Error: ~3
**3. FOLIO Dataset (Bottom Row)**
* **GPT-3.5:** T1: ~14, T2: ~117, T3: ~115, T4: ~150, F1: ~44, Error: ~29
* **GPT-4:** T1: ~19, T2: ~116, T3: ~116, T4: ~118, F1: ~19, Error: ~15
* **LLaMA3.1-8B:** T1: ~62, T2: ~114, T3: ~88, T4: ~167, F1: ~74, Error: ~11
* **LLaMA3.1-70B:** T1: ~44, T2: ~147, T3: ~115, T4: ~119, F1: ~66, Error: ~18
* **Qwen2.5-7B:** T1: ~15, T2: ~133, T3: ~105, T4: ~180, F1: ~114, Error: ~9
* **QwQ-32B:** T1: ~18, T2: ~114, T3: ~113, T4: ~180, F1: ~110, Error: ~15
* **DS-R1-Qwen7B:** T1: ~7, T2: ~95, T3: ~80, T4: ~179, F1: ~110, Error: ~14
* **DS-R1-Qwen32B:** T1: ~8, T2: ~74, T3: ~38, T4: ~175, F1: ~111, Error: ~8
* **DeepSeek-R1:** T1: ~8, T2: ~45, T3: ~38, T4: ~175, F1: ~110, Error: ~7
* **GPT-04-mini:** T1: ~11, T2: ~116, T3: ~115, T4: ~175, F1: ~116, Error: ~5
### Key Observations
* **T4 Dominance:** Across all datasets and models, the "T4" response type consistently has the highest count, indicating it's the most frequent type of response generated.
* **Error Rates:** Error rates are generally low, but vary significantly between models. DeepSeek-R1 consistently shows very low error rates.
* **Model Performance Variation:** GPT-4 and DeepSeek-R1 generally exhibit higher counts in T4 and lower error rates compared to other models.
* **Dataset Impact:** The distribution of response types varies across datasets. For example, F1 responses are more prominent in the ProofWriter dataset.
### Interpretation
This chart provides a comparative analysis of language model performance across different datasets, categorized by response types. The dominance of "T4" suggests that this response type represents a common or default behavior of these models. The low error rates across most models indicate a generally high level of reliability. The variations in performance between models and datasets highlight the importance of selecting the appropriate model for a specific task. The consistent strong performance of DeepSeek-R1 and GPT-4 suggests they are robust and reliable choices. The differences between the 8B and 70B versions of LLaMA indicate that model size impacts performance, but not always linearly. The chart allows for a nuanced understanding of the strengths and weaknesses of each model, enabling informed decision-making in natural language processing applications.
</details>
Figure 5. Category Distribution of LLM-Generated Reasoning Chains on Benchmark Datasets.
4.4.1. Analysis of Model Performance
The overall category distribution is shown in Figure 5. The Error part indicates cases where MATP fails to evaluate. The failure rate of MATP analysis cases averages 1.04% on PrOntoQA-OOD, 1.22% on ProofWriter, and 31.92% on FOLIO. The notably higher rate on FOLIO suggests that MATP is more sensitive to complex, natural language structures, mainly due to challenges in NL2FOL translation. The specific failure reasons are discussed in § 4.4.3. These failed cases are excluded from subsequent classification analysis.
While reasoning and general models achieve similar answer accuracy on simple datasets like PrOntoQA-OOD, they differ significantly in actual reasoning quality. Reasoning models (e.g., DeepSeek-R1, QwQ-32B) consistently generate valid reasoning chains (T1–T2), with DeepSeek-R1 reaching over 96% T1 on PrOntoQA-OOD. In contrast, general models (e.g., LLaMA3.1–8B) often rely on shallow or inconsistent logic, lacking valid proof paths despite high accuracy. General models also show issues like redundant logic (LLaMA) or overuse of irrelevant premises (GPT-3.5), leading to correct but weakly justified answers. Even reasoning models struggle on challenging datasets like ProofWriter, where incomplete or invalid chains (T3/T4) still exist. On FOLIO, the proportion of T2 and T4 increases across all models. This stems partly from the evaluation tool’s difficulty in handling truly natural language, and partly from the dataset’s reliance on background knowledge not always captured in the explicit premises. Model scale also affects performance. Larger models such as LLaMA3.1–70B generally yield higher T1 ratios and fewer errors than smaller variants, yet still lag behind reasoning-specialized models in logical coherence.
In summary, answer accuracy alone fails to capture reasoning strength. Our classification strategy reveals critical differences in logical validity and robustness, highlighting the need to evaluate reasoning processes, not just final answers.
Table 2. Special Cases of Reasoning Chain Categorization with Representative Examples. In the Reasoning Response, sentences highlighted in orange are considered $Unknown$ relative to the task premises, while black sentences are $True$ .
| Description | Reasoning Response | Task Name |
| --- | --- | --- |
| T2: If the $Unknown$ step is excluded, this answer is a standard response. | GPT-4o: 1) The tiger eats the dog. 2) If someone eats the dog then the dog needs the bear. 3) The dog eats the dog. 4) The dog needs the bear. 5) There is evidence to conclude that the dog needs the bear. | Task ① : ProofWriter -RelNeg-OWA-D5-226-Q3 |
| T3: The conclusion that needs to be proven is “Fiona is not big.”. However, the model is proving “Anne is big.”. | GPT-3.5: … 5) If Anne is white then Anne is big. 6) There is evidence to conclude that Anne is big. | Task ② : ProofWriter -AttNeg-OWA-D5-1003-Q5 |
| T4: The model introduce an $Unknown$ information to fabricate a valid proof path. | DS-R1-Qwen7B: 1) Sally is a dumpus. 2) Sally is a gorpus. 3) Every gorpus is a zumpus. 4) Therefore, Sally is a zumpus. 5) Every zumpus is a romrus. 6) Therefore, Sally is a romrus. | Task ③ : PrOntoQA-OOD -4hop-Composed-random-noadj-69-4 |
| F1: The model’s reasoning process contains sufficient information to derive the conclusion, yet it incorrectly responds that it cannot. | QwQ-32B: 1) Fiona is quiet. 2) Quiet things are green. 3) Fiona must be green. 4) Fiona is rough. … 9) Therefore, Fiona is not green. | Task ④ : ProofWriter -AttNeg-OWA-D5-630-Q4 |
| F1: The model’s reasoning steps are entirely correct, but the final answer is incorrect. | GPT-4o: 1) Bob is quiet. 2) Bob is smart. 3) All smart things are green. 4) Bob is green. 5) Green things are white. 6) Bob is white. 7) There is evidence to conclude that Bob is white. | Task ⑤ : ProofWriter -AttNeg-OWA-D5-327-Q5 |
| F1: The model enters a loop during reasoning, causing the inference process to stall. | LLaMA3.1-8B: 1) Every lorpus is a numpus. 2) Every lorpus is a numpus. … 20) Every lorpus is a numpus. … | Task ⑥ : PrOntoQA-OOD -4hop-Composed-random-noadj-22-7 |
4.4.2. Analysis of Reasoning Chain Categories
We further analyze each category to identify common patterns and provide representative examples in Table 2.
T1 chains that are fully correct in both step-level logic and overall consistency, representing ideal outputs. Nonetheless, even when satisfying our classification criteria, there remain minor issues that warrant further discussion, such as redundant steps that are correct but irrelevant, and skipped steps where a step relies on multiple unstated premises. Such cases are illustrated in GPT-4o’s output in Figure 1 (step 1 and step 4).
T2 responses resemble T1 but contain one or more incorrect steps that do not affect the final conclusion. Once removed, the remaining steps form an entirely correct and valid proof (i.e., task ① ).
T3 chains consist of correct steps but fail to form a valid proof path. This often results from implicit reasoning, where key premises are omitted, or accidental correctness, where an unrelated conclusion is proven that happens to share the same truth value (i.e., task ② ). Models often default to answering $False$ when uncertain, which may also produce coincidentally correct answers.
T4 exhibits the same issues as T3 but also includes incorrect reasoning steps. These outputs are typically disorganized and incoherent. Some cases even introduce non-existent facts to fabricate plausible chains (i.e., task ③ ).
F1 and F2 responses both yield incorrect final predicted answers. Reasoning chains in F1 contain only correct steps, whereas in F2 include at least one incorrect step. Common issues include incomplete reasoning due to missing or poorly integrated premises (i.e., task ④ ). We also observe special failure modes: models may derive the correct conclusion but answer it incorrectly (i.e., task ⑤ ), or enter repetitive loops that stall the reasoning process (i.e., task ⑥ ).
Table 3. MATP Misclassifications on DeepSeek-R1’s Response for folio-train-57-168. Red indicates MATP ’s erroneous outputs, while green marks the expected correct ones.
| Task Info and Reasoning Response | Step-FOL Generated by GPT-4o | MATP Output |
| --- | --- | --- |
| Conclusion: Leo is an animal. (True) Filtered Resoning Steps: 1) All pets are animals. 2) Charlie has a naughty pet dog named Leo. 3) A pet dog is a type of pet. 4) Since all pets are animals, Leo being a pet implies Leo is an animal. | 1) $∀ x(pet(x)→ animal(x))$ 2) $pet(leo)\land dog(leo)\land naughty(leo)\land haspet(charlie,leo)$ 3) ${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}∀ x(dog(x)→ pet(x))}$ 3) ${\color[rgb]{0.203125,0.66015625,0.32421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.203125,0.66015625,0.32421875}∀ x(pet(x)\land dog(x)→ pet(x))}$ 4) $∀ x((pet(x)\land animal(x))→(pet(leo)→ animal(leo)))$ | S1: True S2: True S3: Unknown S3: True S4: True Cate: T2 Cate: T1 |
In summary, T1 and T2 exhibit the most reliable reasoning, while T3 and T4 are less stable. F1 shows potential for improvement, while F2 is the most flawed. Overall reasoning quality follows: T1 $>$ T2 $>$ T3 $>$ T4 $>$ F1 $>$ F2. Manual inspection also reveals a few misclassifications. As shown in Table 3, an NL2FOL translation error in one step leads to T1 being mislabeled as T2. While the classification is not perfectly accurate, it reliably captures overall reasoning patterns and pinpoints potential error steps, offering clearer consistency and interpretability than prompt-based baselines.
Table 4. Representative Error Cases in NL2FOL Translation. Key erroneous parts are highlighted in red.
| Description | NL Sentences | FOL Representation | Dataset |
| --- | --- | --- | --- |
| The domain of the universal quantifier in FOL is wrong. | If someone is smart and not kind then they are young. | $∀ x{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(}smart(x)\land\neg kind(x){\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0})}→ young(x)$ | Case ❶ from ProofWriter |
| The wrong use of $\land$ instead of $\lor$ for “or”. | Alex is a gorpus, a sterpus, a numpus, or a gorpus. | $Gorpus(alex){\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\land}Sterpus(alex)\linebreak{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\land}Numpus(alex){\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\land}Gorpus(alex)$ | Case ❷ from PrOntoQA-OOD |
| $BoyBand(btob4u)$ which is effective for reasoning candidate conclusion is omitted. | Show Your Love is a song recorded by the South Korean boy band BtoB 4u. | $Song(showyourlove)\land RecordedBy(showyourlove,\linebreak btob4u)$ | Case ❸ from FOLIO |
| The predicate is used improperly, where the same word “referee observer” in the context is represented by different predicates. | Brian Winter was appointed as a referee observer after his retirement. Some football referees become referee observer s. | ${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}AppointedObserver}(brian).$ $∃ x(FootballReferee(x)\land{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}RefereeObserver}(x))$ | Case ❹ from FOLIO |
| “Either…or…” represents XOR, which differs from OR and should be denoted using the $\oplus$ . | Everything displayed in the collection is either a plant or an animal. | $∀ x(Displayed(x)→(Plant(x){\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\lor}Animal(x)))$ | Case ❺ from FOLIO |
| The direct use of $\textgreater$ is not grammatical and should be expressed as $MoreRevenue(airbus,boeing)$ . | Airbus made more revenue than Boeing last year. | $Revenue(airbus,lastyear){\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\textgreater}\linebreak Revenue(boeing,lastyear)$ | Case ❻ from FOLIO |
4.4.3. Analysis of Error Cases
Most evaluation failures originate from NL2FOL translation errors. Table 4 presents representative cases. While translation from PrOntoQA-OOD and ProofWriter is largely accurate, occasional issues remain, such as incorrect quantifier scope (i.e., case ❶ ) or misinterpreting “or” as a conjunction when linking multiple entities (i.e., case ❷ ). In contrast, FOLIO introduces more diverse and complex errors due to its rich natural language. We summarize common error patterns as follows.
Information Omission. Key details are omitted when sentences contain multiple facts (case ❸ ).
Improper Predicate Usage. The same concept may be mapped to different predicates, causing semantic inconsistency (i.e., case ❹ ).
XOR vs. OR Confusion. Expressions involving exclusive choice, such as “either…or…”, are often mistakenly represented as disjunction ( $\lor$ ) rather than exclusive or ( $\oplus$ ), even when explicitly prompted (i.e., case ❺ ).
Inadequacy in Handling Domain-Specific Expressions. Domain-specific expressions involving comparatives, superlatives, mathematics, or time are often poorly handled, resulting in ungrammatical FOL (i.e., case ❻ ).
Annotation Errors. In addition to the extraction issues above, we also observe annotation errors in the FOLIO dataset during manual inspection. Figure 6 provides an example of such a mislabeling. We find that the FOL ground truth representation of the fourth premise in the task is incorrectly given as “ $∀ x((Professional(x)\land HighWinRatio(x))→ Big3(x))$ ”, which may be the cause of the labeling error. Similar issues are also found in tasks such as folio-train-63-186, 167-480, 167-479, 302-746, 470-1359, and 470-1360.
<details>
<summary>x5.png Details</summary>
### Visual Description
\n
## Textual Document: MATP Check Result
### Overview
The image presents a document detailing a MATP (likely a Machine Assisted Truth Prediction) check result. It outlines premises, their formalization in First-Order Logic (FOL), a conclusion, its FOL representation, and a final "Vampire Result" indicating the outcome of a logical proof attempt. The document also includes a ground truth label and a visual indicator of whether the conclusion is considered true or false.
### Components/Axes
The document is divided into three main sections:
1. **Premises:** A numbered list of statements.
2. **MATP Check Result:** This section is further divided into:
* **Premises-FOL:** The formalization of the premises in First-Order Logic.
* **Conclusion-FOL:** The formalization of the conclusion in First-Order Logic.
* **Vampire Result:** The outcome of a logical proof attempt using a tool named "Vampire".
3. **Conclusion & Ground Truth Label:** The conclusion statement, its ground truth label, and a visual representation of the correctness.
### Detailed Analysis or Content Details
**Premises:**
1. Rafa Nadal was born in Mallorca.
2. Rafa Nadal is a professional tennis player.
3. Nadal’s win ratio is high.
4. All players in the Big 3 are professionals who have a high win ratio.
**Premises-FOL:**
1. BornInMallorca(rafa)
2. Professional(rafa) ∧ TennisPlayer(rafa)
3. HighWinRatio(rafa)
4. ∀x (Big3(x) → (Professional(x) ∧ HighWinRatio(x)))
**Conclusion-FOL:**
Big3(rafa)
**Conclusion & Ground Truth Label:**
Nadalis in the Big 3 → True. A red "X" is superimposed on this statement.
**Vampire Result:** Unknown. This is written in green text.
### Key Observations
* The conclusion "Nadal is in the Big 3" is labeled as "True" according to the ground truth, but is marked with a red "X", indicating a discrepancy.
* The Vampire Result is "Unknown", suggesting the logical prover could not determine the truth value of the conclusion based on the given premises.
* The FOL representations provide a formalization of the natural language premises and conclusion.
### Interpretation
This document appears to be part of a system designed to verify the logical validity of statements. The system takes natural language premises and a conclusion, translates them into First-Order Logic, and then attempts to prove the conclusion using a theorem prover (Vampire).
The discrepancy between the ground truth ("True") and the visual indicator (red "X") suggests that the system failed to correctly prove the conclusion, despite it being factually correct. The "Unknown" Vampire Result reinforces this, indicating the prover couldn't establish the conclusion's truth based on the provided premises. This could be due to limitations in the theorem prover, an incomplete set of premises, or a flaw in the formalization process.
The document highlights the challenges of automated reasoning and the potential for discrepancies between logical proof and real-world truth. It suggests that while formal logic can be a powerful tool for verification, it is not always sufficient to capture the complexities of real-world knowledge. The use of FOL and a theorem prover like Vampire indicates a focus on rigorous, symbolic reasoning.
</details>
Figure 6. Example of Annotation Error in FOLIO. The task ID is folio-train-34-99.
ANSWER to RQ3
MATP reveals clear differences in reasoning behavior across LLMs. Despite similar answer accuracy, reasoning models yield more coherent logic than general models, highlighting the need to assess reasoning quality beyond final answers.
4.5. Ablation Study
We conduct an ablation study comparing MATP ’s performance with and without feedback during NL2FOL regeneration.
Setup. As shown in Figure 5, most analysis failures occur on FOLIO. Therefore, we evaluate the responses of two models, GPT-4o and DeepSeek-R1, on 355 tasks from FOLIO. Since pinpointing specific errors is difficult, we use the entire previous generation as feedback. We extend the original prompt in Figure 3 by adding a Feedback field under Input instance, containing the prior NL2FOL translation with conversion errors. This field helps the model avoid similar mistakes during regeneration. Similarly, the maximum number of regeneration attempts is set to three. We focus on the number of failures in both feedback and non-feedback settings.
Results. As shown in Table 5, using Feedback has minimal effect, with non-feedback settings sometimes yielding better results. Additionally, feedback increases resource consumption. Therefore, feedback is excluded during MATP’s actual implementation.
Table 5. Impact of Feedback on MATP Failures.
| Model | With Feedback | Without Feedback |
| --- | --- | --- |
| GPT-4o | 118 | 116 |
| DeepSeek-R1 | 119 | 111 |
5. Discussion
5.1. Future Enhancement
This paper proposes (1) a framework for translating informal LLM reasoning into formal logic and verifying with ATP tools, and (2) a multi-level classification strategy beyond binary answer correctness. Thanks to the modular design of MATP, we can independently upgrade each component, making it adaptable for deployment in high-stakes scenarios that require rigorous reasoning validation. Several directions remain for future exploration:
Enhanced Formalization. MATP ’s accuracy depends on reliable NL2FOL translation. Current prompt-based methods still show limitations with complex natural language inputs. Future work may incorporate more robust or domain-adapted translation tools.
Open-Domain Knowledge Requirement. Some mappings (e.g., “Low” to “ $\neg$ High”) require external knowledge not present in the premises. To ensure a strict one-to-one mapping between natural and formal language while handling implicit common knowledge, the model needs to autonomously introduce necessary knowledge (e.g., “low” equals “not high”) either before or during translation.
Improved Evaluation Metrics. Evaluation of extracted FOL typically relies on gold-standard annotations and similarity-based metrics, which often fail to reflect semantic fidelity and logical validity (thatikonda2025assessing). This underscores the need for more principled and automated evaluation methods.
Reconstructing Reasoning Graphs. Future work may model reasoning steps as nodes and ATP-detected inferences as directed edges, constructing a reasoning graph from LLM-generated reasoning outputs. This structure enables fine-grained verification and helps identify redundant, missing, or conflicting logic beyond simple path existence checks.
Expanded Reasoning Support. Beyond forward entailment, supporting reverse reasoning could broaden applicability.
5.2. Optimization on Response Analysis
To improve efficiency and reduce manual effort—particularly in NL2FOL evaluation, we leverage LLM internal features using entropy and Jensen-Shannon (JS) divergence (MENENDEZ1997307) to identify uncertain or potentially flawed reasoning steps. As demonstrated in Figure 7, when Llama3.1-8B series are evaluated on ProofWriter, flawed reasoning often correlates with higher entropy or JS divergence. Note that the full figure across datasets and LLMs is available in (matp).
Based on this, we implement a threshold-based filtering strategy: reasoning outputs with entropy below 7.0 and JS divergence below 0.065 are considered likely correct, allowing us to focus analysis on more uncertain cases. This pre-filtering step effectively reduces the evaluation burden, with correct reasoning coverage rates ranging from 14.7% to 40.5% across datasets and models. While some incorrect responses are mistakenly filtered out (e.g., 8.5% for ProofWriter and 6.7% for FOLIO under Llama3.1-8B), other configurations show near-zero false negatives, validating the approach’s reliability. Overall, this method improves evaluation efficiency by prioritizing uncertain reasoning steps. Future work will explore tighter integration of LLM internal signals to enable automated filtering and semi-supervised reasoning quality assessment.
<details>
<summary>x6.png Details</summary>
### Visual Description
## Scatter Plots: JS Divergence vs. Entropy for ProofWriter - Llama Models
### Overview
The image presents two scatter plots comparing JS Divergence against Entropy for two Llama models: Llama3.1-8B (top plot) and Llama3.1-70B (bottom plot). Each plot visualizes the relationship between these two metrics for correct (T) and incorrect (F) predictions. A dashed horizontal line is present in both plots, likely representing a threshold. Vertical dashed lines are also present, labeled "Lowest Entropy (Incorrect)".
### Components/Axes
Both plots share the following components:
* **X-axis:** Labeled "Entropy", ranging from 0 to approximately 40 in the top plot and 0 to 70 in the bottom plot.
* **Y-axis:** Labeled "JS Divergence", ranging from 0.04 to 0.12 in the top plot and 0.04 to 0.14 in the bottom plot.
* **Title:** Top plot: "ProofWriter - Llama3.1-8B". Bottom plot: "ProofWriter - Llama3.1-70B".
* **Legend:** Located in the top-right corner of each plot.
* Blue circles: "Correct (T)"
* Red circles: "Incorrect (F)"
* **Horizontal Dashed Line:** Present in both plots, approximately at JS Divergence = 0.075.
* **Vertical Dashed Line:** Present in both plots, labeled "Lowest Entropy (Incorrect)". The line is positioned at approximately Entropy = 10 in the top plot and Entropy = 20 in the bottom plot.
### Detailed Analysis or Content Details
**Plot 1: ProofWriter - Llama3.1-8B**
* **Correct (T) - Blue Circles:** The data points generally cluster in the lower-left region of the plot (low Entropy, low JS Divergence). The points are densely packed between Entropy 0-10 and JS Divergence 0.04-0.08. As Entropy increases beyond 10, the points become more scattered, with some extending to Entropy ~40 and JS Divergence ~0.11.
* **Incorrect (F) - Red Circles:** These points are more dispersed across the plot. A significant number of points are located in the region of higher Entropy (10-40) and higher JS Divergence (0.07-0.12). There is a noticeable concentration of points around Entropy 10-20 and JS Divergence 0.08-0.10.
* **Trend:** The blue points show a slight upward trend, indicating that as Entropy increases, JS Divergence tends to increase, but the correlation is weak. The red points are more scattered, with no clear trend.
**Plot 2: ProofWriter - Llama3.1-70B**
* **Correct (T) - Blue Circles:** Similar to the 8B model, the blue points are concentrated in the lower-left region (low Entropy, low JS Divergence). The density is highest between Entropy 0-15 and JS Divergence 0.04-0.08. The points extend to Entropy ~60 and JS Divergence ~0.13.
* **Incorrect (F) - Red Circles:** These points are also dispersed, but appear to be more concentrated at higher JS Divergence values compared to the 8B model. There's a cluster around Entropy 20-40 and JS Divergence 0.09-0.13.
* **Trend:** The blue points exhibit a similar slight upward trend as in the 8B model. The red points are scattered, with no strong trend.
### Key Observations
* **Model Size Impact:** The 70B model appears to have a wider distribution of both correct and incorrect predictions across the Entropy and JS Divergence space compared to the 8B model.
* **Threshold:** The horizontal dashed line seems to separate a region of generally correct predictions (below the line) from a region of more incorrect predictions (above the line).
* **Lowest Entropy:** The vertical dashed line highlights that incorrect predictions tend to occur at lower entropy values.
* **Overlap:** There is significant overlap between the correct and incorrect predictions in both plots, indicating that neither Entropy nor JS Divergence alone are perfect predictors of correctness.
### Interpretation
These plots explore the relationship between Entropy and JS Divergence as indicators of prediction correctness for the ProofWriter task using two different sizes of the Llama model. Entropy, in this context, likely represents the confidence or predictability of the model's output. JS Divergence measures the difference between the model's predicted probability distribution and the true distribution.
The data suggests that lower Entropy and lower JS Divergence are generally associated with correct predictions. However, the overlap between the correct and incorrect predictions indicates that these metrics are not definitive. The 70B model's wider distribution suggests that it explores a broader range of possibilities, potentially leading to both more accurate and more diverse (and sometimes incorrect) predictions.
The "Lowest Entropy (Incorrect)" line suggests that when the model is *too* confident (low Entropy) in an incorrect prediction, it is particularly problematic. This could indicate that the model is overconfident in its errors. The horizontal dashed line acts as a threshold for JS Divergence, above which predictions are more likely to be incorrect. The fact that the 70B model has more points above this threshold suggests that while it can explore more possibilities, it also has a higher chance of making more divergent (and incorrect) predictions.
The plots provide insights into the model's behavior and potential areas for improvement. Focusing on reducing JS Divergence, especially for low-entropy predictions, could lead to more reliable results.
</details>
Figure 7. Comparison of entropy and Jensen–Shannon divergence distributions for correct (T) and incorrect (F) reasoning responses for Llama3.1 series on ProofWriter.
6. Related Work
Automatically Generating Formal Specifications. LLMs have been increasingly applied to automate formal specification generation and logical translation from natural language. SpecGen (ma2024specgen) adopts a conversational and mutation-based approach to generate program specifications without relying on templates. NL2CTL (10.1007/978-981-96-0617-7_1) translates requirements into Computation Tree Logic (CTL) by constructing an NL-CTL dataset through prompt engineering and fine-tuning a T5 model. SAFE (chen2024automated) targets Rust, integrating data synthesis, fine-tuning, and symbolic verification to automate proof generation with over 70% accuracy. NL2FOL (Lalwani2024NL2FOLTN) converts natural language into FOL, using SMT solvers for fallacy detection and explanation. NL2SPEC (cosler2023nl2spec) supports interactive translation into temporal logic, allowing iterative refinement to resolve ambiguity.
Enhancing Reasoning Capabilities of LLMs. Enhancing LLM reasoning is critical for high-stakes tasks. Internally, DeepSeek-R1 (guo2025deepseek) combines supervised fine-tuning and reinforcement learning to enable reasoning abilities such as chain-of-thought and self-verification. Externally, prompting strategies like Logic-of-Thought (liu2024logic) and Chain-of-Knowledge (wang-etal-2024-boosting-language) improve logical completeness and factual coherence by injecting structured logic or knowledge into prompts. Tool-augmented methods improve reasoning accuracy by using LLMs as semantic parsers to translating natural language into formal languages, which are subsequently processed by external symbolic tools. LINC (olausson-etal-2023-linc) converts NL into FOL for logic theorem proving. SatLM (NEURIPS2023_8e9c7d4a) translates NL into declarative task specifications for Z3 SMT solver (de2008z3), targeting mathematical and logical reasoning tasks. Logic-LM (pan2023logiclm) covers four categories of formal languages and corresponding tools, selecting appropriate ones for different types of reasoning tasks. Our work adopts a similar strategy but focuses on evaluating the correctness and logical consistency of LLM responses to reasoning tasks.
Evaluating Reasoning Capabilities of LLMs. Evaluating LLM reasoning has become a key research focus. Prior studies assess model performance across diverse tasks, such as code understanding correctness at both the function (li2024mutation) and software engineering (tanzil2024chatgpt) levels, as well as factual hallucination detection in real-world reasoning scenarios (li2024drowzee). As reasoning abilities advance, evaluation objectives have expanded beyond overall task correctness to step-by-step reasoning analysis. The survey (lee2025evaluating) summarizes four key dimensions for evaluating reasoning steps: factuality, validity, coherence, and utility. Despite progress, most methods either rely on labor-intensive gold-standard reasoning chains (golovneva2022roscoe; PrOntoQA) or probabilistic LLM-based evaluations (zeng2024mrgsm8kmetareasoningbenchmarklarge; xia2024evaluatingmathematicalreasoning), which undermine logical rigor. ROSCOE (golovneva2022roscoe) proposes several metrics using embedding-based calculations among reasoning steps, reference steps, and problems for evaluation. MR-GSM8K (zeng2024mrgsm8kmetareasoningbenchmarklarge) prompts LLMs to check reasoning correctness, outputting structured fields like Solution Correctness, First Error Step, and Error Analysis. ReasonEval (xia2024evaluatingmathematicalreasoning) fine-tunes LLMs on high-quality labeled data to score validity and redundancy for each reasoning step. Our work extends this research line by incorporating automated theorem provers to evaluate LLM-generated reasoning steps.
7. Conclusion
In this paper, we presented MATP, an evaluation framework that bridges the gap between informal LLM reasoning and formal verification through automated theorem proving. By systematically converting natural language reasoning into First-Order Logic and applying rigorous verification at each step, MATP provides unprecedented insight into the logical validity of LLM-generated reasoning chains. Our extensive evaluation demonstrates that MATP not only achieves high accuracy in FOL translation and reasoning verification, but also enables fine-grained classification that distinguishes genuine deductive reasoning from superficial pattern matching or accidental correctness. The stark differences revealed between models underscore the critical need for formal verification in high-stakes applications. While challenges remain in handling complex linguistic constructs, MATP establishes a foundational framework for ensuring reliable, verifiable AI reasoning in safety-critical domains where trust through logical soundness is paramount.