Technical Summary: LLMs Lean on Priors, Not Programming Language Semantics

Problem Statement

Current large language models (LLMs) are increasingly deployed to solve programming tasks that ostensibly require reasoning about program behavior, such as predicting outputs, repairing code, or generating new code. A fundamental open question remains: do these models rely primarily on statistical regularities acquired during pre-training (lexical priors), or can they flexibly condition their reasoning on explicitly provided behavioral rules?

While LLMs often perform well on standard programming tasks, it is unclear if they can adapt their reasoning to externally specified formal systems when those systems conflict with entrenched priors learned from data. For instance, if the symbol '+' is explicitly defined to perform subtraction in a provided rule set, a model relying on priors would likely still output addition, whereas a model conditioned on the rules would adapt. This paper investigates whether LLMs can condition their reasoning on formal semantics through program execution, specifically testing their ability to override learned symbol-meaning associations in favor of supplied inference rules.

Methodology

The authors introduce PLSEMANTICSBENCH, a semantics-driven benchmark designed to probe rule-conditioned reasoning under controlled distribution shifts. The methodology involves three core components:

1. Formalism and Language

The benchmark utilizes a featherweight imperative language, C⋆, derived from C but simplified to avoid syntactic ambiguities (e.g., explicit block delimiters {} are used to avoid indentation sensitivity issues found in Python). The language is paired with two distinct formal semantic systems:

• Small-step Structural Operational Semantics (S): A fine-grained system where each rule represents one atomic computation step.
• K Semantics (K): A coarser, rewriting-based system.

These formalisms allow for the systematic alteration of rule definitions without changing the surface syntax of the programs.

2. Semantic Shifts and Stressors

To decouple semantic reasoning from syntactic familiarity, the benchmark introduces two types of semantic mutations:

• KeywordSwap: Selected syntactic operators (e.g., +, -) exchange their semantic interpretations. For example, + is defined to perform subtraction. This creates a direct conflict with pretraining priors while preserving surface syntax.
• KeywordObf: Standard keywords and operators are replaced with novel symbols (drawn from the Caucasian-Albanian script) whose meanings are defined only by the supplied rules. This removes all syntactic priors.

The benchmark evaluates models across three dataset splits with increasing structural complexity:

• Human-Written: Programs adapted from standard coding benchmarks (LeetCode, HumanEval, etc.).
• LLM-Translated: C++ solutions translated to C⋆ by LLMs.
• Fuzzer-Generated: Programs automatically generated by a depth-controlled, semantics-aware fuzzer to maximize control-flow and data-flow complexity.

3. Evaluation Tasks

The benchmark probes four specific hypotheses regarding model capabilities:

• H1 (Global Rule Conditioning): Can models compose many rule applications to correctly predict final program states? (Task: PredState)
• H2 (State-Free Rule Conditioning): Can models select correct operational rules when the program state does not mutate? (Task: PredRule)
• H3 (Long-Horizon Rule Conditioning): Can models sustain rule-conditioned reasoning across long execution traces (loops, nested control flow)? (Task: PredTrace)
• H4 (Rule Conditioning Under Semantic Shift): Do models continue to follow supplied rules under novel semantics that conflict with priors?

The study evaluates 11 frontier LLMs, including non-reasoning models (e.g., Llama-3.3, Qwen2.5-Inst) and reasoning-oriented models (e.g., DeepSeek-R1 variants, O3-mini, GPT-5-mini, Gemini-2.5-pro).

Key Contributions

1. PLSEMANTICSBENCH: The first large-scale benchmark explicitly designed to test whether LLMs condition reasoning on formal rules rather than statistical priors, utilizing program execution as a controlled probe.
2. Formal Semantic Shifts: The introduction of KeywordSwap and KeywordObf transformations that systematically perturb symbol-meaning mappings while preserving rule structure, allowing for the isolation of reliance on lexical associations versus formal definitions.
3. Granular Analysis of Reasoning: A decomposition of program execution reasoning into global state prediction, local rule selection, and long-horizon trace generation, revealing specific failure modes in current models.
4. Comprehensive Empirical Evaluation: A systematic evaluation across 11 models, three dataset complexities, and two semantic formalisms, providing a detailed map of current capabilities and limitations.

Results

The experiments yield several critical findings:

• Reliance on Priors: Under standard semantics, many models achieve high accuracy (up to 90%) on simple tasks. However, under semantic mutations (KeywordSwap), performance drops sharply by 40–60 percentage points. This indicates that models predominantly rely on pretrained lexical associations rather than the supplied formal rules.
• Semantic Shift Sensitivity: The KeywordSwap mutation causes significantly larger performance degradation than KeywordObf. This suggests that the presence of familiar syntax (even with altered meaning) triggers strong prior-based responses that models fail to override.
• Long-Horizon Fragility: Sustaining rule-conditioned reasoning over long execution traces is extremely brittle. Only a handful of models achieve non-zero accuracy on the PredTrace task, and even the best systems reach only ~35% accuracy. Most models collapse to zero accuracy when required to track state and apply rules repeatedly over dozens of steps.
• Impact of Complexity: Performance deteriorates systematically with increased structural complexity (control-flow depth, data-flow dependencies). While reasoning-oriented models benefit from access to formal rules on simple, human-written programs, this advantage often vanishes or reverses on complex, fuzzer-generated programs.
• Chain-of-Thought (CoT) Limitations: CoT prompting boosts performance on standard semantics for non-reasoning models but fails to overcome the bias introduced by semantic swaps, indicating that reasoning traces alone do not enable models to override entrenched operator priors.
• Notation Understanding: Models generally demonstrate high competence in understanding the formal notation itself (NL→Rule and Rule→NL tasks), suggesting that failures in execution tasks stem from reasoning limitations rather than an inability to parse the formalism.

Significance and Claims

The paper positions inferential rule conditioning as a largely unsolved capability axis for learning-based systems in programming languages. The authors claim that contemporary LLMs often fail to condition their reasoning on externally specified formal systems when those systems conflict with data-derived priors.

The significance of this work lies in:

1. Diagnostic Capability: Providing a rigorous method to distinguish between statistical pattern matching and genuine rule-following in LLMs.
2. Limitation Identification: Highlighting that current models lack the robustness to adapt to novel formal semantics, a critical requirement for applications involving operator overloading, domain-specific languages (DSLs), and formal verification.
3. Future Direction: Motivating the development of models that can reason more faithfully about formal specifications, moving beyond the reliance on "entrenched lexical associations" toward systems capable of true conditional reasoning based on provided rules.

The authors conclude that while LLMs show promise in standard execution tasks, their ability to condition reasoning on explicit formal rules remains a significant bottleneck, particularly under semantic shifts and long execution horizons.