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

Mohannad Alhanahnah<EMAIL_ADDRESS>University of Wisconsin-
MadisonMadisonWIUSA ,  Md Rashedul Hasan<EMAIL_ADDRESS>University of
Nebraska-LincolnLincolnNEUSA and  Hamid Bagheri<EMAIL_ADDRESS>University of Nebraska-LincolnLincolnNEUSA

###### Abstract.

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
presents a systematic investigation into the capacity of Large Language Models
(LLMs) for repairing declarative specifications in Alloy, a declarative formal
language used for software specification. We propose a novel repair pipeline
that integrates a dual-agent LLM framework, comprising a Repair Agent and a
Prompt Agent. Through extensive empirical evaluation, we compare the
effectiveness of LLM-based repair with state-of-the-art Alloy APR techniques
on a comprehensive set of benchmarks. Our study reveals that LLMs,
particularly GPT-4 variants, outperform existing techniques in terms of repair
efficacy, albeit with a marginal increase in runtime and token usage. This
research contributes to advancing the field of automatic repair for
declarative specifications and highlights the promising potential of LLMs in
this domain.

Declarative specification, Automatic Program Repair, formal methods, Alloy
language, LLMs

††copyright: none

##  1\. Introduction

Declarative specification languages have become instrumental in addressing a
multitude of software engineering challenges. Among these languages, the Alloy
specification language (Jackson, 2006) has emerged as a powerful tool,
leveraging relational algebra and first-order logic to tackle a diverse array
of tasks within the software engineering domain. Its application spans across
software verification (Bagheri et al., [n. d.]), the security analysis of
cutting-edge platforms such as the IoT and Android systems (Bagheri et al.,
2016, 2021; Alhanahnah et al., [n. d.]), and the creation of test cases
(Khurshid and Marinov, 2004; Mirzaei et al., 2016). The integration of Alloy
with the Alloy Analyzer has facilitated automated property verification,
simplifying the process of checking whether specifications adhere to desired
properties and seamlessly integrating it into the Alloy environment. Despite
these advancements, Alloy users, akin to developers in imperative languages,
encounter challenges in debugging and correcting subtle bugs that may arise
during specification writing, particularly for complex systems.

While the Alloy Analyzer aids in automatic property verification and
counterexample generation, debugging and rectifying issues in Alloy
specifications remain laborious and manual tasks. Unlike the rich literature
and techniques available for automatic program repair (APR) in imperative
languages, the landscape for APR in declarative languages is relatively
sparse. Early approaches like ARepair (Wang et al., 2019) primarily rely on
failing test cases to identify and rectify bugs, assuming the presence of
tests for verification. However, this paradigm does not align well with
Alloy’s assertion-based specification approach, where users articulate
expectations using assertions rather than tests. Existing APR techniques like
ARepair (Wang et al., 2019) may succumb to overfitting issues when test
coverage is insufficient, compromising the correctness of generated repairs.
Despite efforts to mitigate these challenges with techniques like BeAFix
(Brida et al., 2021), which leverages assertions as correctness oracles, there
is room for improvement in terms of efficiency and effectiveness.

The emergence of Large Language Models (LLMs) has revolutionized various
domains, including natural language processing and code generation. These pre-
trained models, such as GPT-3.5-Turbo and GPT-4, exhibit remarkable accuracy
in predicting natural language and generating code. Inspired by these
advancements and the persistent challenges in repairing formal specifications,
we embark on a systematic empirical study to explore the potential of
utilizing LLMs for repairing faulty Alloy specifications. Our research aims to
address key questions regarding the effectiveness, performance, adaptive
prompting, failure characteristics, and repair costs associated with employing
LLMs in Alloy specification repair.

This paper presents a methodical exploration and the results of our
comprehensive evaluation of LLMs’ efficacy in repairing faulty Alloy
specifications, juxtaposed against state-of-the-art Alloy APR techniques. We
introduce a novel repair pipeline integrating a dual-agent LLM framework
comprising a Repair Agent and a Prompt Agent 111Our implementation and
artifacts are available at: https://github.com/Mohannadcse/AlloySpecRepair.
This iterative strategy centralizes around repairing bugs in defective
specifications and generating specialized prompts to guide the repair process.

We conduct an extensive evaluation of LLM effectiveness in repairing flawed
Alloy specifications, benchmarking it against several state-of-the-art Alloy
APR techniques, including ARepair(Wang et al., 2019), ICEBAR (Gutiérrez Brida
et al., 2023), BeAFix (Brida et al., 2021), and ATR (Zheng et al., 2022),
shedding light on their capabilities, benefits, and potential limitations. Our
evaluation encompassed two comprehensive sets of benchmarks, comprising 1,974
defective specifications sourced from ARepair (Wang et al., 2019) and
Alloy4Fun (Macedo et al., 2021), developed by external research groups. The
repair pipeline facilitates the rectification of each defective specification
under six distinct scenarios, with up to six iterations per scenario. Our
findings contribute to advancing the field of automatic repair for declarative
specifications and provide insights into leveraging LLMs for effective Alloy
specification repair.

##  2\. Background and Motivation

This section provides an overview of multi-agent large language models
followed by an illustrative example of a faulty Alloy specification to
motivate the research and help the reader follow the discussions that ensue.

###  2.1. Multi-Agent Large Language Models

####  2.1.1. Large Language Models

Emerging pre-trained Large Language Models (LLMs) have demonstrated impressive
performance on natural language tasks, such as text generation (Brown et al.,
2020; Chowdhery et al., 2022; Vaswani et al., 2017) and conversations
(Thoppilan et al., 2022; OpenAI, 2023). LLMs have also been proven effective
in translating natural language specifications and instructions into
executable code (Fan et al., 2023; Jain et al., 2022; Che, 2021). These models
have been trained on extensive corpora and possess the ability to execute
specific tasks without the need for additional training or hard coding (Bubeck
et al., 2023). They are invoked and controlled simply by providing a natural
language prompt. The degree to which LLMs understand tasks depends largely on
the prompting techniques used to convey user-provided instructions. These
prompts are categorized into two frameworks: “zero-shot” learning and “few-
shot” learning (Brown et al., 2020). Within the “zero-shot” learning
framework, the prompt includes a description of the problem and the
instructions for its resolution, aiming that LLMs can tackle previously unseen
tasks. Conversely, in the context of “few-shot” learning, LLMs are provided
with examples, supplementing the guidance offered in the “zero-shot” prompt.

####  2.1.2. Multi-Agent LLMs.

With recent advancements in LLMs, developers are embracing the idea of
creating autonomous agents that can solve various tasks and interact with
environments, humans, and other agents using natural language interfaces (Zhou
et al., 2023a). These agents provide several features including planning,
memory, tool usage, and multi-agent communication. Therefore, LLM-based
autonomous agents have gained tremendous interest in industry and academia
(Wang et al., 2023). Several frameworks have been developed to support
harnessing multi-agent LLM applications. AGENTS (Zhou et al., 2023b) is a
unified framework and open-source library for language agents. AGENTS aims to
facilitate developers to build applications with language agents. AutoGPT
(Aut, [n. d.]) a multi-agent framework for LLMs, is designed to support
autonomous applications of LLMs. LangChain (Chase, 2022) supports end-to-end
language agents that can automatically solve tasks specified in natural
language. It also facilitates the connection between LLM agents and external
tools. Langroid (lan, 2024) is another framework that supports the development
of multi-agent LLMs. It offers the capability to manage the history of
messages, thus controlling the context window of LLMs. This is a crucial
functionality for LLM apps operating iteratively (i.e., Self-Refine (Madaan et
al., 2023) and Reflexion (Shinn et al., 2024)). Moreover, Langroid enables
seamless integration with a variety of LLMs.

####  2.1.3. tools and function calling

