TLA+-Bench：以执行结果为依据评测自然语言到TLA+规范生成

TLA+-Bench用TLA+模型检查器遍历完整可达状态空间，评测自然语言生成规范是否真正满足配置声明的性质。数据集包含403个模型检查金标准和897个仅通过解析的银标准，覆盖13个公共仓库。研究显示，评测设定会将正确率从1.7%放大到10.0%，提供接口名称后上限可达18.7%；最强模型默认正确率仅16%。