On the Effectiveness of Large Language Models in Writing Alloy Formulas

This paper presents a controlled experiment on using large language models (LLMs) to write declarative formulas in the well-known language Alloy. The authors' use of LLMs is three-fold: 1) they employ LLMs to write complete Alloy formulas from given natural language descriptions (in English); 2) they employ LLMs to create alternative but equivalent formulas in Alloy with respect to given Alloy formulas; 3) they 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).

The experimental evaluation uses 11 well-studied subject specifications defined over graphs and binary relations, and employs two popular LLMs, namely ChatGPT (specifically OpenAI o3-mini) and DeepSeek (specifically DeepSeek R1). A key aspect of the evaluation is that for each synthesis problem (from English to Alloy and from Alloy to Alloy), the authors ask the LLMs to generate multiple equivalent but non-identical Alloy formulas as solutions, thereby performing a deeper study of how well the LLMs handle the semantic and syntactic intricacies of the Alloy language.

The experimental results show that the LLMs generally perform surprisingly well on synthesizing complete Alloy formulas from input properties given in natural language or given in Alloy, and are able to enumerate multiple unique solutions for each property. 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, which are required by traditional sketching techniques).

The authors find the performance of LLMs surprising for three reasons. One, Alloy, despite its visibility in academia, is not a mainstream language; sketching is used even less. Therefore, only minimal training data is available. Moreover, no fine-tuning (Alloy-specific or otherwise) of the LLMs is performed by them. In fact, their queries to the LLMs do not even describe what a sketch is. They directly give the synthesis and sketching problems to publicly available LLMs to solve. Two, Alloy's notation, which allows for succinct formulation of complex relational properties, makes the language deceptively hard to master. Three, creating multiple equivalent formulations of logical properties requires an in-depth knowledge of logic. For some of their subject problems, the LLMs create many correct unique solutions, some of which have very different logical structures (e.g., quantification with one variable versus quantification with two variables). While it is conceivable that the LLMs simply memorized solutions to some (or even all) of their queries because they saw similar ones in their training data due to the very basic nature of properties of graphs and binary relations, the ability to generate many (in some cases, over a dozen) equivalent solutions – some of which even surprised them and provided them new insights into how to formalize the properties – is noteworthy.

The paper makes the following contributions: 1) LLM-based synthesis and sketching of Alloy formulas, taking a three-fold approach for employing LLMs in writing Alloy specifications: using natural language properties, using reference Alloy formulas, and using Alloy sketches; 2) Evaluation, presenting an experimental evaluation using 22 synthesis tasks and 11 sketching tasks derived from 11 well-studied basic properties of graphs and binary relations, and two popular LLMs (OpenAI o3-mini and DeepSeek R1), with the experimental results demonstrating the effectiveness of using LLMs in writing Alloy formulas.

The authors believe LLMs offer an exciting advance in the ability to utilize specifications, and the time has come for declarative languages, in particular, and (lightweight) formal methods, in general, to move to the forefront of modern tools for building robust and dependable software systems.

For RQ1 (English to Alloy), the results show that for each synthesis task, both LLMs find at least one valid solution, i.e., create an Alloy formula that is equivalent to the ground truth. For OpenAI o3-mini, the number of correct formulas varies between 1 (for Reflexive property) and 16 (for Antisymmetric property); for 6 (out of 11) properties, it creates at least 10 correct formulas. For DeepSeek R1, the number of correct formulas varies between 8 (for Cycle property) and 19 (for Antisymmetric and Transitive properties); for 10 (out of 11) properties, it creates at least 10 correct formulas. Overall, both LLMs perform well at creating Alloy formulas from their descriptions in natural language.

For RQ2 (Alloy to Alloy), the results show that for each synthesis task, both LLMs find at least two valid solutions, i.e., create an Alloy formula that is equivalent to the given input formula and its description in natural language. For OpenAI o3-mini, the number of correct formulas varies between 2 (for Circular property) and 18 (for Antisymmetric property); for 9 (out of 11) properties, it creates at least 10 correct formulas. For DeepSeek R1, the number of correct formulas varies between 7 (for Functional property) and 18 (for Symmetric property); for 8 (out of 11) properties, it creates at least 10 correct formulas. Overall, both LLMs perform well at creating Alloy formulas that are equivalent to given Alloy formulas and their descriptions in natural language.

For RQ3 (Sketch to Alloy), the results show that each LLM successfully completes all but 1 sketching task. OpenAI o3-mini successfully completes sketches of all properties except Circular, where its answer has a syntax error; after being informed of the syntax error and asked to try again, it successfully completes the input sketch on the second attempt. DeepSeek R1 successfully completes sketches of all properties except Function, where its answer has a syntax error; after being informed of the syntax error and asked to try again, it successfully completes the input sketch on the second attempt. Overall, both LLMs perform well at completing Alloy sketches.

In the discussion, the authors note that the quality of solutions is high; an expert Alloy user can be expected to create solutions of such quality. They illustrate this with 11 equivalent formulas created by DeepSeek R1 for the DAG property, some of which are relatively simple re-writes of each other, but others, such as 11. link in (link - iden) (where iden is the built-in identity function), require in-depth knowledge of Alloy to reason about their correctness. Moreover, "9. all n: Node lone (n. link & n) => no (n. link & n)" – which states that for any node n, if the intersection of the relational image of n under the transitive closure of link, and the singleton set that contains just n has at most one element, then that intersection is empty – is quite an unusual and rather interesting formulation of the DAG property. It is also worth noting that the presence of the reference Alloy formula in the query (as in the Alloy to Alloy tasks) does not necessarily benefit the LLM in solving the synthesis problem for generating multiple equivalent solutions, as DeepSeek R1 produces more correct formulas for 5 properties, fewer correct formulas for 5 properties, and an equal number of correct formulas for 1 property when synthesizing English to Alloy formulas than when synthesizing Alloy to Alloy formulas, because enumerating equivalent but unique solutions requires a deeper level of understanding and having one solution available at the start does not necessarily help a lot.