Multi-agent frameworks and recent versions of OpenAI’s LLM have introduced a
feature known as function
calling222https://platform.openai.com/docs/guides/text-generation/function-
calling. This feature enables users to provide function descriptions to the
LLM. In turn, the LLM responds with a structured response (i.e., JSON data
containing the requisite arguments for invoking any available functions).
These functions serve as action executors and provide the option to supply
APIs that the LLM can query to obtain essential information for responding to
users. For example, when a user inquires about the current weather in a
specific city and provides the LLM with a weather API call description, the
LLM can augment its response with information retrieved from the API. This
facilitates a seamless and efficient interaction between the user and the LLM
and provides rich responses to avoid hallucinations.

###  2.2. Motivating Example

Alloy, a formal modeling language, provides a comprehensible syntax inspired
by object-oriented notations and is grounded on first-order relational logic
(All, [n. d.]). Within an Alloy specification, three primary components shape
its structure: data types, constraints expressed through formulas, and
commands to initiate the analyzer.

The language relies on sig to define fundamental data types, which can be
organized using fields to capture relationships between signatures.
Additionally, Alloy employs fact to introduce constraints that persist in
every instance of the specification. These constraints restrict the model
space, ensuring its consistency. Further structuring of formulas is achieved
through pred and fun, which are named parameterized Alloy formulas, and assert
encapsulates the properties intended for validation.

Commands such as check and run activate the automated analyzer. Check verifies
assertions, while run executes predicates, aiming to identify model instances
that satisfy specified conditions. Alloy’s expressiveness stems from its use
of relational logic, a first-order logic extended with relational operators.
These include all, some, one, and lone quantifiers, along with operators like
relational join and transitive closure.

To illustrate the Alloy language and motivate the research, we examine the
specification of the River Crossing puzzle, a classic problem of safely
transporting a farmer, a fox, a chicken, and a sack of grain across a river.
Listing 1 presents an abbreviated Alloy specification snippet of the farmer
model from ARepair benchmark (Wang et al., 2019). In the River Crossing
puzzle, the goal is to transport all objects from one side of the river to the
other safely. However, there are constraints to consider: the farmer can only
take one item with them in the boat, and if the farmer leaves the fox with the
chicken, or the chicken with the grain, without supervision, a dire
consequence will occur. This puzzle’s Alloy specification defines objects like
the Farmer, Fox, Chicken, and Grain, along with their attributes and
constraints.

However, the model contains a flaw in the crossRiver predicate, where the
logic mistakenly assumes the occurrence of eating actions on the wrong side of
the river. This oversight allows scenarios where the fox can eat the chicken
without the farmer’s supervision, violating the puzzle’s rules. Interestingly,
state-of-the-art automated repair techniques have struggled to address this
particular bug. To repair this model, the erroneous logic within the
crossRiver predicate must be corrected. However, this task presents a
significant challenge due to the complexity of the puzzle’s logic and
interactions between its components. Rectifying these logical errors requires
a deep understanding of the problem domain and intricate relationships within
the specification.

The objective of our study is to assess the effectiveness of repair methods
for such buggy specifications using LLMs compared to state-of-the-art Alloy
repair techniques. LLMs offer potential in uncovering complex violations and
evaluating repair methods by reasoning about broader system contexts and
intended behaviors. In the following sections, we explore the ability of LLMs
to address such challenges and the specific conditions under which they can do
so.

⬇

1abstract sig Object { eats: set Object }

2one sig Farmer, Fox, Chicken, Grain extends Object {}

3fact eating { eats = Fox->Chicken + Chicken->Grain }

4sig State {

5 near: set Object,

6 far: set Object

7}

8fact initialState {

9 let s0 = ord/first |

10 s0.near = Object && no s0.far

11}

12// Bug found in original model crossRiver

13pred crossRiver [from, from’, to, to’: set Object] {

14 // Fix: replace "from’ = from - Farmer && to’ = to - to.eats + Farmer" with
"from’ = from - Farmer - from’.eats && to’ = to + Farmer".

15 (from’ = from - Farmer && to’ = to - to.eats + Farmer)

16 // Fix: replace "from’ = from - Farmer - item && to’ = to - to.eats +
Farmer + item" with "from’ = from - Farmer - item - from’.eats && to’ = to +
Farmer + item".

17 || (some item: from - Farmer {

18 from’ = from - Farmer - item

19 to’ = to - to.eats + Farmer + item })

20}

21fact stateTransition {

22 all s: State, s’: ord/next[s] {

23 Farmer in s.near =>

24 crossRiver[s.near, s’.near, s.far, s’.far] else

25 crossRiver[s.far, s’.far, s.near, s’.near]

26 }

27}

28pred solvePuzzle { ord/last.far = Object }

29run solvePuzzle for 8 State expect 1

30assert NoQuantumObjects {

31 no s : State | some x : Object | x in s.near and x in s.far

32}

33check NoQuantumObjects for 8 State expect 0

Listing 1: A snippet of the flawed farmer Alloy specification sourced from the
ARepair benchmark444https://github.com/guolong-
zheng/atmprep/blob/master/benchmark/arepair/farmer1.als.

##  3\. Methodology

This section outlines the repair pipeline, detailing its architecture and
workflow. The pipeline is driven by the APR phases as outlined in (Zhang et
al., 2023), including localization, repair, and verification. Our
implementation of this pipeline utilizes the Langroid framework (lan, 2024).

Figure 1. LLM-assisted APR Pipeline.

###  3.1. Overall Workflow

In this section, we overview our repair pipeline specifically tailored for
iterative self-refinement. Our approach revolves around the concept of
iterative refinement, wherein the repair process for a defective Alloy model
operates within a predetermined budget, defined by the number of iterations
allocated. Previous research has indicated that this iterative prompting
method yields superior outcomes compared to traditional single-step
approaches, enhancing task efficiency by an average of 20

The workflow of our Automatic Program Repair (APR) pipeline, as depicted in
Figure 1, comprises two primary components: the Repair Agent and the Prompt
Agent. Each agent maintains its context, tools, and prompts, but they
collaborate to adaptively refine the prompt for enhanced effectiveness, as
elaborated below. Our pipeline supports various feedback levels, employing a
zero-shot prompting approach (Paul et al., 2023), where tasks are performed
without explicit examples, as detailed in Table 1.

Upon receiving defective Alloy specifications and the prompt, our APR pipeline
dispatches these elements to the LLM, which generates a revised version aimed
at rectifying the defect. Subsequently, the Repair Agent compares the proposed
specifications with the buggy ones to evaluate LLM’s ability to localize
faults and adhere to instructions. The correctness of the proposed
specifications is then assessed by triggering the Alloy Analyzer tool, which
runs the proposed specifications for validation. If the Alloy analyzer
confirms the bug’s resolution, the repair process concludes. Conversely, if
errors persist, the pipeline initiates another iteration, contingent upon the
remaining repair budget. If the budget is depleted, the pipeline terminates
operations.

Our adaptive prompt is designed to evolve and refine based on different
settings (detailed in Section 3.3), ensuring continual improvement after each
unsuccessful attempt.

The following sections provide a comprehensive overview of each component of
the pipeline.

Table 1. Zero-shot prompts used by the repair pipeline

