TLDR: A new research paper investigates the effectiveness of large language models (LLMs) like ChatGPT and DeepSeek in writing declarative formulas in the Alloy language. The study explores three methods: generating Alloy formulas from natural language descriptions, creating equivalent formulas from existing ones, and completing partial formula sketches. The results demonstrate that LLMs perform surprisingly well across all tasks, generating multiple unique and correct solutions, even for a niche language like Alloy, suggesting a promising future for AI in formal software specification.
Declarative specifications are crucial for building safe and reliable software systems. However, writing these specifications correctly can be quite challenging, often requiring developers to learn new, unfamiliar notations that differ significantly from the imperative languages they use daily for coding.
A recent research paper explores how large language models (LLMs), such as ChatGPT and DeepSeek, can assist in writing these complex declarative formulas, specifically focusing on the well-known language Alloy. Alloy is a declarative language based on relational first-order logic, used for analyzing software designs and finding bugs through its SAT-based backend.
Three Ways LLMs Can Help
The researchers investigated three primary ways LLMs can be employed to write Alloy formulas:
1. Natural Language to Alloy: LLMs are used to generate complete Alloy formulas directly from natural language descriptions (English) of desired properties. For example, given a description like “No element in S is related to itself,” an LLM would produce the corresponding Alloy formula.
2. Alloy to Alloy: LLMs are tasked with creating alternative, but equivalent, Alloy formulas based on an existing Alloy formula. This tests their ability to understand the semantic intricacies of the language and generate diverse, correct expressions for the same property.
3. Sketching Alloy: This involves LLMs completing partial Alloy formulas, known as “sketches.” The LLM fills in missing expressions and operators (the “holes” in the sketch) to accurately represent a property described in natural language. This is particularly interesting because traditional sketching techniques often require test cases, which LLMs do not need in this approach.
Experimental Setup and Surprising Results
The study conducted a controlled experiment using 11 well-studied subject specifications, covering properties of graphs and binary relations. They used OpenAI o3-mini (ChatGPT) and DeepSeek R1. For the synthesis tasks (English to Alloy and Alloy to Alloy), LLMs were asked to generate 20 unique solutions for each property, providing a deep dive into their understanding of Alloy’s semantics and syntax.
The experimental results were quite surprising. Both LLMs performed remarkably well across all three tasks. They successfully synthesized complete Alloy formulas from natural language and existing Alloy formulas, often enumerating multiple unique and correct solutions. Even for the sketching tasks, where LLMs were given no prior instruction on what a “sketch” was, they successfully completed nearly all of them, sometimes even on a second attempt after being informed of a syntax error.
The researchers noted the high quality of the generated solutions, some of which were quite complex and offered new insights into formalizing properties. This performance is particularly noteworthy because Alloy is not a mainstream language, meaning minimal training data would have been available to the LLMs, and no fine-tuning was performed by the researchers.
Also Read:
- AI for Debugging: A Reality Check on Verified Bug Fixes
- Large Language Models: A New Frontier for User Story Creation and Quality Assurance
Implications for Software Development
This research suggests that LLMs offer a significant advancement in our ability to write declarative specifications. By potentially reducing the learning curve associated with languages like Alloy, LLMs could help formal methods play a more central role in software development, leading to more robust and dependable software systems.
For more details, you can read the full research paper here.
