# Automated Repair of Declarative Software Specifications in the Era of Large Language Models

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 22 of its 88 references that are in the map.
- First posted on arXiv 19 Oct 2023.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer](https://mlsanity.com/paper/1910.10683/) (2019)
- [RoBERTa: A Robustly Optimized BERT Pretraining Approach](https://mlsanity.com/paper/1907.11692/) (2019)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [BART: Denoising Sequence-to-Sequence Pre-training for Natural Language Generation, Translation, and Comprehension](https://mlsanity.com/paper/1910.13461/) (2019)
- [Fine-Tuning Language Models from Human Preferences](https://mlsanity.com/paper/1909.08593/) (2019)
- [CodeBERT: A Pre-Trained Model for Programming and Natural Languages](https://mlsanity.com/paper/2002.08155/) (2020)
- [CodeT5: Identifier-aware Unified Pre-trained Encoder-Decoder Models for Code Understanding and Generation](https://mlsanity.com/paper/2109.00859/) (2021)
- [GraphCodeBERT: Pre-training Code Representations with Data Flow](https://mlsanity.com/paper/2009.08366/) (2020)
- [A Systematic Evaluation of Large Language Models of Code](https://mlsanity.com/paper/2202.13169/) (2022)
- [Semi-supervised Sequence Learning](https://mlsanity.com/paper/1511.01432/) (2015)
- [Keep the Conversation Going: Fixing 162 out of 337 bugs for 0.42 each using ChatGPT](https://mlsanity.com/paper/2304.00385/) (2023)
- [ChatGPT for Programming Numerical Methods](https://mlsanity.com/paper/2303.12093/) (2023)
- [FixMiner: Mining Relevant Fix Patterns for Automated Program Repair](https://mlsanity.com/paper/1810.01791/) (2018)
- [Teaching Autoregressive Language Models Complex Tasks By Demonstration](https://mlsanity.com/paper/2109.02102/) (2021)
- [iFixR: Bug Report driven Program Repair](https://mlsanity.com/paper/1907.05620/) (2019)
- [Fault Localization for Declarative Models in Alloy](https://mlsanity.com/paper/1807.08707/) (2018)
- [Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation](https://mlsanity.com/paper/1903.11765/) (2019)
- [Bounded Exhaustive Search of Alloy Specification Repairs](https://mlsanity.com/paper/2103.00327/) (2021)

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

- [On the Effectiveness of Large Language Models in Writing Alloy Formulas](https://mlsanity.com/paper/2502.15441/) (2025)

## Abstract (arXiv)

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 provide new opportunities for the automatic repair of declarative specifications. In this study, we assess the effectiveness of utilizing OpenAI's ChatGPT 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 ChatGPT's ability to improve the correctness and completeness of Alloy declarative specifications through automatic repairs. We analyze the results produced by ChatGPT and compare them with those of leading automatic Alloy repair methods. Our study revealed that while ChatGPT falls short in comparison to existing techniques, it was able to successfully repair bugs that no other technique could address. Our analysis also identified errors in ChatGPT's generated repairs, including improper operator usage, type errors, higher-order logic misuse, and relational arity mismatches. Additionally, we observed instances of hallucinations in ChatGPT-generated repairs and inconsistency in its results. Our study provides valuable insights for software practitioners, researchers, and tool builders considering ChatGPT for declarative specification repairs.