Agent |  Message Type |  Message content
---|---|---
Repair Agent |  Agent-Instruction |  You are an expert in repairing Alloy declarative specifications. You will be presented with Alloy ¡Faulty_SPECIFICATIONS¿. Your task is to FIX/REPAIR the ¡Faulty_SPECIFICATIONS¿. Use the tool ‘run_alloy_analyzer‘ to demonstrate and validate the ¡FIXED_SPECIFICATIONS¿. Wait for my feedback, which may include error messages or Alloy solver results. You will have 5 trials to fix the ¡Faulty_SPECIFICATIONS¿. **Adhere to the Following Rules**: - The ¡FIXED_SPECIFICATIONS¿ should be consistent (having instances) and all the assertions should be valid (no counterexample). - DO NOT REPEAT the ¡FIXED_SPECIFICATIONS¿ that I sent you. - DO NOT provide any commentary and always send me anything ONLY using the tool ‘run_alloy_analyzer‘. - The ¡FIXED_SPECIFICATIONS¿ MUST be different than the ¡Faulty_SPECIFICATIONS¿.
Tool-instruction |  ALL AVAILABLE TOOLS and THEIR JSON FORMAT INSTRUCTIONS: You have access to the following TOOLS to accomplish your task: TOOL: run_alloy_analyzer, PURPOSE: To show a ¡FIXED_SPECIFICATIONS¿ to the user. Use this tool whenever you want to SHOW or VALIDATE the ¡FIXED_SPECIFICATIONS¿. NEVER list out a ¡FIXED_SPECIFICATIONS¿ without using this tool. JSON FORMAT: ”type”: ”object”, ”properties”: ”request”: ”default”: ”run_alloy_analyzer”, ”type”: ”string”,”specification”: ”type”: ”string”, ”required”: [ ”specification”, ”request”]. When one of the above TOOLs is applicable, you must express your request as ”TOOL:” followed by the request in the above JSON format.
Prompt Agent |  Agent-Instruction |  You are Expert in Analyzing Alloy Analyzer reports. Can you describe concisely and precisely the modifications needed to fix the error in at most 2 sentences? Based on this report from Alloy Analyzer: {Alloy_report_msg} After running this Alloy Model is: {proposed_spec}

###  3.2. Pipeline Agents

As depicted in Figure 1, the pipeline comprises two agents. This design
facilitates evaluating the recent deployment of LLM apps as multi-agent
applications.

####  3.2.1. Repair Agent

This agent is the core component of the APR pipeline. It has access to
tools/functions (i.e., “run_alloy_analyzer”), maintains its context (i.e.,
history of messages) over the iterations, and decides the process for handling
subsequent iterations.

The agent’s prompt encompasses a set of messages combined as a system message.
These messages are listed in Table 1.

  * •

Agent Instruction. This message provides a general guideline to the Repair
Agent, commencing with the agent’s persona as an “expert in repairing Alloy
specifications”. It proceeds to notify LLM of defects within the provided
Alloy model, without disclosing the defects’ locations. The message finally
describes the tools (i.e., “run_alloy_analyzer”) to which this agent has
access. In conclusion, it enumerates a set of procedural steps to be executed
by the LLM.

  * •

Tool Instruction. Offers instructions delineate the conditions and procedures
for utilizing the tool “run_alloy_analyzer”. It further specifies the data
required from the LLM to ensure the proper activation of this tool. This
instruction guides the LLM to transmit a JSON formatted response,
encapsulating two fields: (1) request, denoting the tool designation intended
for use by the LLM, and (2) proposed_specification, representing the LLM’s
suggested version for rectifying the identified bug.

####  3.2.2. Prompt Agent

This agent has its LLM settings and context and generates feedback based on
the report generated by Alloy Analyzer and the proposed specification. The
produced feedback guides the Repair Agent on the methods for rectifying the
bug. The system message that provides the instructions to this agent is
described in Table 1. Unlike the system message of the Repair Agent, the
agent’s persona is described as “Expert in Analyzing Alloy Analyzer reports”.
This agent does not share the same context or prompts with the Repair Agent.
But the response of the Prompt Agent is appended to the prompt that will be
used in the next iteration by the Repair Agent.

###  3.3. Feedback Messages

The initial prompt contains only Agent Instruction and Tool Instruction
defined by the Repair Agent, as described in Table 1. The pipeline refines the
prompts in response to the behavior of the proposed specification. This
refinement process is contingent upon repetitive buggy specifications, errors
that emerge after the execution of these specifications through the Alloy
analyzer, or LLM failure to send a response based on the required JSON format.

To this end, Table 2 presents the feedback messages that are supported by the
pipeline. These feedback messages will be appended to the initial prompt.
Following is a description of these:

  * •

Tool fallback. This message informs LLM that the response received does not
comply with the tool’s JSON format, consequently impeding the extraction of
the proposed specification. To address this issue, we developed a parser atop
the Langroid JSON parser, specifically to retrieve Alloy specifications from
the response. Nonetheless, the parser cannot handle all scenarios, resulting
in the dispatch of this feedback to the LLM, soliciting adherence to the
mandated JSON format.

  * •

Repeated Spec. This message is triggered when the proposed spec is the same as
the buggy specification. In this situation, this message tells the LLM not to
repeat the buggy specification.

  * •

Alloy Analyzer Report. This message relays the feedback of the verification
process using Alloy Analyzer. Table 2 presents three feedback levels.

In the following, we discuss the details of the various feedback levels
supported by the pipeline.

Table 2. Feedback Messages used by the repair pipeline

Feedback Type |  Generated By |  Message Content
---|---|---
Tool-fallback |  Alloy Analyzer |  You must use the CORRECT format described in the tool ‘run_alloy_analyzer‘ to send me the fixed specifications. You either forgot to use it, or you used it with the WRONG format. Make sure all fields are filled out.
Repeated spec |  The proposed ¡FIXED_SPECIFICATIONS¿ is IDENTICAL to the Alloy ¡Faulty_SPECIFICATIONS¿ that I sent you. **DO NOT** send Alloy specifications that I sent you again. ALWAYS USE the tool ‘run_alloy_analyzer‘ to send me a new ¡FIXED_SPECIFICATIONS¿.
No-feedback |  The proposed specification DID NOT fix the bug.
Generic-feedback |  Below are the results from the Alloy Analyzer. Fix all Errors and Counterexamples before sending me the next ¡FIXED_SPECIFICATIONS¿.
Auto-feedback |  Prompt Agent |  The message content will be dynamically constructed by the agent based on the supplied information.

Alloy Analyzer Feedback Levels: The verification stage involves running the
proposed specifications with the Alloy Analyzer. Subsequently, feedback
conveying the Alloy Analyzer’s report is generated, available at different
levels of detail. This process aids in assessing the effectiveness of various
refinements made to the prompts.

In this study, we consider three feedback levels to refine the prompt as
outlined in Table 2. These levels reflect errors, counterexamples, and
instances identified after running the Alloy Analyzer in each iteration. They
also mimic different repair scenarios, as described below:

  1. (1)

No-feedback. In this setting, the Alloy Analyzer agent returns only a single
response (i.e., The proposed specification DID NOT fix the bug.) to LLM
without describing the details of the report generated by the Alloy Analyzer.
This setting is designed to demonstrate the ability of LLMs to identify and
fix errors in a faulty model solely based on the content of the buggy model
itself, mirroring the function of a programming language compiler.

  2. (2)

Generic-feedback. We use a template to send the Alloy Analyzer report to LLM.
This report summarizes counterexamples, instances, and errors. This scenario
represents a common situation where the developer shares a summary of the
issue on a question-and-answer platform (such as Stack Overflow) to get help.

  3. (3)

Auto-feedback. When this setting is enabled, the feedback response to LLM will
be generated by another LLM agent (i.e., prompt agent). We forward the report
generated by the Alloy Analyzer and the proposed Alloy specifications to the
prompt agent, which generates a prompt to instruct the Repair Agent.

The different reports reflect the ability of LLMs to (1) locate bugs and (2)
correctly perform the repair process. For example, Generic-feedback and Auto-
feedback show the ability of LLM to perform its reasoning based on a human-
created prompt versus an LLM-generated prompt, which has no access to the
repair context. Also, the latter reflects a real scenario wherein the user
cannot repair the buggy specification, then they consult experts or other
forums to get assistance.

##  4\. Experiment Design

In this study, we address the following research questions (RQs):

  * •

RQ1 (Effectiveness): How effective is the APR pipeline in repairing compared
to the state of the art?

  * •

RQ2 (Performance): What is the repair performance when employing pre-trained
LLMs?

  * •

RQ3 (Adaptive Prompting): What is the impact of applying the adaptive
prompting technique?

  * •

RQ4 (Failure Characteristics): What are the characteristics of failures
encountered during the repair process?

  * •

RQ5 (Repair Costs): What is the cost associated with using the APR pipeline
with various LLMs?

###  4.1. Dataset

