EngineeringSoftware/PLSemanticsBench

<div align="center"> <p>The 43rd International Conference on Machine Learning (ICML 2026), Seoul, South Korea</p> <h1> LLMs Lean on Priors, Not Programming Language <span style="white-space: nowrap;"> Semantics <img src="https://raw.githubusercontent.com/EngineeringSoftware/PLSemanticsBench/main/docs/icons/logo.png" alt="PLSemanticsBench logo" width="60" style="display: inline-block !important; vertical-align: -1.0em; margin-left: 10px; margin-bottom: 0;"> </span> </h1>

<p style="font-size: 20px;"> by <a href="https://www.adityathimmaiah.com">Aditya Thimmaiah</a>¹, <a href="https://jiyangzhang.github.io/">Jiyang Zhang</a>¹, <a href="https://scholar.google.com/citations?user=HtNfeKYAAAAJ&hl=en">Jayanth Srinivasa</a>², <a href="https://www.jessyli.com">Junyi Jessy Li</a>¹, <a href="https://users.ece.utexas.edu/~gligoric/">Milos Gligoric</a>¹ </p>

<p> ¹The University of Texas at Austin &nbsp;&nbsp;&nbsp; ²Cisco Research </p> </div>

<div align="center">

   

</div>

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. LLMs don't faithfully interpret the semantics they are given—they retrieve what symbols usually mean from pretraining.

Abstract

Recent work asks whether large language models (LLMs) condition their reasoning on explicit rules rather than statistical regularities from pre-training. 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.

Table of Contents

• —About
• —Installation
• —Quick Start
• —Detailed Usage
• —Benchmark
• —Citation

About

PLSemanticsBench is the first counterfactual PL semantics dataset for rule-conditioned reasoning of LLMs. We introduce three tasks to evaluate this:

You must implement BaseRunner(_query method) to evaluate your models. We provide two example implementations for OpenAI models (GPTRunner) and Ollama models (OllamaRunner).

Installation

System Requirements

• —Python 3.11 or higher
• —OpenAI API key (for running experiments with OpenAI models)

Step-by-Step Installation

1. 1.Create and activate the conda environment:

conda env create -f env.yaml
conda activate plsemanticsbench

1. 1.Set up your OpenAI API key (only for OpenAI models):

export OPENAI_API_KEY='your-api-key-here'

Quick Start

We provide a bash script quick that:

1. 1.Sets up the plsemanticsbench conda environment.
2. 2.Pulls the DeepSeek-R1 1.5B model.
3. 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.
4. 4.Prints the accuracy and malformed-count to screen.
5. 5.Creates metrics-predstate-deepseek-r1:1.5b.json that contains the evaluation result.

bash quick

Detailed Usage

Basic Example

Here's a minimal example to get started:

from plsemanticsbench import GPTRunner
from plsemanticsbench import ExperimentArgs, LLMEvaluator
from plsemanticsbench import (
    PROMPT_STRATEGY,
    Task,
    Formalization,
    Semantics_Type,
    Language,
    PLDataset
)

# Model name
model_name = "o3-mini"

# Experiment args: Run the PredState task on the IMP language with
# standard semantics formalized using SOS and with direct prompting
exp_args = ExperimentArgs(
    dataset=PLDataset.Human_Written,
    task=Task.PredState,
    language=Language.IMP,
    formalization=Formalization.SOS,
    semantics_type=Semantics_Type.Standard,
    model_name=model_name,
    prompt_strategy=PROMPT_STRATEGY.DA,
    num_datapoints_to_run=2, # Run just 2 datapoints (omit to run entire dataset)
)
                        
# Run inference using the OpenAI API
gpt_runner = GPTRunner(args=exp_args)

# Generation (generate LLM prediction on the predstate task)
predictions = gpt_runner.do_experiment() # path to dump results can be provided

