On the Effectiveness of Large Language Models in Writing Alloy Formulas

📄 arXiv: 2502.15441v1 📥 PDF

作者: Yang Hong, Shan Jiang, Yulei Fu, Sarfraz Khurshid

分类: cs.SE, cs.AI, cs.FL, cs.PL

发布日期: 2025-02-21

💡 一句话要点

利用大型语言模型自动生成Alloy公式，提升软件规约编写效率

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 Alloy 形式化规约 软件工程 自动代码生成

📋 核心要点

  1. 编写正确的软件规约仍然极具挑战性，现有方法难以保证规约的准确性和完整性。
  2. 利用大型语言模型理解自然语言描述，并自动生成、转换和补全Alloy公式，从而降低编写规约的难度。
  3. 实验表明，LLMs能够有效地合成完整的Alloy公式，生成等价公式，并补全公式草图，无需测试用例。

📝 摘要（中文）

本文研究了大型语言模型（LLMs）在编写Alloy语言声明式规约方面的有效性。研究包含三个方面：一是利用LLMs从自然语言描述（英语）生成完整的Alloy公式；二是利用LLMs根据给定的Alloy公式创建等价的替代公式；三是利用LLMs完成Alloy公式的草图，通过合成Alloy表达式和操作符来填充草图中的空缺，使完成的公式准确地表示所需的属性（以自然语言给出）。我们使用11个经过充分研究的规约作为实验对象，并采用ChatGPT和DeepSeek两个流行的LLMs进行实验评估。实验结果表明，LLMs在从自然语言或Alloy给出的输入属性中合成完整的Alloy公式方面表现良好，并且能够枚举多个独特的解决方案。此外，LLMs还成功地完成了给定Alloy公式草图，并满足所需属性的自然语言描述（无需测试用例）。我们相信LLMs为编写规约提供了一个非常令人兴奋的进步，可以帮助规约在软件开发中发挥关键作用，并提高我们构建健壮软件的能力。

🔬 方法详解

问题定义：论文旨在解决软件开发中编写形式化规约困难的问题。现有方法需要人工编写，容易出错且效率低下，难以保证规约的正确性和完整性。Alloy作为一种形式化规约语言，虽然表达能力强，但编写难度较高，阻碍了其在工业界的广泛应用。

核心思路：论文的核心思路是利用大型语言模型（LLMs）强大的自然语言理解和代码生成能力，自动生成、转换和补全Alloy公式。通过将自然语言描述的需求转化为Alloy代码，降低编写规约的门槛，提高开发效率和规约质量。

技术框架：论文主要包含三个方面的研究：1) 从自然语言生成完整的Alloy公式；2) 生成等价的Alloy公式；3) 补全Alloy公式草图。整体流程是：首先，将自然语言描述的需求或已有的Alloy公式作为输入；然后，利用LLMs进行处理，生成或补全Alloy公式；最后，对生成的公式进行验证，评估其正确性和有效性。

关键创新：论文的关键创新在于将大型语言模型应用于形式化规约的自动生成和转换。与传统方法相比，该方法无需人工编写大量代码，而是通过自然语言交互，即可快速生成满足需求的Alloy公式。此外，该方法还能够生成等价的Alloy公式，为规约的优化和验证提供了新的思路。

关键设计：论文使用了ChatGPT和DeepSeek两个流行的LLMs。实验中，作者设计了11个well-studied的Alloy规约作为测试用例，并评估了LLMs在不同任务上的性能，包括公式生成、公式转换和公式补全。具体的参数设置和损失函数等技术细节在论文中没有详细描述，属于LLM本身的设计。

🖼️ 关键图片

fig_0
fig_1

📊 实验亮点

实验结果表明，LLMs在合成完整的Alloy公式、生成等价公式和补全公式草图方面表现良好。LLMs能够生成多个独特的解决方案，并且在补全公式草图时无需测试用例。这些结果表明LLMs在自动生成形式化规约方面具有巨大的潜力。

🎯 应用场景

该研究成果可应用于软件工程领域，特别是形式化方法和模型驱动开发。通过自动生成和转换Alloy公式，可以降低软件规约编写的难度，提高开发效率和软件质量。未来，该技术有望集成到软件开发工具链中，帮助开发人员更轻松地编写和验证软件规约，从而构建更可靠的软件系统。

📄 摘要（原文）

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.