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

cs.CLOct 21, 2026

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

Authors: Arslan Bisharat, Mujtaba Nazari, Khushboo Bhadauria, Brian Ortiz, Eric Spencer, Beatriz Santos, TaiNing Wang, George K. Thiruvathukal,

Organizations: Loyola University Chicago

Abstract

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.

Figures & tables

Panel of Figure 1 — Figure 1: The Barrier task as the model receives it, with the configuration that checks the output. Renamed parts are shaded, and the description states neither required name.

Panel of Figure 2 — Figure 2: The test set (top) and the three experiments (bottom), each with its models, grade and controls.

Claude Opus 4.8
Measure	Original	Random	Meaningful
Parse (SANY)	80.4	81.6	81.0
Correct, name	28.3	18.2	20.0
Correct, behavior	38.4	35.3	37.7
GPT-5
Parse (SANY)	66.1	70.5	69.1

Table 1: Frontier models on the test set, in percent. Meaningful names use the 77 tasks with a valid meaningful renaming, and the behavior-based rows use the 90 that the grade covers.

Qwen2.5-Coder-14B
Measure	Exposure	DiD	Unseen cost
Correct, behavior	7.6 [3.8, 12.0]	3.3 [ $-$ 0.2, 7.3]	4.9 [2.0, 8.4]
Correct, name	5.6 [2.2, 9.6]	3.5 [0.4, 6.9]	4.4 [1.5, 7.6]
Likelihood	0.34 [0.30, 0.39]	0.16 [0.13, 0.19]	–
Likelihood, other	0.31 [0.27, 0.35]	0.07 [0.06, 0.09]	–
Gemma 4 31B

Table 2: Effects of task-pair exposure for two model families with 95% CIs, in percentage points for correctness and in mean token log-likelihood for likelihood. Unseen cost is original minus renamed on unseen tasks, and other uses only tokens outside renamed identifiers.

Appendix figures & tables11 assets

Supplementary material from the paper’s appendix.

Appendix

Kind	Example	Renamed	Hidden
Domain words	BarrierProperty	599 (34%)	148 (44%)
Conventions	TypeOK	415 (23%)	77 (23%)
Abbreviations	hr	774 (43%)	108 (32%)
Total		1,788	333

Appendix

Table C.1: Identifier kinds in the 111 test tasks, over renamed and hidden required names.

Panel of Figure 6 — Figure D.1: The HourClock specification (left) and its renamed copy (right). Every author-defined identifier (shaded) changes. Keywords and the standard module Naturals stay the same. The renamed copy passes SANY and TLC with the renamed configuration.

Measure	Behavior grade	Name grade
Tasks	90	110
Original, seen / unseen	22.0 / 14.0	19.5 / 11.6
Renamed, seen / unseen	17.1 / 12.7	9.5 / 7.5
Exposure effect	8.0 [3.6, 12.9]	7.8 [3.6, 12.4]
DiD	3.6 [ $-$ 0.9, 8.2]	5.8 [1.5, 10.5]
Unseen cost	1.3 [ $-$ 2.0, 4.9]	4.2 [0.4, 8.5]

Appendix

Table F.1: Gemma 4 31B under task-pair exposure, in percent and percentage points with 95% CIs.

Control	$n$	Passed
Reference against itself	102	90
Operator-renamed reference	56	56
Renamed reference and modules	90	90
Mutant with other reachable states	105	0

Appendix

Table J.1: Validation of the behavior-based grade on the 102 eligible tasks. A positive control should pass and a negative control should fail.

Set	$n$	Used for
TLA + -Bench system specifications	146	starting pool
Pass SANY and TLC after CIR (test set)	111	Experiment 1
With a TLC configuration	110	Experiment 2, name-based grading
No test fixtures or random values	102	grader validation
Reference passes behavior-based grading	90	Experiments 2 and 3, behavior-based grading
With a valid meaningful renaming	77	meaningful-name control

Appendix

Table K.1: Task counts. Indented rows are subsets of the row above, and the last two rows split the test set. The last column gives what each set is used for.

Measure	Task-pair exposure	Specification-only exposure
Exposure effect, original descriptions	7.6 [3.8, 12.0]	2.7 [ $-$ 0.2, 5.8]
Exposure effect, renamed descriptions	4.2 [1.1, 7.8]	0.0 [ $-$ 3.1, 3.3]
Difference in differences	3.3 [ $-$ 0.2, 7.3]	2.7 [ $-$ 1.8, 7.3]
Renaming cost, unseen tasks	4.9 [2.0, 8.4]	0.4 [ $-$ 3.6, 4.4]
Log-likelihood, difference in differences	0.16 [0.13, 0.19]	0.08 [0.07, 0.10]
Log-likelihood, tokens outside renamed identifiers	0.07 [0.06, 0.09]	0.04 [0.03, 0.05]

