PaperlayerView exact revision on arXiv

Source-linked AI summary

ALIAS: Evaluating Performance and Memorization in LLM-Written TLA+ Specifications

Arslan Bisharat, Mujtaba Nazari, Khushboo Bhadauria, Brian Ortiz, Eric Spencer, Beatriz Santos, TaiNing Wang, George K. Thiruvathukal, Konstantin Laufer, Mohammed Abuhamad

arXiv:2610.29767v1cs.CLcs.SE

TL;DR

Public TLA+ benchmark specifications may overlap model training data, while consistent identifier renaming treats lower renamed-task scores as evidence of memorization. The paper tests this approach using TLC to verify behavior-preserving renamings and compares grading and controlled exposure; behavior-based grading reduces the observed decrease, showing that score drops can mix several effects.

  • Problem

    Because public TLA+ benchmark specifications may overlap model training data, it is unknown whether models recall them, while CIR treats lower renamed-task scores as evidence of memorization.

    Source: §1 · p. 1

  • Method

    The study evaluates CIR on 111 TLA+-Bench tasks, uses TLC to verify behavior-preserving renamings, and compares name-based, behavior-based, and controlled-exposure evaluations.

    Source: §1 · p. 2

  • Results

    Under behavior-based grading, Opus 4.8’s decrease is 3.1 points and GPT-5’s decrease is 0.0 points; renaming also removes about half the likelihood gain from training exposure.

    Source: §4 · p. 7

  • Takeaways & Limitations

    A lower score after CIR can reflect memorization, name-based grading, and the added difficulty of unfamiliar names, rather than memorization alone.

    Source: §1 · p. 2

    The behavior-based grader requires matching variable and constant counts, searches at most 60 variable mappings, and can accept extra fairness conditions.

    Source: Limitations · p. 9

Abstract

from arXiv · show

Memorization inflates the benchmark scores of large language models (LLMs), since a model can reproduce answers it saw in training. Researchers test for it with consistent identifier renaming (CIR), which gives every identifier in a task a new name, and treat a lower score on the renamed task as evidence of recall. We test this method on the Temporal Logic of Actions Plus (TLA+) language, whose model checker acts as an oracle by confirming whether a renamed task preserves the exact behaviors of the original. Across 111 TLA+-Bench tasks, renaming lowers the correctness of Claude Opus 4.8 from 28% to 18% and of GPT-5 from 9% to 7%. Most of this decrease comes from how the test grades, which requires exact names that most descriptions never state. Grading by behavior shrinks the decrease to about 3 percentage points for Opus 4.8 and to 0 for GPT-5. In two model families fine-tuned on disjoint halves of the tasks, renaming removes about half of the training gain in likelihood and costs 4.9 percentage points (Qwen) and 1.3 percentage points (Gemma) on unseen tasks. A lower score after renaming therefore mixes memorization, name-based grading, and the cost of new names.

1 Introduction

The paper tests whether consistent identifier renaming (CIR) measures memorization in LLM-written TLA+ specifications. It argues that score decreases can also reflect name-based grading and the difficulty of unfamiliar names.

1 Introduction

  • TLA+-Bench checks generated specifications with the SANY parser and TLC model checker, while writing correct specifications requires time and expertise.The paper motivates LLM-written specifications as a way to help more engineers use TLA+ methods.Source: §1 · p. 1
  • Public TLA+ benchmark specifications may overlap model training data, and CIR treats lower scores on renamed tasks as evidence of memorization.The paper calls this procedure consistent identifier renaming because each identifier receives one new name throughout the task.Source: §1 · p. 1
  • The study tests CIR on TLA+ because TLC can verify whether renamed tasks preserve the original behaviors and can grade outputs by behavior.CIR gives each identifier one new name wherever it appears.Source: §1 · p. 1
  • The Barrier figure shows renamed task parts alongside a checker configuration, while the description omits both required names.This illustrates how a name-based check can penalize outputs for names the model was not given.Source: §1 · p. 1, Figure 1 · p. 2
  • The paper identifies memorization, grading that requires unstated names, and unfamiliar-name difficulty as three possible causes of lower scores after renaming.Its experiments compare name-based and behavior-based grades and use controlled fine-tuning to separate exposure from renaming effects.Source: §1 · p. 2

