A TLA+ benchmark can reject a correct LLM specification because the model didn’t guess a name the prompt never supplied.
In ALIAS, Arslan Bisharat and colleagues tested identifier renaming across 111 TLA+ tasks. Under name-based grading, Claude Opus 4.8 correctness fell from 28% to 18%. GPT-5 correctness fell from 9% to 7%.
Those decreases look like evidence of memorization. But most of the decrease came from the grading procedure. When the researchers graded the same outputs by behavior, the decrease shrank to about 3 points for Claude Opus 4.8. For GPT-5, it shrank to 0.
That distinction matters if you’re choosing a language model to write specifications. A benchmark that requires hidden names mixes the model’s ability to describe a system with its ability to reproduce an interface it never received.
The hidden name problem
TLA+ describes a system’s possible behaviors. Engineers use it to find design errors in concurrent and distributed systems before they build them.
The TLC model checker explores reachable states and checks properties. Its configuration names the properties it must check. If the configuration asks for TypeOK, the generated specification must define TypeOK.
A description can explain the required property without supplying that name.
The paper’s barrier example makes the problem concrete. The description asks for a type correctness condition and a temporal barrier property. The configuration requires TypeOK and BarrierProperty. The description supplies neither name.
After renaming, the configuration requires Octvcq and Bvwcdylhaazalut.
The model still has to express the barrier’s behavior. But name-based grading also requires those exact names. A specification can describe the right behavior and fail because its property names differ.
Familiar names give the model a chance to guess. Random names remove that chance. The resulting decrease doesn’t isolate memorization.
Renaming preserves behavior, but changes the task
Consistent identifier renaming gives each identifier a new name everywhere it appears.
Researchers use this technique to test memorization. If a model succeeds on an original task and fails after renaming, recall might explain its original success.
That interpretation depends on the renamed task having the same difficulty.
ALIAS tests that assumption with TLA+. The researchers used SANY and TLC to check the renamed reference specifications. Their test set contains the 111 tasks whose renamed reference specifications passed both checks.
But preserving behavior doesn’t establish equal difficulty for a language model.
Meaningful names connect a description to a specification. Random names can make that work harder. And hidden configuration names introduce a separate requirement that behavior alone cannot satisfy.
The paper separates these possible causes of a decrease.
- Memorization of the original task.
- Name-based grading that requires hidden names.
- The difficulty of unfamiliar random names.
A single decrease cannot tell a builder how much each cause contributed.
Known exposure changes the interpretation
The researchers also fine-tuned model copies on disjoint halves of the tasks. Each task was seen by one copy and unseen by the other.
That design gave them known training exposure. They could compare renaming on seen tasks with renaming on unseen tasks.
Renaming removed about half of the training gain in likelihood. But renaming also cost 4.9 points for Qwen on unseen tasks. For Gemma, it cost 1.3 points on unseen tasks.
The unseen results matter. They show that renaming can hurt performance without exposure to that task during the controlled fine-tuning.
The result supports a narrower reading of a renaming test. A decrease can contain evidence of memorization, but the whole decrease is not a measurement of memorization.
What I would require from a benchmark
I’d want every required interface name in the prompt. If the configuration requires a property name, the model needs that name.
I’d also want behavior-based grading alongside name-based grading. The ALIAS comparison shows why. The same model outputs support substantially different conclusions when the grade stops requiring exact names.
And I’d want a control with known training exposure before interpreting the remaining decrease as memorization.
ALIAS doesn’t establish that memorization disappears under behavior-based grading. It establishes that a renaming decrease combines causes that builders need to separate.
For a builder, the cost is a misleading model comparison. Before trusting a specification benchmark, check whether it measures system behavior or requires the model to guess a hidden name.
Top comments (0)