2512.23511

# 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 Technology Wuhan China > National University of Singapore Singapore > Peking University Beijing China > Nanyang Technological University Singapore (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 ## Flowchart: Logical Reasoning Process with Premises and Conclusions ### Overview The image depicts a structured logical reasoning task with 23 premises, a conclusion ("The cat is not cold"), and two model-generated reasoning processes (GPT-3.5-Turbo and GPT-4). It highlights challenges in unstructured responses and subtle reasoning errors. ### Components/Axes 1. **Premises**: - 23 numbered statements (e.g., "The bear is green," "The cat visits the mouse"). - Color-coded: - **Blue**: Conditional premises (e.g., "If something is green..."). - **Red**: Negative premises (e.g., "The cat is not cold"). - **Black**: Neutral premises (e.g., "The dog is round"). 2. **Conclusion & Ground Truth**: - Conclusion: "The cat is not cold." - Ground Truth Label: **False** (marked in red). 3. **Reasoning Processes**: - **GPT-3.5-Turbo**: - 13 steps, including invalid reasoning (e.g., "The cat is not cold" derived from unrelated premises). - Marked with a red cross for errors. - **GPT-4**: - 7 steps, correctly identifying the conclusion as **False** with valid references to premises (e.g., "Premise 17"). - Marked with a green check. 4. **Challenges**: - **Challenge #1**: Unstructured LLM responses (e.g., GPT-3.5-Turbo’s invalid steps). - **Challenge #2**: Subtle/silent reasoning errors (e.g., GPT-4’s correct but incomplete reasoning). ### Content Details - **Premises**: - Key relationships: - Bear, cat, dog, and mouse interactions (e.g., "The bear likes the cat," "The mouse visits the dog"). - Conditional logic (e.g., "If something is green..."). - Contradictions: Premise 9 ("The cat visits the mouse") vs. Premise 18 ("If something is cold..."). - **Reasoning Processes**: - **GPT-3.5-Turbo**: - Step 13: Incorrectly concludes "The cat is not cold" without valid premise support. - **GPT-4**: - Step 7: Correctly identifies the conclusion as **False** using Premise 17 ("If something visits the mouse and the mouse visits the dog..."). ### Key Observations 1. **Model Discrepancies**: - GPT-3.5-Turbo produces unstructured, error-prone reasoning (e.g., Step 7: "Unknown" logic). - GPT-4 provides structured, accurate reasoning but misses some implicit connections. 2. **Logical Gaps**: - Premise 17 is critical for the conclusion but is overlooked in GPT-3.5-Turbo’s process. - Premise 9 ("The cat visits the mouse") conflicts with the conclusion’s validity. 3. **Color Coding**: - Blue/Red/Black coding aids in tracing conditional vs. factual premises but introduces ambiguity in Step 7 (GPT-3.5-Turbo). ### Interpretation - **Structured vs. Unstructured Reasoning**: - GPT-4’s structured approach (referencing specific premises) outperforms GPT-3.5-Turbo’s fragmented logic. - The conclusion’s falsity hinges on Premise 17, which GPT-3.5-Turbo fails to integrate. - **Challenges in Logical Tasks**: - Unstructured responses (Challenge #1) lead to invalid conclusions due to missing premise linkages. - Subtle errors (Challenge #2) arise when models omit critical premises (e.g., GPT-4’s omission of Premise 9). - **Implications**: - Highlights the need for explicit premise referencing in LLM reasoning to avoid errors. - Demonstrates how color coding and premise numbering can aid or hinder logical clarity. </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 ( $\rightarrow$ ), and quantifiers ( $\forall$ for “for all”, $\exists$ 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},\ldots,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 ## Flowchart: Automated Logical Reasoning and Verification Process ### Overview The image depicts a multi-stage flowchart for automated logical reasoning and verification. It outlines a process starting with a reasoning task, progressing through formal logic transformation, automated verification, and response analysis. The diagram uses color-coded sections, arrows, and decision nodes to represent workflow and validation criteria. ### Components/Axes 1. **Sections**: - **Reasoning Task** (Leftmost) - **§3.2 NL2FOL** (Center-left) - **§3.3 Automated Logic Verification** (Center-right) - **§3.4 Response Analysis and Classification** (Rightmost) 2. **Key Elements**: - **Premises (P1-P6)**: Six initial statements about cats, bears, mice, and dogs. - **Conclusion (C)**: "The cat is not cold." - **Ground Truth (L)**: "False" (Conclusion is incorrect). - **Reasoning Steps (S1-S4)**: Logical deductions derived from premises. - **FOL (First-Order Logic)**: Formalized version of premises. - **ATP Tool**: Automated Theorem Prover for verification. - **TPTP**: Thousands of Problems for Theorem Provers format. - **Decision Nodes**: Binary outcomes (True/False, Yes/No). 3. **Flow Arrows**: - Blue arrows indicate progression between sections. - Red arrows highlight errors or failures. - Pink arrows denote conditional checks in response analysis. ### Detailed Analysis #### Reasoning Task - **Premises**: - 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 is cold, then it likes the cat." - 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 (L)**: "False" (Conclusion contradicts premises). #### §3.2 NL2FOL (Natural Language to First-Order Logic) - **Reasoning Steps Filtering**: - Parses premises and conclusions into FOL. - Example: "See(cat, bear)" → `See(x, bear)`. - **FOL Representation**: - P1: `See(cat, bear)` - P2: `Visit(cat, mouse)` - P3: `Cold(mouse)` - P4: `Visit(x, mouse) ∧ Cold(mouse) → Like(x, cat)` - P5: `Like(x, cat) → Visit(x, dog)` - P6: `Cold(x) → Like(x, cat)` - **Error**: "Generation limit exceeded" (Red arrow indicates failure). #### §3.3 Automated Logic Verification - **Single Statement Verification**: - Uses ATP (Automated Theorem Prover) to validate FOL statements. - Example: `State_Ver(P, S)` checks premise-conclusion relationships. - **Outcome**: - **Execution Fail**: Red arrow indicates ATP tool failure. - **FOL to TPTP**: Converts FOL into TPTP format for verification. - **Valid Proof Path**: - Checks if a logical path exists from premises to conclusion (`State_Ver(P, C) = L`). #### §3.4 Response Analysis and Classification - **Decision Tree**: 1. **With Correct Predicted Answer?** - **Yes**: Proceeds to proof path validation. - **No**: Classifies as incorrect. 2. **With Valid Proof Path?** - **Yes**: Further checks for false steps. - **No**: Classifies as invalid. 3. **Without False Step?** - **Yes**: Classifies as "T1" (True with valid proof). - **No**: Classifies as "T4" (False with invalid proof). ### Key Observations 1. **Logical Contradiction**: The conclusion "The cat is not cold" directly contradicts premise P3 ("The mouse is cold") and P6 ("If something is cold, then it likes the cat"), which implies the cat should be cold. 2. **FOL Transformation**: Premises are converted into formal logic to enable automated verification. 3. **ATP Tool Limitations**: The red "Execution fail" arrow suggests the ATP tool could not verify the FOL statements. 4. **Classification Complexity**: The final classification depends on three nested conditions (correctness, proof path validity, and absence of false steps). ### Interpretation This flowchart illustrates a structured approach to verifying logical reasoning using automated tools. The process begins with natural language premises, transforms them into formal logic (FOL), and uses an ATP tool to validate conclusions. The red "Execution fail" indicates a critical failure in the verification stage, suggesting the FOL statements may be unsolvable or the ATP tool lacks capability. The final classification system (T1-T4) emphasizes the importance of both correctness and logical coherence, highlighting that even a "correct" answer may be invalid if derived through flawed reasoning. The diagram underscores the challenges of automated reasoning, including handling logical contradictions and ensuring proof path integrity. </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},\dots,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\in\{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},\dots,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\in\{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 \in\{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}\subseteq 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 ( $\forall$ x or $\exists$ 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},\dots,P_{n}\}$ , candidate statement $S$ 2: Check Result (True, False, Unknown, or Error) 3: function VerifySingleStatement ( $P,S$ ) 4: $res_{1}\leftarrow$ ATPRun ( $P,S$ ) and $res_{2}\leftarrow$ 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},\dots,P_{n}\}$ , candidate conclusion $C$ , ground truth label $L$ , reasoning steps $S=\{S_{1},S_{2},\dots,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$ ) $\neq$ $L$ then 5: return Error $\triangleright$ NL2FOL translation error or labeling error 6: $S_{correctness}\leftarrow[]$ $\triangleright$ Initialize step correctness list 7: for $i\leftarrow 1$ to $m$ do 8: Append ( $S_{correctness}$ , VerifySingleStatement ( $P,S_{i}$ )) 9: $AnswerCorrectness\leftarrow(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}\subseteq 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},\dots,S_{m}\}$ , step correctness annotation $S_{correctness}$ 2: Returns $HasValidProofPath$ 3: function VerifyReasoningProofPath ( $C,L,S,S_{correctness}$ ) 4: $S_{inProofPath}\leftarrow[]$ 5: for $i\leftarrow 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\leftarrow($ 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 ## Heatmaps: Model Prediction Accuracy Comparison ### Overview The image displays three comparative heatmaps evaluating the accuracy of three models (MATP, GPT-4o, DeepSeek-R1) in classifying four categories (T1-T4). Each heatmap visualizes the relationship between ground truth labels (y-axis) and predicted labels (x-axis), with numerical counts in each cell indicating prediction frequencies. ### Components/Axes - **X-axis (Predicted Label)**: Categories T1, T2, T3, T4 - **Y-axis (Ground Truth Label)**: Categories T1, T2, T3, T4 - **Legend**: Not explicitly visible, but cell shading implies darker green = higher counts - **Titles**: - Top row: "MATP Predicted Label", "GPT-4o Predicted Label", "DeepSeek-R1 Predicted Label" - Left column: "Ground Truth Label" (shared across all heatmaps) ### Detailed Analysis #### 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**: Perfect diagonal dominance (100% accuracy for T1-T3, 98% for T4) - **Anomaly**: 2 misclassifications of T3 as T4 #### GPT-4o Predicted Label | | T1 | T2 | T3 | T4 | |-------|----|----|----|----| | **T1**| 48 | 2 | 0 | 0 | | **T2**| 1 | 49 | 0 | 0 | | **T3**| 0 | 0 | 50 | 0 | | **T4**| 0 | 0 | 3 | 47 | - **Trend**: Strong diagonal dominance (96% accuracy for T1, 98% for T2, 100% for T3, 94% for T4) - **Anomaly**: 2 misclassifications of T1 as T2, 1 misclassification of T2 as T1, 3 misclassifications of T4 as T3 #### DeepSeek-R1 Predicted Label | | T1 | T2 | T3 | T4 | |-------|----|----|----|----| | **T1**| 49 | 1 | 0 | 0 | | **T2**| 0 | 50 | 0 | 0 | | **T3**| 0 | 0 | 50 | 0 | | **T4**| 0 | 0 | 4 | 46 | - **Trend**: Strong diagonal dominance (98% accuracy for T1, 100% for T2-T3, 92% for T4) - **Anomaly**: 1 misclassification of T1 as T2, 4 misclassifications of T4 as T3 </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 Across Evaluation Frameworks ### Overview The image displays a grouped bar chart comparing model performance across three evaluation frameworks: **PrOntoQA-OOD**, **ProofWriter**, and **FOLIO**. Each framework contains seven data series (T1–T4, F1, F2, Error), represented by distinct colors. The y-axis measures "Count" (0–400), and the x-axis lists models like GPT-3.5, GPT-4o, LLaMA3.1-8B, etc. The legend is positioned at the top, with colors mapped to data series. --- ### Components/Axes - **Legend**: - **T1** (dark green), **T2** (light green), **T3** (yellow-green), **T4** (orange), **F1** (red), **F2** (dark red), **Error** (purple). - Positioned at the top-center, spanning the width of the chart. - **Y-Axis**: - Labeled "Count" with a scale from 0 to 400 in increments of 50. - Positioned on the left side of the chart. - **X-Axis**: - Labeled with model names (e.g., GPT-3.5, GPT-4o, LLaMA3.1-8B, etc.). - Positioned at the bottom of each sub-chart. - **Sub-Charts**: - Three vertical sections labeled **PrOntoQA-OOD** (top), **ProofWriter** (middle), and **FOLIO** (bottom). --- ### Detailed Analysis #### PrOntoQA-OOD - **T1** (dark green): Highest counts (340, 322, 370, 320, 360). - **T2** (light green): Lower than T1 (e.g., 81, 24, 109, 15, 8). - **T3** (yellow-green): Minimal counts (3, 2, 4, 3, 2). - **F1** (red): Moderate counts (135, 64, 10, 26, 4). - **F2** (dark red): Low counts (9, 4, 4, 3, 4). - **Error** (purple): Very low (3, 1, 4, 4, 7). #### ProofWriter - **T1** (dark green): Highest counts (224, 155, 265, 216, 309). - **T2** (light green): Lower than T1 (e.g., 105, 65, 46, 21, 17). - **T3** (yellow-green): Moderate (52, 33, 20, 11, 9). - **F1** (red): Moderate (64, 39, 89, 26, 22). - **F2** (dark red): Low (29, 10, 8, 5, 4). - **Error** (purple): Very low (2, 1, 4, 8, 1). #### FOLIO - **T1** (dark green): Highest counts (158, 147, 180, 173, 175). - **T2** (light green): Lower than T1 (e.g., 35, 43, 23, 17, 29). - **T3** (yellow-green): Moderate (19, 11, 8, 18, 15). - **F1** (red): Moderate (44, 27, 116, 12, 11). - **F2** (dark red): Low (16, 5, 9, 16, 5). - **Error** (purple): High (117, 115, 116, 113, 116). --- ### Key Observations 1. **T1 Dominance**: T1 consistently achieves the highest counts across all frameworks and models, suggesting superior performance. 2. **Error Bars**: Error counts are generally low but vary (e.g., FOLIO’s Error bars are notably high for GPT-4o and GPT-o4-mini). 3. **Framework-Specific Trends**: - **PrOntoQA-OOD**: T1 > T2 > F1 > F2 > T3 > T4 > Error. - **ProofWriter**: T1 > T2 > F1 > T3 > F2 > T4 > Error. - **FOLIO**: T1 > F1 > T2 > Error > T3 > F2 > T4. 4. **Model Variability**: Models like GPT-4o and LLaMA3.1-8B show higher variability in Error counts compared to others. --- ### Interpretation - **T1’s Consistency**: The dominance of T1 across frameworks implies it may represent a robust or foundational metric (e.g., accuracy, precision) that outperforms other tasks (T2–T4) and failure modes (F1, F2). - **Error Patterns**: Higher Error counts in FOLIO (e.g., GPT-4o: 116) suggest some models struggle with specific failure modes in this framework. - **Framework Differences**: - **PrOntoQA-OOD** emphasizes T1 and F1, possibly testing core QA tasks. - **ProofWriter** balances T1 and F1, indicating a focus on proof-writing accuracy. - **FOLIO** highlights T1 and Error, suggesting it evaluates robustness or edge cases. - **Model Limitations**: Models like GPT-4o and GPT-o4-mini exhibit higher Error rates, indicating potential overfitting or sensitivity to specific tasks. --- ### Spatial Grounding & Verification - **Legend Alignment**: All bar colors match the legend (e.g., T1 = dark green, Error = purple). - **Trend Consistency**: T1 bars are consistently taller than others in each sub-chart, confirming the trend. - **Axis Labels**: X-axis labels are legible and correctly positioned under each sub-chart. --- ### Conclusion The chart demonstrates that **T1** is the most critical metric across all frameworks, with models like GPT-4o and LLaMA3.1-8B showing mixed performance. The Error bars highlight areas for improvement, particularly in FOLIO. This data could guide model optimization by prioritizing T1-related tasks and addressing failure modes in F1/F2. </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) $\forall x(pet(x)\rightarrow 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}\forall x(dog(x)\rightarrow pet(x))}$ 3) ${\color[rgb]{0.203125,0.66015625,0.32421875}\definecolor[named]{pgfstrokecolor}{rgb}{0.203125,0.66015625,0.32421875}\forall x(pet(x)\land dog(x)\rightarrow pet(x))}$ 4) $\forall x((pet(x)\land animal(x))\rightarrow(pet(leo)\rightarrow 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. | $\forall 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})}\rightarrow 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).$ $\exists 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. | $\forall x(Displayed(x)\rightarrow(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 “ $\forall x((Professional(x)\land HighWinRatio(x))\rightarrow 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 ## Screenshot: Logical Reasoning Analysis Interface ### Overview The image displays a technical interface for evaluating logical reasoning, comparing premises, conclusions, and automated verification results. It includes two main sections: "Premises" (user-defined statements) and "MATP Check Result" (system-generated logical analysis). ### Components/Axes - **Premises Section**: - **Labels**: 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: Marked as **False** with a red "X". - **MATP Check Result Section**: - **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**: - Marked as **Unknown** with a green checkmark. ### Content Details - **Premises**: 1. Factual statement about Nadal’s birthplace. 2. Factual statement about Nadal’s profession. 3. Factual statement about Nadal’s performance. 4. General rule defining the "Big 3" criteria. - **MATP Check**: - Premises translated into first-order logic (FOL) with quantifiers (`∀x`) and logical operators (`∧`, `→`). - Conclusion-FOL directly encodes the statement "Nadal is in the Big 3" as `Big3(rafa)`. - Vampire Result: System output labeled **Unknown**, indicating inconclusive verification. ### Key Observations 1. The ground truth explicitly labels the conclusion "Nadal is in the Big 3" as **False**, contradicting the premises’ implication. 2. The MATP system’s "Unknown" result suggests it could not resolve the conclusion’s validity despite the premises. 3. The red "X" and green checkmark visually distinguish conflicting outcomes (ground truth vs. system result). ### Interpretation - The MATP system’s "Unknown" result implies a limitation in its logical framework: while the premises define the Big 3 criteria, they do not explicitly confirm Nadal’s membership. This highlights a gap between the premises’ *implied* conclusion and the system’s inability to deduce it definitively. - The ground truth’s "False" label suggests Nadal is not part of the Big 3 in reality, but the system’s analysis fails to align with this, possibly due to incomplete premise coverage or logical constraints. - The interface underscores challenges in automated reasoning, where human-defined premises may not fully constrain a system’s conclusions without explicit logical entailment. </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: ProofWriter - Llama3.1-8B and Llama3.1-70B ### Overview Two scatter plots compare **JS Divergence** (y-axis) and **Entropy** (x-axis) for correct (blue) and incorrect (red) outputs from the ProofWriter system using Llama3.1-8B and Llama3.1-70B models. Key annotations include a "Lowest Entropy (Incorrect)" label and a purple dashed line at JS Divergence = 0.07. --- ### Components/Axes 1. **Top Plot (Llama3.1-8B)**: - **X-axis (Entropy)**: Ranges from 0 to ~40. - **Y-axis (JS Divergence)**: Ranges from 0 to ~0.12. - **Legend**: Blue = Correct (T), Red = Incorrect (F). - **Annotations**: - "Lowest Entropy (Incorrect)" at (Entropy ≈ 8, JS Divergence ≈ 0.07). - Purple dashed line at JS Divergence = 0.07. - Green dashed vertical line at Entropy = 10. 2. **Bottom Plot (Llama3.1-70B)**: - **X-axis (Entropy)**: Ranges from 0 to ~70. - **Y-axis (JS Divergence)**: Ranges from 0 to ~0.14. - **Legend**: Same as above. - **Annotations**: - "Lowest Entropy (Incorrect)" at (Entropy ≈ 10, JS Divergence ≈ 0.08). - Purple dashed line at JS Divergence = 0.07. - Green dashed vertical line at Entropy = 10. --- ### Detailed Analysis #### Llama3.1-8B (Top Plot) - **Data Trends**: - Correct (blue) points cluster tightly around low Entropy (0–15) and low JS Divergence (0–0.06). - Incorrect (red) points spread widely, with higher Entropy (15–40) and JS Divergence (0.06–0.12). - The "Lowest Entropy (Incorrect)" point (Entropy ≈ 8, JS Divergence ≈ 0.07) lies just above the purple threshold line. - **Key Features**: - Vertical green line at Entropy = 10 separates clusters of correct/incorrect points. - Most incorrect points exceed JS Divergence = 0.07. #### Llama3.1-70B (Bottom Plot) - **Data Trends**: - Correct (blue) points dominate low Entropy (0–25) and low JS Divergence (0–0.10). - Incorrect (red) points extend to higher Entropy (25–70) and JS Divergence (0.08–0.14). - The "Lowest Entropy (Incorrect)" point (Entropy ≈ 10, JS Divergence ≈ 0.08) lies slightly above the purple threshold. - **Key Features**: - Vertical green line at Entropy = 10 is less distinct; incorrect points appear beyond this boundary. - JS Divergence threshold (0.07) is crossed by many incorrect points, even at low Entropy. --- ### Key Observations 1. **Model Size Correlation**: - Llama3.1-70B exhibits higher Entropy and JS Divergence values overall compared to 8B. - Incorrect answers in 70B are more dispersed across the plot, suggesting greater uncertainty in outputs. 2. **Threshold Behavior**: - The JS Divergence = 0.07 line (purple) acts as a rough boundary for correctness in 8B but is less effective for 70B, where incorrect points frequently exceed this threshold. 3. **Entropy Threshold**: - The green line at Entropy = 10 marks a transition point in 8B, where incorrect answers become more prevalent. In 70B, incorrect answers appear even at lower Entropy values. --- ### Interpretation - **Model Performance**: - Larger models (70B) generate outputs with higher uncertainty (Entropy) and divergence from ground truth (JS Divergence), potentially indicating overconfidence or complexity in handling tasks. - The "Lowest Entropy (Incorrect)" points suggest that some errors occur even in low-uncertainty regions, possibly due to model biases or edge-case failures. - **Threshold Implications**: - The JS Divergence = 0.07 threshold may not reliably distinguish correctness in larger models, as incorrect answers frequently exceed this value. - The Entropy = 10 boundary highlights a critical region where model performance degrades, particularly for the 8B variant. - **Design Considerations**: - The plots emphasize trade-offs between model size, uncertainty quantification, and error rates. Larger models may require refined calibration to balance accuracy and confidence. </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.