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

The article introduces ForEx (Formal Verification for Explainable Reasoning), a framework that formalizes the evaluation of Large Language Models (LLMs) in logical fallacy detection by translating their explanations into Lean4 for formal verification. It emphasizes the distinction between predicted labels and the formal derivability of reasoning, revealing that while over 90% of LLM outputs can be verified as formal reasoning chains, only about 20% align with human annotations. This framework provides a method for practitioners to assess LLMs beyond traditional label accuracy, focusing on the machine-checkable integrity of reasoning processes.