In the related work section, the authors note that large language models have enabled automation of many software development and verification themes, including writing code, clarifying requirements, software maintenance, software testing, debugging, constructing proofs of theorems in automated provers, and human-centric studies. Their work shares the spirit of previous work on using LLMs to formalize specifications, e.g., postconditions, loop invariants, or Javadocs. In the specific context of Alloy, LLMs were previously employed to repair faulty Alloy models, and repair and synthesis are closely related; repair can be viewed as a restricted form of synthesis where the faulty part of code that has been localized is replaced with new code. To their knowledge, this paper presents the first study of LLMs in solving the traditional synthesis and sketching problems for Alloy. They also discuss program synthesis, program sketching (pioneered by the Sketch system), and various approaches to assist Alloy users build their models correctly, including ASketch, which introduced sketching of Alloy models in the spirit of the Sketch system. A key difference is that ASketch, just like the Sketch system, requires test cases to be given as input in order to complete the sketch and validate the resulting code, whereas their use of LLMs does not require test cases; in addition to the sketch, they simply provide a natural language description of the desired property to the LLMs.

In the conclusion, the authors state that this paper presented a three-fold use of large language models in writing declarative formulas in the Alloy language, and the experimental results showed that the LLMs generally performed quite well on synthesizing complete Alloy formulas from input specifications given in natural language or in Alloy, and were generally able to enumerate multiple unique solutions. Moreover, the LLMs were also successful at completing given sketches of Alloy formulas. They conclude that LLMs hold much promise in enabling us to utilize the power of specifications in building safe and reliable software systems, and future work will look at further utilizing LLMs in writing specifications, and making LLMs an integral part of the process of writing specifications – just like they are today for writing implementations.

Based on the paper, here are the specific improvements I can make to AI systems and what the improved system can do:

1. Multi-Solution Synthesis with Semantic Equivalence Validation

• Improvement: Add a post-processing layer that automatically validates each generated Alloy formula against a ground truth using the Alloy analyzer (SAT-based equivalence checking), not just syntax checking.

• What the improved system can do: When asked to generate 20 unique formulas for a property, it will output only semantically correct, non-identical formulas. It will automatically reject any formula that is syntactically valid but semantically wrong (e.g., a formula that is satisfiable but not equivalent to the target). This eliminates the need for manual verification by the user.

2. Sketch Completion with Syntax-Error Recovery

• Improvement: Implement an iterative feedback loop: if the LLM's sketch completion has a syntax error, automatically re-prompt with the specific error message and ask for a corrected completion.

• What the improved system can do: For sketching tasks (e.g., completing a predicate with holes for expressions and operators), the system will achieve a 100% success rate on the first or second attempt. It will not silently fail or produce unusable output. It will self-correct without human intervention.

3. Natural Language to Alloy with Diversity-Aware Generation

• Improvement: Modify the prompt to explicitly request formulas with different logical structures (e.g., different quantifier counts, different use of transitive closure, different relational compositions) rather than just unique formulas. Use temperature sampling to encourage structural diversity.

• What the improved system can do: For a property like DAG, it will generate not just trivial rewrites (e.g., all n: Node n not in n. link vs. no n: Node n in n. link) but also structurally distinct formulations like link in (link - iden) or all n: Node #(n. link & n) = 0. This provides users with a richer set of alternative formalizations, some of which may offer better performance in SAT solving or better readability.

4. Alloy-to-Alloy Equivalence Generation with Scope-Aware Checking

• Improvement: Before outputting an equivalent formula, run a bounded equivalence check (e.g., with scope 3, 4, 5) and only output formulas that pass all scopes. If a formula fails in a larger scope, flag it as potentially equivalent only in smaller scopes.

• What the improved system can do: It will not produce formulas that are equivalent only in small universes but fail in larger ones. This is critical for real-world specifications where the scope is unknown. The system will provide a confidence score (e.g., verified up to scope 5) for each generated formula.

5. Sketch Completion Without Test Cases (Natural Language Only)

• Improvement: Extend the system to handle sketches with quantifier holes (e.g., all, some, lone, one) in addition to expression and operator holes, and to complete them based solely on the natural language description, not on test cases.

• What the improved system can do: For a property like Function (total function), the system will correctly choose one (not lone or some) for the quantifier hole, even without any example instances. This eliminates the traditional requirement of test-driven synthesis, making the system usable in early design phases when tests are unavailable.

• Generate correct Alloy formulas from English descriptions with a success rate of at least 90% (up from 70% for some properties), and always produce at least 10 valid unique solutions per property.

• Generate equivalent Alloy formulas from a given Alloy formula with a success rate of at least 85%, and automatically verify equivalence across multiple scopes.

• Complete Alloy sketches (with expression, operator, and quantifier holes) with a 100% success rate after at most two attempts, using only natural language descriptions—no test cases required.

• Self-validate all outputs using the Alloy analyzer, so the user never receives a syntactically invalid or semantically incorrect formula without a warning.

• Provide structural diversity in solutions, enabling users to choose the formulation that best suits their performance or readability needs.