In our evaluation, we utilize two distinct benchmark suites: ARepair (Wang et
al., 2019) and Alloy4Fun (Macedo et al., 2021). These benchmark suites have
undergone extensive study and been developed by independent research groups,
enabling a fair comparison of various techniques.

The benchmark datasets consist of specifications varying from tens to hundreds
of lines, featuring real bugs authored by humans. The defects within the
benchmarks span a diverse range, from straightforward issues that can be
addressed by modifying a single operator to complex challenges necessitating
the synthesis of novel expressions and the substitution of entire predicate
bodies.

The ARepair benchmark (Wang et al., 2019) encompasses 38 faulty specifications
extracted from a total of 12 Alloy problems. Within this benchmark, both
single and multi-line errors are present, distributed across 28 faulty models
with single-line errors and 10 faulty models with multi-line errors. The
Alloy4Fun benchmark (Macedo et al., 2021) comprises a collection of 1,938
handwritten defective models sourced from student submissions across six
different Alloy problems. All bugs within this benchmark are single-line bugs.
Both benchmarks are accompanied by correct versions of the specifications,
serving as ground truths for verifying the accuracy of the obtained results.

###  4.2. Pre-processing Benchmark Dataset

As mentioned earlier, the benchmark datasets include comments indicating bug
locations and their corresponding fixes. To ensure a fair evaluation, we have
removed these comments from the defective models. Specifically, we have
eliminated all lines starting with the phrase ”Fix:” in the defective models.
This line typically outlines the necessary changes required to resolve the
bug. Models with multiple ”Fix:” comments are categorized as having multi-line
bugs, whereas those with only one ”Fix:” comment are considered to have
single-line bugs.

This process of removing comments is crucial as it prevents LLMs from being
provided with explicit clues about the locations of bugs and their respective
fixes. By doing so, we aim to accurately assess the repair capabilities of
LLMs and observe their effectiveness in localizing bugs within the defective
models.

###  4.3. Implementation

Our implementation of the APR pipeline was realized using Python 3.11, with
the assistance of Langroid to facilitate the integration of multi-agent LLMs.
This implementation encompasses several crucial functionalities. Firstly, it
offers support for various LLMs, including local LLMs, ensuring flexibility in
model selection. Secondly, it incorporates a message history control
mechanism, essential for preventing context length limitations, particularly
during iterative repair processes. Lastly, our implementation facilitates the
creation and customization of tools, allowing for the definition of response
formats and fields. Additionally, we developed a specialized parser to address
issues caused by special situations that could impede the extraction of
proposed specifications.

The experiments were carried out on a system equipped with a 2.3 GHz Quad-Core
Intel Core i7 processor, 32 GB of RAM, and running macOS Sonoma. Furthermore,
the system was configured with Oracle Java SE Development Kit 8u202 (64-bit
version), ensuring compatibility and optimal performance throughout the
execution of the APR pipeline.

###  4.4. Subject LLMs

To assess the performance of existing pre-trained LLMs, we have carefully
chosen three representative models555While exploring local models such as
Llama-2 and Mistral, it became apparent that they lacked support for tools,
making it challenging to process their responses, which often contained
incomplete Alloy specifications.:

  * •

GPT-3.5-Turbo: This standard LLM, provided by OpenAI and utilized in ChatGPT,
boasts a sophisticated architecture with 175 billion parameters, endowing it
with extensive capabilities. Engineered to tackle a wide array of natural
language processing (NLP) tasks, including text generation and completion,
GPT-3.5-Turbo epitomizes advanced computational linguistics. Within the
context of our study, we utilize the gpt-3.5-Turbo variant accessed via the
OpenAI API for evaluative purposes.

  * •

GPT-4-32k: Representing the state-of-the-art in LLM models from OpenAI, this
model contains over 1.76 trillion parameters, demonstrating significantly
enhanced capabilities compared to GPT-3.5. For our study, we leverage the
GPT-4-32k-0613 model version.

  * •

GPT-4-Turbo: Another iteration of the GPT-4 model, GPT-4-Turbo features an
updated knowledge cutoff as of April 2023 and introduces a 128k context
window. Moreover, it offers cost-effectiveness compared to GPT-4, alongside
notable enhancements such as improved instruction following, JSON mode, and
reproducible outputs (OpenAI, [n. d.]).

Table 3 provides more details about the characteristics of these pre-trained
LLMs.

Table 3. Characteristics of Pre-trained LLMs

Model | Version | Cut-off |  | Context Window
---
(Tokens)
| Input Cost
---
per 1M tokens
| Output Cost
---
per 1M tokens
GPT-3.5 Turbo | 1106 | Sep 2021 | 16,385 | $1 | $2
GPT-4-32k | 0613 | Sep 2021 | 32,768 | $60 | $120
GPT-4 Turbo | 1106-preview | Apr 2023 | 128k | $10 | $30

###  4.5. Subject SOTA Systems

We conducted a comparative analysis of repair performance against several
state-of-the-art Alloy repair tools: ARepair (Wang et al., 2019), ICEBAR
(Gutiérrez Brida et al., 2023), BeAFix (Brida et al., 2021), ATR (Zheng et
al., 2022), and Hasan et al. (Hasan et al., 2023). Each tool employs a
distinct development approach and tackles specification attributes
differently.

ARepair (Wang et al., 2019) generates fixes for Alloy specifications that
violate test cases. ICEBAR (Gutiérrez Brida et al., 2023) utilizes ARepair as
a backend tool to repair faulty Alloy specifications based on a predefined set
of Alloy tests. ATR (Zheng et al., 2022) adopts a template-based methodology
to enhance the repair process, leveraging fault localization strategies to
identify potentially erroneous Alloy expressions leading to assertion
failures. BeAFix (Brida et al., 2021) relies on user input to identify faulty
statements. It exhaustively explores all possible repair candidates up to a
certain threshold through mutation and employs Alloy counterexamples to
evaluate the feasibility of generalization. Fianlly, Hasan et al. (Hasan et
al., 2023) employed ChatGPT for repairing faulty specifications across five
scenarios. For our comparison, we exclude scenarios where ChatGPT is provided
with “Fix:” comments, as this represents an unrealistic setting and does not
align with our ”Benchmark Pre-processing” step (cf. Section 4.2).

###  4.6. Experimental Configuration and Settings

LLM Temperature: To balance between deterministic progression and iterative
refinement, we set the temperature parameter of the Large Language Models
(LLMs) to 0.2, allowing for a moderate level of randomness while maintaining
some level of determinism throughout the repair process (Kong et al., 2024;
Zhang et al., 2024).

Number of Iterations: Initially, we conducted a preliminary experiment using
the ARepair benchmark framework with GPT-4-32k, allocating a budget of ten
iterations. However, we observed diminishing returns after six iterations in
most cases. Therefore, we opted for a six-iteration budget in the APR
pipeline.

Metric for Comparing Repair Performance of LLMs: We employ the Correct@k
metric (Liu et al., 2024) to evaluate the success rate of the techniques in
repairing defective Alloy specifications. This metric quantifies the number of
defects successfully repaired within a maximum of $k$ iterations, where $k$ is
set to 6 in our study (denoted as Correct@6). The formula for this metric is
described in Equation 1.

(1) $\footnotesize\text{Correct@}k=\left(\frac{\text{\\# of bugs successfully
repaired within }k\text{ iterations}}{\text{Total number of bugs
evaluated}}\right)\times 100$

Experiment Settings and Baseline: Our evaluation encompasses a total of 1,974
defective models. We assess three distinct LLMs, as outlined in Table 3. The
APR pipeline supports three levels of report granularity and permits multiple
iterations, resulting in a total of 106,596 repair attempts (calculated as the
product of 1,974 benchmarks, three LLMs, three feedback levels, and up to six
iterations). To manage costs associated with GPT-4 models, we conducted two
experiments for RQ1. The first experiment focuses on repairing Alloy4Fun and
ARepair benchmarks using GPT-3.5, followed by a comparison with state-of-the-
art (SoTA) tools. In the second experiment, we limit the repair task to the
ARepair benchmark, utilizing GPT-4 and GPT-4-Turbo exclusively. Table 4
provides details of the different combinations of LLMs and feedback
intensities used in the latter experiment.

