标题： 大型语言模型在编写合金公式中的有效性 显示英文标题

标题： On the Effectiveness of Large Language Models in Writing Alloy Formulas

摘要： 声明性规范在开发安全和可靠的软件系统中起着至关重要的作用。然而，正确编写规范仍然是一个特别具有挑战性的问题。本文介绍了一个控制实验，研究使用大型语言模型（LLMs）在著名的Alloy语言中编写声明性公式。我们对LLMs的使用有三个方面的应用。第一，我们利用LLMs从给定的自然语言描述（英文）中编写完整的Alloy公式。第二，我们利用LLMs根据给定的Alloy公式创建替代但等效的Alloy公式。第三，我们利用LLMs完成Alloy公式的草图，并通过合成Alloy表达式和运算符来填充草图中的空白，使得完成的公式准确地表示所需的属性（这些属性以自然语言给出）。我们使用11个广泛研究的受试规范进行实验评估，并采用两种流行的LLMs，即ChatGPT和DeepSeek。实验结果表明，LLMs在从以自然语言或Alloy形式给出的输入属性中合成完整的Alloy公式方面表现良好，并能够枚举多个唯一的解决方案。此外，LLMs在根据所需属性的自然语言描述完成给定的Alloy公式草图方面也取得了成功（无需测试用例）。我们认为，LLMs在我们编写规范的能力方面提供了一个非常令人兴奋的进展，并可以帮助使规范在软件开发中发挥关键作用，并增强我们构建健壮软件的能力。 显示英文摘要

摘要： Declarative specifications have a vital role to play in developing safe and dependable software systems. Writing specifications correctly, however, remains particularly challenging. This paper presents a controlled experiment on using large language models (LLMs) to write declarative formulas in the well-known language Alloy. Our use of LLMs is three-fold. One, we employ LLMs to write complete Alloy formulas from given natural language descriptions (in English). Two, we employ LLMs to create alternative but equivalent formulas in Alloy with respect to given Alloy formulas. Three, we employ LLMs to complete sketches of Alloy formulas and populate the holes in the sketches by synthesizing Alloy expressions and operators so that the completed formulas accurately represent the desired properties (that are given in natural language). We conduct the experimental evaluation using 11 well-studied subject specifications and employ two popular LLMs, namely ChatGPT and DeepSeek. The experimental results show that the LLMs generally perform well in synthesizing complete Alloy formulas from input properties given in natural language or in Alloy, and are able to enumerate multiple unique solutions. Moreover, the LLMs are also successful at completing given sketches of Alloy formulas with respect to natural language descriptions of desired properties (without requiring test cases). We believe LLMs offer a very exciting advance in our ability to write specifications, and can help make specifications take a pivotal role in software development and enhance our ability to build robust software.