Same Formulas, Different Semantics: Do Language Models Follow Modal Logic Specifications?

AI summary

Overview

Research area: NLP evaluation of reasoning, specifically whether large language models follow explicitly stated modal logic specifications (Kripke frame properties and first-order domain conditions). Technical level: Advanced. Scope: a diagnostic benchmark of paired modal problems with identical premises and conjectures but opposing oracle labels, used to test whether five recent models track the declared semantics or fall back on familiar logical defaults.

What This Paper Is About

Whether an inference about necessity and possibility is valid depends on assumptions about which worlds are accessible and which objects exist at each world, so the same formula can be valid under one modal system and invalid under another. Existing benchmarks mostly fix one intended logic and vary the facts or proof depth, which lets a model succeed by learning a single dominant inference regime. This paper holds the object-level problem fixed and changes only the declared semantics, then checks whether model judgments change accordingly.

Key Contributions

1. A paired-problem design in which each item shares identical premises and conjecture across two specifications differing in one frame or domain condition, with an automated-reasoning oracle verifying opposite labels.
2. A balanced non-nested core of 160 pairs that removes the "condition shortcut," so mapping a semantic condition to an answer without reading the formula caps strict pair accuracy at 50%.
3. A broad nested set of 800 pairs spanning five frame-property contrasts (K–D, K–T, T–B, T–S4, B–S5) and three first-order domain contrasts (varying–cumulative, varying–decreasing, cumulative–constant).
4. Diagnostic analyses of reasoning mode, output format, premise ablation, semantic affinity to K, D, T, B, S4 and S5, and representation sensitivity, with released formulas, oracle artifacts, countermodels, and responses.

Main Findings

• Failure of semantic control on the balanced core: Four of five models score below the 50% condition-only baseline under direct prompting, ranging from 2.5% to 25.0% mean strict pair accuracy; only Claude Sonnet 5 exceeds it at 65.0%. DeepSeek V4 Flash scores 4.4% [2.1, 8.8], DeepSeek V4 Pro 2.5% [1.0, 6.3], GPT-5.6 Luna 21.2% [15.6, 28.2], and GPT-5.6 Terra 25.0% [18.9, 32.2]. Since the formula is fixed within a pair, changing only the stipulated semantics often fails to change the judgment.
• Reasoning mode restores sensitivity: On unchanged prompts, DeepSeek V4 Flash rises from 4.4% to 88.1% [82.2, 92.3] on the balanced core. On the 400-pair Frame axis it moves from 5.8% to 92.5% (delta +86.8), and on Domain from 17.5% to 90.0% (delta +72.5); GPT-5.6 Luna moves from 18.2% to 63.7% on Frame with medium effort (delta +45.5).
• Defaults exist but do not explain errors: With frame specifications omitted, models fit familiar logics coherently — DeepSeek V4 Flash and Claude Sonnet 5 fit K best, DeepSeek V4 Pro, GPT-5.6 Luna and GPT-5.6 Terra fit T best — yet these affinities do not reliably predict explicit errors.
• Broad nested set results are higher and partly shortcut-driven: Mean strict accuracy is 11.6% (Flash), 18.6% (Pro), 38.2% (Luna), 62.9% (Terra) and 79.1% (Sonnet) against a 63.5% mean condition-only baseline (60.0 Frame, 67.0 Domain).
• Representation is not a simple fix: On a matched 50-pair Frame subset, GPT-5.6 Terra scores 38.0% with named conditions, 6.0% with relational definitions and 44.0% with TPTP; DeepSeek V4 Flash scores 6.0%, 10.0% and 24.0% respectively, and GPT-4.1 scores 4.0%, 10.0% and 0.0%.
• Prompted rationale versus reasoning mode: On the matched 50-pair Frame mini-set, GPT-4.1 improves from 6.0% to 30.0% with a prompted rationale, while DeepSeek V4 Flash improves from 6.0% to 86.0% with high-effort reasoning mode and an unchanged prompt.
• Errors can look like valid derivations: A documented T–S4 case shows a rationale that treats reflexivity as if it propagated accessibility paths, a step that requires transitivity.
• Formatting affects reported scores: Claude Sonnet 5's overall strict accuracy goes from 79.1% reported to 90.3% when conditioned on both sides parsing, with 101 malformed sides (98 empty, 3 nonempty).

Methodology in Plain English