Table 4. Settings corresponding to various combinations of LLMs and feedback levels Setting No. | LLM | Feedback Level
---|---|---
Setting-1 | GPT-4-32k | No-Feedback
Setting-2 | GPT-4-32k | Generic-Feedback
Setting-3 | GPT-4-32k | Auto-Feedback
Setting-4 | GPT-4-Turbo | No-Feedback
Setting-5 | GPT-4-Turbo | Generic-Feedback
Setting-6 | GPT-4-Turbo | Auto-Feedback

##  5\. Experimental Results

This section summarizes the data we collected, its interpretation, and our
results.

###  5.1. Results for RQ1: Effectiveness

Table 5. Comparing against state-of-the-art Alloy repair techniques (ARepair
(Wang et al., 2019), ICEBAR (Gutiérrez Brida et al., 2023), BeAFix (Brida et
al., 2021), ATR (Zheng et al., 2022), and Hasan et al. (Hasan et al., 2023))
on the ARepair and Alloy4Fun benchmarks, using GPT-3.5-Turbo as our LLM
baseline.

| Total | Arepair | ICEBAR | BeAFix | ATR | Hasan et al. | No-Feedback | Generic-Feedback | Auto-Feedback
---|---|---|---|---|---|---|---|---|---
| #specs | #repairs | #repairs | #repairs | #repairs | #repairs | #repairs | #repairs | #repairs
Alloy4Fun | 1936 | 185 | 1051 | 981 | 1286 | 147 | 156 | 231 | 278
ARepair | 38 | 9 | 21 | 24 | 22 | 4 | 4 | 6 | 18

Table 6. Comparing with state-of-the-art Alloy repair techniques (ARepair
(Wang et al., 2019), ICEBAR (Gutiérrez Brida et al., 2023), BeAFix (Brida et
al., 2021), ATR (Zheng et al., 2022), and Hasan et al. (Hasan et al., 2023))
on the ARepair benchmarks, using various combinations of LLMs and report
levels as outlined in Table 4.

Model | Total | Arepair | ICEBAR | BeAFix | ATR | Hasan et al. | Setting-1 | Setting-2 | Setting-3 | Setting-4 | Setting-5 | Setting-6
---|---|---|---|---|---|---|---|---|---|---|---|---
|  | #specs | #repairs | #repairs | #repairs | #repairs | #repairs | #repairs | #repairs | #repairs | #repairs | #repairs | #repairs
ARepair | addr | 1 | 1 | 1 | 1 | 1 | 0 | 0 | 0 | 1 | 0 | 1 | 1
arr | 2 | 2 | 2 | 2 | 1 | 0 | 0 | 0 | 0 | 1 | 0 | 1
balancedBST | 3 | 1 | 2 | 1 | 1 | 1 | 1 | 1 | 2 | 1 | 1 | 1
bempl | 1 | 0 | 1 | 0 | 1 | 0 | 0 | 0 | 0 | 1 | 1 | 1
cd | 2 | 0 | 2 | 2 | 2 | 1 | 1 | 2 | 2 | 2 | 1 | 2
ctree | 1 | 1 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 | 1
dll | 4 | 0 | 3 | 3 | 2 | 4 | 4 | 4 | 4 | 2 | 2 | 4
farmer | 1 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 1 | 1 | 1
fsm | 2 | 2 | 2 | 1 | 2 | 1 | 1 | 1 | 2 | 0 | 0 | 1
grade | 1 | 0 | 1 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 1
other | 1 | 0 | 0 | 1 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 1
student | 19 | 2 | 7 | 13 | 10 | 6 | 6 | 6 | 9 | 8 | 11 | 13
Summary | 38 | 9 | 21 | 24 | 22 | 15 | 15 | 16 | 22 | 17 | 19 | 28

Figure 2. Venn diagrams illustrating the exclusive and overlapping cases of
successful repairs by different repair methods, highlighting the complementary
and unique capabilities of the APR pipeline compared to SoTA repair tools.

Table 5 provides a comparison using GPT-3.5-Turbo as the baseline. The column
”Total #specs” indicates the total number of defective specifications in each
benchmark, while the subsequent columns show the number of correctly repaired
specifications by each state-of-the-art Alloy repair tool. The last three
columns display the repair outcomes based on different report levels employed
in the pipeline. The performance of the baseline LLM (GPT-3.5-Turbo) is
notably inferior compared to traditional state-of-the-art tools, consistent
with prior findings by Hasan et al. (Hasan et al., 2023). However, the two-
agent (auto-feedback) configuration demonstrated the most promising
performance among the feedback levels across both benchmarks.

Table 6 presents comparison results for the ARepair benchmark using GPT-4-32k
and GPT-4-Turbo. The ”Models” column categorizes model groups in the ARepair
benchmark, while the last six columns illustrate the total count of accurately
fixed specifications under different pipeline settings (summarized in Table
4). Setting-6 notably outperforms all state-of-the-art tools, while Setting-3
performs similarly to BeAFix and surpasses other traditional tools. It’s
noteworthy that the specification farmer remained unresolved by all SoTA
repair tools, but was successfully repaired in the APR pipeline across all
settings. This suggests that GPT-4 family models can effectively address
complex specifications, particularly those with multi-line bugs. Further, the
results observed in Setting-3 and Setting-6 surpass those of other settings
(in Table 4) and align with the ”Auto-Feedback” column in Table 5. This
alignment underscores the efficacy of prompt construction using LLMs over
generic prompts developed by humans, advocating for the use of multi-agent LLM
setups.

To gain deeper insights into the complementarity of these methods, Venn
diagrams in Figure 2 illustrate cases exclusively fixed by one tool but not by
others, as well as the overlap between techniques (i.e., cases correctly
repaired by multiple tools). Notably, the repair pipeline successfully
addresses faulty models that other SoTA repair tools fail to resolve.

The metric Correct@6 is utilized to compare the performance of all LLMs across
various feedback levels. Table 7 showcases the comparison results using the
ARepair benchmark. While GPT-3.5-Turbo exhibited less effective repair
capabilities, GPT-4-Turbo demonstrated superior performance across different
feedback levels, attributable to its cut-off and context window parameters
relative to its counterparts (see Table 3), alongside enhanced features
integrated into this model (detailed in Section 4.4).

The results for RQ1 demonstrate that the APR pipeline, particularly with
GPT-4-Turbo and multi-agent setups, outperforms traditional state-of-the-art
Alloy repair tools, effectively addressing complex multi-line bugs and
showcasing superior performance across various feedback levels.

Table 7. Comparison results presenting the repair performance of different LLMs across various feedback levels, i.e., No-Feedback (NF), Generic-Feedback (GF), Auto-Feedback (AF), measured by the Correct@6 metric.  GPT-3.5-Turbo | GPT-4-32k | GPT-4-Turbo
---|---|---
NF | GF | AF | NF | GF | AF | NF | GF | AF
10.5 | 15.8 | 47.4 | 39.5 | 42.1 | 57.9 | 44.7 | 50.0 | 57.9

###  5.2. Results for RQ2: Performance

This research question delves into the repair performance of various pre-
trained Language Model Models (LLMs) concerning factors such as repair
iteration budget, bug type, localization capabilities, and adherence to
instructions. Our analysis focuses on two LLM variants: GPT-4-32k and
GPT-4-Turbo, utilizing the results provided in Table 6 and the settings
outlined in Table 4.

Repair Iteration Budget: The box-whisker plot in Figure 3(a) illustrates the
iterations needed by different settings to rectify faulty specifications.
Across all settings, the median number of iterations predominantly centers
around 1.0, except for Setting 3 & 6, where Setting-3 increases to 2.5,
indicating a demand for additional iterations. However, median values for
Settings 1, 2, 4, and 5 remain at 1.0, suggesting that at least half of the
issues are resolved within the first iteration.

