Source-linked AI summary
Predicting Program Exit Code with LLMs and Programming Language Semantics
Lara Marinov, Aditya Thimmaiah, Jayanth Srinivasa, Junyi Jessy Li, Milos Gligoric
TL;DR
The paper asks whether LLMs truly apply explicit programming-language semantics or instead rely on pre-training priors. It introduces PrEx, a benchmark using valid and systematically transformed invalid programs across semantic formalisms, shifts, and complexity levels. Results show prior reliance, especially under modified semantics, with further degradation as program complexity increases.
Problem
It remains unclear whether LLMs apply supplied programming-language semantics or rely on pre-training priors despite strong performance on software-engineering tasks.
Method
PrEx asks models to classify program executability and identify violated semantic rules using supplied syntax and operational semantics across controlled program and semantic conditions.
Results
LLMs lean on pre-training priors, perform especially poorly under KeywordSwap and KeywordObf, and degrade on LLM-Translated and Fuzzer-Generated programs.
Takeaways & Limitations
The findings indicate that current LLMs do not systematically follow explicitly provided programming-language rules, particularly when familiar semantics or program structure are altered.
Takeaways & Limitations
One Fuzzer-Generated program was removed because its full prompt exceeded the 32K context window of the Qwen2.5-Coder models.
Abstract
from arXiv · showhide
Large language models (LLMs) have shown proficiency in various software engineering tasks, such as code generation and translation. However, a key limitation in their performance may be their (lack of) understanding of programming-language semantics. Even when explicit semantics are given, it remains unclear whether LLMs apply those rules or lean on priors learned during pre-training instead. We study if LLMs lean on priors or given semantics with a novel task--Program Executability Prediction (PrEx)--that asks models to predict whether a program is semantically valid or invalid (and, if invalid, which formal rule it violates) given the program's syntax and operational semantics. Because PrEx requires both valid and invalid programs, we build a dataset with systematically generated invalid transformations derived from valid programs. We evaluate open-source coding LLMs under two semantic formalisms and two semantic shifts across Human-Written, LLM-Translated, and Fuzzer-Generated program splits. Our findings show that LLMs lean on pre-training priors rather than systematically applying the given rules, performing especially poorly on modified semantics and degrading further as program complexity increases. PrEx is available at https://github.com/EngineeringSoftware/prex.
1 Introduction
The paper introduces PrEx to test whether LLMs apply supplied programming-language semantics or rely on pre-training priors. It evaluates this question across semantic formalisms, semantic shifts, and program splits with increasing complexity.
- Task and motivation: LLM coding performance may reflect pattern matching and memorized training data rather than systematic logical simulation of program execution.Subtle loop-bound changes, variable-name obfuscation, or redefined operators can trigger failures.
- Task and motivation: PrEx asks models to predict whether execution succeeds or halts with a semantic error, and identify the violated rule when execution fails.The task uses a discrete executability verdict rather than a long execution trace.
- Benchmark design: The benchmark extends valid programs with matched invalid counterparts generated through semantics-aware transformations across Human-Written, LLM-Translated, and Fuzzer-Generated splits.Program length and complexity increase across the three splits.
- Benchmark design: The evaluation compares small-step operational semantics with the K-framework and tests KeywordSwap and KeywordObf semantic shifts.These conditions vary rule granularity and require models to override familiar symbol meanings or use novel symbols.
- Findings: LLMs lean on pre-training priors rather than systematically applying supplied rules, with especially poor performance under semantic shifts and further degradation on more complex splits.The evaluation includes both direct-answer and chain-of-thought settings for applicable models.
2 Task Description
PrEx asks LLMs to detect semantic errors using a program and its formal language semantics, then identify the violated rule for invalid programs. The task isolates semantic judgment from generating a full execution trace.
- Task motivation: PrEx evaluates whether an LLM can detect semantic errors as a step toward assessing LLMs as program interpreters.The semantic analyzer in traditional interpretation typically follows parsing.
- Task definition: Each prompt supplies the program, formal semantics, and inference rules governing valid and invalid executions.This setup tests whether models reason about semantic correctness from explicit rules.
- Task definition: For an invalid program, the model must classify it as invalid and specify the rule that formalizes the error.A valid program is classified as valid without requiring full step-by-step execution simulation.
3 Methodology
The methodology combines the C∗ language, two semantic formalisms, two semantic shifts, and a prompt requiring an executability verdict plus any violated rule.
- Language and prompt: Experiments use C∗, a small imperative language with C-like syntax specified by a complete EBNF grammar.The grammar is provided to models as part of the prompt.
- Small-step operational semantics: Small-step operational semantics represents execution as repeated applications of fine-grained rules, each describing one atomic computation.Rules use Gentzen-style inference notation with premises and side conditions above conclusions.
- Small-step operational semantics: The S rules include successful and erroneous variable lookup and division behavior, while addition applies after operands are reduced to values.Undeclared-variable and division-by-zero cases are represented by explicit error rules.
- K-framework: The K-framework evaluates code through coarser rewriting steps that handle intermediate reductions in larger chunks.K parallels the S rules for variable lookup and division while differing in how intermediate computations are represented.
- Semantic shifts: KeywordSwap changes familiar operator meanings, whereas KeywordObf assigns standard meanings to novel single-token symbols.Both shifts test adherence to supplied semantics instead of recognizable pre-training associations.
- Full prompt: Each prompt contains the C∗ grammar, either S or K rules, and a program; the model outputs ##success## or ##error## and identifies the violated rule when needed.Non-reasoning models are evaluated with direct-answer and chain-of-thought prompt variants.
4 Dataset Construction
The dataset pairs valid C∗ programs with invalid counterparts produced by semantics-aware transformations across three program-source and complexity splits. Five semantic error categories provide controlled invalid examples.
- Program splits: The benchmark uses Human-Written, LLM-Translated, and Fuzzer-Generated program splits, with source and structural complexity varying across them.Human-Written programs are adapted from C++ sources, LLM-Translated programs come from LLM conversions, and Fuzzer-Generated programs use a grammar-based fuzzer.
- Program complexity: Median program length increases from Human-Written to LLM-Translated to Fuzzer-Generated, with every shortest Fuzzer-Generated program exceeding the longest Human-Written program.Program size is measured in lines of code and tokenizer tokens.
- Invalid-program generation: 491 valid programs are transformed into 2455 semantically invalid programs using an ANTLR-based parser-visitor.Each invalid program applies one random transformation corresponding to a semantic error rule.
- Invalid-program generation: The five injected errors are break outside a loop, continue outside a loop, division by zero, modulo by zero, and use of an undeclared variable.Table 5 maps these errors to their corresponding S and K rules and reports their dataset counts.
5 Experiments and Results
PrEx evaluates open-source coding LLMs across dataset splits, semantic formalisms, and semantic shifts. Accuracy is strongest on Human-Written programs but declines sharply on generated or translated programs and modified semantics, with failures increasingly reflecting false executable judgments.
- Experimental Setup: Models are evaluated under Standard, KeywordSwap, and KeywordObf configurations across Human-Written, LLM-Translated, and Fuzzer-Generated splits.Each table reports accuracy by K and S semantic formalisms and semantic-shift configuration.
- Performance Across Dataset Splits: Fuzzer-Generated programs produce mean accuracy drops of 19pp, 24.8pp, and 33.3pp for DeepSeek-Qwen 32B, Ministral 3 14B-CoT, and Qwen2.5-Coder 32B-CoT, respectively, versus Human-Written programs.The corresponding LLM-Translated declines are 2.9pp, 8.7pp, and 8.6pp.
- Performance Across Dataset Splits: 13pp to 40pp: every capable model loses substantial mean accuracy on Fuzzer-Generated programs, with a median decline of 24pp.Capable models are defined here as having mean Human-Written accuracy of at least 45%.
- Performance on KeywordSwap and KeywordObf: 32pp: median Human-Written accuracy drops from Standard to KeywordObf, compared with 19pp for KeywordSwap across models and formalisms.KeywordObf is consistently harder than KeywordSwap on Human-Written programs.
- Main Failure Modes by Dataset Split: Keyword-dependent errors shrink more under KeywordObf than arithmetic and other error types, especially on Fuzzer-Generated programs.Radar plots show substantially smaller per-error accuracy polygons on the Fuzzer-Generated split.
- Main Failure Modes by Dataset Split: Human-Written failures are relatively rare and often involve wrong-rule confusions, whereas translated and fuzzed programs more frequently yield false-success predictions.Fuzzer-Generated programs additionally show frequent wrong-rule and false-error predictions, especially for modulo-by-zero, break-outside-loop, and variable-use-before-declare.
6 Qualitative Study
The qualitative study examines failure modes in PrEx using rule-level correctness and minimal Human-Written counterexamples. Even short invalid programs expose false predictions and wrong-rule citations, with control-flow error identification weaker than arithmetic errors.
- Failure taxonomy: The analysis classifies mispredictions as false success, false error, wrong rule, or malformed output.A prediction is correct only when executability and, for invalid programs, the violated rule both match the ground truth.
- Per-error-type patterns: Figure 5 compares per-error-type accuracy across models and Human-Written or Fuzzer-Generated programs under S-semantics.Radar axes represent models, colored polygons represent semantic error types, and radial grids show accuracy percentages.
- Minimal counterexamples: The study inspects the two shortest non-empty failing programs for each model and PrEx configuration.The selected examples are intended as minimal counterexamples rather than cherry-picked hard cases.
- Per-error-type patterns: Continue-outside-loop and break-outside-loop identification degrades more than arithmetic-error identification.This pattern appears alongside a case where a model identifies invalidity but cites the wrong control-flow rule.
- Minimal counterexamples: A five-line modulo-by-zero example is recognized as invalid by all three models, but one model cites Rule 24 instead of Rule 23.The cited Rule 24 concerns an unrelated unary-expression rule, so the prediction remains incorrect under the rule-level metric.
7 Related Work
Related work evaluates LLMs’ execution reasoning, runtime-behavior prediction, and sensitivity to program semantics and surface cues. These studies span direct execution, trace-based training, behavioral benchmarks, formal properties, and code-analysis tasks.
- LLM-based predictive execution: Prior work treats LLMs as direct code executors or trains them to inspect execution traces for runtime reasoning.Examples include direct output prediction and self-training with chain-of-thought rationales for program repair.
- Execution and runtime behavior: Execution benchmarks evaluate outputs, inputs, and intermediate runtime behavior on real-world or short-function programs.The cited work includes paired input-output prediction and frameworks covering coverage, program state, and execution behavior.
- Semantics and formal properties: Identifier perturbations can substantially degrade CodeBERT’s code-analysis performance, indicating reliance on identifier semantics rather than logic alone.Other work evaluates termination classification, witness-proof validity, and dead-code elimination with LLM-based systems.
- Semantics and formal properties: These studies motivate testing whether models reason from formal program semantics or depend on surface cues and learned patterns.The related work includes semantic-property evaluation and code-analysis settings where names or structural cues may influence performance.
8 Conclusion
The conclusion introduces PrEx to test whether LLMs apply supplied programming-language semantics or rely on pre-training priors. Across semantic formalisms, semantic shifts, and program splits, models struggle especially on modified semantics and more complex programs.
- Contribution: PrEx asks models to predict execution success or semantic failure and identify the violated formal rule when execution fails.The benchmark extends valid C∗ programs with invalid programs generated by five semantics-aware transformations.
- Evaluation scope: The evaluation covers S and K formalisms, KeywordSwap and KeywordObf semantic shifts, and Human-Written, LLM-Translated, and Fuzzer-Generated splits.These settings vary semantic formalism, surface form, and program source or complexity.
- Findings: Accuracy is highest on short Human-Written programs under standard semantics but drops under semantic shifts and on longer, structurally complex programs.The strongest degradation occurs on LLM-Translated and Fuzzer-Generated programs.
- Findings: The results indicate that current LLMs do not reliably reason from supplied formal semantics and heavily rely on pre-training patterns.The conclusion frames PrEx as evidence about the contrast between explicit semantic rules and learned priors.