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

AI summary

Overview

Research area: Evaluation of logical reasoning in large language models (LLMs), specifically a benchmark for formal reasoning that separates distinct logical subskills.

Technical level: Intermediate. The paper is an evaluation/benchmark paper, but it assumes familiarity with first-order logic notation, model theory (countermodels, validity, satisfiability), and standard LLM evaluation practice.

Scope (one sentence): The paper introduces LogicSkills, a solver-verified benchmark that isolates formal symbolization, countermodel construction, and validity assessment over the two-variable fragment of first-order logic in English and a Carrollian nonce-word language, and reports systematic skill profiles across ten open- and closed-weight LLMs.

Authors and venue details: Brian Rabern (Oregon State University – Cascades, Bend, OR, USA; Niche, Inc., Bend, OR, USA), Philipp Mondorf (Munich Center for Machine Learning, Munich, Germany), and Barbara Plank (Munich Center for Machine Learning; MaiNLP, LMU Munich, Germany). Posted as arXiv:2602.06533v3 [cs.AI], dated 06 Sep 2026. Code for dataset generation, task construction, and model evaluation is available at https://github.com/brianrabern/LogicSkills.

What This Paper Is About

Most logical reasoning benchmarks for LLMs bundle several distinct abilities — parsing natural language, translating it into a formal representation, and drawing inferences — into one composite score, so it is impossible to tell which underlying logical skill a model actually has. The authors build LogicSkills to separate three fundamental skills: turning sentences into first-order logic (formal symbolization), showing an argument is invalid by constructing a finite countermodel (countermodel construction), and deciding whether a conclusion follows from premises (validity assessment). The goal is to reveal whether high accuracy on a task like validity judgment reflects genuine formal reasoning or conceals weaknesses in the subskills that formal reasoning depends on.

Key Contributions

1. A skill-decomposed benchmark for formal reasoning. LogicSkills isolates three logical skills drawn from formal logic pedagogy (Kalish and Montague, 1964): formal symbolization, countermodel construction, and validity assessment, in contrast to prior composite suites such as ProofWriter, LogicBench, and LogicAsker.

2. A solver-verified, bilingual generation pipeline. A compositional generator produces grammatical natural-language sentences paired with formulas in the two-variable fragment of first-order logic without identity (FO2). Every formula is realized in both controlled English and a Carroll-style nonsense lexicon, and all deductive instances are verified with Z3 (de Moura and Bjørner, 2008) for correctness and non-triviality.

3. Semantic rather than string-based scoring. Symbolizations are judged by logical equivalence and countermodels by whether they satisfy the premises and falsify the conclusion, so multiple correct answers are accepted.

4. A cross-model skill profile plus a fine-tuning transfer study. The paper reports accuracy across eight conventional instruction-tuned models and two reasoning-tuned models (Qwen3-32B and OpenAI-o3), and a LoRA fine-tuning study on Llama-3.2-3B-Instruct testing whether symbolization and countermodel skills transfer to validity assessment.

Main Findings

• Conventional instruction-tuned models show a large validity-vs-subskill gap. GPT-4o achieves 86.3% on validity assessment but only 10.0% on countermodel construction; Gemini-2.5-Flash reaches 95.2% on validity versus 13.3% on countermodel construction. Accuracy on validity assessment clusters near ceiling for these models, while formal symbolization remains a consistent bottleneck and countermodel construction is the most discriminative task.

• Reasoning-tuned models perform strongly across all three skills. OpenAI-o3 achieves 98.8% on validity assessment, 98.7% on countermodel construction, and 95.3% on formal symbolization. Qwen3-32B also performs strongly (0.89 on countermodel construction in Table 2, versus 0.35 for DeepSeek-Chat and 0.42 for Claude-3.7-Sonnet).

• Bilingual results show only minor differences. Averaging across models, English and Carroll results were closely aligned (validity 83.0% vs. 84.4%; symbolization 70.7% vs. 69.2%), with a maximum difference of 6.7 percentage points across all conditions. The authors read this as a null result suggesting models are not relying primarily on semantic heuristics.

• Error patterns differ by task. In formal symbolization, over half of the 1,803 incorrect outputs (50.2%) are semantically incorrect despite syntactic well-formedness, with the remainder showing structural issues such as predicate-arity mismatches or ill-formed parentheses. In countermodel construction, most erroneous outputs (72.9% of 2,020) are structurally well-formed but fail to falsify the argument, typically because one or more premises are false; the other 27.1% reflect missing interpretations or malformed predicate definitions. In validity assessment, a majority of the 980 incorrect outputs (58.4%) include the correct answer alongside additional invalid options.

• Fine-tuning produces in-task gains but no transfer to validity. Llama-3.2-3B-Instruct fine-tuned with LoRA on 100k symbolization and 100k countermodel examples rose from 8.3% to 95.0% on symbolization and from 0.0% to 23.0% on countermodel construction, but validity accuracy declined under joint training by 15.3%. The decline is not a decline in judgment: the proportion of responses that resolved into a selection among the candidate conclusions dropped from 97.3% (base) to 61.0% (joint training), while accuracy among responses that did resolve was essentially unchanged (37.7% base vs. 35.0% joint).

• High task-level accuracy can mask weak core skills. Because a competent validity judgment should involve some representation of logical structure and some form of model-theoretic check, the authors argue that conventional models may reach correct validity judgments without robustly symbolizing premises or explicitly constructing countermodels.

Methodology in Plain English

