大型语言模型在编写 Alloy 公式方面的有效性研究
软件工程
2025-07-22 v1 人工智能
形式语言与自动机理论
编程语言
摘要
声明式规范在开发安全可靠的软件系统中发挥着关键作用。然而，正确编写规范仍然具有挑战性。本文提出了一项关于使用大型语言模型（LLM）编写 Alloy 声明式公式的控制实验。我们的 LLM 用途包括三方面：其一，我们利用 LLM 根据给定的自然语言描述（英文）编写完整的 Alloy 公式；其二，我们利用 LLM 创建等价于给定 Alloy 公式的备选公式；其三，我们利用 LLM 完成 Alloy 公式的草图，并通过合成 Alloy 表达式和运算符来填充草图中的空白，使完成后的公式准确地表示给定自然语言中所述的期望属性。我们采用 11 个经典主题规范进行实验评估，并使用两款流行的 LLM，即 ChatGPT 和 DeepSeek。实验结果表明，LLM 在从输入属性（以自然语言或 Alloy 格式）合成完整 Alloy 公式方面总体表现良好，能够枚举出多个唯一解决方案。此外，LLM 也成功完成了根据自然语言描述所需属性（无需测试用例）的 Alloy 公式草图。我们认为 LLM 为我们编写规范的能力带来了非常激动人心的进展，可以帮助规范在软件开发中发挥关键作用，增强我们构建稳健软件的能力。
引用
@article{arxiv.2502.15441,
title = {On the Effectiveness of Large Language Models in Writing Alloy Formulas},
author = {Yang Hong and Shan Jiang and Yulei Fu and Sarfraz Khurshid},
journal= {arXiv preprint arXiv:2502.15441},
year = {2025}
}