EngineeringSoftware/PLSemanticsBench
The 43rd International Conference on Machine Learning (ICML 2026), Seoul, South Korea LLMs Lean on Priors, Not Programming Language Semantics by Aditya Thimmaiah1, Jiyang Zhang1, Jayanth Srinivasa2, Junyi Jessy Li1, Milos Gligoric1 1The University of Texas at Austin 2Cisco Research TLDR: Frontier LLMs execute programs with up to 90–100% accuracy when symbols retain their usual… See the full description on the dataset page: https://huggingface.co/datasets/EngineeringSoftware/PLSemanticsBench.
1152
1---2license: cc-by-4.03configs:4 - config_name: nl2rule5 data_files:6 - split: K_Standard_NumRule57 path: nl2rule/K_Standard_NumRule5-*8 - split: K_NonStandard_NumRule59 path: nl2rule/K_NonStandard_NumRule5-*10 - split: S_Standard_NumRule511 path: nl2rule/S_Standard_NumRule5-*12 - split: S_NonStandard_NumRule513 path: nl2rule/S_NonStandard_NumRule5-*14 15 - config_name: rule2nl16 data_files:17 - split: K_Standard_NumDescription518 path: rule2nl/K_Standard_NumDescription5-*19 - split: K_NonStandard_NumDescription520 path: rule2nl/K_NonStandard_NumDescription5-*21 - split: S_Standard_NumDescription522 path: rule2nl/S_Standard_NumDescription5-*23 - split: S_NonStandard_NumDescription524 path: rule2nl/S_NonStandard_NumDescription5-*25 26 - config_name: predrule27 data_files:28 - split: K_Standard_Human_Written29 path: predrule/K_Standard_Human_Written-*30 - split: K_NonStandard_Human_Written31 path: predrule/K_NonStandard_Human_Written-*32 - split: S_Standard_Human_Written33 path: predrule/S_Standard_Human_Written-*34 - split: S_NonStandard_Human_Written35 path: predrule/S_NonStandard_Human_Written-*36 37 - config_name: predstate38 data_files:39 - split: K_Standard_Human_Written40 path: predstate/K_Standard_Human_Written-*41 - split: K_NonStandard_Human_Written42 path: predstate/K_NonStandard_Human_Written-*43 - split: S_Standard_Human_Written44 path: predstate/S_Standard_Human_Written-*45 46 - split: S_NonStandard_Human_Written47 path: predstate/S_NonStandard_Human_Written-*48 49 - split: K_Standard_LLM_Translated50 path: predstate/K_Standard_LLM_Translated-*51 - split: K_NonStandard_LLM_Translated52 path: predstate/K_NonStandard_LLM_Translated-*53 - split: S_Standard_LLM_Translated54 path: predstate/S_Standard_LLM_Translated-*55 - split: S_NonStandard_LLM_Translated56 path: predstate/S_NonStandard_LLM_Translated-*57 58 - split: K_Standard_Fuzzer_Generated59 path: predstate/K_Standard_Fuzzer_Generated-*60 - split: K_NonStandard_Fuzzer_Generated61 path: predstate/K_NonStandard_Fuzzer_Generated-*62 - split: S_Standard_Fuzzer_Generated63 path: predstate/S_Standard_Fuzzer_Generated-*64 - split: S_NonStandard_Fuzzer_Generated65 path: predstate/S_NonStandard_Fuzzer_Generated-*66 67 - config_name: predtrace68 data_files:69 - split: K_Standard_Human_Written70 path: predtrace/K_Standard_Human_Written-*71 - split: K_NonStandard_Human_Written72 path: predtrace/K_NonStandard_Human_Written-*73 - split: S_Standard_Human_Written74 path: predtrace/S_Standard_Human_Written-*75 - split: S_NonStandard_Human_Written76 path: predtrace/S_NonStandard_Human_Written-*77---78 79<div align="center">80 <p>The 43rd International Conference on Machine Learning (ICML 2026), Seoul, South Korea</p>81 <h1>82 LLMs Lean on Priors, Not Programming Language83 <span style="white-space: nowrap;">84 Semantics85 <img86 src="https://raw.githubusercontent.com/EngineeringSoftware/PLSemanticsBench/main/docs/icons/logo.png"87 alt="PLSemanticsBench logo"88 width="60"89 style="display: inline-block !important;90 vertical-align: -1.0em;91 margin-left: 10px;92 margin-bottom: 0;">93 </span>94 </h1>95 96 <p style="font-size: 20px;">97 by98 <a href="https://www.adityathimmaiah.com">Aditya Thimmaiah</a><sup>1</sup>,99 <a href="https://jiyangzhang.github.io/">Jiyang Zhang</a><sup>1</sup>,100 <a href="https://scholar.google.com/citations?user=HtNfeKYAAAAJ&hl=en">Jayanth Srinivasa</a><sup>2</sup>,101 <a href="https://www.jessyli.com">Junyi Jessy Li</a><sup>1</sup>,102 <a href="https://users.ece.utexas.edu/~gligoric/">Milos Gligoric</a><sup>1</sup>103 </p>104 105 <p>106 <sup>1</sup>The University of Texas at Austin 107 <sup>2</sup>Cisco Research108 </p>109</div>110 111<div align="center">112 113[](https://engineeringsoftware.github.io/PLSemanticsBench/)114[](https://arxiv.org/pdf/2510.03415v3)115[](https://github.com/EngineeringSoftware/PLSemanticsBench)116[](https://huggingface.co/datasets/EngineeringSoftware/PLSemanticsBench)117 118</div>119 120---121 122**TLDR:** 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.123LLMs don't faithfully interpret the semantics they are given—they retrieve what symbols usually mean from pretraining.124 125## Abstract126Recent work asks whether large language models (LLMs) condition their reasoning on explicit rules rather than statistical regularities from pre-training. 127Program execution provides a canonical instance: formal semantics define behavior through symbolic transition rules that can be systematically altered 128under distribution shift. We investigate whether LLMs can condition their reasoning on formal semantics through program execution and introduce PLSEMANTICSBENCH, 129pairing featherweight C programs with two semantic systems—small-step operational semantics and K semantics—and probing four capabilities: composing rules for 130final states, selecting rules when state is unmutated, sustaining such conditioning over long traces, and following supplied rules under novel semantics. To 131decouple semantic reasoning from syntactic familiarity, we redefine familiar operators to induce symbol-meaning conflict and introduce novel symbols defined only132through the supplied rules, and stress-test models on Human-Written, LLM-Translated, and Fuzzer-Generated splits with increasing structural complexity. Across 13311 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 increasing134structural complexity. Only a handful of models achieve non-zero long-horizon conditioning accuracy, and even the best systems reach just 35%. Together, these results 135suggest that contemporary LLMs often rely on pretrained lexical associations rather than systematically conditioning on supplied formal rules.136 137## Table of Contents138- [About](#about)139- [Installation](#installation)140- [Quick Start](#quick-start)141- [Detailed Usage](#detailed-usage)142- [Benchmark](#benchmark)143- [Citation](#citation)144 145## About146PLSemanticsBench is the first counterfactual programming language (PL) semantics dataset for evaluating rule-conditioned reasoning in LLMs.147It contains the semantics formalization of `C*`, a featherweight C programming language, in two approaches: small-step 148operational semantics and the K-framework semantics. Execution of `C*` programs under counterfactual and standard semantics is then used as a 149lens for evaluating rule-conditioned reasoning in LLMs via three tasks:150 151| Task | Description |152|------|-------------|153| ✨ **PredState**| Predict the final program state |154| ✨ **PredRule** | Predict the ordered sequence of semantic rules needed to evaluate a program|155| ✨ **PredTrace**| Predict the step-by-step execution of a program |156 157It also includes the auxiliary tasks below, to rule out formal notation understanding as an influencing158factor: 159 160| Task | Description |161|------|-------------|162| ✨ **NL2Rule**| Select the correct formal semantic rule (out of 5) given its natural language description |163| ✨ **Rule2NL** | Select the correct natural language description (out of 5) given the formal semantic rule|164 165## Installation166 167### System Requirements168- [Conda](https://docs.conda.io/projects/conda/en/stable/user-guide/install/index.html) package management system169- Python 3.11 or higher170- OpenAI API key (for running experiments with OpenAI models)171 172 173### Step-by-Step Installation1741. Create and activate the conda environment:175```bash176conda env create -f env.yaml177conda activate plsemanticsbench178```179 1802. Set up your OpenAI API key (only for OpenAI models):181```bash182export OPENAI_API_KEY='your-api-key-here'183```184 185## Quick Start186 187We provide a bash script `quick` that:188 1. Sets up the `plsemanticsbench` conda environment.189 2. Pulls the `DeepSeek-R1 1.5B` model.190 3. Evaluates the `DeepSeek-R1 1.5B` model on the `PredState` task with `no-semantics` and `chain-of-thought` prompting on the `Human-Written` dataset.191 4. Prints the `accuracy` and `malformed-count` to screen.192 5. Creates `metrics-predstate-deepseek-r1:1.5b.json` that contains the evaluation result.193 194```bash195bash quick196```197 198## Detailed Usage199 200### Basic Example201Here's a minimal example to get started:202 203```python204from plsemanticsbench import GPTRunner205from plsemanticsbench import ExperimentArgs, LLMEvaluator206from plsemanticsbench import (207 PROMPT_STRATEGY,208 Task,209 Formalization,210 Semantics_Type,211 Language,212 PLDataset213)214 215# Model name216model_name = "o3-mini"217 218# Experiment args: Run the PredState task on the C* language with219# standard semantics formalized using SOS and with direct prompting220exp_args = ExperimentArgs(221 dataset=PLDataset.Human_Written,222 task=Task.PredState,223 language=Language.CSTAR,224 formalization=Formalization.SOS,225 semantics_type=Semantics_Type.Standard,226 model_name=model_name,227 prompt_strategy=PROMPT_STRATEGY.DA,228 num_datapoints_to_run=2, # Run just 2 datapoints (omit to run entire dataset)229)230 231# Run inference using the OpenAI API232gpt_runner = GPTRunner(args=exp_args)233 234# Generation (generate LLM prediction on the predstate task)235predictions = gpt_runner.do_experiment() # path to dump results can be provided236 237# Evaluation (evaluate LLM prediction against ground-truth)238llm_eval = LLMEvaluator(task=exp_args.task, semantics_type=exp_args.semantics_type)239evaluation_result = llm_eval.evaluate_from_list(results=predictions, model_name=model_name)240print(evaluation_result)241```242 243### Expected Output244 245```python246{247 'accuracy': 1,248 'malformed-count': 0,249}250```251 252### Extending Providers253 254You must implement [BaseRunner](https://github.com/EngineeringSoftware/PLSemanticsBench/blob/main/src/plsemanticsbench/core/exps/base_experiment.py)(`_query` method) to evaluate your models. We provide two example implementations for OpenAI models ([GPTRunner](https://github.com/EngineeringSoftware/PLSemanticsBench/blob/main/src/plsemanticsbench/core/exps/gpt_experiment.py)) and Ollama models ([OllamaRunner](https://github.com/EngineeringSoftware/PLSemanticsBench/blob/main/src/plsemanticsbench/core/exps/ollama_experiment.py)).255 256## Dataset257 258### Access259You can load the dataset using the `datasets` library. Here is an example:260```python261from datasets import load_dataset262 263# Load PredState task with standard semantics under K formalization for the LLM Translated dataset264predstate_K_standard_llm_translated = load_dataset("EngineeringSoftware/PLSemanticsBench", name="predstate")["K_Standard_LLM_Translated"]265 266# Load PredRule task with nonstandard semantics under S formalization for the Human Written dataset267predrule_S_nonstandard_human_written = load_dataset("EngineeringSoftware/PLSemanticsBench", name="predrule")["S_NonStandard_Human_Written"]268 269# Load nl2rule task with standard semantics under S formalization270nl2rule_S_standard = load_dataset("EngineeringSoftware/PLSemanticsBench", name="nl2rule")["S_Standard_NumRule5"]271```272 273### Splits274 275<table>276 <tr>277 <th>Task</th>278 <th>Split</th>279 <th>Description</th>280 </tr>281 <tr>282 <td rowspan="4">✨ <strong>PredState</strong><br>(Final State Prediction)</td>283 <td> predstate/K_Standard_{dataset-name} </td>284 <td>Standard semantics with K formalization</td>285 </tr>286 <tr>287 <td> predstate/K_NonStandard_{dataset-name} </td>288 <td>Nonstandard semantics with K formalization</td>289 </tr>290 <tr>291 <td> predstate/S_Standard_{dataset-name} </td>292 <td>Standard semantics with S formalization</td>293 </tr>294 <tr>295 <td> predstate/S_NonStandard_{dataset-name} </td>296 <td>Nonstandard semantics with S formalization</td>297 </tr>298 <tr>299 <td rowspan="4">✨ <strong>PredRule</strong><br>(Semantic Rule Prediction)</td>300 <td> predrule/K_Standard_Human_Written </td>301 <td>Standard semantics with K formalization</td>302 </tr>303 <tr>304 <td> predrule/K_NonStandard_Human_Written </td>305 <td>Nonstandard semantics with K formalization</td>306 </tr>307 <tr>308 <td> predrule/S_Standard_Human_Written </td>309 <td>Standard semantics with S formalization</td>310 </tr>311 <tr>312 <td> predrule/S_NonStandard_Human_Written </td>313 <td>Nonstandard semantics with S formalization</td>314 </tr>315 <tr>316 <td rowspan="4">✨ <strong>PredTrace</strong><br>(Execution Trace Prediction)</td>317 <td> predtrace/K_Standard_Human_Written </td>318 <td>Standard semantics with K formalization</td>319 </tr>320 <tr>321 <td> predtrace/K_NonStandard_Human_Written </td>322 <td>Nonstandard semantics with K formalization</td>323 </tr>324 <tr>325 <td> predtrace/S_Standard_Human_Written </td>326 <td>Standard semantics with S formalization</td>327 </tr>328 <tr>329 <td> predtrace/S_NonStandard_Human_Written </td>330 <td>Nonstandard semantics with S formalization</td>331 </tr>332 <tr>333 <td colspan="3" align="center"><strong>Auxiliary Tasks (formal notation understanding)</strong></td>334 </tr>335 <tr>336 <td rowspan="4">✨ <strong>NL2Rule</strong><br>(Natural language description to semantic rule)</td>337 <td> nl2rule/K_Standard_NumRule5 </td>338 <td>Standard semantics with K formalization</td>339 </tr>340 <tr>341 <td> nl2rule/K_NonStandard_NumRule5 </td>342 <td>Nonstandard semantics with K formalization</td>343 </tr>344 <tr>345 <td> nl2rule/S_Standard_NumRule5 </td>346 <td>Standard semantics with S formalization</td>347 </tr>348 <tr>349 <td> nl2rule/S_NonStandard_NumRule5 </td>350 <td>Nonstandard semantics with S formalization</td>351 </tr>352 <tr>353 <td rowspan="4">✨ <strong>Rule2NL</strong><br>(Semantic rule to natural language description)</td>354 <td> rule2nl/K_Standard_NumDescription5 </td>355 <td>Standard semantics with K formalization</td>356 </tr>357 <tr>358 <td> rule2nl/K_NonStandard_NumDescription5 </td>359 <td>Nonstandard semantics with K formalization</td>360 </tr>361 <tr>362 <td> rule2nl/S_Standard_NumDescription5 </td>363 <td>Standard semantics with S formalization</td>364 </tr>365 <tr>366 <td> rule2nl/S_NonStandard_NumDescription5 </td>367 <td>Nonstandard semantics with S formalization</td>368 </tr>369</table>370 371 372### Example Data Point373 374An example of a data point from the `predstate/None-human-written` split:375```json376{377 "program": "int ans; ans = 1; ...",378 "syntax": "<program> :: ...",379 "semantics": "ℤ := Set of integers ...",380 "mutated-program": "int ans; ans = 1; ...",381 "mutation-pattern": "KeyWordSwap",382 "exec-trace": [383 {384 "linenumber": 1,385 "rule": ["Rule 38", "Rule 39"],386 "state": {"ans": 1}387 }388 ],389 "ground-truth": "<answer>...</answer>"390}391```392 393## Citation394```bibtex395@inproceedings{ThimmaiahETAL25PLSemanticsBench,396 title = {LLMs Lean on Priors, Not Programming Language Semantics},397 author = {Aditya Thimmaiah, Jiyang Zhang, Jayanth Srinivasa, Junyi Jessy Li, Milos Gligoric},398 year = {2026},399 booktitle = {ICML}, 400}401```402 403 404## License405This project is licensed under the [CC BY 4.0 License](https://creativecommons.org/licenses/by/4.0/).406