2 Background and Related Work

The background explains how TLA+ specifications describe system behaviors and how SANY and TLC check them. Related work covers formal-artifact benchmarks, contamination tests, and task perturbations, including identifier renaming.

2 Background and Related Work

  • A TLA+ specification defines variables, starting states, permitted state changes, and properties; TLC explores reachable states and checks invariants and temporal properties.TLC can also check refinement by comparing the behaviors of a generated specification with those of a reference.Source: §2 · p. 2
  • TLC identifies constants and properties by the names in a configuration file, and TLA+-Bench requires outputs to use the exact configured names.The task description is shown to the model, but the human-written reference module is not.Source: §2 · p. 2
  • TLA+ authors often choose identifiers tied to domain concepts, which can help human readers connect formal specifications to natural-language descriptions.The passage illustrates this with the names door, radiation, and DoorSafety in Läufer’s Microwave specification.Source: §2 · p. 2
  • Prior TLA+ benchmarks use model checking and related checks, while TLA+-Bench adds LLM-written descriptions to model-checked and parse-only specifications (Cheng et al., 2026; Bisharat et al., 2026a,b).Interface names raise TLA+-Bench correctness up to 11-fold (Bisharat et al., 2026b).Source: §2 · pp. 2–3
  • Prior contamination studies search training data or control exposure, while perturbation studies rename identifiers or otherwise change tasks while aiming to preserve meaning (Jiang et al., 2024).The cited work notes that counterfactual variants may simply be harder, leaving the source of score decreases unclear when training exposure is unknown (De Koning et al., 2026; Li, 2026; Yang et al., 2026).Source: §2 · p. 3

3 Methods

The methods compare original and consistently renamed TLA+ tasks using name-based and behavior-based grading. Three experiments test frontier-model performance, controlled task exposure, and whether grading by behavior changes the measured renaming cost.

3 Methods

  • The test set contains 111 tasks whose renamed references pass SANY and TLC, and the three experiments compare model outputs across original and renamed conditions.The test set and experiments are organized with their models, grades, and controls in Figure 2.Source: §3 · p. 3, Figure 2 · p. 4
  • CIR replaces author-defined names consistently, while description rewriting preserves lowercase words and module names and renames other identifiers by fixed rules.The rules avoid changing unrelated words that happen to be identifiers; 78 of 111 tasks have at least one configuration-listed name absent from the description.Source: §3 · pp. 3–4
  • Name-based grading requires an output to parse and pass TLC with its condition’s configuration, whereas behavior-based grading requires forward and reverse refinement checks without requiring configuration names.The behavior-based grade covers tasks whose references pass the grader’s self-check; disagreements are also reviewed and an upper-bound error analysis is reported.Source: §3 · pp. 4–6
  • Pass rates are measured over five samples per task, with condition differences summarized using task-level bootstrap confidence intervals and sign tests.The analysis also tests equivalence between renamings using a five-point margin and a 90% bootstrap interval.Source: §3 · p. 5
  • Experiment 1 tests Claude Opus 4.8 and GPT-5 with controls for hidden required names, meaningful renamings, and file continuation.Both models receive the same prompt and produce five independent samples per task and condition.Source: §3 · p. 5
  • Experiment 2 fine-tunes Qwen and Gemma on disjoint task halves to compare seen and unseen tasks, while likelihood analysis measures exposure gains and their change under renaming.Experiment 3 regrades Experiment 1 outputs by behavior; the difference-in-differences compares renaming’s effect on seen versus unseen tasks.Source: §3 · pp. 5–6

4 Results and Discussion

Identifier renaming lowers correctness under TLA+-Bench grading, but much of the drop reflects required names absent from task descriptions. Behavior-based grading and controlled exposure show that renaming also imposes a cost on unseen tasks, while a single score decrease cannot isolate memorization.

