Technical Summary: Same Formulas, Different Semantics

Problem Statement

The paper addresses a critical gap in evaluating the reasoning capabilities of Large Language Models (LLMs) regarding modal logic. While existing benchmarks (e.g., ProofWriter, FOLIO, LogicNLI) evaluate deduction under a fixed, implicit background logic, they fail to test whether models can adapt their reasoning to explicitly stated semantic specifications. In modal logic, the validity of an inference often depends on specific frame properties (e.g., reflexivity, transitivity, symmetry) or domain conditions (e.g., constant vs. varying domains). A model may perform well by learning a dominant inference regime (a "familiar" logic like S5) rather than adhering to the specific constraints provided in the prompt. The core problem is determining whether LLMs can suppress their default logical intuitions to follow stipulated, potentially non-standard, semantic conditions.

Methodology

The authors construct a diagnostic benchmark designed to isolate semantic control from formulaic pattern matching.

1. Benchmark Construction:

• Paired Problems: The core dataset consists of pairs of problems where the premises ($P$) and conjecture ($C$) are identical, but the semantic specification ($S$) differs by exactly one condition (e.g., swapping a reflexive frame for a transitive one, or a cumulative domain for a decreasing one).
• Oracle Verification: An automated reasoning oracle (using Vampire and Leo-III via the LET embedding toolchain) verifies that the two specifications yield opposite truth values ($y_a \neq y_b$) for the same formula.
• Balanced Core: To prevent models from exploiting a "condition-only" shortcut (where the answer is determined solely by the semantic label without reading the formula), the authors created a "balanced non-nested core" of 160 pairs. In this subset, each semantic condition appears equally often with both True and False labels. Success here strictly requires reading the formula to determine which condition validates it.
• Scope: The dataset covers five frame-property contrasts (K–D, K–T, T–B, T–S4, B–S5) and three domain contrasts (varying–cumulative, varying–decreasing, cumulative–constant), totaling 800 nested-system pairs and 160 balanced-core pairs.
• Prompting: Prompts use controlled English to explicitly state rules (e.g., "The accessibility relation is reflexive and symmetric") without using conventional system names (like "S4"), forcing the model to rely on the provided rules.

2. Experimental Protocol:

• Models: The study evaluates five recent models: DeepSeek V4 (Flash and Pro), GPT-5.6 (Luna and Terra), and Claude Sonnet 5.
• Conditions:
  • Direct Prompting: Standard inference without reasoning mode.
  • Reasoning Mode: Enabled for specific models (e.g., DeepSeek Flash "high effort") to test if increased inference-time computation aids semantic adherence.
  • Representation Sensitivity: A subset tests performance across named English conditions, relational definitions, and formal TPTP syntax.
  • Semantic Affinity: Experiments omit frame specifications to identify which "default" logic models favor when unconstrained.

Key Results

1. Failure of Semantic Control under Direct Prompting:
On the balanced core, four of the five models performed significantly below the 50% "condition-only" baseline (which assumes the model ignores the formula and guesses based on the condition label).

• DeepSeek V4 Flash: 4.4% strict pair accuracy.
• DeepSeek V4 Pro: 2.5%.
• GPT-5.6 Luna: 21.2%.
• GPT-5.6 Terra: 25.0%.
• Claude Sonnet 5: 65.0% (the only model exceeding the baseline).
  This indicates that most models fail to track stated semantics, instead applying a fixed, familiar logic regardless of the prompt's constraints.

2. Reasoning Mode as a Restorative Mechanism:
Enabling reasoning mode dramatically improved performance for DeepSeek V4 Flash, raising its accuracy on the balanced core from 4.4% to 88.1%. Similar gains were observed for GPT-5.6 Luna on frame problems. This suggests that the failure is not necessarily a lack of logical knowledge, but a failure to activate the correct inference mode to process the specific constraints.

3. Semantic Affinity and Defaults:
When specifications were omitted, models exhibited coherent affinities with familiar logics (e.g., DeepSeek Flash favored K, while Sonnet favored K, and others favored T). However, these defaults did not reliably predict errors when explicit constraints were present; models often agreed on underspecified problems but failed to adjust when constraints were added.

4. Representation Sensitivity:
Changing the input format (from named conditions to relational definitions or TPTP) altered performance rankings but did not consistently restore semantic control. For instance, GPT-5.6 Terra's accuracy dropped from 38% (named) to 6% (relational definitions), indicating that surface-level formatting is not a simple fix for the underlying semantic adherence issue.

Key Contributions

• Diagnostic Benchmark: Introduction of a controlled evaluation framework that holds the object-level problem fixed while varying the semantic specification, specifically designed to test "specification sensitivity."
• Balanced Core: A novel dataset design that eliminates the possibility of solving problems by mapping semantic conditions to answers without reading the logical formula.
• Empirical Evidence of Mode Dependence: Demonstration that the ability to follow modal semantics is highly dependent on the inference mode (direct vs. reasoning), challenging the notion of static logical reasoning capabilities in LLMs.
• Resource Release: Public release of the formulas, oracle artifacts, countermodels, and model responses.

Significance and Claims

The paper argues that fixed-semantics benchmarks may overstate the robustness of LLM reasoning. The primary finding is that modal knowledge (knowing the logic) is distinct from semantic control (applying the specific logic given). A model may possess the necessary logical rules but fail to let a local specification govern its answer, defaulting instead to a familiar inference regime.

The authors modestly claim that their work separates these two capabilities. They note that while reasoning mode can restore sensitivity to semantic interventions, it does not guarantee the correctness of intermediate derivation steps (e.g., a model might correctly switch logic but still derive a false conclusion due to a reasoning error). The study concludes that future evaluations must explicitly test whether models can adapt to stated constraints rather than relying on fixed background assumptions. The paper does not propose new applications or future architectural changes, focusing strictly on the diagnostic evaluation of current models.