Technical Summary: ForEx – A Formal Verification Framework for Explainable Reasoning in Logical Fallacy Detection

1. Problem Statement

Current evaluations of Large Language Models (LLMs) on logical fallacy detection predominantly rely on prediction accuracy (label correctness). However, this approach fails to verify whether the reasoning provided by the model actually supports the predicted label. Correct predictions may stem from superficial correlations rather than genuine logical derivation, while incorrect predictions might be accompanied by reasoning that is formally sound under a specific interpretation but diverges from human annotations.

Furthermore, existing symbolic approaches (e.g., NL2FOL) typically formalize the input argument to check satisfiability, rather than formalizing the model's generated reasoning chain. Additionally, standard annotation practices often compress interpretive variations into single "gold" labels, potentially obscuring plausible alternative readings of an argument. There is a lack of a framework that jointly analyzes predicted labels, generated explanations, and the formal derivability of those explanations.

2. Methodology: The ForEx Framework

The authors propose ForEx (Formal Verification for Explainable Reasoning), a framework that translates LLM-generated natural language explanations into Lean4 (a formal proof assistant) to verify if the translated rationale is derivable under encoded premises. The workflow consists of three stages:

A. Reasoning Candidates Generation

A "Reasoner" model receives an input statement and generates up to $k$ candidates. Each candidate is a tuple $(f_i, a_i, s_i)$ containing:

• $f_i$: The predicted logical fallacy type.
• $a_i$: The natural language explanation (rationale).
• $s_i$: The Lean4 structure formalizing the explanation.

A "Modifier" converts $s_i$ into initial Lean4 code.

B. Execution Feedback & Lean4 Verification

This stage employs an iterative repair loop to ensure the generated Lean4 code compiles:

1. Compilation Attempt: The "Executor" attempts to compile the Lean4 code.
2. Feedback Loop: If compilation fails (state F), the Executor receives the error message and the original explanation $a_i$ to revise the code.
3. Constraints: Revisions are strictly constrained to the original explanation and initial code to prevent semantic drift; the Executor cannot introduce new logical content.
4. Termination: The loop continues until the code compiles successfully (state T) or the maximum repair iterations ($iter_{max}$) are exhausted.

C. Label Consistency Evaluation

The framework introduces the LLM Argument Verification Matrix to decouple label correctness from formal verification status. The matrix classifies outputs into four quadrants based on two axes:

1. Lean4 Verification: Pass (compiles) vs. Fail (does not compile).
2. Label Consistency: Match (prediction equals human annotation) vs. Mismatch.

The four resulting categories are:

• Compilable-Correct (CC): Pass & Match.
• Compilable-Alternative (CA): Pass & Mismatch (indicates a formally valid reasoning chain that supports a label different from the human annotation).
• Uncompilable-Correct (UC): Fail & Match.
• Uncompilable-Incorrect (UI): Fail & Mismatch.

D. Consensus-Guided Annotation Pipeline

To address annotation ambiguity, the authors propose a pipeline that:

1. Represents models and human annotations as multi-hot vectors over fallacy categories.
2. Uses Principal Component Analysis (PCA) and Mahalanobis distance to identify and filter out outlier models.
3. Calculates pairwise Jaccard distances to identify "high-consensus" statements (low disagreement).
4. Augments annotations for high-consensus statements if at least 50% of retained models assign a specific label under formal verification.

3. Key Contributions

1. ForEx Framework: A novel system that translates LLM-generated explanations into Lean4, enabling machine-checkable analysis of formalized reasoning chains rather than just input arguments.
2. LLM Argument Verification Matrix: A metric that separates label consistency from formal verification status, exposing cases where models provide formally derivable reasoning that contradicts existing human labels (the "Compilable-Alternative" category).
3. Consensus-Guided Annotation Pipeline: A method combining human standards, multi-LLM agreement, and formal verification to support annotation analysis and conservative label augmentation, treating annotation disagreement as a signal of interpretive variation rather than noise.

4. Experimental Results

The framework was evaluated on the LOGIC-Climate dataset (1,074 instances, 13 fallacy categories), using a 10% sampled subset and 15 different Reasoner models (including thinking and non-thinking variants).

• Compilation Success: The average pass rate for Lean4 compilation increased from 36.70% (initial) to 98.65% after four repair iterations. Most gains occurred after the first iteration.
• Verification vs. Label Agreement:
  • The combined Compilable-Correct (CC) + Compilable-Alternative (CA) rate was consistently high, exceeding 90% for most models (peaking at 97.59%). This indicates that the vast majority of LLM outputs can be translated into formal reasoning chains that pass verification.
  • However, the CC rate (agreement with human labels) was significantly lower, ranging roughly between 17% and 23% across top models.
  • The CA rate was dominant, suggesting that many formally verified reasoning chains support labels different from the human annotations.
• Error Analysis:
  • Uncompilable-Correct (UC) rates were very low (<2%), indicating that correct labels rarely arise without a verifiable reasoning chain in this setting.
  • Uncompilable-Incorrect (UI) failures were often due to "No Fallacy" (NF) predictions, potentially caused by the lack of context in isolated single-sentence inputs.
• Annotation Augmentation: The consensus-guided pipeline identified a subset of high-consensus statements. Augmented annotations achieved a 0.77 recall against original human annotations, preserving most original labels while adding formally supported alternatives.

5. Significance and Claims

The paper claims that ForEx moves LLM evaluation beyond simple label correctness toward a machine-checkable analysis of formalized reasoning chains.

• Systematic Gap: The results expose a systematic gap between formal derivability and label agreement. The high prevalence of "Compilable-Alternative" outputs suggests that existing human annotations may not fully capture plausible interpretations of input arguments, or that models are reasoning correctly under different assumptions.
• Beyond Prediction: The framework demonstrates that a model can provide a reasoning chain that is formally valid (derivable under encoded premises) even if it disagrees with the "gold" label. This distinction is invisible to standard prediction-based metrics.
• Annotation Utility: ForEx is presented not only as a verification tool but as a mechanism for downstream annotation analysis. It can identify cases where gold labels might be insufficient or where multiple valid interpretations exist, supporting the augmentation of datasets with consensus-based alternative labels.

The authors remain modest regarding the implications, noting that formal verification in Lean4 certifies derivability under encoded premises but does not guarantee semantic alignment with the original natural language statement. They acknowledge that natural language lacks a fully specified semantic foundation, and thus formal results may overstate model capability if the formalization itself is imperfect. Future work is proposed to improve alignment between verification outcomes and semantic correctness by incorporating richer argument structures and contextual information.