ForEx: A Formal Verification Framework for Explainable Reasoning in Logical Fallacy Detection and Annotation
For researchers evaluating LLMs on logical reasoning, this work introduces a method to assess the formal validity of explanations beyond label accuracy, exposing a systematic gap invisible to prediction-based metrics.
The paper proposes ForEx, a framework that translates LLM-generated explanations for logical fallacy detection into Lean4 for formal verification. Experiments on LOGIC-Climate show over 90% of outputs pass verification, but agreement with human annotations is only around 20%, revealing a gap between formal derivability and label agreement.
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.