Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation

这篇论文把自然语言到 TLA+ 的生成结果交给 SANY parser 和 TLC model checker，而不是只看表面格式。作者在 205 个规格数据集上评估 30 个模型：25 个开源模型四种 prompting 共 2,600 次，5 个闭源模型 few-shot 共 130 次。最高 syntactic correctness 26.6%、semantic correctness 8.6%，并且成功只出现在 progressive prompting，这对形式化规格自动生成是一个很硬的基线。