# 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
## Logical Reasoning Evaluation: LLM Performance on a Deductive Task
### Overview
The image presents a logical reasoning challenge and evaluates the performance of two Large Language Models (LLMs), GPT-3.5-Turbo and GPT-4o, in solving it. The challenge involves determining the truth value of a conclusion based on a set of premises. The image shows the premises, the conclusion, the answers and reasoning processes of the two models, and an assessment of their correctness.
### Components/Axes
* **Premises:** A list of 23 statements that serve as the foundation for the logical reasoning.
* **Conclusion & Ground Truth Label:** The statement to be evaluated ("The cat is not cold.") and its correct truth value (False).
* **Challenge #1: Unstructured LLM Responses:** Indicates that the LLMs were given the challenge without specific formatting instructions.
* **GPT-3.5-Turbo Answer:** The answer and reasoning process provided by the GPT-3.5-Turbo model.
* **GPT-4o Answer:** The answer and reasoning process provided by the GPT-4o model.
* **Correct Answer & Correct Reasoning:** Indicates that the GPT-4o model provided the correct answer and a valid reasoning process.
* **Correct Answer & Invalid Reasoning:** Indicates that the GPT-3.5-Turbo model provided the correct answer but with an invalid reasoning process.
* **Challenge #2: Subtle and Silent Reasoning Errors:** Highlights the presence of subtle errors in the reasoning processes of the models.
### Detailed Analysis or Content Details
**Premises:**
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 cold then it likes the cat.
23. If something is big and it visits the bear then the bear is green.
**Conclusion & Ground Truth Label:**
* The cat is not cold. -> False
**GPT-3.5-Turbo Answer: False. GPT-3.5-Turbo Reasoning Process:**
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 cat is not cold. (False)
**GPT-4o Answer: False. GPT-4o Reasoning Process:**
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 15 & Premise 19 & Premise 18)
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)
### Key Observations
* Both GPT-3.5-Turbo and GPT-4o correctly identified the conclusion as False.
* GPT-4o's reasoning process is deemed correct, while GPT-3.5-Turbo's reasoning is considered invalid.
* The image highlights the importance of not only getting the correct answer but also having a valid reasoning process.
### Interpretation
The image demonstrates a comparative analysis of the logical reasoning capabilities of two LLMs. While both models arrived at the correct answer, the quality of their reasoning processes differed significantly. GPT-4o exhibited a more coherent and logically sound approach, leading to its assessment as "Correct Answer & Correct Reasoning." In contrast, GPT-3.5-Turbo's reasoning was deemed invalid, despite arriving at the correct conclusion. This underscores the importance of evaluating not only the accuracy of LLM outputs but also the validity of their underlying reasoning processes, particularly in tasks requiring deductive logic and inference. The "Challenge #2" label suggests that even when models provide correct answers, subtle errors in reasoning can be present, highlighting the need for careful scrutiny of LLM-generated explanations.
</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
## Flow Diagram: MATP - Reasoning and Verification Process
### Overview
The image presents a flow diagram titled "MATP" which outlines a process for reasoning and verification, likely in the context of natural language processing or automated reasoning systems. The diagram is divided into four main sections: Reasoning Task, NL2FOL (Natural Language to First-Order Logic), Automated Logic Verification, and Response Analysis and Classification. It illustrates the steps involved in converting natural language premises and conclusions into logical formulas, verifying them using an automated theorem prover (ATP), and analyzing the correctness of the predicted answer and reasoning steps.
### Components/Axes
* **Header:** The title "MATP" is located at the top-right of the diagram. Section titles are prefixed with "§" and a number (e.g., "§3.2 NL2FOL").
* **Reasoning Task (Top-Left):**
* Sub-sections: Premises (P), Conclusion (C), Ground Truth Label (L), Interact with Target LLMs, Reasoning Steps (S), Predicted Answer (A).
* Labels: "True" or "False" are used for truth values.
* **§3.2 NL2FOL (Top-Middle):**
* Title: Reasoning Steps Filtering
* Sub-sections: Premises-FOL, Conclusions-FOL
* Component: NL2FOL LLM
* **§3.3 Automated Logic Verification (Top-Right):**
* Sub-sections: Single Statement Verification with ATP, FOL to TPTP, FOL Verification, Predicted Answer Correctness, Reasoning Steps Correctness, Valid Proof Path Existence.
* Components: ATP TOOL
* Labels: "True", "False", "Unknown", "Error", "Yes", "No"
* **§3.4 Response Analysis and Classification (Bottom-Right):**
* Decision points: "With Correct Predicted Answer?", "With Valid Proof Path?", "Without False Step?"
* Outcomes: F1, F2, T1, T2, T3, T4 (likely representing different classifications or states)
* **Arrows:** Arrows indicate the flow of information and control between different stages.
* **Error Handling:** "Generation limit exceeded" and "Error (Analysis fail)" are indicated at the bottom of the NL2FOL section.
### Detailed Analysis or ### Content Details
**1. Reasoning Task (Top-Left):**
* **Premises (P):** A set of six premises (P1-P6) are given in natural language.
* P1: The cat sees the bear.
* P2: The cat visits the mouse.
* P3: The mouse is cold.
* P4: If something visits the mouse and the mouse visits the dog then it is cold.
* P5: If something likes the cat then it visits the dog.
* P6: If something is cold then it likes the cat.
* **Conclusion (C):** The cat is not cold.
* **Ground Truth Label (L):** False.
* **Interact with Target LLMs:** Instructions to answer whether the conclusion is True or False based on the premises.
* **Reasoning Steps (S):** A set of four reasoning steps (S1-S4) are given in natural language.
* S1: The cat sees the bear.
* S2: If something is cold then it likes the cat.
* S3: If something visits the mouse and the mouse visits the dog then it is cold.
* S4: The cat is not cold.
* **Predicted Answer (A):** False.
**2. §3.2 NL2FOL (Top-Middle):**
* **Reasoning Steps Filtering:** The premises and conclusions are parsed into first-order logic formulas.
* **Premises-FOL:** The first-order logic representation of the premises.
* P1: See(cat, bear).
* P2: Visit(cat, mouse).
* P3: Cold(mouse).
* P4: ∀x ((Visit(x, mouse) ∧ Visit(mouse, dog)) → Cold(x)).
* P5: ∀x (Like(x, cat) → Visit(x, dog)).
* P6: ∀x (Cold(x) → Like(x, cat)).
* **Conclusions-FOL:** The first-order logic representation of the conclusions.
* S1: See(cat, bear).
* S2: ∀x (Cold(x) → Like(x, cat)).
* S3: ∀x ((Visit(x, mouse) ∧ Visit(mouse, dog)) → Cold(x)).
* S4: ¬Cold(cat).
* C: ¬Cold(cat).
* **Error Handling:** "Generation limit exceeded" leads to "Error (Analysis fail)".
**3. §3.3 Automated Logic Verification (Top-Right):**
* **Single Statement Verification with ATP:**
* `State_Ver(P, S) -> res1 -> True/False/Unknown/Error`
* `State_Ver(F, S) -> res2 -> Error`
* "Execution fail" leads to "Error".
* **FOL to TPTP:** Conversion of first-order logic to TPTP format.
* **FOL Verification:** `State_Ver(P, C) = L?`
* If "No", the process stops.
* If "Yes", proceeds to the next step.
* **Predicted Answer Correctness:** `A = L?`
* If "True", proceeds to "Reasoning Steps Correctness".
* **Reasoning Steps Correctness:** `State_Ver(P, Sk), Sk ∈ S`
* **Valid Proof Path Existence:** `State_Ver(SinProofPath, C), SinProofPath ∈ S, Sk ∈ SinProofPath: Sk: True`
* If "False", the process stops.
**4. §3.4 Response Analysis and Classification (Bottom-Right):**
* **Decision Points:**
* "With Correct Predicted Answer?" (Yes/No)
* "With Valid Proof Path?" (Yes/No)
* "Without False Step?" (Yes/No)
* **Outcomes:** T1, T2, T3, T4, F1, F2. These outcomes are reached based on the answers to the decision point questions.
### Key Observations
* The diagram illustrates a pipeline for automated reasoning, starting from natural language input and ending with a classification of the response.
* The process involves converting natural language to first-order logic, verifying the logic using an ATP, and analyzing the correctness of the predicted answer and reasoning steps.
* Error handling is included to address cases where generation limits are exceeded or analysis fails.
* The final classification (T1-T4, F1-F2) depends on the correctness of the predicted answer, the validity of the proof path, and the presence of false steps.
### Interpretation
The MATP diagram describes a system for evaluating the reasoning capabilities of a target LLM. The system takes natural language premises and a conclusion, converts them into formal logic, and then uses an automated theorem prover to verify the conclusion. The system also checks the correctness of the reasoning steps provided by the LLM. The final classification (T1-T4, F1-F2) provides a detailed assessment of the LLM's reasoning performance, taking into account both the correctness of the final answer and the validity of the reasoning process. This type of system is valuable for developing and evaluating AI models that can reason logically and provide accurate and reliable answers. The error handling mechanisms suggest that the system is designed to be robust and handle cases where the LLM's reasoning is flawed or incomplete.
</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
## Confusion Matrix Comparison: Model Performance
### Overview
The image presents a comparison of confusion matrices for three different models: MATP, GPT-4o, and DeepSeek-R1. Each matrix visualizes the performance of the model in predicting labels, with the rows representing the ground truth labels and the columns representing the predicted labels. The values within each cell indicate the number of instances that fall into that particular combination of ground truth and predicted labels.
### Components/Axes
* **Title:** The image contains three separate confusion matrices, each with a title indicating the model: "MATP Predicted Label", "GPT-4o Predicted Label", and "DeepSeek-R1 Predicted Label".
* **Y-Axis Label:** "Ground Truth Label" (applies to all three matrices).
* **X-Axis Labels:** T1, T2, T3, T4 (applies to all three matrices).
* **Y-Axis Labels:** T1, T2, T3, T4 (applies to all three matrices).
* **Cell Values:** Each cell contains a numerical value representing the count of instances. The color of the cell indicates the magnitude of the value, with darker shades of green representing higher values.
### Detailed Analysis or ### Content Details
**1. MATP Predicted Label**
| | T1 | T2 | T3 | T4 |
| :---- | :-- | :-- | :-- | :-- |
| **T1** | 50 | 0 | 0 | 0 |
| **T2** | 0 | 50 | 0 | 0 |
| **T3** | 0 | 0 | 50 | 0 |
| **T4** | 0 | 0 | 2 | 48 |
* **Trend:** The MATP model shows perfect classification for T1, T2, and T3. It misclassifies 2 instances of T4 as T3.
**2. GPT-4o Predicted Label**
| | T1 | T2 | T3 | T4 |
| :---- | :-- | :-- | :-- | :-- |
| **T1** | 39 | 4 | 0 | 7 |
| **T2** | 1 | 36 | 0 | 13 |
| **T3** | 5 | 1 | 42 | 2 |
| **T4** | 0 | 5 | 0 | 45 |
* **Trend:** The GPT-4o model shows more varied performance. It has some confusion between all classes, with T1 and T2 being most frequently confused with T4.
**3. DeepSeek-R1 Predicted Label**
| | T1 | T2 | T3 | T4 |
| :---- | :-- | :-- | :-- | :-- |
| **T1** | 48 | 1 | 0 | 1 |
| **T2** | 0 | 45 | 0 | 5 |
| **T3** | 4 | 0 | 46 | 0 |
| **T4** | 0 | 9 | 0 | 41 |
* **Trend:** The DeepSeek-R1 model performs well, but has some confusion. T2 is confused with T4, T1 is confused with T2, and T4 is confused with T2.
### Key Observations
* **MATP:** Achieves perfect classification for T1, T2, and T3. It only misclassifies T4 instances as T3.
* **GPT-4o:** Shows more confusion across all classes, with a tendency to misclassify T1 and T2 as T4.
* **DeepSeek-R1:** Generally performs well, but exhibits some confusion between T1 and T2, and between T2 and T4.
### Interpretation
The confusion matrices provide a clear visual comparison of the performance of the three models. MATP appears to be the most accurate, achieving perfect classification for three out of the four classes. GPT-4o shows the most confusion, indicating that it struggles to accurately distinguish between the different classes. DeepSeek-R1 falls in between, performing reasonably well but with some noticeable confusion between specific pairs of classes.
The data suggests that MATP is the most reliable model for this particular classification task. The errors made by GPT-4o and DeepSeek-R1 could be further investigated to identify the specific characteristics of the instances that are being misclassified. This information could then be used to improve the performance of these models.
</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: Model Performance Comparison on Different Datasets
### Overview
The image presents a series of bar charts comparing the performance of various language models on three different datasets: PrOntoQA-OOD, ProofWriter, and FOLIO. The charts display counts for different categories (T1, T2, T3, T4, F1, F2, and Error) for each model. The x-axis represents the different language models, and the y-axis represents the count.
### Components/Axes
* **Y-axis:** "Count", ranging from 0 to 400 for PrOntoQA-OOD, 0 to 300 for ProofWriter, and 0 to 200 for FOLIO.
* **X-axis:** Language models: GPT-3.5, GPT-4o, LLaMA3.1-8B, LLaMA3.1-70B, Qwen2.5-7B, QwQ-32B, DS-R1-Qwen7B, DS-R1-Qwen32B, DeepSeek-R1, GPT-o4-mini.
* **Datasets (Rows):** PrOntoQA-OOD (top), ProofWriter (middle), FOLIO (bottom).
* **Legend (Top):**
* T1: Dark Green
* T2: Green
* T3: Light Green
* T4: Yellow
* F1: Orange
* F2: Red
* Error: Dark Red
### Detailed Analysis
#### PrOntoQA-OOD Dataset (Top Chart)
* **GPT-3.5:**
* T1: 99
* T2: 25
* T3: 36
* T4: 22
* F1: 64
* F2: 3
* Error: 0
* **GPT-4o:**
* T1: 135
* T2: 12
* T3: 14
* T4: 9
* F1: 4
* F2: 0
* Error: 0
* **LLaMA3.1-8B:**
* T1: 224
* T2: 41
* T3: 24
* T4: 1
* F1: 10
* F2: 3
* Error: 0
* **LLaMA3.1-70B:**
* T1: 81
* T2: 27
* T3: 5
* T4: 0
* F1: 17
* F2: 9
* Error: 4
* **Qwen2.5-7B:**
* T1: 199
* T2: 16
* T3: 26
* T4: 5
* F1: 26
* F2: 4
* Error: 4
* **QwQ-32B:**
* T1: 340
* T2: 3
* T3: 12
* T4: 2
* F1: 14
* F2: 9
* Error: 4
* **DS-R1-Qwen7B:**
* T1: 370
* T2: 10
* T3: 1
* T4: 0
* F1: 0
* F2: 0
* Error: 3
* **DS-R1-Qwen32B:**
* T1: 138
* T2: 33
* T3: 31
* T4: 30
* F1: 66
* F2: 4
* Error: 0
* **DeepSeek-R1:**
* T1: 320
* T2: 44
* T3: 8
* T4: 3
* F1: 3
* F2: 2
* Error: 4
* **GPT-o4-mini:**
* T1: 370
* T2: 13
* T3: 1
* T4: 2
* F1: 0
* F2: 1
* Error: 7
#### ProofWriter Dataset (Middle Chart)
* **GPT-3.5:**
* T1: 69
* T2: 52
* T3: 13
* T4: 0
* F1: 64
* F2: 39
* Error: 2
* **GPT-4o:**
* T1: 105
* T2: 54
* T3: 20
* T4: 4
* F1: 52
* F2: 29
* Error: 3
* **LLaMA3.1-8B:**
* T1: 87
* T2: 23
* T3: 33
* T4: 1
* F1: 70
* F2: 76
* Error: 0
* **LLaMA3.1-70B:**
* T1: 70
* T2: 15
* T3: 17
* T4: 10
* F1: 65
* F2: 37
* Error: 45
* **Qwen2.5-7B:**
* T1: 155
* T2: 22
* T3: 21
* T4: 4
* F1: 74
* F2: 62
* Error: 72
* **QwQ-32B:**
* T1: 87
* T2: 7
* T3: 11
* T4: 1
* F1: 19
* F2: 36
* Error: 5
* **DS-R1-Qwen7B:**
* T1: 265
* T2: 11
* T3: 20
* T4: 26
* F1: 88
* F2: 85
* Error: 8
* **DS-R1-Qwen32B:**
* T1: 106
* T2: 3
* T3: 2
* T4: 4
* F1: 46
* F2: 51
* Error: 22
* **DeepSeek-R1:**
* T1: 216
* T2: 1
* T3: 4
* T4: 4
* F1: 22
* F2: 4
* Error: 4
* **GPT-o4-mini:**
* T1: 306
* T2: 3
* T3: 2
* T4: 9
* F1: 17
* F2: 3
* Error: 1
#### FOLIO Dataset (Bottom Chart)
* **GPT-3.5:**
* T1: 31
* T2: 19
* T3: 12
* T4: 13
* F1: 44
* F2: 27
* Error: 104
* **GPT-4o:**
* T1: 117
* T2: 35
* T3: 19
* T4: 16
* F1: 116
* F2: 6
* Error: 158
* **LLaMA3.1-8B:**
* T1: 90
* T2: 12
* T3: 12
* T4: 13
* F1: 74
* F2: 44
* Error: 116
* **LLaMA3.1-70B:**
* T1: 116
* T2: 11
* T3: 16
* T4: 15
* F1: 43
* F2: 15
* Error: 147
* **Qwen2.5-7B:**
* T1: 115
* T2: 15
* T3: 15
* T4: 12
* F1: 133
* F2: 15
* Error: 133
* **QwQ-32B:**
* T1: 114
* T2: 23
* T3: 18
* T4: 8
* F1: 105
* F2: 4
* Error: 180
* **DS-R1-Qwen7B:**
* T1: 113
* T2: 15
* T3: 16
* T4: 6
* F1: 113
* F2: 80
* Error: 114
* **DS-R1-Qwen32B:**
* T1: 173
* T2: 17
* T3: 7
* T4: 6
* F1: 37
* F2: 38
* Error: 113
* **DeepSeek-R1:**
* T1: 179
* T2: 3
* T3: 2
* T4: 9
* F1: 38
* F2: 7
* Error: 110
* **GPT-o4-mini:**
* T1: 175
* T2: 3
* T3: 2
* T4: 9
* F1: 29
* F2: 11
* Error: 116
### Key Observations
* **PrOntoQA-OOD:** DS-R1-Qwen7B and GPT-o4-mini show the highest T1 counts, indicating better performance on this dataset.
* **ProofWriter:** GPT-o4-mini and DS-R1-Qwen7B also perform well, with high T1 counts.
* **FOLIO:** DS-R1-Qwen32B and DeepSeek-R1 have the highest T1 counts, but also significant error counts.
* **Error Rates:** FOLIO generally has higher error rates across all models compared to the other two datasets.
* **Model Variation:** Performance varies significantly across different models and datasets, suggesting that some models are better suited for specific types of tasks or data.
### Interpretation
The bar charts provide a comparative analysis of various language models across three different datasets. The T1 category likely represents the most accurate or desired outcome, while T2-T4 represent varying degrees of correctness or relevance. F1 and F2 likely represent different types of failures, and "Error" represents outright incorrect responses.
The data suggests that:
* Some models (e.g., DS-R1-Qwen7B, GPT-o4-mini) excel on specific datasets like PrOntoQA-OOD and ProofWriter, indicating they might be better trained or suited for the types of questions or tasks in those datasets.
* The FOLIO dataset appears to be more challenging, as evidenced by the higher error rates across all models. This could be due to the complexity of the data, the nature of the questions, or the specific training of the models.
* There is no single "best" model across all datasets. The optimal choice depends on the specific application and the characteristics of the data.
* The distribution of T1-T4 values provides insights into the types of errors each model makes. For example, a model with a high T1 and low error rate is generally preferable to one with a high T1 but also a high error rate.
* The F1 and F2 categories could represent different types of failure modes, such as incorrect answers or irrelevant responses. Analyzing these categories can help identify specific weaknesses in each model.
</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
## Diagram: Logical Inference Check
### Overview
The image presents a logical inference check, evaluating whether a conclusion ("Nadal is in the Big 3") can be derived from a set of premises. It shows both the natural language premises and their formal logic (FOL) representations, along with the ground truth label and the result of a theorem prover (MATP).
### Components/Axes
The diagram is divided into two main sections: "Premises" (left) and "MATP Check Result" (right).
**Left Section: Premises**
* **Title:** Premises
* A list of four premises in natural language.
* **Title:** Conclusion & Ground Truth Label
* The conclusion statement: "Nadal is in the Big 3."
* Ground truth label: "True" (indicated by a right arrow)
* A red "X" symbol indicating the conclusion is false based on the premises.
**Right Section: MATP Check Result**
* **Title:** MATP Check Result
* **Sub-section:** Premises-FOL: A list of the four premises translated into First-Order Logic (FOL).
* **Sub-section:** Conclusion-FOL: The conclusion translated into FOL.
* **Sub-section:** Vampire Result: The result of the Vampire theorem prover, which is "Unknown".
* A green checkmark symbol.
### Detailed Analysis or ### Content Details
**Premises (Natural Language):**
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.
**Conclusion & Ground Truth Label:**
* Statement: Nadal is in the Big 3.
* Ground Truth: True (indicated by the arrow and the word "True" in red).
* The red "X" indicates that the conclusion cannot be derived from the premises.
**MATP Check Result (First-Order Logic):**
* **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)
* **Vampire Result:** Unknown (Indicated by a green checkmark)
### Key Observations
* The natural language premises are translated into First-Order Logic.
* The ground truth label indicates that the conclusion "Nadal is in the Big 3" is true.
* The Vampire theorem prover returns "Unknown," suggesting that it could not derive the conclusion from the premises.
* The red "X" next to the conclusion indicates that the premises are insufficient to prove the conclusion.
### Interpretation
The diagram illustrates a scenario where a set of premises, while seemingly related, fails to logically entail a known true conclusion. The Vampire theorem prover's "Unknown" result highlights the limitations of the given premises in formally proving that Nadal is in the Big 3. The discrepancy between the ground truth (Nadal is in the Big 3) and the logical derivation suggests that either the premises are incomplete, or the formalization in FOL is not capturing all the relevant information. The red "X" reinforces the idea that the provided premises do not logically support the conclusion, even though the conclusion is factually true. This demonstrates the importance of having a complete and accurate set of premises for logical inference.
</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: Entropy vs. JS Divergence for ProofWriter with Llama3.1 Models
### Overview
The image contains two scatter plots comparing the relationship between Entropy and JS Divergence for the ProofWriter dataset using Llama3.1-8B (top) and Llama3.1-70B (bottom) models. Each plot distinguishes between correct (T) and incorrect (F) predictions using blue and red data points, respectively. The plots also include visual aids such as a vertical green line indicating a low entropy threshold and a horizontal purple dashed line.
### Components/Axes
**Top Plot (ProofWriter - Llama3.1-8B):**
* **Title:** ProofWriter - Llama3.1-8B
* **X-axis:** Entropy, with ticks at 0, 10, 20, 30, and 40.
* **Y-axis:** JS Divergence, with ticks at 0.04, 0.06, 0.08, 0.10, and 0.12.
* **Legend (top-right):**
* Blue: Correct (T)
* Red: Incorrect (F)
* **Visual Aids:**
* Vertical green line at approximately x = 2.
* Horizontal purple dashed line at approximately y = 0.07.
* **Annotation:** "Lowest Entropy (Incorrect)" with an arrow pointing to the cluster of points near the vertical green line.
**Bottom Plot (ProofWriter - Llama3.1-70B):**
* **Title:** ProofWriter - Llama3.1-70B
* **X-axis:** Entropy, with ticks at 0, 10, 20, 30, 40, 50, 60, and 70.
* **Y-axis:** JS Divergence, with ticks at 0.04, 0.06, 0.08, 0.10, 0.12, and 0.14.
* **Legend (top-right):**
* Blue: Correct (T)
* Red: Incorrect (F)
* **Visual Aids:**
* Vertical green line at approximately x = 8.
* Horizontal purple dashed line at approximately y = 0.08.
* **Annotation:** "Lowest Entropy (Incorrect)" with an arrow pointing to the cluster of points near the vertical green line.
### Detailed Analysis
**Top Plot (Llama3.1-8B):**
* **Correct (T) - Blue:** The blue points are concentrated at lower entropy values (0-20) and JS Divergence values ranging from 0.04 to 0.10. The density of blue points decreases as entropy increases.
* **Incorrect (F) - Red:** The red points are more scattered across the entropy range (0-45), with JS Divergence values ranging from 0.04 to 0.12. There is a cluster of red points at higher entropy values (25-45).
* **Trend:** As entropy increases, the proportion of incorrect (red) predictions appears to increase.
**Bottom Plot (Llama3.1-70B):**
* **Correct (T) - Blue:** The blue points are concentrated at lower entropy values (0-20) and JS Divergence values ranging from 0.04 to 0.12. The density of blue points decreases as entropy increases.
* **Incorrect (F) - Red:** The red points are more scattered across the entropy range (0-70), with JS Divergence values ranging from 0.06 to 0.14. There is a cluster of red points at higher entropy values (30-70).
* **Trend:** As entropy increases, the proportion of incorrect (red) predictions appears to increase.
### Key Observations
* Both models show a trend where lower entropy values are associated with correct predictions, while higher entropy values are associated with incorrect predictions.
* The Llama3.1-70B model has a wider range of entropy values compared to the Llama3.1-8B model.
* The annotation "Lowest Entropy (Incorrect)" highlights that even at low entropy, there are still incorrect predictions.
* The vertical green line seems to indicate a threshold below which the model is expected to perform well, but this is not always the case.
* The horizontal purple dashed line appears to represent an average JS Divergence value.
### Interpretation
The scatter plots suggest that entropy is a useful, but imperfect, indicator of prediction accuracy for these models on the ProofWriter dataset. Lower entropy generally correlates with correct predictions, but there are still instances of incorrect predictions at low entropy. As entropy increases, the likelihood of incorrect predictions also increases. The Llama3.1-70B model, with its wider entropy range, may be exhibiting more diverse or complex behaviors compared to the Llama3.1-8B model. The presence of incorrect predictions even at low entropy suggests that other factors beyond entropy are influencing the model's accuracy. The plots highlight the importance of considering entropy as one of several metrics when evaluating the performance of language models.
</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.