Experiment 1: Name-Based Grading

  • 28.3% to 18.2%: Claude Opus 4.8’s name-based correctness fell 10.1 points, mostly on tasks with hidden required names.On 78 hidden-name tasks, correctness fell from 11.3% to 0.0%; on 33 tasks stating every required name, the 7.3-point decrease had a confidence interval including 0.Source: §4 · pp. 6–7

Experiment 2: Controlled Exposure

  • 4.9 points: Qwen’s correctness fell on unseen tasks under behavior-based grading; Gemma’s 1.3-point decrease had a confidence interval including 0.Renaming removed about half of the training-related likelihood gain in both model families; the likelihood difference-in-differences was 0.16 for Qwen and 0.15 for Gemma.Source: §4 · p. 7, Table 2 · p. 7
  • Known exposure separates memory from name cost: renaming reduced the likelihood gain on seen tasks, while the Qwen unseen-task correctness decrease cannot come from task memory.The correctness difference-in-differences interval includes 0 under behavior-based grading for both families.Source: §4 · p. 7

Experiment 3: Behavior-Based Grading

  • 10.4 to 3.1 points: Opus 4.8’s correctness decrease shrank under behavior-based grading, while GPT-5’s fell from 2.4 points to 0.0 points.For Opus 4.8, the behavior-based interval still reaches 7.3 points, leaving room for a cost of new names.Source: §4 · pp. 7–8

Discussion

  • Reference-configuration grading checks names as well as behavior, and 78 of 111 tasks omit a required name from the description.Listing every required name can reveal which invariants and properties to write, removing part of the task; name-based checks can also accept outputs with weaker invariants.Source: §4 · p. 8
  • For contamination studies, one renaming decrease combines memory and the cost of new names, so known-exposure evaluations can report seen and unseen items separately.The authors also suggest behavior-based grading, reporting hidden-name tasks separately when grading depends on names, counting semantic errors as parse failures, and re-verifying renamed copies.Source: §4 · p. 8

5 Conclusion

The conclusion is that a lower score after identifier renaming does not by itself demonstrate memorization. The experiments attribute decreases to memorization, name-based grading, and the cost of working with new names.

5 Conclusion

  • Across 111 model-checked TLA+ specifications, renamed copies preserved the original behaviors, but the score decrease mixed memorization, name-based grading, and new-name costs.Under TLA+-Bench grading, Opus 4.8 fell from 28.3% to 18.2%, mostly because descriptions omit required configuration names; behavior-based decreases were 3.1 points for Opus 4.8 and 0.0 for GPT-5.Source: §5 · p. 8

Limitations

The study’s conclusions are bounded by its descriptions, operational definitions, benchmark, and sample size. The exposure results also come from one split and seed per model.

Internal validity

  • The descriptions retain known algorithm names, and the exposure models share original-name training data, so unseen tasks still reflect learned naming conventions.The authors describe the risk from algorithm names as small and say a direct test using only an algorithm name needs further study.Source: Limitations · pp. 8–9

Construct validity

  • Correctness is measured on finite instances, while the behavior-based grade imposes structural requirements and checks only the output’s safety formula in reverse.The grade can reject behavior-matching outputs that split variables or derive declared constants, and it can accept extra fairness conditions.Source: Limitations · p. 9

External and statistical validity

  • The study covers one benchmark of mostly single-module specifications, and the unseen-task renaming cost differs between Qwen and Gemma.The authors note that the cost may differ for frontier models; small samples and pass rates leave decreases of a few points within the intervals.Source: Limitations · p. 9

Statistical conclusion validity

  • Each exposure model is trained once with one task split and one seed, and the bootstrap does not capture variation between training runs.The authors also report several comparisons without correction for multiple tests.Source: Limitations · p. 9

Ethical Considerations

The paper reports its data and model-query practices, specifies the requested TLA+ outputs and checked properties, and describes identifier and fine-tuning procedures.

Ethical Considerations

  • The study uses specifications from redistributable public repositories, includes no human participants or personal data, and queries commercial APIs under provider terms.Source: Ethical Considerations · p. 9