(a)

(b)

(c)

Figure 3. (a) Iteration count distribution for repairing specifications across
various settings. (b) Repair distribution in ARepair benchmark categorized by
bug type: single-line or multi-line (higher values preferred). (c) The
incident count for initial repair attempts mirroring the buggy specification
(lower values preferred), derived from the ARepair benchmark.

Repairing Based on Bug Type: Figure 3(b) depicts the repair capabilities of
GPT-4-32k and GPT-4-Turbo concerning bug types, namely single-line and multi-
line bugs. The best performance for GPT-4-Turbo (auto-feedback, Setting-6)
achieved the highest repair rate, fixing 16 single-line bugs and 12 multi-line
bugs. In contrast, the best result for GPT-4-32k (auto-feedback, Setting-3)
demonstrated superior performance in correcting single-line bugs (12 models)
compared to multi-line bugs (10 models). Additionally, we examine the repair
outcomes achieved by GPT-3.5-Turbo, showing repair capabilities for both
single-line and multi-line bugs.

Following Instructions: Adherence to instructions is crucial in tasks like APR
to ensure repair quality and control costs. However, Figure 3(c) reveals that
both GPT-4 models sometimes repeat buggy models in their initial repair
iterations, despite system instructions to avoid this. GPT-4-Turbo generally
shows better compliance, particularly in Setting-6, where it exhibits the
lowest number of repeated buggy specifications.

The comparison between the APR pipeline utilizing different feedback levels
and state-of-the-art Alloy repair techniques, along with the performance of
various LLMs, revealed that the auto-feedback approach exhibited the best
performance across both benchmarks, surpassing traditional SoTA repair tools.

###  5.3. Results for RQ3: Adaptive Prompting

The APR pipeline facilitates three feedback levels—No-feedback, Generic-
Feedback, and Auto-Feedback—as outlined in Section 2. This research question
delves into the implications of these feedback levels on LLM performance,
drawing insights from the following analysis:

Overall Repair Performance: Examination of Tables 5 and 6 reveals a notable
correlation between the use of ”auto-feedback” and superior repair efficacy
across all LLMs, including GPT-3.5-Turbo. Conversely, the absence of feedback,
characterized by ”No-feedback,” resulted in the poorest repair performance,
indicating that prompt updates driven by information from the Alloy Analyzer
report significantly contribute to repair success.

Bug-type Repair: Across all LLMs, Settings 3 and 6 consistently demonstrate a
higher ability to repair complex specifications, as illustrated in Figure
3(b). This suggests that adaptive prompting, particularly in Settings 3 and 6,
enhances the pipeline’s capacity to address intricate bugs effectively.

Iteration Budget Analysis: Figure 3(a) showcases a slight increase in the
requirement for additional iterations in Settings 3 and 6. While these
settings exhibit superior repair capabilities, they may necessitate a
marginally higher number of iterations to achieve optimal outcomes.

These observations underscore the advantage of leveraging LLMs to
automatically generate prompts based on Alloy Analyzer reports, leading to
enhanced repair performance compared to Generic-Feedback. However, this
advantage may be accompanied by the need for additional iterations.

###  5.4. Results for RQ4: Characteristics of Failed Repairs

This research inquiry delves into the root causes of failures encountered
during the iterative repair process across various settings. The following
elucidates the key findings derived from this investigation.

Figure 4. Error types observed in failed repair iterations across all settings

Figure 4 illustrates the distribution of failed iterations across distinct
settings and provides a comprehensive breakdown of failure reasons.
Predominantly, failures arise when the proposed repairs fail to fulfill
assertions, resulting in the generation of counterexamples. Additionally,
syntax errors in proposed repairs impede the compilation process by Alloy
Analyzer. Settings 1-3, employing GPT-4-32k, manifest instances of failures
attributed to incorrect message formats, a phenomenon absent in Settings 4-6
utilizing GPT-4-Turbo. Such disparities suggest discrepancies in the
compliance of LLM responses with the JSON format mandated by the
alloy_analyzer_tool. Categories such as ”Repetition” and ”No instances”
exhibit lower prevalence. ”Repetition” denotes instances where proposed
repairs mimic defective models, while ”No instances” signify scenarios where
proposed models fail to generate instances, indicative of an incapacity to
meet model constraints.

Figure 5. Repair progress in Setting-6 (GPT-4-Turbo and Auto-Feedback) across
iterations. Percentage numbers show transition volumes between statuses in
subsequent iterations. Cumulative counts of fixed models follow each ’Fixed’
block.

Figure 5 tracks outcomes across all iterations in Setting-6, revealing the
evolving nature of failure categories during the iterative prompting process.
While instances of ”Counterexample” failures are effectively addressed,
challenges persist in rectifying issues classified under ”Repetition.”
Moreover, a discernible transition of cases between distinct failure
categories underscores the dynamic nature of failure characteristics
throughout the repair endeavor.

Analysis of failure characteristics during the repair process highlights
common issues such as proposed repairs failing assertions and syntax errors,
with observed transitions between failure categories over iterative prompting.

###  5.5. Results for RQ5: Repair Costs

To assess the financial implications of utilizing the APR pipeline with
different LLMs, we consider two primary cost factors: (i) time taken for bug
resolution and (ii) monetary expenses associated with token consumption, based
on OpenAI’s pricing as of March 2024.

Time Analysis: We measure the time taken for bug resolution using the results
presented in Table 6, which leverages GPT-4 models. Figure 6 illustrates the
runtime analysis, contrasting fixed and unfixed scenarios. Across different
settings, the median duration required for bug repair varies from 37.3 seconds
in Setting-1 to 120.3 seconds in Setting-3. Notably, the maximum time spent on
repairs reached 493.28 seconds in Setting-5. Conversely, the median duration
associated with unfixed bugs amounted to 273.8 seconds and 392.2 seconds in
Settings-1 and 4, respectively.

Figure 6. Distribution of running time across all settings for fixed bugs
(left) and unfixed bugs (right).

Monetary Costs: Figure 7 presents the monetary costs incurred under each
setting for both fixed and unfixed models. Settings utilizing GPT-4-Turbo show
the lowest costs for both fixed and unfixed models, attributed to the cheaper
cost per token for GPT-4-Turbo compared to GPT-4-32k. Additionally, settings
employing the prompt-agent (Settings-3 and 6) exhibit marginally higher costs
than their counterparts utilizing the same LLM.

Figure 7. Monetary distribution across all settings for fixed bugs (left) and
unfixed bugs (right).

The analysis of repair costs in RQ5 reveals variations in both time and
monetary expenses across different settings, with GPT-4-Turbo exhibiting the
lowest costs for bug resolution, and settings utilizing the prompt-agent
showing slightly higher expenses.

##  6\. Threats to Validity

Internal Validity. Variations in prompt design and format may introduce biases
in the repair process, affecting the outcomes independently of the LLM’s
capabilities. To mitigate this threat, we carefully standardized the prompt
design across all experiments, ensuring consistency in the information
provided to the LLMs. Additionally, we conducted analyses to assess the impact
of prompt variations on repair performance, enabling us to isolate the effects
of LLM capabilities from potential biases introduced by prompt design.

External Validity. The generalizability of our findings may be limited by the
specific characteristics of the benchmarks used. To address this, we utilized
diverse benchmark suites and evaluated the performance of the repair pipeline
across various scenarios. Furthermore, we documented the experimental setup
comprehensively to facilitate replication and external validation of our
results.

Construct Validity. Biases in the measurement of repair performance metrics
could distort our assessment of LLM capabilities. To mitigate this, we
employed standardized metrics and conducted sensitivity analyses to validate
the robustness of our findings. Additionally, we ensured transparency and
reproducibility in our methodology to enhance the validity of our
measurements.

##  7\. Related Work

