The 43rd International Conference on Machine Learning (ICML 2026), Seoul, South Korea

LLMs Lean on Priors, Not Programming Language Semantics

by Aditya Thimmaiah¹, Jiyang Zhang¹, Jayanth Srinivasa², Junyi Jessy Li¹, Milos Gligoric¹

¹The University of Texas at Austin     ²Cisco Research

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:

Task	Description
✨ PredState	Predicts the final program state
✨ PredRule	Predicts the ordered sequence of semantic rules needed to evaluate a program
✨ PredTrace	Predicts the step-by-step execution of a program

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

Task	Description
✨ NL2Rule	Select the correct formal semantic rule (out of 5) given its natural language description
✨ Rule2NL	Select the correct natural language description (out of 5) given the formal semantic rule

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

• Conda package management system
• Python 3.11 or higher
• OpenAI API key (for running experiments with OpenAI models)

Step-by-Step Installation

1. Create and activate the conda environment:

conda env create -f env.yaml
conda activate plsemanticsbench

2. 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. Sets up the plsemanticsbench conda environment.
2. Pulls the DeepSeek-R1 1.5B model.
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. Prints the accuracy and malformed-count to screen.
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,
}

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 PredState task with standard semantics but without explicitly providing the formal semantics rules, for the Fuzzer Generated dataset
predstate_none_fuzzer_generated = load_dataset("EngineeringSoftware/PLSemanticsBench", name="predstate/None-fuzzer-generated")

Splits

Task	Split	Description
✨ PredState (Final State Prediction)	predstate/None-{dataset-name}	No semantics
	predstate/K-Standard-{dataset-name}	Standard semantics with K formalization
	predstate/K-NonStandard-{dataset-name}	Nonstandard semantics with K formalization
	predstate/S-Standard-{dataset-name}	Standard semantics with S formalization
	predstate/S-NonStandard-{dataset-name}	Nonstandard semantics with S formalization
✨ PredRule (Semantic Rule Prediction)	predrule/K-Standard-human-written	Standard semantics with K formalization
	predrule/K-NonStandard-human-written	Nonstandard semantics with K formalization
	predrule/S-Standard-human-written	Standard semantics with S formalization
	predrule/S-NonStandard-human-written	Nonstandard semantics with S formalization
✨ PredTrace (Execution Trace Prediction)	predtrace/K-Standard-human-written	Standard semantics with K formalization
	predtrace/K-NonStandard-human-written	Nonstandard semantics with K formalization
	predtrace/S-Standard-human-written	Standard semantics with S formalization
	predtrace/S-NonStandard-human-written	Nonstandard semantics with S formalization

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