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.29767

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

View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.CL cs.SE

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Arslan Bisharat, Mujtaba Nazari, Khushboo Bhadauria, Brian Ortiz, Eric Spencer, Beatriz Santos, TaiNing Wang, George K. Thiruvathukal, Konstantin Laufer, Mohammed Abuhamad. 2026-10-21. ALIAS: Evaluating Performance and Memorization in LLM-Written TLA+ Specifications. https://arxiv.org/abs/2610.29767

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

AnnoCaseLaw: Legal Annotation Benchmark of Civil Negligence

Language models offer a way to scale costly, labour-intensive expert annotation, but their ability to reproduce expert judgements remains uncertain. This is particularly challenging in law, where annotators must distinguish the reasoning supporting judicial decisions from other legally relevant discussion. We present AnnoCaseLaw as a densely annotated benchmark comprising $471$ U.S. civil-negligence court opinions with more than $12,000$ expert highlights across five annotation categories. We evaluate proprietary frontier, open-weight, legal-specialised, and decision models on their ability to reproduce these annotations. Models perform better on Facts and Outcome than on Application of Law to Facts, Procedural History, and Relevant Precedents. On Application of Law to Facts, proprietary frontier models achieve the strongest balance of reasoning coverage and precision, while the open-weight model Gemma 4 achieves comparable Macro-F1 to proprietary frontier models at a fraction of the estimated inference cost. Our findings highlight the importance of evaluating annotation coverage and cost alongside aggregate scores when assessing the feasibility of automated legal annotation.

cs.CL↗

arXiv2026

Neither Stochastic Parroting nor AGI: LLMs Solve Tasks through Context-Directed Extrapolation from Training Data Priors

This position paper argues that many behaviours framed as either "stochastic parroting" or "advanced reasoning" are better explained as context-directed extrapolation from training-data priors, and that ML and NLP research communities would benefit from evaluations that distinguish remembering and basic extrapolation from genuine application-level generalisation. Our central contribution is an actionable evaluation checklist and design patterns that make these distinctions testable in practice. Our framework posits that LLMs extrapolate from training data priors while using context to guide the model to the appropriate priors; we call this "context-directed extrapolation." Specifically, this context direction is achieved through examples in base models, leading to in-context learning, while instruction tuning allows analogous task specification via prompts rather than explicit examples. We argue that adopting this more realistic framework and controls for improving evaluation would better calibrate claims about LLM "reasoning," refocus research on how LLM performance interacts with training data and generalisability to out-of-domain tasks, and reduce miscalibration in deployment and policy decisions.

cs.CL↗

arXiv2026

Effects of Theory of Mind and Prosocial Beliefs on Steering Human-Aligned Behaviors of LLMs in Ultimatum Games

Large Language Models (LLMs) have shown potential in simulating human behaviors and performing theory-of-mind (ToM) reasoning, crucial for complex social interactions. We investigate ToM reasoning's role in aligning agentic behaviors with human norms in negotiation tasks, using the ultimatum game as our referenced task. We initialized LLM agents with different prosocial beliefs (Greedy, Fair, Selfless) and reasoning methods (chain of thought and ToM reasoning of varying levels), examining their decision-making processes and outcomes across multiple LLMs, including reasoning models like o3-mini and DeepSeek-R1 Distilled Qwen 32B. We perform 2,700 simulations to show that ToM reasoning enhances behavioral alignment with human norms, decision-making consistency, and negotiation outcomes. Consistent with prior findings, reasoning LLMs exhibit limited capability compared to ToM-enhanced LLMs, with different game roles benefiting from different ToM orders. Agents almost always chose strategies consistent with their assigned beliefs, and doing so aligned better with human norms in nearly every role, yet Greedy and Selfless agents still fell short of their norms in outcomes. Human verification further revealed that Llama 3.3 70B produces reasoning most consistent with its actions and beliefs. Our findings advance understanding of ToM's role in human-AI interaction and cooperative decision-making. The code used for our experiments can be found at https://github.com/Stealth-py/UltimatumToM.

cs.CL↗