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 programming language (PL) semantics dataset for evaluating rule-conditioned reasoning in LLMs. It contains the semantics formalization of C*, a featherweight C programming language, in two approaches: small-step operational semantics and the K-framework semantics. Execution of C* programs under counterfactual and standard semantics is then used as a lens for evaluating rule-conditioned reasoning in LLMs via three tasks:

It also includes the auxiliary tasks below, to rule out formal notation understanding as an influencing factor:

Installation

System Requirements

• —Conda package management system
• —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 C* language with
# standard semantics formalized using SOS and with direct prompting
exp_args = ExperimentArgs(
    dataset=PLDataset.Human_Written,
    task=Task.PredState,
    language=Language.CSTAR,
    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,
}

Extending Providers

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

Dataset

Access

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

from datasets import load_dataset

# Load PredState task with standard semantics under K formalization for the LLM Translated dataset
predstate_K_standard_llm_translated = load_dataset("EngineeringSoftware/PLSemanticsBench", name="predstate")["K_Standard_LLM_Translated"]

# Load PredRule task with nonstandard semantics under S formalization for the Human Written dataset
predrule_S_nonstandard_human_written = load_dataset("EngineeringSoftware/PLSemanticsBench", name="predrule")["S_NonStandard_Human_Written"]

# Load nl2rule task with standard semantics under S formalization
nl2rule_S_standard = load_dataset("EngineeringSoftware/PLSemanticsBench", name="nl2rule")["S_Standard_NumRule5"]

Splits

<table> <tr> <th>Task</th> <th>Split</th> <th>Description</th> </tr> <tr> <td rowspan="4">✨ <strong>PredState</strong><br>(Final State Prediction)</td> <td> predstate/KStandard{dataset-name} </td> <td>Standard semantics with K formalization</td> </tr> <tr> <td> predstate/KNonStandard{dataset-name} </td> <td>Nonstandard semantics with K formalization</td> </tr> <tr> <td> predstate/SStandard{dataset-name} </td> <td>Standard semantics with S formalization</td> </tr> <tr> <td> predstate/SNonStandard{dataset-name} </td> <td>Nonstandard semantics with S formalization</td> </tr> <tr> <td rowspan="4">✨ <strong>PredRule</strong><br>(Semantic Rule Prediction)</td> <td> predrule/KStandardHumanWritten </td> <td>Standard semantics with K formalization</td> </tr> <tr> <td> predrule/KNonStandardHumanWritten </td> <td>Nonstandard semantics with K formalization</td> </tr> <tr> <td> predrule/SStandardHumanWritten </td> <td>Standard semantics with S formalization</td> </tr> <tr> <td> predrule/SNonStandardHumanWritten </td> <td>Nonstandard semantics with S formalization</td> </tr> <tr> <td rowspan="4">✨ <strong>PredTrace</strong><br>(Execution Trace Prediction)</td> <td> predtrace/KStandardHumanWritten </td> <td>Standard semantics with K formalization</td> </tr> <tr> <td> predtrace/KNonStandardHumanWritten </td> <td>Nonstandard semantics with K formalization</td> </tr> <tr> <td> predtrace/SStandardHumanWritten </td> <td>Standard semantics with S formalization</td> </tr> <tr> <td> predtrace/SNonStandardHumanWritten </td> <td>Nonstandard semantics with S formalization</td> </tr> <tr> <td colspan="3" align="center"><strong>Auxiliary Tasks (formal notation understanding)</strong></td> </tr> <tr> <td rowspan="4">✨ <strong>NL2Rule</strong><br>(Natural language description to semantic rule)</td> <td> nl2rule/KStandardNumRule5 </td> <td>Standard semantics with K formalization</td> </tr> <tr> <td> nl2rule/KNonStandardNumRule5 </td> <td>Nonstandard semantics with K formalization</td> </tr> <tr> <td> nl2rule/SStandardNumRule5 </td> <td>Standard semantics with S formalization</td> </tr> <tr> <td> nl2rule/SNonStandardNumRule5 </td> <td>Nonstandard semantics with S formalization</td> </tr> <tr> <td rowspan="4">✨ <strong>Rule2NL</strong><br>(Semantic rule to natural language description)</td> <td> rule2nl/KStandardNumDescription5 </td> <td>Standard semantics with K formalization</td> </tr> <tr> <td> rule2nl/KNonStandardNumDescription5 </td> <td>Nonstandard semantics with K formalization</td> </tr> <tr> <td> rule2nl/SStandardNumDescription5 </td> <td>Standard semantics with S formalization</td> </tr> <tr> <td> rule2nl/SNonStandardNumDescription5 </td> <td>Nonstandard semantics with S formalization</td> </tr> </table>

Example Data Point

An example of a data point from the predstate/None-human-written split:

{
  "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    = {Aditya Thimmaiah, Jiyang Zhang, Jayanth Srinivasa, Junyi Jessy Li, Milos Gligoric},
  year      = {2026},
  booktitle = {ICML}, 
}

License

This project is licensed under the CC BY 4.0 License.