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

📄 arXiv: 2610.29767v1 📥 PDF

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

分类: cs.CL, cs.SE

发布日期: 2026-10-21

备注: 19 pages (8 main + appendix), 6 figures, 9 tables. Code and data: https://github.com/LUC-AI4FM/ALIAS

💡 一句话要点

提出ALIAS方法评估LLM在TLA+规范中的表现与记忆化问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 记忆化 TLA+ 一致标识符重命名 模型评估 行为评分 性能测试

📋 核心要点

  1. 现有方法在评估大型语言模型的记忆化现象时，容易受到标识符命名的影响，导致结果不准确。
  2. 论文提出了一种基于一致标识符重命名的方法，通过TLA+语言的模型检查器验证重命名任务的行为一致性。
  3. 实验结果表明，重命名显著降低了模型的正确率，但通过行为评分可以减小这一影响，提升了评估的准确性。

📝 摘要（中文）

记忆化现象会夸大大型语言模型（LLMs）的基准分数，因为模型可以重现其训练中见过的答案。研究者通过一致标识符重命名（CIR）来检测这一现象，给任务中的每个标识符一个新名称，并将重命名任务的较低分数视为记忆的证据。本文在时间逻辑动作加（TLA+）语言上测试该方法，模型检查器作为一个oracle确认重命名任务是否保留了原始任务的确切行为。在111个TLA+-Bench任务中，重命名使Claude Opus 4.8的正确率从28%降至18%，GPT-5从9%降至7%。大部分下降源于测试评分的要求，评分需要精确的名称，而大多数描述从未说明。通过行为评分，Opus 4.8的下降缩小至约3个百分点，GPT-5则为0。在两个在任务不重叠的半部分上微调的模型家族中，重命名使得训练增益的约一半消失，并在未见任务上损失了4.9个百分点（Qwen）和1.3个百分点（Gemma）。因此，重命名后的较低分数混合了记忆化、基于名称的评分和新名称的成本。

🔬 方法详解

问题定义：本文旨在解决大型语言模型在基准测试中因记忆化现象而导致的分数夸大问题。现有方法主要依赖于标识符的命名，容易受到影响，导致评估结果不准确。

核心思路：论文的核心思路是通过一致标识符重命名（CIR）来测试模型的记忆化现象，利用TLA+语言的模型检查器作为oracle，确认重命名任务是否保留了原始任务的行为。

技术框架：整体架构包括三个主要模块：1) 标识符重命名模块，负责为任务中的每个标识符生成新名称；2) 模型评估模块，通过模型检查器验证重命名任务的行为一致性；3) 结果分析模块，分析重命名对模型性能的影响。

关键创新：最重要的技术创新点在于结合了模型检查器的行为验证与重命名策略，提供了一种新的评估LLM记忆化现象的方法，与传统的基于名称的评分方法本质上不同。

关键设计：在实验中，重命名策略的设计考虑了标识符的唯一性和一致性，确保每个任务的标识符都被有效重命名。同时，评分机制采用了行为评分而非名称评分，以减少因名称不一致导致的评分偏差。

📊 实验亮点

实验结果显示，重命名导致Claude Opus 4.8的正确率从28%降至18%，GPT-5从9%降至7%。然而，通过行为评分，Opus 4.8的下降缩小至约3个百分点，GPT-5的下降则为0，表明行为评分在评估中的重要性。

🎯 应用场景

该研究的潜在应用领域包括大型语言模型的性能评估、自动化测试生成以及软件验证等。通过改进评估方法，可以更准确地理解模型的能力和局限性，从而推动更可靠的AI系统开发。未来，该方法可能影响到模型训练和评估的标准化流程。

📄 摘要（原文）

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.