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.

翻译：近期研究探讨大语言模型（LLMs）的推理是否基于显式规则而非预训练中的统计规律。程序执行提供了一个典型实例：形式语义通过符号转换规则定义行为，这些规则可在分布偏移下系统性地被改变。我们探究LLMs能否通过程序执行依据形式语义进行推理，并引入PLSemanticsBench基准：将轻量级C程序与两套语义系统（小步操作语义和K语义）配对，评估四项能力——组合规则推导最终状态、在状态不变时选择规则、在长轨迹中维持这种条件推理、以及遵循新型语义下的给定规则。为分离语义推理与语法熟悉度，我们重新定义常见算子以引发符号-含义冲突，并引入仅通过所给规则定义的新符号，同时在人工编写、LLM翻译和模糊器生成的三个数据划分上测试模型（结构复杂度递增）。在11个前沿LLM中，标准语义下的最终状态准确率（最高90%）在语义变异和结构复杂度增加时急剧下降——降幅达40-60个百分点。仅少数模型在长时域条件推理中实现非零准确率，最佳系统亦仅达35%。这些结果共同表明，当代LLMs常依赖预训练的词法关联，而非系统性地遵循所给形式规则。PLSemanticsBench已公开于https://EngineeringSoftware.github.io/PLSemanticsBench。