ForEx: A Formal Verification Framework for Explainable Reasoning in Logical Fallacy Detection and Annotation
Researchers introduce ForEx, a framework that translates LLM-generated explanations into formal logic (Lean4) to verify whether reasoning actually supports predicted labels on logical fallacy detection tasks. The study reveals a critical gap: while 90% of LLM outputs can be formally verified as logically sound, agreement with human annotations remains around 20%, exposing that formal correctness differs fundamentally from label accuracy.