# On the Effectiveness of Large Language Models in Writing Alloy Formulas

arXiv: https://arxiv.org/abs/2502.15441 · HTML: https://mlsanity.com/paper/2502.15441/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Builds on 22 of its 83 references that are in the map.
- First posted on arXiv 21 Feb 2025.

## Builds on (most cited first, 22 of 22)

- [A Survey of Large Language Models](https://mlsanity.com/paper/2303.18223/) (2023)
- [Agentless: Demystifying LLM-based Software Engineering Agents](https://mlsanity.com/paper/2407.01489/) (2024)
- [Using an LLM to Help With Code Understanding](https://mlsanity.com/paper/2307.08177/) (2023)
- [CodePlan: Repository-level Coding using LLMs and Planning](https://mlsanity.com/paper/2309.12499/) (2023)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Code-Aware Prompting: A study of Coverage Guided Test Generation in Regression Setting using LLM](https://mlsanity.com/paper/2402.00097/) (2024)
- [TOGA: A Neural Method for Test Oracle Generation](https://mlsanity.com/paper/2109.09262/) (2021)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [A Quantitative and Qualitative Evaluation of LLM-Based Explainable Fault Localization](https://mlsanity.com/paper/2308.05487/) (2023)
- [Make LLM a Testing Expert: Bringing Human-like Interaction to Mobile GUI Testing via Functionality-aware Decisions](https://mlsanity.com/paper/2310.15780/) (2023)
- [Ranking LLM-Generated Loop Invariants for Program Verification](https://mlsanity.com/paper/2310.09342/) (2023)
- [LILAC: Log Parsing using LLMs with Adaptive Parsing Cache](https://mlsanity.com/paper/2310.01796/) (2023)
- [LLMParser: An Exploratory Study on Using Large Language Models for Log Parsing](https://mlsanity.com/paper/2404.18001/) (2024)
- [Unprecedented Code Change Automation: The Fusion of LLMs and Transformation by Example](https://mlsanity.com/paper/2402.07138/) (2024)
- [Rocks Coding, Not Development--A Human-Centric, Experimental Evaluation of LLM-Supported SE Tasks](https://mlsanity.com/paper/2402.05650/) (2024)
- [Generating executable oracles to check conformance of client code to requirements of JDK Javadocs using LLMs](https://mlsanity.com/paper/2411.01789/) (2024)
- [Uncovering the Causes of Emotions in Software Developer Communication Using Zero-shot LLMs](https://mlsanity.com/paper/2312.09731/) (2023)
- [An Empirical Evaluation of Pre-trained Large Language Models for Repairing Declarative Formal Specifications](https://mlsanity.com/paper/2404.11050/) (2024)
- [JSKETCH: Sketching for Java](https://mlsanity.com/paper/1507.03577/) (2015)
- [CD2Alloy: Class Diagrams Analysis Using Alloy Revisited](https://mlsanity.com/paper/1409.2314/) (2014)
- [CDDiff: Semantic Differencing for Class Diagrams](https://mlsanity.com/paper/1409.2355/) (2014)
- [Automated Repair of Declarative Software Specifications in the Era of Large Language Models](https://mlsanity.com/paper/2310.12425/) (2023)

## Built on by (most cited first, 7 of 7)

- [CASCADE: LLM-Powered JavaScript Deobfuscator at Google](https://mlsanity.com/paper/2507.17691/) (2025)
- [PAT-Agent: Autoformalization for Model Checking](https://mlsanity.com/paper/2509.23675/) (2025)
- [Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair](https://mlsanity.com/paper/2605.17475/) (2026)
- [OBsmith: LLM-Powered JavaScript Obfuscator Testing](https://mlsanity.com/paper/2510.10066/) (2025)
- [Semantic Voting: Execution-Grounded Consensus for LLM Code Generation](https://mlsanity.com/paper/2605.08680/) (2026)
- [APRIL: API Synthesis with Automatic Prompt Optimization and Reinforcement Learning](https://mlsanity.com/paper/2509.25196/) (2025)
- [Sketch-and-Verify: Structured Inference-Time Scaling via Program Sketching](https://mlsanity.com/paper/2605.08658/) (2026)

## Abstract (arXiv)

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.