Appendix

Table O.1: Task-pair and specification-only exposure on the 90 tasks the behavior-based grade covers. Task-pair models saw each specification with its test description, three times. Specification-only models saw the raw .tla file, three times. Effects are in percentage points with 95% bootstrap CIs, except the log-likelihood row, which uses the mean token log-likelihood of the reference. The last row counts the tasks for which the seen model assigns the higher likelihood to the reference.

Benchmark and task	Check	Hidden name
TLA + -Bench Bisharat et al. (2026b) , description to specification	SANY and TLC with the reference configuration	78/111
SysMoBench Cheng et al. (2026) , code to system model	SANY, TLC, trace validation and invariant templates, with names mapped by an LLM	no
TLAPS-Bench The tlaps-bench Authors (2026) , theorem to proof	TLAPS on the stated theorem	no
TLAi+Bench Kuppe (2025) , puzzle to specification	TLC counterexample and a refinement mapping to the gold specification	no

Appendix

Table Q.1: Whether four TLA + benchmarks need a name that the task does not state.

Figure S.1: Frontier models under the name-based grade, five samples per task, split by whether a required name is hidden.

Figure T.1: Randomized exposure on the 90 tasks the behavior-based grade covers, with two Qwen2.5-Coder-14B models trained on disjoint halves. (a) Behavior-based pass rate. (b) Effects with 95% CIs over tasks.

Figure U.1: Frontier models on the 90 tasks the behavior-based grade covers, graded by name and by behavior. Each decrease is original minus renamed with a 95% CI.

Claude Opus 4.8
Measure	Original	Random	Meaningful
BLEU-4	47.3	41.9	44.3
ROUGE-L	60.0	56.9	58.6
GPT-5
BLEU-4	36.1	32.1	33.9
ROUGE-L	51.0	48.4	49.9

Appendix

Table V.1: Text similarity of frontier outputs to the reference of their condition, after comments are removed, in percent, averaged over samples and then tasks.

Memorization in Language Models

Memorization in language models studies how training examples and facts are stored, recalled, generalized, and exposed by model parameters.

See all 115 papers

TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation
Jul 26, 2026Arslan Bisharat, Eric Spencer, Brian Ortiz +8LLM Evaluation Formal Verification
Loyola University Chicago Chicago, Illinois, USA
Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation
Jun 4, 2026Arslan Bisharat, Brian Ortiz, Eric Spencer +5LLM Evaluation Formal Verification
Department of Computer Science, Loyola University Chicago, Chicago, IL 60660, USA
TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
Jun 4, 2026Eric Spencer, Arslan Bisharat, Brian Ortiz +6LLM-Based Program Synthesis Formal Verification
Department of Computer Science, Loyola University Chicago, Chicago, IL 60660, USA

Jul 26, 2026J/K move · Enter open · S save

TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation

Arslan Bisharat, Eric Spencer, Brian Ortiz, Khushboo Bhadauria+7

Loyola University Chicago Chicago, Illinois, USA

LLM Evaluation Formal Verification Autoformalization

Open paper AskPDF arXiv

Large language models increasingly write TLA

^{+}

formal specifications from natural-language descriptions, but progress is hard to measure: existing resources grade by resemblance to a reference or by whether the output parses, neither of which shows correctness. We present TLA

^{+}

-Bench, a dataset and benchmark that grades by execution. Every gold specification ships a configuration the TLA

^{+}

model checker runs over the full reachable state space, deciding exactly whether the specification holds the properties that configuration names. The dataset holds 403 model-checked gold and 897 parse-only silver specifications from 13 public repositories, subsumes prior TLA

^{+}

generation data, and carries four model-written descriptions in two styles from two providers, with difficulty and category labels. Our main finding is about measurement itself: an exact oracle gives not one correctness number but a range. Varying only the grading choices earlier benchmarks leave unstated, on one fixed set of model outputs, the correct rate moves sixfold, from 10.0% to 1.7%; adding the interface-supply choice, where the model is told the configuration's names, widens the range to elevenfold, from 18.7% to 1.7%. We call this range the correctness envelope and measure each of its bounds. The findings inside it are stable. Every model writes valid TLA

^{+}

far more often than correct TLA

^{+}

: the strongest is correct 16% of the time by default and 26% when given the interface names, open models at most 1%, and correctness falls sharply with difficulty.

Abstract

Memorization in Language Models

Explore similar work

TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation

Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation

TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation