评测大模型生成TLA+规范的正确性，发现其语义正确率仅8.6%。
Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation
- 用30个大模型在205个规范上测试自然语言转TLA+，通过解析器和模型检查器验证
- 最高语法正确率达26.6%，但语义正确率仅为8.6%，仅渐进式提示有效
- 模型大小不决定质量，代码专用模型反而表现更差，适合形式化验证研究者参考
TLA+已在亚马逊、微软等公司支持工业级验证，但由自然语言编写正确TLA+规范仍需大量时间和专业知识，限制了其应用。大模型虽有潜力，但此前缺乏对其生成的TLA+规范语义正确性的系统评估。本文首次对基于大模型的自然语言到TLA+规范合成进行系统评估。研究在自建的205个规范数据集上，测试了30个大模型（8个系列），包括25个开源模型在4种提示策略下共2,600次运行，以及5个专有模型在少样本提示下130次运行，全部使用SANY解析器和TLC模型检查器验证。结果显示，最大语法正确率为26.6%，但语义正确率仅为8.6%，且成功仅出现在渐进式提示中。结果表明，模型规模无法预测质量，例如DeepSeek r1:8b在所有策略下均优于其70B版本，说明形式化语言中的推理对齐至关重要。代码专用模型表现持续较差，可能源于主流语言训练带来的负向迁移。研究识别出五类常见幻觉，均可追溯至特定训练数据偏差。结论表明，当前大模型无法在无专家监督下生成可靠的TLA+规范。论文发布评估框架、代码与数据集以支持可复现性与后续研究。
原文摘要 · Abstract (English)
TLA+ has supported industrial verification at companies such as Amazon and Microsoft, yet writing correct TLA+ specifications from natural language still requires time and expertise, which limits adoption. LLMs show promise, but no prior study measures whether they produce semantically correct TLA+ specifications from natural language. This paper presents the first systematic evaluation of LLM-based TLA+ specification synthesis from natural language. Our study evaluates 30 LLMs across eight families on a curated dataset of 205 TLA+ specifications: 25 open-weight models across four prompting strategies (2,600 runs) and 5 proprietary models under few-shot prompting (130 runs), all validated by the SANY parser and TLC model checker. LLMs achieve up to 26.6% syntactic correctness but only 8.6% semantic correctness, with successes exclusive to progressive prompting. Results show that model size does not predict quality, e.g., DeepSeek r1:8b outperforms its 70B variant across all strategies, which suggests the importance of reasoning alignment for formal languages. Code-specialized models consistently underperform due to negative transfer from mainstream language training. We identify five recurring hallucination categories, all traceable to specific training data biases. These results suggest that current LLMs do not generate reliable TLA+ specifications without expert oversight. We release the evaluation framework, code, and dataset to support reproducibility and future research.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。