测试大模型真正掌握的逻辑能力，发现多数模型有隐藏短板。
LogicSkills: A Structured Benchmark for Formal Reasoning in Large Language Models
- 分离出符号化、反例构造和有效性判断三种核心逻辑技能
- 传统模型在符号化与反例构造上表现差，仅有效性评估达标
- 新推理调优模型在三项任务上均表现优异，适合研究逻辑能力
大型语言模型在诸多逻辑推理基准上表现良好，但其真正掌握的核心逻辑能力尚不明确。为此，我们提出LogicSkills基准，专门考察三项基础逻辑技能：(i) 形式符号化——将前提翻译为一阶逻辑；(ii) 反例构造——通过构建有限反例证明论证无效；(iii) 有效性评估——判断结论是否由前提逻辑推出。题目取自不含等号的二元一阶逻辑片段，以英语和卡罗尔虚构词语言双语呈现。所有题目均经Z3求解器验证正确性与非平凡性。在常规指令微调的LLM中，有效性评估表现良好，但在形式符号化与反例构造上显著下降，表明高任务级准确率可能掩盖底层逻辑能力缺陷。相反，近期推理调优模型在三项任务上均表现强劲，显示出更系统化的逻辑能力。
原文摘要 · Abstract (English)
Large language models perform well on many logical reasoning benchmarks, but it remains unclear which core logical skills they truly master. To address this, we introduce LogicSkills, a benchmark that isolates three fundamental logical skills: (i) $\textit{formal symbolization}\unicode{x2014}{}$translating premises into first-order logic; (ii) $\textit{countermodel construction}\unicode{x2014}$showing that an argument is logically invalid by constructing a finite countermodel; and (iii) $\textit{validity assessment}\unicode{x2014}$determining whether a conclusion follows from a set of premises. Items are drawn from the two-variable fragment of first-order logic without identity and are presented in both English and a Carrollian nonce-word language. All instances are solver-verified with Z3 for correctness and non-triviality. Across conventional instruction-tuned LLMs, performance is high on $\textit{validity assessment}$ but substantially lower on $\textit{formal symbolization}$ and $\textit{countermodel construction}$, highlighting that high task-level accuracy can mask weaknesses in core logical skills. In contrast, recent reasoning-tuned models perform strongly across all three tasks, suggesting a more systematic logical skill profile.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。