A Prompt

  • Frontier models are prompted to produce a complete TLA+ module that passes SANY and includes the described invariants, temporal properties, and fairness conditions.The prompt supplies the natural-language system description and requests only the specification as output.Source: A Prompt · p. 13

B Properties That TLC Checks

  • TLC checks invariants over reachable states and temporal properties over whole behaviors; liveness claims may require a fairness condition.The clock example contrasts the invariant that its hour stays within 1–12 with eventual display of 12.Source: B Properties That TLC Checks · p. 13

C Identifier Kinds

  • Identifiers are split into component words, and an identifier counts as a domain word only when every component is an English dictionary word.The examples split FinishUpdate into Finish and Update, and max_val into max and val.Source: C Identifier Kinds · p. 13

E Fine-Tuning Settings

  • Qwen fine-tuning uses LoRA, freezing the 14B base weights while training low-rank updates; each task in a model’s half is seen three times.Training runs for three epochs with batch size 1, and loss is computed only on specification tokens.Source: E Fine-Tuning Settings · p. 13

F Gemma 4 Exposure Experiment

The appendix describes Gemma’s task-pair exposure setup, identifier renaming and grading procedures, and validation checks for the behavior-based grader.

F Gemma 4 Exposure Experiment

G Renaming Details

  • Renaming is reproducible with a fixed seed, keeps identifier length to preserve TLA+ formula layout, and changes a median of 11 identifiers per reference specification.The median word-by-word similarity between original and renamed specifications is 0.81.Source: G Renaming Details · pp. 13–14

H Grading Details

  • Name-based grading points configuration entries for Init, Next, and Spec to corresponding output operators, while behavior-based grading checks the output formula against the reference.Configuration constants, state constraints, and symmetry sets apply to both checks.Source: H Grading Details · p. 14

I Control-Label Variables in the Behavior-Based Grade

  • For variables used as control labels, the grader tries one-to-one mappings between string values and otherwise compares projected data-variable state graphs.The graphs must accept the same sequences of observable states.Source: I Control-Label Variables in the… · p. 14

J Validation of the Behavior-Based Grade

  • The behavior-based grade covers 90 of 111 tasks; its controls reject mutants selected because TLC reports a different number of reachable states.The validation excludes tasks without repeatable TLC results or comparable system behavior; the authors note that this selection makes rejection the easier direction and leaves false-negative rates for structurally different outputs uncertain.Source: J Validation of the Behavior-Based Grade · p. 15
  • The grader accepts all 56 valid operator-renamed copies, accepts all 90 renamed references with their renamed imported modules, and rejects all 105 kept mutants.It accepts 90 of 102 eligible references against themselves; the mutants come from 54 task references.Source: J Validation of the Behavior-Based Grade · p. 15

L File Continuation

The continuation and known-name analyses do not show that file overlap or recognizable algorithm names predict the correctness decrease after renaming. Truncation is slightly more frequent after renaming, but the correctness evidence remains weak on tasks without truncated outputs.

L File Continuation

  • 46/111 original specifications and 25 renamed copies had a shared run of at least 50 tokens, but run length did not predict correctness loss (permutation p = 0.70).The original-minus-renamed run correlation with correctness decrease was 0.07 (permutation p = 0.48); the continuation test therefore did not predict which tasks lost correctness.Source: L File Continuation · p. 15

M Known Algorithm Names

  • Under behavior-based grading, known-name tasks had a 1.2-point renaming decrease versus 4.1 points for other tasks (permutation p = 0.59); GPT-5 showed no difference.Marked tasks were more complex, so the comparison cannot rule out a small effect of names.Source: M Known Algorithm Names · p. 16

N Truncation

  • Renamed outputs were slightly more often truncated (18.7% and 16.9%) than original outputs (16.9% and 13.5%), but the renaming cost persisted on 43/90 tasks without truncation.On those tasks, the unseen-task renaming cost was 9.8 points (95% CI 3.7 to 16.3); the difference-in-differences was 7.4 points (95% CI 0.0 to 15.3), with an interval reaching 0.Source: N Truncation · p. 16

