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

Kongzi: A Historical Large Language Model with Fact Enhancement

Large Language Models (LLMs) can exhibit factual inaccuracies during long-chain reasoning or under misleading prompts, limiting their reliability in historical analysis. We propose Kongzi, a language model for historical understanding and reasoning that combines continued pre-training on historical corpora, supervised fine-tuning, and fact-enhanced reinforcement learning. Its factuality reward compares entities and relations extracted from generated responses with historical references through knowledge-graph similarity. We evaluate 0.5B and 7B models on historical question answering and counterfactual reasoning, using reported ratings from three LLM judges, and on CMMLU-Chinese-History. Kongzi-7B receives the highest historical-accuracy ratings among the compared models under all three judges. Reinforcement learning improves the mean answer scores of both model sizes and their CMMLU-Chinese-History accuracy, although Kongzi-7B remains below the strongest reported baselines on that benchmark. These descriptive results support further study of factuality rewards for historical language models.

cs.CL↗

arXiv2026

ShIOEnv: A Command Evaluation Environment for Grammar-Constrained Synthesis and Execution Behavior Modeling

We introduce ShIOEnv, a Gymnasium-compatible Bash environment for synthesizing execution-annotated shell input traces. Datasets containing such traces are useful for training models to perform execution-free shell simulation, which in turn is useful for deploying honeypots for cyber deception. Existing datasets, such as NL2CMD and other Bash command corpora, do not include complete execution artifacts (stdout, stderr, exit status, and changes to the system's state) associated with a command's execution. ShIOEnv synthesizes shell inputs, executes them in a controlled system context, and records stdout, stderr, exit status, and structured filesystem and environment patches. Unconstrained (random) generation of shell inputs (command and arguments) results in multiple instances of arguments that are mostly redundant or result in execution errors. We introduce grammar-constrained synthesis to generate syntactically valid arguments with high input irreducibility, which we estimate through self-ablative contrasts of execution artifacts. We prepare 1.6M samples using grammar-constrained and unconstrained synthesis and collect their execution artifacts for 86 Linux/Bash utilities. Using this dataset, we train small language models (CodeT5) and evaluate their accuracy in predicting the actual execution behavior of attacker-sourced Bash commands. These models outperform commonly used rule-based simulation (Cowrie) and prompted large language models by up to 14.2 pp in output edit similarity (O-ES). We enhance the NL2CMD dataset by constructing 500K samples executable in a grounded system context along with their complete execution artifacts. We empirically demonstrate that models trained on grammar-constrained samples outperform those trained on NL2CMD samples by 22.5 pp in O-ES. ShIOEnv, command grammars, and 2.1M samples used in our primary evaluations are released for use by other researchers.

cs.CL↗

arXiv2026

How Well Does Mathematical Reasoning Transfer Across Languages in English-Centric LLMs?

Recent advances in Reinforcement Post-Training (RPT) have substantially improved the mathematical reasoning capabilities of large language models (LLMs), but it remains unclear how well such gains transfer across languages. In this work, we study cross-lingual mathematical reasoning transfer in English-centric LLMs under controlled multilingual evaluation. We first evaluate a range of English-centric reasoning models on multilingual mathematical reasoning benchmarks and find that transfer is highly variable across initial model choice, target language, and training paradigm. Through controlled comparative experiments, we further find that stronger English-centric initialization does not necessarily lead to stronger relative transfer efficiency, even when it yields higher multilingual reasoning accuracy. Finally, we show that the largest improvement comes from moving beyond English-only supervision: adding a single parallel language yields a substantial gain, while further gains from additional languages are smaller but consistent. Overall, our results highlight the need to evaluate multilingual mathematical reasoning directly, using both absolute performance and relative transfer-efficiency metrics.

cs.CL↗