ForEx: A Formal Verification Framework for Explainable Reasoning in Logical Fallacy Detection and Annotation

• URL: http://arxiv.org/abs/2606.21867v1
• Date: Sat, 20 Jun 2026 04:10:02 GMT
• Title: ForEx: A Formal Verification Framework for Explainable Reasoning in Logical Fallacy Detection and Annotation
• Abstract summary: We propose ForEx, a framework that translates Large Language Models into Lean4.<n>ForEx verifies whether the translated rationale is derivable under encoded premises, not the logical validity of the original natural language argument.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Current evaluations of Large Language Models (LLMs) on logical fallacy detection focus on predicted labels, but do not establish whether those labels are supported by the reasoning the models provide. We propose ForEx (Formal Verification for Explainable Reasoning), a framework that translates LLM-generated explanations into Lean4 and verifies whether the translated rationale is derivable under encoded premises, not the logical validity of the original natural language argument. To distinguish prediction outcomes from the formal status of the supporting reasoning, we introduce the LLM Argument Verification Matrix, which separates label consistency from formal verification status. Experiments on LOGIC-Climate show that over 90% of LLM outputs can be translated into formal reasoning chains that pass verification, while agreement with human annotations remains around 20%. These results expose a systematic gap between formal derivability and label agreement, a distinction invisible to prediction-based metrics. ForEx moves LLM evaluation beyond label correctness toward machine-checkable analysis of formalized reasoning chains.

Related papers

• Position: Logical Soundness is not a Reliable Criterion for Neurosymbolic Fact-Checking with LLMs [6.916679603940271]
  Some neurosymbolic systems verify claims by using large language models (LLMs) to translate natural language into logical formulae.<n>We argue that such approaches structurally fail to detect misleading claims due to systematic divergences between conclusions that are logically sound and inferences that humans typically make and accept.
  arXiv  Detail & Related papers  (2026-04-05T16:48:57Z)
• LLM Reasoning Predicts When Models Are Right: Evidence from Coding Classroom Discourse [0.18268488712787334]
  Large Language Models (LLMs) are increasingly deployed to automatically label and analyze educational dialogue at scale.<n>We investigate whether reasoning generated by LLMs can be used to predict the correctness of a model's own predictions.<n>We analyze 30,300 teacher utterances from classroom dialogue, each labeled by multiple state-of-the-art LLMs with an instructional move construct and an accompanying reasoning.
  arXiv  Detail & Related papers  (2026-02-10T14:38:13Z)
• Uncovering Hidden Correctness in LLM Causal Reasoning via Symbolic Verification [56.51953062869371]
  DoVerifier is a symbolic verifier that checks whether causal expressions are derivable from a given causal graph using rules from do-calculus and probability theory.<n>Our evaluations on synthetic data and causal QA benchmarks show that DoVerifier more accurately captures semantic correctness of causal reasoning traces.
  arXiv  Detail & Related papers  (2026-01-29T03:22:58Z)
• DivLogicEval: A Framework for Benchmarking Logical Reasoning Evaluation in Large Language Models [58.439517684779936]
  This paper proposes a new classical logic benchmark DivLogicEval, consisting of natural sentences composed of diverse statements in a counterintuitive way.<n>To ensure a more reliable evaluation, we also introduce a new evaluation metric that mitigates the influence of bias and randomness inherent in Large Language Models.
  arXiv  Detail & Related papers  (2025-09-19T04:40:46Z)
• CLATTER: Comprehensive Entailment Reasoning for Hallucination Detection [60.98964268961243]
  We propose that guiding models to perform a systematic and comprehensive reasoning process allows models to execute much finer-grained and accurate entailment decisions.<n>We define a 3-step reasoning process, consisting of (i) claim decomposition, (ii) sub-claim attribution and entailment classification, and (iii) aggregated classification, showing that such guided reasoning indeed yields improved hallucination detection.
  arXiv  Detail & Related papers  (2025-06-05T17:02:52Z)
• Towards Logically Sound Natural Language Reasoning with Logic-Enhanced Language Model Agents [3.5083201638203154]
  Logic-Enhanced Language Model Agents (LELMA) is a framework that integrates large language models with formal logic.<n>LeLMA employs autoformalization to translate reasoning into logic representations, which are then used to assess logical validity.<n>LeLMA achieves high accuracy in error detection and improves reasoning correctness via self-refinement.
  arXiv  Detail & Related papers  (2024-08-28T18:25:35Z)
• LogicBench: Towards Systematic Evaluation of Logical Reasoning Ability of Large Language Models [52.03659714625452]
  Recently developed large language models (LLMs) have been shown to perform remarkably well on a wide range of language understanding tasks. But, can they really "reason" over the natural language? This question has been receiving significant research attention and many reasoning skills such as commonsense, numerical, and qualitative have been studied.
  arXiv  Detail & Related papers  (2024-04-23T21:08:49Z)
• A Closer Look at the Self-Verification Abilities of Large Language Models in Logical Reasoning [73.77088902676306]
  We take a closer look at the self-verification abilities of large language models (LLMs) in the context of logical reasoning. Our main findings suggest that existing LLMs could struggle to identify fallacious reasoning steps accurately and may fall short of guaranteeing the validity of self-verification methods.
  arXiv  Detail & Related papers  (2023-11-14T07:13:10Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  We introduce the methodology of Faithfulness-through-Counterfactuals. It generates a counterfactual hypothesis based on the logical predicates expressed in the explanation. It then evaluates if the model's prediction on the counterfactual is consistent with that expressed logic.
  arXiv  Detail & Related papers  (2022-05-25T03:40:59Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.