Several recent studies have explored the integration of Large Language Models
(LLMs) into software engineering tasks, particularly in the realm of program
repair. Xia et al. (Xia and Zhang, 2023) enhanced automated program repair
(APR) performance by incorporating test feedback into prompts, while Kang et
al. (Kang et al., 2023) enabled LLMs to utilize a debugger for information
gathering and patch generation. Additionally, Fuzz4All (Xia et al., 2024)
leverages LLMs as an input generation and mutation engine, employing an auto-
prompting phase to generate concise input prompts. RepairAgent (Bouzenia et
al., 2024) employs LLMs, agents, and dynamic prompts for APR, albeit in the
context of repairing Java applications. TestPilot (Schäfer et al., 2024)
utilizes LLMs for generating unit test cases for JavaScript, employing a few-
shot learning approach to refine prompts with failing tests and error
messages.

In contrast to these efforts, our study focuses specifically on using LLMs for
automated specification repair (ASR), a less explored area in software
engineering. We adopt an approach similar to Fuzz4All’s auto-prompting phase,
albeit with modifications to suit the requirements of repairing Alloy
declarative specifications. Moreover, while existing works predominantly use
LLMs for program repair in imperative languages like Java and JavaScript, our
study extends the application of LLMs to the domain of Alloy specifications,
addressing a gap in the literature regarding ASR techniques for declarative
languages.

##  8\. Conclusion

In this study, we explore the potential of pre-trained LLMs to facilitate the
repair of Alloy specifications, taking into account recent advancements in
LLMs, including the use of agents, feedback mechanisms, zero-shot learning
capabilities, and auto-prompting techniques. The comparative evaluation
highlights the superior performance of the GPT-4 model family over
GPT-3.5-Turbo, underscoring their promising applicability. The investigation
reveals that employing a multi-agent repair pipeline enhances the repair
process, albeit with a marginal increase in token consumption. Overall, the
findings of this research indicate a positive outlook for the application of
LLMs in automated program repair for declarative specifications, particularly
through repair pipelines that integrate contemporary innovations in the field
of LLMs.

