ForEx：逻辑谬误检测与可解释推理的形式验证框架
ForEx: A Formal Verification Framework for Explainable Reasoning in Logical Fallacy Detection and Annotation
AI总结：
提出ForEx框架，将LLM生成的解释翻译为Lean4并验证其形式可推导性，通过论证验证矩阵区分标签一致性与形式验证状态，揭示形式可推导性与标签一致性之间的系统性差距。
摘要：
当前对大型语言模型（LLM）在逻辑谬误检测上的评估侧重于预测标签，但并未确定这些标签是否得到模型提供的推理支持。我们提出ForEx（可解释推理的形式验证）框架，该框架将LLM生成的解释翻译为Lean4，并验证翻译后的推理是否能在编码前提条件下推导出来，而非原始自然语言论证的逻辑有效性。为了区分预测结果与支持推理的形式状态，我们引入了LLM论证验证矩阵，将标签一致性与形式验证状态分开。在LOGIC-Climate上的实验表明，超过90%的LLM输出可以翻译为通过验证的形式推理链，而与人类注释的一致性仍保持在20%左右。这些结果揭示了形式可推导性与标签一致性之间的系统性差距，这是基于预测的指标无法区分的。ForEx将LLM评估从标签正确性转向对形式化推理链的可机器检查分析。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
