摘要
本文首次系统评估了大语言模型从自然语言合成 TLA+ 规范的能力。研究在包含 205 个规范的数据集上测试了 30 个模型，结果显示语法正确率最高为 26.6%，而语义正确率仅为 8.6%。研究发现模型规模并非质量预测指标，特定小模型因推理对齐表现更佳，而代码专用模型因负迁移表现较差。研究识别出五类幻觉并归因于训练数据偏差，结论表明当前模型若无专家监督尚不可靠。
AI 推荐理由
论文评估 LLM 生成形式化规范的能力，核心在于逻辑与语义推理的准确性。
研究机构
Department of Computer Science, Loyola University Chicago, Chicago, IL 60660, USA
论文信息