LLMs Lean on Priors, Not Programming Language Semantics

The 43rd International Conference on Machine Learning (ICML 2026) · Seoul, South Korea

Can a language model condition its reasoning on explicitly supplied formal semantics—even when those semantics contradicts its priors?

Aditya Thimmaiah¹ Jiyang Zhang¹ Jayanth Srinivasa² Junyi Jessy Li¹ Milos Gligoric¹

¹The University of Texas at Austin ²Cisco Research

Paper Code Dataset

Citation

BibTeX

@inproceedings{ThimmaiahETAL25PLSemanticsBench,
  title     = {LLMs Lean on Priors, Not Programming Language Semantics},
  author    = {Thimmaiah, Aditya and Zhang, Jiyang and Srinivasa, Jayanth
               and Li, Junyi Jessy and Gligoric, Milos},
  booktitle = {ICML},
  year      = {2026}
}

Frontier LLMs execute programs with up to 90–100% accuracy when symbols retain their usual meanings (e.g., + means addition). Under counterfactual semantic shifts (e.g., redefining + to mean subtraction) accuracy collapses by 40–70 percentage points. Despite handing the complete formal rules, the models keep answering as if the rules were never changed.

LLMs don't faithfully interpret the semantics they are given—they retrieve what symbols usually mean from pretraining.

The problem

Models rely on the semantics they remember, not the semantics they are given.

Ask a model to execute 2 + 2 under standard semantics where + means addition, and it answers 4 every time. Now supply a complete formal semantics in the prompt in which + is defined—rule by rule—to perform subtraction, and ask again.

Standard semantics · “+ is addition”

2 + 2 → models answer 4 ✓

Counterfactual semantics · “+ is subtraction”

2 + 2 → models still answer 4 ✗ (should be 0)

They are not conditioning on the semantics they are given; instead, they are recalling “+ means add” from their prior knowledge.

This scenario is neither contrived nor purely synthetic; operator overloading in C++, Python, Scala, and DSLs such as Triton routinely assigns new meanings to familiar operators—or introduces symbols a model has never encountered. Models expected to reason about code in these languages must be able to follow the semantic specifications they are given for symbols rather than simply relying on their prior knowledge.

Try it out (PredState task)! COMING SOON Powered by HuggingFace

ZeroGPU

C^★ Program

1 int x;
2 x = (Left operand + Right operand);

Faithful interpreter

x = 4 follows semantics

Prior-driven model

x = 4 same answer

C^★ Small-step Operational Semantics

"+" Semantic Rule

+ evaluates as integer addition.

v₃ = v₁ + v₂ ⟨v₁ + v₂, σ⟩ → ⟨v₃, σ⟩

How we test rule conditioning

Rule out every excuse before measuring the failure.

Formal semantics gives us a controlled intervention: preserve a program’s surface syntax while changing the transition rules that define its behavior. A model that truly conditions on the supplied rules should change its answer immediately. Our methodology makes sure that when models fail, the failure is about reasoning—not parsing, tokenization, or ambiguity.

Step 1

Verify models understand the notation

Before any execution test, models solve two multiple-choice tasks: match a natural-language description to its formal rule (NL → Rule) and vice-versa (Rule → NL), under every semantic shift.

Near-ceiling accuracy for nearly all models across all variants. Downstream failures are not an inability to read and understand the formalism.

Step 2

Change the meaning, keep the syntax

Two systematic transformations of the standard C★ semantics preserve rule structure while perturbing the symbol–meaning map: KeywordSwap creates direct conflict with priors; KeywordObf removes familiarity altogether.

Same programs, same rule structure, different symbol bindings—isolating priors from supplied rules.

Step 3

Stress with structural complexity

Three program splits with sharply increasing control-flow, data-flow, and size complexity—from adapted LeetCode/MBPP solutions to fuzzer-generated programs with 100× the cyclomatic complexity.

Separates “can follow rules once” from “can sustain rule-conditioned execution at scale.”

Standard

Familiar syntax;
familiar meaning

+meansaddition

Syntax and pretrained associations agree. Measures baseline execution ability.

KeywordSwap

Familiar syntax;
conflicting meaning

-meansaddition

The strongest test of whether supplied rules override lexical priors.

KeywordObf

Novel syntax; explicitly
defined meaning

𐔱meansaddition

Familiar symbolic cues are removed while rule structure is preserved.

The semantic shifts

Every operator and keyword is systematically remapped.

KeywordSwap exchanges the semantics of familiar operators (+↔−, *↔/, …). KeywordObf assigns semantics to symbols from the Caucasian-Albanian script.

Standard	`+`	`-`	`*`	`/`	`<`	`<=`	`>`	`>=`	`==`	`!=`	`&&`	`\|\|`	`while`	...
KeywordSwap	`-`	`+`	`/`	`*`	`>`	`>=`	`<`	`<=`	`!=`	`==`	`\|\|`	`&&`	`while`	...
KeywordObf	`𐔱`	`𐔲`	`𐔳`	`𐔴`	`𐔶`	`𐔷`	`𐔸`	`𐔹`	`𐔺`	`𐔻`	`𐔽`	`𐔾`	`𐕀`	...

Rule structure, granularity, and count are identical across all three variants.

PLSemanticsBench

Four hypotheses, three tasks, two formalisms, three program splits.

C★—a featherweight C with explicit block delimiters—is formalized in both fine-grained small-step operational semantics (𝕊) and coarser rewriting-based K semantics (𝕂). Ground truths come from executing each program under the transformed semantics with the K-framework and a custom interpreter.

