# An Empirical Evaluation of Pre-trained Large Language Models for Repairing Declarative Formal Specifications

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Apr 2024.

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

- [From LLMs to LLM-based Agents for Software Engineering: A Survey of Current, Challenges and Future](https://mlsanity.com/paper/2408.02479/) (2024)
- [On the Effectiveness of Large Language Models in Writing Alloy Formulas](https://mlsanity.com/paper/2502.15441/) (2025)
- [CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation](https://mlsanity.com/paper/2604.12268/) (2026)
- [SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems](https://mlsanity.com/paper/2509.23130/) (2025)
- [ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair](https://mlsanity.com/paper/2602.12058/) (2026)

## Abstract (arXiv)

Automatic Program Repair (APR) has garnered significant attention as a practical research domain focused on automatically fixing bugs in programs. While existing APR techniques primarily target imperative programming languages like C and Java, there is a growing need for effective solutions applicable to declarative software specification languages. This paper systematically investigates the capacity of Large Language Models (LLMs) to repair declarative specifications in Alloy, a declarative formal language used for software specification. We designed 12 different repair settings, encompassing single-agent and dual-agent paradigms, utilizing various LLMs. These configurations also incorporate different levels of feedback, including an auto-prompting mechanism for generating prompts autonomously using LLMs. Our study reveals that dual-agent with auto-prompting setup outperforms the other settings, albeit with a marginal increase in the number of iterations and token usage. This dual-agent setup demonstrated superior effectiveness compared to state-of-the-art Alloy APR techniques when evaluated on a comprehensive set of benchmarks. This work is the first to empirically evaluate LLM capabilities to repair declarative specifications, while taking into account recent trending LLM concepts such as LLM-based agents, feedback, auto-prompting, and tools, thus paving the way for future agent-based techniques in software engineering.