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

arXiv: https://arxiv.org/abs/2606.21867 · HTML: https://mlsanity.com/paper/2606.21867/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 15 of its 22 references that are in the map.
- First posted on arXiv 20 Jun 2026.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 15 of 15)

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [GPT-4o System Card](https://mlsanity.com/paper/2410.21276/) (2024)
- [Chain-of-Verification Reduces Hallucination in Large Language Models](https://mlsanity.com/paper/2309.11495/) (2023)
- [Ever: Mitigating Hallucination in Large Language Models through Real-Time Verification and Rectification](https://mlsanity.com/paper/2311.09114/) (2023)
- [Right Answer, Wrong Score: Uncovering the Inconsistencies of LLM Evaluation in Multiple-Choice Question Answering](https://mlsanity.com/paper/2503.14996/) (2025)
- [CrowdTruth 2.0: Quality Metrics for Crowdsourcing with Disagreement](https://mlsanity.com/paper/1808.06080/) (2018)
- [Logical Fallacy Detection](https://mlsanity.com/paper/2202.13758/) (2022)
- [Variation in Verification: Understanding Verification Dynamics in Large Language Models](https://mlsanity.com/paper/2509.17995/) (2025)
- [Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection](https://mlsanity.com/paper/2405.02318/) (2024)
- [Self-Contradictory Reasoning Evaluation and Detection](https://mlsanity.com/paper/2311.09603/) (2023)
- [Reason from Fallacy: Enhancing Large Language Models' Logical Reasoning through Logical Fallacy Understanding](https://mlsanity.com/paper/2404.04293/) (2024)
- [Evaluation of an LLM in Identifying Logical Fallacies: A Call for Rigor When Adopting LLMs in HCI Research](https://mlsanity.com/paper/2404.05213/) (2024)
- [CoCoLoFa: A Dataset of News Comments with Common Logical Fallacies Written by LLM-Assisted Crowds](https://mlsanity.com/paper/2410.03457/) (2024)
- [Boosting Logical Fallacy Reasoning in LLMs via Logical Structure Tree](https://mlsanity.com/paper/2410.12048/) (2024)
- [Follow My Lead: Logical Fallacy Classification with Knowledge-Augmented LLMs](https://mlsanity.com/paper/2510.09970/) (2025)

## Abstract (arXiv)

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.