## References

  * (1)
  * Aut ([n. d.]) [n. d.].  _AutoGPT_.  [Accessed: 30-03-2024].
  * All ([n. d.]) [n. d.].  _D. Jackson, Software Abstractions, 2nd ed. MIT Press, 2012._
  * Che (2021) 2021\.  Evaluating Large Language Models Trained on Code.  _ArXiv_ abs/2107.03374 (2021).  https://api.semanticscholar.org/CorpusID:235755472
  * lan (2024) 2024\.  _Langroid_.  https://github.com/langroid/langroid Accessed: 2024-02-27.
  * Alhanahnah et al. ([n. d.]) Mohannad Alhanahnah, Clay Stevens, and Hamid Bagheri. [n. d.].  Scalable analysis of interaction threats in IoT systems. In _ISSTA’20: 29th ACM SIGSOFT_. 272–285.
  * Bagheri et al. ([n. d.]) Hamid Bagheri, Eunsuk Kang, and Niloofar Mansoor. [n. d.].  Synthesis of assurance cases for software certification. In _ICSE-NIER 2020: 42nd International Conference on Software Engineering, New Ideas and Emerging Results, Seoul, South Korea, 27 June - 19 July, 2020_. ACM, 61–64.
  * Bagheri et al. (2016) Hamid Bagheri, Alireza Sadeghi, Reyhaneh Jabbarvand, and Sam Malek. 2016.  Practical, Formal Synthesis and Automatic Enforcement of Security Policies for Android. In _Proceedings of DSN_. 514–525.
  * Bagheri et al. (2021) Hamid Bagheri, Jianghao Wang, Jarod Aerts, Negar Ghorbani, and Sam Malek. 2021.  Flair: efficient analysis of Android inter-component vulnerabilities in response to incremental changes.  _Empir. Softw. Eng._ 26, 3 (2021), 54.
  * Bouzenia et al. (2024) Islem Bouzenia, Premkumar Devanbu, and Michael Pradel. 2024.  RepairAgent: An Autonomous, LLM-Based Agent for Program Repair.  arXiv:2403.17134 [cs.SE]
  * Brida et al. (2021) Simón Gutiérrez Brida, Germán Regis, Guolong Zheng, Hamid Bagheri, ThanhVu Nguyen, Nazareno Aguirre, and Marcelo Frias. 2021.  Bounded Exhaustive Search of Alloy Specification Repairs. In _Proceedings of the 43rd International Conference on Software Engineering_ (Madrid, Spain) _(ICSE ’21)_. IEEE Press, 1135–1147.  https://doi.org/10.1109/ICSE43902.2021.00105
  * Brown et al. (2020) Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. 2020\.  Language models are few-shot learners.  _Advances in neural information processing systems_ 33 (2020), 1877–1901.
  * Bubeck et al. (2023) Sébastien Bubeck, Varun Chandrasekaran, Ronen Eldan, Johannes Gehrke, Eric Horvitz, Ece Kamar, Peter Lee, Yin Tat Lee, Yuanzhi Li, Scott Lundberg, Harsha Nori, Hamid Palangi, Marco Tulio Ribeiro, and Yi Zhang. 2023.  Sparks of Artificial General Intelligence: Early experiments with GPT-4.  arXiv:2303.12712 [cs.CL]
  * Chase (2022) Harrison Chase. 2022.  _LangChain_.  https://github.com/langchain-ai/langchain Accessed: 2024-02-27.
  * Chowdhery et al. (2022) Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, Parker Schuh, Kensen Shi, Sasha Tsvyashchenko, Joshua Maynez, Abhishek Rao, Parker Barnes, Yi Tay, Noam Shazeer, Vinodkumar Prabhakaran, Emily Reif, Nan Du, Ben Hutchinson, Reiner Pope, James Bradbury, Jacob Austin, Michael Isard, Guy Gur-Ari, Pengcheng Yin, Toju Duke, Anselm Levskaya, Sanjay Ghemawat, Sunipa Dev, Henryk Michalewski, Xavier Garcia, Vedant Misra, Kevin Robinson, Liam Fedus, Denny Zhou, Daphne Ippolito, David Luan, Hyeontaek Lim, Barret Zoph, Alexander Spiridonov, Ryan Sepassi, David Dohan, Shivani Agrawal, Mark Omernick, Andrew M. Dai, Thanumalayan Sankaranarayana Pillai, Marie Pellat, Aitor Lewkowycz, Erica Moreira, Rewon Child, Oleksandr Polozov, Katherine Lee, Zongwei Zhou, Xuezhi Wang, Brennan Saeta, Mark Diaz, Orhan Firat, Michele Catasta, Jason Wei, Kathy Meier-Hellstern, Douglas Eck, Jeff Dean, Slav Petrov, and Noah Fiedel. 2022.  PaLM: Scaling Language Modeling with Pathways.  arXiv:2204.02311 [cs.CL]
  * Fan et al. (2023) Zhiyu Fan, Xiang Gao, Martin Mirchev, Abhik Roychoudhury, and Shin Hwei Tan. 2023.  Automated Repair of Programs from Large Language Models.  arXiv:2205.10583 [cs.SE]
  * Gutiérrez Brida et al. (2023) Simón Gutiérrez Brida, Germán Regis, Guolong Zheng, Hamid Bagheri, Thanhvu Nguyen, Nazareno Aguirre, and Marcelo Frias. 2023.  ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications. In _Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering_ _(ASE ’22)_. Association for Computing Machinery, New York, NY, USA, Article 55, 13 pages.  https://doi.org/10.1145/3551349.3556944
  * Hasan et al. (2023) Md Rashedul Hasan, Jiawei Li, Iftekhar Ahmed, and Hamid Bagheri. 2023.  Automated Repair of Declarative Software Specifications in the Era of Large Language Models.  arXiv:2310.12425 [cs.SE]
  * Jackson (2006) Daniel Jackson. 2006.  _Software Abstractions - Logic, Language, and Analysis_.  MIT Press.
  * Jain et al. (2022) Naman Jain, Skanda Vaidyanath, Arun Iyer, Nagarajan Natarajan, Suresh Parthasarathy, Sriram Rajamani, and Rahul Sharma. 2022.  Jigsaw: Large Language Models Meet Program Synthesis. In _Proceedings of the 44th International Conference on Software Engineering_ (Pittsburgh, Pennsylvania) _(ICSE ’22)_. Association for Computing Machinery, New York, NY, USA, 1219–1231.  https://doi.org/10.1145/3510003.3510203
  * Kang et al. (2023) Sungmin Kang, Bei Chen, Shin Yoo, and Jian-Guang Lou. 2023.  Explainable Automated Debugging via Large Language Model-driven Scientific Debugging.  arXiv:2304.02195 [cs.SE]
  * Khurshid and Marinov (2004) Sarfraz Khurshid and Darko Marinov. 2004.  TestEra: Specification-based Testing of Java Programs Using SAT.  _Automated Software Engineering_ 11 (2004).
  * Kong et al. (2024) Jiaolong Kong, Mingfei Cheng, Xiaofei Xie, Shangqing Liu, Xiaoning Du, and Qi Guo. 2024.  ContrastRepair: Enhancing Conversation-Based Automated Program Repair via Contrastive Test Case Pairs.  _arXiv preprint arXiv:2403.01971_ (2024).
  * Liu et al. (2024) Zhijie Liu, Yutian Tang, Meiyun Li, Xin Jin, Yunfei Long, Liang Feng Zhang, and Xiapu Luo. 2024.  LLM-CompDroid: Repairing Configuration Compatibility Bugs in Android Apps with Pre-trained Large Language Models.  arXiv:2402.15078 [cs.SE]
  * Macedo et al. (2021) Nuno Macedo, Alcino Cunha, José Pereira, Renato Carvalho, Ricardo Silva, Ana C.R. Paiva, Miguel Sozinho Ramalho, and Daniel Silva. 2021.  Experiences on Teaching Alloy with an Automated Assessment Platform.  _Sci. Comput. Program._ 211, C (nov 2021), 21 pages.  https://doi.org/10.1016/j.scico.2021.102690
  * Madaan et al. (2023) Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, Shashank Gupta, Bodhisattwa Prasad Majumder, Katherine Hermann, Sean Welleck, Amir Yazdanbakhsh, and Peter Clark. 2023.  Self-Refine: Iterative Refinement with Self-Feedback. In _Thirty-seventh Conference on Neural Information Processing Systems_.
  * Mirzaei et al. (2016) Nariman Mirzaei, Joshua Garcia, Hamid Bagheri, Alireza Sadeghi, and Sam Malek. 2016.  Reducing Combinatorics in GUI Testing of Android Applications. In _Proceedings ICSE_. 559–570.
  * OpenAI ([n. d.]) OpenAI. [n. d.].  New models and developer products announced at DevDay — openai.com.  https://openai.com/blog/new-models-and-developer-products-announced-at-devday.  [Accessed 29-03-2024].
  * OpenAI (2023) OpenAI. 2023.  GPT-4 Technical Report.  arXiv:2303.08774 [cs.CL]
  * Paul et al. (2023) Rishov Paul, Md. Mohib Hossain, Mohammed Latif Siddiq, Masum Hasan, Anindya Iqbal, and Joanna C. S. Santos. 2023.  Enhancing Automated Program Repair through Fine-tuning and Prompt Engineering.  arXiv:2304.07840 [cs.LG]
  * Schäfer et al. (2024) Max Schäfer, Sarah Nadi, Aryaz Eghbali, and Frank Tip. 2024.  An Empirical Evaluation of Using Large Language Models for Automated Unit Test Generation.  _IEEE Transactions on Software Engineering_ 50, 1 (2024), 85–105.  https://doi.org/10.1109/TSE.2023.3334955
  * Shinn et al. (2024) Noah Shinn, Federico Cassano, Ashwin Gopinath, Karthik Narasimhan, and Shunyu Yao. 2024.  Reflexion: Language agents with verbal reinforcement learning.  _Advances in Neural Information Processing Systems_ 36 (2024).
  * Thoppilan et al. (2022) Romal Thoppilan, Daniel De Freitas, Jamie Hall, Noam Shazeer, Apoorv Kulshreshtha, Heng-Tze Cheng, Alicia Jin, Taylor Bos, Leslie Baker, Yu Du, et al. 2022\.  Lamda: Language models for dialog applications.  _arXiv preprint arXiv:2201.08239_ (2022).
  * Vaswani et al. (2017) Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. 2017.  Attention is all you need.  _Advances in neural information processing systems_ 30 (2017).
  * Wang et al. (2019) Kaiyuan Wang, Allison Sullivan, and Sarfraz Khurshid. 2019.  ARepair: A Repair Framework for Alloy. In _2019 IEEE/ACM 41st International Conference on Software Engineering: Companion Proceedings (ICSE-Companion)_. 103–106.  https://doi.org/10.1109/ICSE-Companion.2019.00049
  * Wang et al. (2023) Lei Wang, Chen Ma, Xueyang Feng, Zeyu Zhang, Hao Yang, Jingsen Zhang, Zhiyuan Chen, Jiakai Tang, Xu Chen, Yankai Lin, et al. 2023\.  A Survey on Large Language Model based Autonomous Agents.  _arXiv e-prints_ (2023), arXiv–2308.
  * Xia et al. (2024) Chunqiu Steven Xia, Matteo Paltenghi, Jia Le Tian, Michael Pradel, and Lingming Zhang. 2024.  Fuzz4All: Universal Fuzzing with Large Language Models. In _Proceedings of the 46th International Conference on Software Engineering_ _(ICSE ’24)_.
  * Xia and Zhang (2023) Chunqiu Steven Xia and Lingming Zhang. 2023.  Conversational Automated Program Repair.  arXiv:2301.13246 [cs.SE]
  * Zhang et al. (2023) Quanjun Zhang, Chunrong Fang, Yuxiang Ma, Weisong Sun, and Zhenyu Chen. 2023.  A Survey of Learning-based Automated Program Repair.  _ACM Trans. Softw. Eng. Methodol._ 33, 2, Article 55 (dec 2023), 69 pages.  https://doi.org/10.1145/3631974
  * Zhang et al. (2024) Yuntong Zhang, Haifeng Ruan, Zhiyu Fan, and Abhik Roychoudhury. 2024.  AutoCodeRover: Autonomous Program Improvement.  _arXiv preprint arXiv:2404.05427_ (2024).
  * Zheng et al. (2022) Guolong Zheng, ThanhVu Nguyen, Simón Gutiérrez Brida, Germán Regis, Nazareno Aguirre, Marcelo F. Frias, and Hamid Bagheri. 2022.  ATR: Template-Based Repair for Alloy Specifications. In _Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis_ _(ISSTA 2022)_. Association for Computing Machinery, New York, NY, USA, 666–677.  https://doi.org/10.1145/3533767.3534369
  * Zhou et al. (2023a) Wangchunshu Zhou, Yuchen Eleanor Jiang, Long Li, Jialong Wu, Tiannan Wang, Shi Qiu, Jintian Zhang, Jing Chen, Ruipu Wu, Shuai Wang, Shiding Zhu, Jiyu Chen, Wentao Zhang, Ningyu Zhang, Huajun Chen, Peng Cui, and Mrinmaya Sachan. 2023a.  Agents: An Open-source Framework for Autonomous Language Agents.  arXiv:2309.07870 [cs.CL]
  * Zhou et al. (2023b) Wangchunshu Zhou, Yuchen Eleanor Jiang, Long Li, Jialong Wu, Tiannan Wang, Shi Qiu, Jintian Zhang, Jing Chen, Ruipu Wu, Shuai Wang, Shiding Zhu, Jiyu Chen, Wentao Zhang, Ningyu Zhang, Huajun Chen, Peng Cui, and Mrinmaya Sachan. 2023b.  Agents: An Open-source Framework for Autonomous Language Agents.  arXiv:2309.07870 [cs.CL]