Global rule conditioning

Models can compose many rule applications to correctly predict final states.

→ PredState

State-free rule conditioning

Models can select correct rules when execution never mutates program state.

→ PredRule

Long-horizon rule conditioning

Models can follow formal rules consistently across full execution traces.

→ PredTrace

Conditioning under semantic shift

Models continue following supplied rules when those rules conflict with priors.

→ Swap / Obf on all tasks

C★ program

Human-written, LLM-translated, or fuzzer-generated.

Formal semantics

Small-step operational semantics or K semantics.

→

Semantic shift

Standard, KeywordSwap, or KeywordObf.

→

Ground truth

Final state, rule sequence, and full execution trace.

Hypothesis H1 · Global conditioning

Predict the final state.

Compose many rule applications across control and data flow to determine all variable values after termination.

<ans>
  <n>5</n>
</ans>

Coarse outcome

Fine-grained trace

Dataset splits · median complexity

Structural complexity is a controlled axis.

Splits are validated by execution: human-written programs are checked against public test oracles; translated programs are filtered by successful K-framework execution; fuzzed programs are generated with legality masks and guaranteed-terminating loops.

Split	Programs	Source	Cyclomatic	Lines of code	DepDegree	Trace length
Human-Written	162	LeetCode, HumanEval, CodeContests, MBPP	3	19	12	20
LLM-Translated	165	CodeForces C++ → C★ via Qwen2.5-Inst 32B	9	106	48	180
Fuzzer-Generated	165	Depth-controlled, semantics-aware grammar fuzzer	100	794	6K	190

semantic formalisms (𝕊 and 𝕂)

program splits of rising complexity

semantic shifts per formalism

tasks from outcomes to full traces

Results

High accuracy under standard semantics hides brittle semantic conditioning.

Explore published results across tasks, program complexity, formalization, and semantic condition. The most revealing contrast is not which model scores highest, but how much accuracy survives when symbol meanings shift.

Task Dataset Formalization

No semantics Standard KeywordSwap KeywordObf

PredState · exact-match accuracy (%)

Human-Written · K semantics

The swap condition creates a direct conflict between familiar symbols and supplied meanings.

Semantic gap: Several models approach ceiling accuracy under standard semantics yet lose tens of percentage points when operator meanings are swapped.

Values reported in Tables 4–6 of the paper (one-shot prompting; reasoning-model results averaged over three runs, std. dev. ≤ 5.2 points). Only models reported for the selected split/task are shown.

Rules help reasoning models.

Supplying formal semantics lifts reasoning models by 9–16 points under standard semantics, but most non-reasoning models actually degrade when given the rules.

KeywordSwap is harder than KeywordObf.

KeywordSwap causes 40–70-point drops where KeywordObf causes modest ones. Conflict with priors—not unfamiliarity—is what breaks models.

Structural complexity overwhelms rule composition.

Moving to fuzzer-generated programs collapses accuracy by 40+ points even under standard semantics. Loop nesting depth, data-flow degree, and trace length are the strongest predictors of failure.

Full-trace conditioning is nearly absent.

Only 4 of 11 models achieve any non-zero PredTrace accuracy; the best result is 35%. Most models cannot stay grounded in the rules for dozens of steps.

Debugging

What doesn’t fix it.

Each control experiment targets a candidate excuse for the failures—prompting style, tokenization, state-tracking burden—and eliminates it. What remains is the core deficit: conditioning on supplied rules.

Attempt 1

Chain-of-thought prompting (CoT)

CoT lifts non-reasoning models by ~50 points under standard semantics (Llama-3.3 70B: 29% → 75%). Under KeywordSwap the gains vanish entirely (4% → 3%).

Reasoning traces aid execution, but do not override pretrained operator biases.

Attempt 2

Tokenizer-controlled symbols (1Tok)

Maybe KeywordObf fails because rare Unicode glyphs shatter into many tokens? Replacing every symbol with a verified single-token alternative changes accuracy by ≤ 2.5 points (e.g., 8.4% → 7.0%).

Failures under novel symbols are not a tokenization artifact.

Attempt 3

Removing state tracking (PredRule)

Even when programs never mutate state—eliminating the long-horizon burden entirely—most models still mispredict rules under KeywordSwap (o3-mini drops ~30 points).

Priors dominate even a single, local rule-selection decision.

Robust rule conditioning exists—but only barely, and only in one model.

Gemini-2.5-pro maintains ≥97% PredState accuracy under KeywordSwap on human-written programs and is the only model whose PredTrace accuracy improves under semantic shift (32% → 35%). This shows mutation-robust rule conditioning is achievable—yet it appears in a single frontier system, is far from a general consequence of scale or reasoning training, and still collapses on fuzzer-generated programs (69% → 26% under swap).

Summary of findings

Conditioning under supplied formal rules is a largely unsolved capability axis.

Across 11 frontier models, two formalisms, three semantic shifts, and three complexity regimes, the picture is consistent: contemporary LLMs rely on pretrained lexical associations rather than systematically conditioning on supplied formal rules.

Notation is not the bottleneck.

Models read the formalism at near-ceiling accuracy—then fail to apply it.

Conflict, not novelty, breaks models.

Swapping familiar meanings hurts far more than introducing unfamiliar symbols.

CoT and scale don’t rescue conditioning.

Gains from reasoning traces evaporate exactly when rules conflict with priors.

Long horizons expose the deficit.

Only 4 models produce any correct full trace; the best reaches 35%.

Icon credits

We credit the creators of the following icons used on this webpage: