用形式化验证评估大模型推理是否真成立，发现标签对但推理错。
ForEx: A Formal Verification Framework for Explainable Reasoning in Logical Fallacy Detection and Annotation
- 把模型解释转成可验证的逻辑代码，检查推理能否从前提推出
- 90%以上模型输出能通过形式验证，但与人工标注仅20%一致
- 适合关注模型推理可信度的研究者，超越单纯看标签对错
当前大模型在逻辑谬误检测中的评估仅关注预测标签，未检验其推理是否真正成立。我们提出ForEx（形式化验证可解释推理框架），将大模型生成的解释转化为Lean4语言，验证其推理是否可在给定前提下推导出结论，而非判断自然语言论证的逻辑有效性。为区分预测结果与推理形式正确性，引入LLM论证验证矩阵，分离标签一致性与形式验证状态。在LOGIC-Climate数据集上的实验显示，超过90%的模型输出可转化为通过验证的形式化推理链，而与人工标注的一致性仅为约20%。这一结果揭示了形式可推导性与标签一致性之间存在系统性差距，传统基于预测的评估无法察觉此差异。ForEx推动大模型评估从标签正确性迈向可机器验证的形式化推理分析。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。