O Specification-Only Exposure

Specification-only exposure reduced likelihood-based evidence of a renaming cost on correctness, while the two grading methods sometimes disagreed. Random and meaningful names performed similarly under name-based grading, but their behavior-based comparison was inconclusive.

O Specification-Only Exposure

  • On unseen tasks, specification-only exposure produced a 0.4-point renaming cost on correctness (95% CI −3.6 to 4.4), while the likelihood difference-in-differences was 0.08 (95% CI 0.07 to 0.10).All three correctness effects had intervals including 0, and correctness ranged from 11.6% to 14.2%, leaving little room to measure a decrease.Source: O Specification-Only Exposure · pp. 16–17

P Disagreements Between the Two Grades

  • The grades disagreed in both directions: among Opus 4.8 samples, 47 original and 71 renamed outputs passed only behavior grading, while 17 and 8 passed only name grading.Some name-only passes had different behavior; others reflected limits of behavior grading. Counting every name-only pass as correct reduced the Opus 4.8 decrease to 5.1 points and the GPT-5 decrease to 0.4 points.Source: P Disagreements Between the Two Grades · p. 17

R Meaningful Names

  • For Opus 4.8 under name-based grading, random and meaningful renamings yielded 19.7% and 20.0% correctness, a difference of −0.3 points (95% CI −2.3 to 1.6).Under behavior-based grading, meaningful renaming yielded 37.7% versus 39.0% with random renaming, a 1.3-point difference whose interval exceeded the 5-point equivalence margin, making the comparison inconclusive.Source: R Meaningful Names · p. 17

S Additional Results of Experiment 1

Additional Experiment 1 results show that the correctness decrease appears across sample positions, while text-similarity metrics also decline under renaming.

S Additional Results of Experiment 1

  • The correctness decrease for Opus 4.8 appeared when each of the five sample positions was analyzed separately.On 100 tasks, first-sample correctness was 27% for Opus 4.8 and 10% for GPT-5; TLA+-Bench reported 16% for Opus 4.5 and 4% for GPT-5 on the same tasks, but with different prompts and generation settings, so rates are not directly comparable.Source: S Additional Results of Experiment 1 · p. 17
  • BLEU-4 and ROUGE-L decreased between 2.6 and 5.4 points under renaming, while outputs stayed close to the reference text.The passage does not specify separate values for the two metrics.Source: S Additional Results of Experiment 1 · p. 17

T Additional Results of Experiment 2

On tokens belonging to renamed identifiers alone, the exposure effect on Qwen-model likelihood was estimated at zero.

T Additional Results of Experiment 2

U Additional Results of Experiment 3

On the 90 tasks covered by both grades, Opus 4.8 has fewer failures after renaming under behavior-based grading than under name-based grading. The additional results also report subgroup scores and describe text-similarity and exposure comparisons.

U Additional Results of Experiment 3

  • For 64 tasks with a hidden required name, Opus 4.8 scores 12.5% and 0.0% under name-based grading versus 22.8% and 20.3% under behavior-based grading, a 2.5-point difference (95% CI −1.9 to 7.2).Source: U Additional Results of Experiment 3 · p. 17

V Text Similarity

  • Table O.1 contrasts task-pair and specification-only exposure on 90 behavior-grade tasks; Figure T.1 tracks randomized exposure for two split-trained Qwen models.Source: Table O.1 · p. 18, Figure T.1 · p. 19
  • Text-similarity analysis compares comment-stripped outputs with same-condition references using BLEU-4 and ROUGE-L; Table Q.1 asks whether four benchmarks require unstated names.Table V.1 reports similarity in percent, averaged over samples and then tasks.Source: V Text Similarity · p. 18, Table Q.1 · p. 18, Table V.1 · p. 19
  • Figure U.1 compares frontier-model renaming decreases under name-based and behavior-based grading, with 95% confidence intervals; Figure S.1 splits name-grade results by whether a required name is hidden.Source: Figure S.1 · p. 18, Figure U.1 · p. 19
Loading 2610.29767v1…