LogicSkills: A Structured Benchmark for Formal Reasoning in Large Language Models

TL;DR

LogicSkills tackles formal reasoning in large language models by disentangling three core subskills within the $FO^2$ fragment: formal symbolization, countermodel construction, and validity assessment. A solver-verified, bilingual (English and Carrollian) data generation pipeline produces 1,500 tasks whose outputs are normalized and checked with Z3, ensuring correctness and non-triviality. Across multiple models, validity remains strong while symbolization and countermodel construction lag, suggesting reliance on surface patterns rather than explicit symbolic or model-theoretic reasoning; an exception (Qwen3-32B) demonstrates broad competence, potentially due to self-scaffolding during inference. These findings highlight the value of subskill-focused benchmarks for diagnosing and guiding improvements in formal reasoning capabilities of large language models.

Abstract

Large language models have demonstrated notable performance across various logical reasoning benchmarks. However, it remains unclear which core logical skills they truly master. To address this, we introduce LogicSkills, a unified benchmark designed to isolate three fundamental skills in formal reasoning: (i) $\textit{formal symbolization}\unicode{x2014}$translating premises into first-order logic; (ii) $\textit{countermodel construction}\unicode{x2014}$formulating a finite structure in which all premises are true while the conclusion is false; and (iii) $\textit{validity assessment}\unicode{x2014}$deciding whether a conclusion follows from a given set of premises. Items are drawn from the two-variable fragment of first-order logic (without identity) and are presented in both natural English and a Carroll-style language with nonce words. All examples are verified for correctness and non-triviality using the SMT solver Z3. Across leading models, performance is high on validity but substantially lower on symbolization and countermodel construction, suggesting reliance on surface-level patterns rather than genuine symbolic or rule-based reasoning.

Figures (5)

• Figure 1: Accuracy of closed models across three skills.
• Figure 2: Skill profile across models (accuracy %; $n{=}300$ per task/language). Grouped bars show Validity, Symbolization, and Countermodel. Most models score highly on validity but lag on subskills, especially countermodels.
• Figure 3: Illustrative instance of the Argument Validity task.
• Figure 4: Illustrative instance of the Formal Symbolization task.
• Figure 5: Illustrative instance of the Countermodel Construction task.