用大模型自动生成或补全Alloy声明式规范，提升软件验证效率。
On the Effectiveness of Large Language Models in Writing Alloy Formulas
- 大模型根据自然语言或部分公式生成完整Alloy表达式
- 在11个真实案例中成功生成多个等价解，准确率达较高水平
- 无需测试用例即可补全公式草图，适合初学者和开发者使用
声明式规范在构建安全可靠的软件系统中至关重要，但正确编写仍具挑战。本文通过控制实验研究大语言模型（LLMs）在Alloy语言中编写声明式公式的有效性。实验采用ChatGPT和DeepSeek两个主流LLM，从三个维度展开：一、根据英文自然语言描述生成完整的Alloy公式；二、基于已有Alloy公式生成语义等价的替代公式；三、根据给定的Alloy公式草图，填补空白并合成表达式与操作符，使其准确反映自然语言描述的属性。实验基于11个经典基准规范进行评估。结果表明，LLMs在从自然语言或已有公式生成完整表达式方面表现良好，能有效枚举多个唯一解；同时在无测试用例情况下成功完成公式草图。我们认为，大模型为编写规范带来显著进步，有望推动规范在软件开发中发挥核心作用，增强系统鲁棒性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。