LLMs Lean on Priors, Not Programming Language Semantics
Abstract
Recent work asks whether large language models (LLMs) condition their reasoning on explicit rules rather than statistical regularities from pretraining. Program execution provides a canonical instance: formal semantics define behavior through symbolic transition rules that can be systematically altered under distribution shift. We investigate whether LLMs can condition their reasoning on formal semantics through program execution and introduce PLSemanticsBench, pairing featherweight C programs with two semantic systems—small-step operational semantics and K semantics—and probing four capabilities: composing rules for final states, selecting rules when state is unmutated, sustaining such conditioning over long traces, and following supplied rules under novel semantics. To decouple semantic reasoning from syntactic familiarity, we redefine familiar operators to induce symbol-meaning conflict and introduce novel symbols defined only through the supplied rules, and stress-test models on Human-Written, LLM-Translated, and Fuzzer-Generated splits with increasing structural complexity. Across 11 frontier LLMs, strong final-state accuracy under standard semantics (up to 90%) drops sharply—by as much as 40–60% points—under semantic mutations and increasing structural complexity. Only a handful of models achieve non-zero long-horizon conditioning accuracy, and even the best systems reach just 35%. Together, these results suggest that contemporary LLMs often rely on pretrained lexical associations rather than systematically conditioning on supplied formal rules. PLSemanticsBench is publicly available at https://EngineeringSoftware.github.io/PLSemanticsBench.
Lay Summary
When a chatbot reads code and tells you what it does, is it actually following the rules of the programming language—or just recognizing familiar patterns from the millions of programs it saw during training? This matters because in real software, familiar symbols sometimes mean unusual things: a "+" might be redefined to subtract. If a model only pattern-matches, it will get these cases wrong. To find out, we built PLSemanticsBench, a test that hands AI models the exact rules of a small programming language and then asks them to run programs by those rules. The twist: we secretly rewrite the rules—swapping what "+" and "−" mean, or replacing symbols with characters from an ancient alphabet the models have never seen. A model that truly follows the supplied rules adapts instantly; one that relies on memorized habits stumbles. We tested eleven leading AI models. Most did well under normal rules (up to 90% accurate) but collapsed once we changed the rules, dropping by 40 to 60 percentage points, with only one model staying reliable. Our findings show that today's AI often leans on memorized associations rather than genuinely reasoning from the instructions it's given—an important limitation for anyone trusting these systems with code.