论文
ForEx：逻辑谬误检测与标注中可解释推理的形式化验证框架
ForEx: A Formal Verification Framework for Explainable Reasoning in Logical Fallacy Detection and Annotation
摘要
当前对大语言模型（LLM）逻辑谬误检测的评估聚焦预测标签——但不确立这些标签是否被模型提供的推理支撑。我们提出ForEx（可解释推理的形式化验证）——把LLM生成的解释翻译为Lean4——并验证翻译后的理据是否在编码前提下可推导的框架——而非原始自然语言论证的逻辑有效性。为区分预测结果与支撑推理的形式化地位——我们引入LLM论证验证矩阵——分离标签一致性与形式验证状态。LOGIC-Climate上的实验表明超90%的LLM输出可翻译为通过验证的形式推理链——而与人类标注的一致性仅约20%。这些结果暴露形式可推导性与标签一致性之间的系统缺口——该区别对基于预测的指标不可见。ForEx把LLM评估从标签正确性推进到形式化推理链的机器可查分析。