The authors built a programmatic generator that produces sentences in the two-variable fragment of first-order logic without identity. Each sentence is stored with its surface form, a schema of abbreviation mapping logical symbols to lexical items, its FO2 formula, its abstract syntax tree, a language tag, and a counterpart identifier linking its English and Carrollian realizations. The fixed lexicons contain 3 constants (names) and 13 predicates, which bounds the maximum vocabulary size of any sentence; in practice, sentences used to instantiate tasks involve only 3–4 predicates and 1–2 constants (4–6 symbols total).

Arguments are assembled by sampling 3–5 jointly satisfiable premises, then using Z3 to find semantically relevant, non-trivial conclusions that follow. To enforce non-triviality the authors exclude theorems, conclusions derivable from domain constraints alone, and conclusions derivable from only a proper subset (at most 20%) of the premises. Each valid conclusion is paired with 5 structurally similar distractor conclusions that do not follow, constrained to share subject matter (same predicates and constants) with the valid conclusion and preferentially match its syntactic type.

Three tasks instantiate the skills: given a symbol key, produce one well-formed formula (symbolization); given an invalid argument, produce a finite structure making all premises true and the conclusion false (countermodel construction); and given premises plus six candidate conclusions, return the indices of those that must follow (validity assessment, scored by set equality). The countermodel task fixes the domain to {0,1,2}; the authors ran Schwarz's tree proof generator (tpg) on every invalid argument admitted to the task and found the maximum domain size observed across all 300 items was 3, confirming each item is solvable within the fixed domain.

The evaluation set is 1,500 fixed problems: 600 symbolization, 600 validity, and 300 countermodel. Symbolization and validity are evaluated bilingually (300 English and 300 Carroll each); countermodel construction is language-neutral. The generator is fully programmatic and can produce far more — over 200k problem instances were generated for the PEFT experiments.

Ten models are evaluated with greedy decoding: Llama-3.1-8B, Llama-3.1-70B, Qwen2.5-Math-72B, Claude-3.7-Sonnet, GPT-4o, Gemini-2.5-Flash, DeepSeek-Chat, Phi-4, Qwen3-32B, and OpenAI-o3. Responses are processed in two stages: first an extractor LLM (GPT-4o) cleans and normalizes raw completions, then task-specific verification checks correctness. Cosmetic notational variants (∧ as &, ¬ as ∼, → as ⊃, R(x,y) vs. Rxy) are tolerated. A meta-evaluation on 100 randomly sampled instances found an effective extraction accuracy of 98–99%, with one clear extraction error and one ambiguous case after human adjudication.

Why This Matters

Impact on research. The paper argues that composite logical reasoning scores can hide which skills a model has and which it lacks. It gives the field a solver-verified instrument for separating symbolization, model construction, and validity judgment, and it documents a dissociation — near-ceiling validity with weak symbolization and countermodels — that task-level accuracy alone would not expose. It also provides a controlled bilingual probe: because English and Carrollian realizations share logical form, the near-identical scores argue against purely semantic shortcuts. The authors connect the work to a long tradition, from Leibniz's (1685) "let us calculate" to Frege's Begriffsschrift (1879), in which reliability in reasoning is tied to explicit formalization.

Real-world applications (the paper does not enumerate applications; these follow from the skills it measures):

• Natural-language-to-formal-language pipelines, where a system must translate requirements or specifications into logic rather than only answer yes/no questions about them.
• Automated reasoning and verification tooling, where producing a concrete falsifying structure is often more useful than asserting invalidity.
• Educational technology for logic and formal methods instruction, where the three measured skills map onto standard coursework components.
• Auditing deployed LLM reasoning claims, where a model's high score on a composite task may overstate its competence on the underlying subskills.

Industry relevance. The finding that reasoning-tuned models perform strongly across all three tasks — o3 at 98.8% validity, 98.7% countermodel, 95.3% symbolization — is directly relevant to teams deciding which model class to use for formal or verification-adjacent workloads. The PEFT result is equally relevant to teams considering targeted fine-tuning: in-task gains were large (symbolization 8.3% to 95.0%; countermodel 0.0% to 23.0%) but did not transfer, and joint training degraded the fine-tuned model's ability to produce resolvable answers on the validity task (97.3% to 61.0% of responses resolving).

Future Directions

• Scaling the benchmark beyond FO2. The authors note that all tasks are drawn from the two-variable fragment of first-order logic without identity, excluding full first-order logic, identity, and modal operators, so results may not generalize to more expressive logical systems. The generation pipeline is fully programmatic and supports large-scale expansion, but the reported evaluation set is fixed in size.

• Broadening linguistic coverage. The benchmark relies on a controlled fragment of English and a synthetically generated Carrollian language, which isolates logical structure but limits linguistic diversity and does not capture many sources of difficulty in naturally occurring language.

• Determining whether strong reasoning-tuned performance is genuinely model-theoretic. The paper evaluates reasoning behaviorally and explicitly leaves open whether models that pass all three tasks are approximating model-theoretic reasoning or achieving this through more powerful but equally opaque means — a question for mechanistic investigation.

• Understanding why subskills fail to compose. The PEFT study shows symbolization and countermodel skills are acquired in isolation without composing into a workflow the model can deploy on the validity task; the authors describe this as parallel to a student trained on translation and model construction but never shown how they bear on assessing an argument. How to make those components connect remains unresolved. The authors also note their fine-tuning data contained only symbolization and countermodel examples with no validity or general instruction data mixed in, so drift toward the training tasks' response format is expected.

Target Audience

Researchers working on LLM reasoning evaluation and benchmark design; logicians and philosophers of logic interested in what language models do and do not capture about formal methods; NLP practitioners who need models to translate natural language into formal representations or to produce verifiable counterexamples; and engineers selecting or fine-tuning models for verification-adjacent tasks. Readers should be comfortable with first-order logic notation and with the ideas of validity, satisfiability, and countermodels.

Authors’ abstract

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.