# Evaluation (evaluate LLM prediction against ground-truth)
llm_eval = LLMEvaluator(task=exp_args.task, semantics_type=exp_args.semantics_type)
evaluation_result = llm_eval.evaluate_from_list(results=predictions, model_name=model_name)
print(evaluation_result)

Expected Output

{
    'accuracy': 1,
    'malformed-count': 0,
}

Benchmark

You can load the dataset using the datasets library. Here is an example:

from datasets import load_dataset

# Load PredState task with standard semantics (uk) and K-semantics formalization (K) and with the Human Written (human-written) dataset
predstate_IMP_K_uk_human_written = load_dataset("EngineeringSoftware/PLSemanticsBench", name="predstate-IMP-K-uk-human-written")

# Load PredRule task with nonstandard semantics (mk) ans SOS formalization (SOS) and with the LLM Translated (llm-translated) dataset
predrule_IMP_SOS_mk_llm_translated = load_dataset("EngineeringSoftware/PLSemanticsBench", name="predrule-IMP-SOS-mk-llm-translated")

# Load PredState task with no-semantics (nk) and with the Fuzzer Generated (fuzzer-generated) dataset
predstate_IMP_nk_fuzzer_generated = load_dataset("EngineeringSoftware/PLSemanticsBench", name="predstate-IMP-nk-fuzzer-generated")

Dataset Split

<table> <tr> <th>Task</th> <th>Split</th> <th>Description</th> </tr> <tr> <td rowspan="5">✨ <strong>PredState</strong><br>(Final State Prediction)</td> <td> predstate-IMP-nk-{dataset-name} </td> <td> No semantics </td> </tr> <tr> <td> predstate-IMP-K-uk-{dataset-name} </td> <td>Standard semantics with K-semantics formalization</td> </tr> <tr> <td> predstate-IMP-K-mk-{dataset-name} </td> <td>Nonstandard semantics with K-semantics formalization</td> </tr> <tr> <td> predstate-IMP-SOS-uk-{dataset-name} </td> <td>Standard semantics with SOS formalization</td> </tr> <tr> <td> predstate-IMP-SOS-mk-{dataset-name} </td> <td>Nonstandard semantics with SOS formalization</td> </tr> <tr> <td rowspan="4">✨ <strong>PredRule</strong><br>(Semantic Rule Prediction)</td> <td> predrule-IMP-K-uk-human-written </td> <td>Standard semantics with K-semantics formalization</td> </tr> <tr> <td> predrule-IMP-K-mk-human-written </td> <td>Nonstandard semantics with K-semantics formalization</td> </tr> <tr> <td> predrule-IMP-SOS-uk-human-written </td> <td>Standard semantics with SOS formalization</td> </tr> <tr> <td> predrule-IMP-SOS-mk-human-written </td> <td>Nonstandard semantics with SOS formalization</td> </tr> <tr> <td rowspan="4">✨ <strong>PredTrace</strong><br>(Execution Trace Prediction)</td> <td> predtrace-IMP-K-uk-human-written </td> <td>Standard semantics with K-semantics formalization</td> </tr> <tr> <td> predtrace-IMP-K-mk-human-written </td> <td>Nonstandard semantics with K-semantics formalization</td> </tr> <tr> <td> predtrace-IMP-SOS-uk-human-written </td> <td>Standard semantics with SOS formalization</td> </tr> <tr> <td> predtrace-IMP-SOS-mk-human-written </td> <td>Nonstandard semantics with SOS formalization</td> </tr> </table>

Data Example

One example of the dataset is as follows:

{
  "program": "int ans; ans = 1; ...",
  "syntax": "<program> :: ...",
  "semantics": "ℤ := Set of integers ...",
  "mutated-program": "int ans; ans = 1; ...",
  "mutation-pattern": "KeyWordSwap",
  "exec-trace": [
    {
      "linenumber": 1,
      "rule": ["Rule 38", "Rule 39"],
      "state": {"ans": 1}
    }
  ],
  "ground-truth": "<answer>...</answer>"
}

Citation

@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}
}

License

This project is licensed under the CC BY 4.0 License.