The authors generate candidate problem families that each target a single contrast rather than sampling every combination of formula and semantics. For every retained pair, the premises and conjecture are literally the same text; only one explicit semantic rule changes, for example switching a reflexive-and-symmetric frame for a reflexive-and-transitive one, or switching a "no disappearance" domain for a "no appearance" domain. An automated reasoning pipeline checks each side: problems are serialized in non-classical TPTP, translated to higher-order logic with the LET embedding toolchain, and solved with Vampire and Leo-III. The authors never treat a failure to prove validity as proof of invalidity; they keep only sides with a decisive proof or countermodel and discard conflicts, unresolved sides and 15 timed-out candidates. Of 1,600 accepted sides, 727 have dual-prover agreement and 873 have one decisive result with no contradiction; within the balanced core, every invalid side has a two- or three-world countermodel checked by an independent Kripke evaluator, and 136 of 160 valid sides have dual agreement. Prompts are rendered deterministically in controlled English with neutral vocabulary, state the rules directly, and withhold conventional system names such as B or S4. Five models (DeepSeek V4 Flash, DeepSeek V4 Pro, GPT-5.6 Luna, GPT-5.6 Terra, Claude Sonnet 5) receive all 800 pairs at temperature zero with one response per side; malformed answers count as incorrect, and reasoning-mode runs use identical prompts with an API effort setting.

Why This Matters

The paper separates knowing modal logic from obeying a locally stated specification. A model can hold a coherent default logic and still fail to let the declared model class govern its answer, and extra inference-time computation can restore that sensitivity without guaranteeing valid intermediate steps. This means fixed-semantics benchmarks may overstate robustness, and evaluation claims about logical reasoning need to distinguish compliance with a specification from success under a familiar one.

Real-world applications:

• Deontic and legal reasoning, where obligations and permissions depend on which situations are reachable and which entities persist.
• Reasoning under stated constraints in formal verification or compliance checking, where the system's assumptions are given explicitly rather than assumed.
• Ontology and knowledge-base inference over changing or growing domains, where quantifier–modality ordering changes what follows.
• Any deployed assistant that must apply a user-specified rule set instead of a habitual default, such as policy or configuration reasoning.

Industry relevance: the results argue for testing models against stated specifications rather than assuming a single canonical logic, and suggest that enabling reasoning mode at inference time is a materially different condition from prompting a rationale, which matters for how vendors and deployers configure evaluation and production calls.

Future Directions

• Extending beyond controlled English to broader paraphrase and few-shot tests, since success on synthetic formulas does not establish robust modal reasoning in natural discourse.
• Covering flexible names, which were excluded because the prover portfolio did not reliably resolve their countermodels, and multi-agent cases, which were excluded to keep interventions focused.
• Testing domain contrasts beyond serial frames, since all domain problems here use system D and transfer to other frame classes remains open.
• Investigating representation effects more broadly, as the small representation study leaves room for model- and contrast-specific effects, and clarifying the role of API reasoning levels, which are neither transparent nor calibrated across vendors.
• Establishing human baselines, since the benchmark tests compliance with explicit semantics rather than difficulty for untrained humans and includes no human comparison.

Target Audience

Researchers and practitioners working on logical reasoning evaluation, formal semantics, and LLM benchmarking, along with anyone building systems that must reason under explicit constraints — such as deontic, legal or verification-oriented applications. Readers need some familiarity with modal logic terminology (frames, accessibility, domains, K/T/B/S4/S5) to follow the contrasts, though the paired design and diagnostics are legible without deep expertise in automated theorem proving.

Authors’ abstract

Reasoning about necessity and possibility depends on assumptions about accessibility between worlds and about which objects exist at each one. The same inference may therefore hold under one modal system and fail under another. Evaluating language models on such problems requires testing whether their judgments follow the stated semantics rather than a familiar logic. We construct paired modal problems with identical premises and conjecture but different frame or domain conditions; automated reasoning verifies opposite labels. A balanced core prevents the semantic condition alone from revealing the answer. On this core, four of five recent models perform below the condition-only baseline under direct prompting. Yet enabling reasoning mode raises DeepSeek V4 Flash from 4.4% to 88.1% on unchanged prompts. Following stipulated modal semantics thus depends strongly on inference mode as well as model identity. When frame conditions are omitted, models often agree but fit different familiar logics best. We release the formulas, oracle artifacts, countermodels, and responses.