.png){kind=icon}
.png){kind=icon}
Return
Automated Repair of Alloy Specifications in the Era of Large Language Models
.png){kind=icon}
PRE
AI
M
J
I
H
DOI：10.1109/tse.2026.3682711.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
The growing adoption of declarative software specification languages, coupled with their inherent difficulty in debugging, has underscored the need for effective and automated repair techniques applicable to such languages. Researchers have recently explored various methods to automatically repair declarative software specifications, such as template-based repair, feedback-driven iterative repair, and bounded exhaustive approaches. The latest developments in Large Language Models (LLMs) provide new opportunities for the automatic repair of declarative specifications. In this study, we assess the effectiveness of utilizing different LLMs to repair software specifications written in the Alloy declarative language. Unlike imperative languages, specifications in Alloy are not executed but rather translated into logical formulas and evaluated using backend constraint solvers to identify specification instances and counterexamples to assertions. Our evaluation focuses on LLMs’ ability to improve the correctness and completeness of Alloy declarative specifications through automatic repairs. We analyze the results produced by each LLM and compare them with those of leading automatic Alloy repair methods. Our study revealed that while LLMs fall short in comparison to existing techniques in many cases, they were able to successfully repair bugs that no other technique could address. Our analysis also identified errors in LLM-generated repairs, including constraint-related issues (over-constraint and under-constraint), quantifier logic errors, boolean operator misuse, binary relation mismatches, and syntax structure violations. Additionally, we observed instances of hallucinations in LLM-generated repairs and inconsistencies in their results in certain cases. Our study provides valuable insights for software practitioners, researchers, and tool builders considering LLMs for declarative specification repairs.
Keywords:
Declarative specification
automated repair
Alloy
LLMs
Journal
IF:
5.6
Papers:
2.8K
Citations:
1.1W
Organization
Cited Papers