Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages
Authors: Federico Mora
Justin Wong
Haley Lepe
Sahil Bhatia
Karim Elmaaroufi
George Varghese
Joseph E. Gonzalez
Elizabeth Polgreen
Sanjit A. Seshia
Venue: NeurIPS 2024 poster (2024)
Keywords: Text-to-Code
Low-Resource Programming Languages
MAX-SAT
Parsing
Program Repair
Primary area: machine_learning_for_other_sciences_and_fields
TL;DR: Design an intermediate language and use a MAX-SAT solver to improve LLM-based text-to-code for very low resource programming langauges.

Abstract: Recent advances in large language models (LLMs) for code applications have demonstrated remarkable zero-shot fluency and instruction following on challenging code related tasks ranging from test case generation to self-repair. Unsurprisingly, however, models struggle to compose syntactically valid programs in programming languages unrepresented in pre-training, referred to as very low-resource Programming Languages (VLPLs). VLPLs appear in crucial settings, including domain-specific languages for internal tools, tool-chains for legacy languages, and formal verification frameworks. Inspired by a technique called natural programming elicitation, we propose designing an intermediate language that LLMs ``naturally'' know how to use and which can be automatically compiled to a target VLPL. When LLMs generate code that lies outside of this intermediate language, we use compiler techniques to repair the code into programs in the intermediate language. Overall, we introduce _synthetic programming elicitation and compilation_ (SPEAC), an approach that enables LLMs to generate syntactically valid code even for VLPLs. We empirically evaluate the performance of SPEAC in a case study for the UCLID5 formal verification language and find that, compared to existing retrieval and fine-tuning baselines, SPEAC produces syntactically correct programs more frequently and without sacrificing semantic correctness.

Synthetic Programming Elicitation for Text-to-Code in Very Low-Resouree Programming and Formal Languages
Federico Mora'
Justin Wong' Haley Lepe" Sahil Bhatia' Karim Elmaaroufi
George Varghese Joseph E. González' Elizabeth Polgreen' Sanjit A. Seshia'
UC Berkeley Stanford University UCLA *University of Edinburgh
{fmora, justin. wong, sahilbhatia, k.e, jegonzal, (heshia)@berkeleer edu halepe@stanford. edu, varghesedcs ucla. edu, elth,elia elizabeth, polgreenced uk
Abstract
Recent advances large language models (LLMs) for code applications have demonstrated remarkable zero-shot fluency and instruction following on challeng- ing code related tasks ranging from test case generation to self-repair. Unsur- prisingly, however, models struggle to compose syntactically valid programs in programming languages unrepresented in pre-training, referred as very low- resource Programming Languages (VLPLs). VLPLs appear in crucial settings, including domain-specinn languages for internal tools, tool-chains for legacy lan- guages, and formal verification frameworks. Inspired by a technique called natural programming elicitation, we propose designing an intermediate language that LLMs "naturally" know how to and which can be automatically compiled a target VLPL. When LLMs generate code that lies outside of this intermediate language,
compiler techniques to repair the code into programs in the inter- mediate language. Overall, we introduce synthetic programming elicitation and compilation (SPEAC), an approach that enables L.LMs to generate syntactically valid code even for sL.PL.. We empirically evaluate the performance of SPEAC in case study for the UCLID5 formal verification language and find that, com- pared to existing retrieval and fine-tuning baselines, SPEAC produces syntactically correct programs more frequently and without sacrificing semantic correctness.
Introduction
Large language models (LLMs) have demonstrated an exceptional ability to generate code from natu- ral language prompts for popular programming languages, like Python and Java [13] Unfortunately. these same language models struggle to generate code for low-resource programming languages, like many domain-specifi, languages (e.g., CUDA [40]). These challenges are even more pronounced for very low-resource programming languages (VLPLs) (e.g., formal verification languages like UCLIDS [34] (. Existing work has attempted remedy this issue through prompting, constrained decoding, and fine-tuning strategies. Unfortunately, these approaches fail to capture the intricacies of real VLPLs and success remains limited. To see why, consider the following three exemplars.
First, Wang at [42 include context-free grammars in text-to-code prompts to guide LLMs toward syntactically correct answers. This approach works well for simple languages but cannot capture many programming languages that are context-sensitive. Second, Agrawal al. [ use static analysis techniques to reject tokens that lead to syntactically incorrect output programs. This technique can go beyond context-free languages but assumes a linear programming process. Unfortunately. it is well known that the root cause of a programming error need not surface it is written [32), necessitating
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

backtracking and a nonlinear programming process. Third, Cassano et al. [ translate training data from high resource languages low resource languages and then use this new data to fine-tune models. This approach is restricted to languages where the LIM is able to translate to the language reliably but unable to generate code from natural language. Further, this approach makes the overly restrictive assumption that the target low-resource language is general purpose: e.g., we cannot translate arbitrary Java programs to CUDA.
In this paper, we propose a text-to-code approach that is fundamentally different (and complementary) to prompting, decoding, and fine-tuning strategies. The first key idea behind our approach comes from natural programming elicitation, a kind of study that helps programming language designers understand how programmers "naturally" approach problems from given programming domain [29 I.. Programming language designers use the results of these studies to create languages that are aligned with the expectations of users, leading to less programming friction and more effective developers. We borrow this idea for the setting where L.MSs are the "users" of programming languages. Akin to uncovering what human users find "natural" for a given domain, we uncover what LLMs find "natural." Specifically, our first insight is to embrace LLM's tendencies and design an intermediate language that aligns with these LLM expectations.
The second key idea in our approach is that program analyses and repair that are overly aggressive for human users may be suitable for LLM "users." For example, in UCLIDS, all variables have to be declared and statically typed: an assignment like x = 0; would require a corresponding declaration like var x: integer; But, if an LLM generates code that had an assignment without a declaration, instead of crashing, one could automatically "repair" the program and output the result.
We use these two ideas to define new text-to-code approach called synthetic programming elicitation and compilation (SPEAC, pronounced "speak"). Specifically, for a target VLPL I', we use synthetic programming elicitation to select an intermediate language P (the "parent" language) and define subset of the language C' (the "child" language). The language P should be one that LLMs are good at generating (e.g. Python); the language C should be easy to compile to the target VLPL T. Our approach takes P, C, and a compiler from C' to T, and produces a text-to-code pipeline for the VLPL T. This pipeline uses deductive techniques to automatically repair programs generated by LLMs that are in P but not in C. When these deductive techniques are unable to fully repair a program, we insert a "hole" and ask an L.LM to finish the repair, repeating as necessary.
We demonstrate the effectiveness of this idea by implementing a prototype, called Eudoxus, that targets UCLID5 34 (7], language used for formal modeling and verification of state transition systems, UCLIDS has code examples numbering in the hundreds rather than thousands or millions. Furthermore, UCLIDS programs rely heavily on the notion of transition system, which is not frequently found in other programming languages. As such, state-of-the-art LLMs are unable to generate any useful UCLIDS code out-of-the of-tth---oox (see $5.I). In our case study, we use Python as the parent language P and a subset of Python as the child language C, and improve the performance of LLM code generation for UCLIDS.
Overall, we make the following contributions: 1) We present SPEAC, a novel method for generating syntactically correct code from LLMs in very low resource programming languages; 2) We implement this method for the UCLID5 verification language; and 3) We demonstrate substantial improvement with SPEAC in syntactic correctness, producing parsable code in UCLID5 84.8% of the time compared to 9.1 % by gpt-3.5-turbo fine-tuning and 12. 1 % by gpt-4-turbo in-context learning.
2 Related Work
LLMs for Code Generation. Modern language models perform exceptionally well natural
language to code generation tasks. For example, proprietary models like GPT-4 [3]], the Gemini [4]
and Claude 3 Families [ and open-source models such as Code-Llama (35] and Deepseek-Coder (20
have achieved impressive success on benchmarks such as HumanEval [13] Mostly Basic Python
Problems (MBPP) [3 and LiveCodeBench 22 However, LLMs perform better on popular program-
ming languages that are well represented in training sets (e.g., Python) than less popular programming
languages (e.g., Bash) 20 26 33 This effect is even more pronounced for very low resource
programming languages, like UCLIDS, as shown in 6
http://www.aahhppgcccoo//essssss

---

Model state machine describing traffic light at a pedestrian crosswalk. This is a time triggered machine that assumes it will react once second. It starts in the red state and counts 60 seconds with the help of the variable count. It then transitions to green, where it will remain until the pure input pedestrian is present. That input is generated by some other subsystem that detects when pedestrian present, and should be modelled as nondeterministic. When pedestrian is present, the machine transitions to yellow if it has been green for least 60 seconds. Otherwise, transitions to pending, where stays for the remainder of the 60 second interval. This ensures that once the light goes green, it stays green for at least 60 seconds, At the end of 60 seconds, will transition to yellow..
module TrahticLight
var sigG, sigR, sigY: boolean:
var count, state: integer;
var pedestrian: boolcan; init
sigG false; sigY = false; sigR true;
state 0; count = pedestrian false;
procedure step()
modifies sigG; modifies sigY; modifies sigR;
modifies count; modifies state;
10
(state ==
sigG = false; sigY = false; sigR = true;
12
count 0;
13
if (count 60) count (count 1);
14
else state 1:]]
else if (state == 1)
sigR = false; sigY false; sigG true; if (pedestrian) if (count >= 60) state
17
18
19
else state = 3: }}]
21
(b)
Figure Partial task description from Lee and Seshia [23 (a) and partial output of Eudoxus in UCLIDS (b). We interpret sigG, sigR, sigY to represent green, red, and yellow light signals, respectively. The procedure step captures the transition relation of the state machine. state appears to be bookkeeping variable that is used to track the cases in the task, and count represents timer.
Training Free Approaches for Low-Resource Programming Languages. In constrained decoding, syntactically incorrect code is avoided by rejecting impossible prefixes, without producing the full code [18 1 36 27 In the context of autoregressive LLMs that naturally produce code left to right, it remains an open problem how best include the inductive bias of grammar. Bhatia al. [8 use LLMs to rewrite existing code into domain-specific languages and prove that the translation is correct.
Misu al. (28) use retrieval-augmentee generation to write Dafny code, another low-resource language for verification [25]. Unlike these works, we focus very low resourced languages (VL.PLs), which have far fewer training examples in the public domain. Our approach is most similar to techniques that allow LLMs to hallucinate but iteratively repair errors [38] [4] (3). For example, Elmaaroufi et al. [16] use a mixture of prompting and compiler feedback to generate and iteratively repair Scenic code probabilistic VLPL that looks like Python [17]
Training LLMs for Low-Resuurce Programming Languages. Recent work has considered aug- menting LLMs with support for low-resource programming languages [10 20). Chen et al. [12] show that, on smaller 125M parameter encoder-only models, fine-tuning on adjacent languages improves the monolingual performance coding tasks. Synthetic fine-tuning datasets curated and cleaned by LLMS have shown promise for programming tasks. For example, Cassano al. [T]] targets low-resource programming languages (e.g.. Julia), using LLM to translate code examples from high-resource languages to the low-resource language. This process is promising for cases where the language model already has bascline knowledge necessary to translate the low-resource language and the target language general purpose, which is not always the case for VLPLs.
3 Overview and Running Example
Given a natural language description of programming task and target programming language T, the text-to-code problem is to generate a program T that satisfies the task specification. Fig. [hoows a real input-output pair generated by an instance of our approach targeting the UCLIDS programming language. Specifically, Fig. Ta shows a task extracted from Lee and Seshia 23]. and
Fig. Th shows the output corresponding to that task using prototype implementation of our approach.
Fig. lb passes all compiler checks but has subtle semantic mistake line 4.
3

---

Repair
p'
Largest
Model-
Has Holes?
No.
1(p')
LLM
Consissennt
Driven
Subtree
Repair
Yes
Figure 2: The SPEAC workflow. Users input q, task in natural language, and C, description of the intermediate language. The L.M takes these inputs and generates a program P. We use formal techniques repair p and produce p', a program in C. that possibly contains holes. If pf does not contain holes, SPEAC applies f. a compiler from C' to the target language, T, and returns the result. Otherwise, SPEAC generates new prompt, q', and repeats by asking the LLM fill in the holes.
Fig. 2 shows the workflow that generates models based on task descriptions as shown in Fig. lb The workflow is parameterized by an LLM, L (e.g., ppt-3.5-turbo-0125) target language, T (e.g.. UCLID5); parent language, P (e.g., Python); a child language, C C P (e.g., subset of Python); and a compiler. f. from C to T (e.g., syntax -iireetdd translation from the subset of Python to UCLID5). Given an input task, we create prompt q that asks the LLM L to generate code, which satisfies the task description, q. The second step of the workflow to repair p. If there nothing wrong with or p can be fixed using formal techniques described in $5.3 and $5.4) then repairing will generate a new, complete program p' and return f(p') (i.e., a program in the target language, like Fig. lb). Frequently, however, repairing will generate partial program containing "holes" (denoted "??"). For example, Fig. 5 shows the first p generated for the task in Fig. Ta and 5 shows the corresponding partial program y/ that was automatically generated using our formal techniques. Programs with holes cannot be compiled to the target language, so the third step workflow is ask the LLM to complete the partial program p'. generating in Fig. 4b to generate the LLM prompt. Fig. 6a shows the output generated by gpt-3.5- 1at.3..5tturbo00111 when asked to repair the partial program in Fig. [a This program is still incorrect, but, it is close enough that we can automatically repair it to a complete program without holes. Fig. 6b shows the relevant portion of that complete program. This final, complete program is directly translated to the output in Fig. 1b elabboraee on each of the workflow components.
C,
p. We use the template
To understand the subtle mistake in Fig. Tb one needs some understanding of UCLIDS 34 UCLIDS verification language used to model hardware and software systems as "state machine" like transition systems and to automatically check if the transition system does indeed satisfy formal logic specification. UCLIDS transition systems primarily consist a state space given by a set of variable declarations (e.g.. lines 2-4 in Fig. Ib]. an initialization block that represents set of acceptable start states (c.g.. lines 5-7 Fig. [b]. and a transition relation block that defines how the transition system moves from one state to the next state (e.g., code starting line 8 in Fig. [b). The var keyword used to declare variables that are internal to the transition system in question while the input keyword is used to declare read-only variables that outside the control of the transition system in question. Fig. [b]ppases all compiler checks but has a subtle semantic mistake on line 4: var pedestrian: boolean; should be input pedestrian: boolean; because the presence of a pedestrian should not be controlled by the traffic light transition system. When manually assessing correctness $6 this subtle mistake would prevent from marking this example as fully correct.
37
Background
In this section we provide the necessary technical background to understand the formal techniques that are used in our approach and are described in $5.3 and $5.4
4.1 Algebraic Data Types and Abstract Syntax Trees
Algebraic data types (ADTs) representation of finite trees that common in functional programming languages. We provide an informal definition of ADTs and point the interested reader to Barrett al. (6] for more formal treatment.
An ADT consists of a set of constructors (node names), selectors (directed edge names), and testers (predicates). Each constructor has fixed set of selectors associated with it (possible edges out).

---

from FormalVeriiicationLiiaa import Module # GTCODE I: imports class from the hypothetical library Module("my Module") GTCODE 2: creates an instance of imported class
print(m) # GTCODE 3: uses a dunder method (in this case _xtr of an imported class
Figure 3: Hypothetical LLM output with grounded theory codes as comments. Codes are determined and assigned manually.
Each selector has an associated type (each edge can only point to a fixed set of node names). Every constructor associated with exactly one unique tester: that tester returns true on a given tree iff the root of the tree is labeled with the corresponding constructor. Every instance of an ADT (a particular finite tree built from those node and edge names) must be acyclic.
Abstract syntax trees (ASTs) are instances of ADTs-i.c. ASTs are concrete finite trees-that represent programs. Every programming language has corresponding ADT that represents superset of all possible programs in that programming language. Some instances of languages's ADT will not correspond to valid programs, e.g.. if they do not additionally type check.
4.2 Satisfiability Modulo Theories and Weighted Maximum Satisfiability
Satisfiability Modulo Theories (SMT) is a class of problems generalizing Boolean satisfiability (SAT) to first-order logics with additional background logical theories. We give an informal presen- tation of satisfiability modulo theories (SMT) that focuses on only the theory ADTs and covers weighted maximum satisfiability (MAX-SMT). Further details may be found in book chapter (7].
Let I be set of ADTs and let V be set of typed variables (pairs of names and types). For simplicity we assume that variable types are exactly elements of I'. In reality, variables can also have function types (c.g., V = [(z, Bool), (f, Bool Bool)} would be fine). An atomic formula an equation or the application of single tester over V (e.g..
True and is__nndn {s] are both atomic formulas). theory literal is an atomic formula or its negation. A clause is set of theory literals. A conjunctive normal form formula, or formula for short, is a set of clauses. For example, if = (Bool) } and mapping from variables to elements of their corresponding type. For example, T(x) = True if x = and T(x) False otherwise, is an interpretation. Interpretations are extended atomic formulas the natural way When an atomic formula & evaluates to true under an interpretation J, we say that T literals, clauses, and formulas in the natural way and reuse the same notation. The satisfiability modulo theories problem is to determine if, for a given formula d, there exists an interpretation / such that / }= Φ. When such an exists we say that is satisfiable (sat). When such exists, we say that & is unsatisfiable (unsat). For example, { {f2 = True), ). [is_And(z)}} is unsat.
V = {(z. Bool)] then {f2 = True), (is__nn((2)) }} is a formula. An interpretation
satisfies @ and write T F Φb We extend the notion of satisfiability
The maximum satisfiability problem is, for given (CNF) formula é. to determine the largest subset of & that sat (solvers aim to satisfy as many clauses as possible). The weighted maximum satisfiability problem (MAX-SMT) is variation with two differences. First, some clauses can be they must be satisfied. Second, every "soft" clause (any clause that is not "hard") has an associated weight. The problem is then to determine subset of é that maximizes the sum of weights while being sat and containing all "hard" clauses.
5 Approach
In this section we describe the SPEAC approach. We begin with how to select P and C ($5.1. We then describe the promoting we use to interface with LLMs ($5.2) and two formal techniques the heart of our automated repair (55. and $5.4)
5.1 Synthetic Programming Elicitation
In this section, present synthetic programming elicitation as kind of programming study-where L.MS are the subject-that follows three steps. The results of these studies are used to select and C. We call this process synthetic programming clicitation since it is inspired heavily by natural
5

---

programming elicitation (2]]. To make this section more concrete, for each step of the study, we describe the specific steps we followed for targeting UCLIDS.
First Step: Setup. First prepare LLM subjects, select a target language, and collect or construct set of programming tasks. In our case, our target language is UCLIDS, our LLM subjects gpt-4-turbo-2024-PP 0000000-200000--0000000 and gpt-3.5-turbo-0123 and our programming tasks are a set of regression tests written by UCLIDS developers with corresponding natural language descriptions that were written by hand (see $6 for more details on all the benchmarks).
The second part of the study setup is to create multiple kinds of specialized prompts. The first will ask for the output to be in the target language directly. Subsequent prompts will ask for the output to use an imaginary API in a popular host language, like Python Java. For example, for UCLIDS, we generated prompts that look like the following.
1. "Write UCLIDS model for system that counts the number of times the temperature exceeds threshold [...]"
2. " Formal Verificattion is a Python library for generating verification models [...]. Use the Formal Verificationnibrant to model system that counts the number of times the temperature exceeds a threshold [...]"'
Second Step: Execute. Now we execute every LLM subject on every prompt and collect the outputs. Each query should be executed independently.
Third Step: Analyze and Design. Finally, we analyze the collected LLM outputs and select P and C' based on the analysis. To do this analysis, we follow lightweight version of grounded theory [9] Seee.g. e.g., Stol et al. [39 for general guidelines on how to use grounded theory in software engineering research. See e.g., Barke et al. [5] for specific, detailed case-study. Synthetic programming elicitation studies are inspired by and borrow many of the methods from those works. Our studies are categorically different, however, because we are not working with humans. We cannot interact with our participants in the same way, e.g., we cannot conduct semi-structured interviews. The goal of our studies is design an intermediate language that more closely matches the code that LLMs tend to generate when compared to our desired target language.
The first step of our lightweight grounded theory analysis is to "code" the outputs generated by the LLMs. In grounded theory parlance. "code" is akin to manually labeling parts of the generated outputs. For example, Fig. shows hypothetical LLM output for our running example along with grounded theory codes as comments. The second step is to group codes into concepts. Concepts are slightly more abstract than codes. For example, concept that may emerge from Fig. Bs the group of codes 1, 2, and 3. The corresponding concept could be "using a class from the hypothetical library." In the third step, we group concepts into categories. For example, we may group concepts related to the object oriented programming paradigm as one category. Finally, we select a P and C' that are consistent with the final categories we observed across multiple prompts.
In our study, we found that, when asked to write UCLIDS code without any special prompting or training, no LLM was able to produce code that parses (660 attempts: 10 samples per LLM per benchmark, 33 benchmarks, two LLMs). Worse still, the code generated by LLMs was inconsistent, with each LLM giving different outputs that resemble different programming languages different times. When asked to write Python code that used a non-existent formal verification API, however, the LLM outputs were more consistent. Therefore, selected Python our parent language, P.
Specifically, the Python code was more consistent because LLM outputs fell into three broad categories, which we call "from-scratch," "procduurrl and "object-oriented"" " respectively. Programs in the "from-scratch" category used cxisting APIs (c.g., the Z3 solver API (I5)) to re-implement what UCLID5 does, e.g., manually model transition systems. This was the smallest significant category. Programs in the "procedural" category imported a class from the hypothetical API, created an instance of it, and then called methods from the class to declare variables, assert specifications and so on. Programs in the "object-oriented" category imported a class from the hypothetical API and extended it, including methods that correspond closely to parts of UCLID5 code. For example, these extended classes often included a method that represented a transition relation a critical component of UCLID5 programs and of transition systems generally.
After analyzing the outputs, we concluded that would be easiest to translate Python programs from the "object-oriented" category to UCLID5. For example, we observed that methods which represent

---

Write [PARENT LANGUAGE] code complete the following task.
Fix the following [PARENT LANGUAGE] code by
replacing every occurrence of "??" with the correct code.
> [TASK GOES HERE]
Reply with your code inside one unique code block
ICODE WITH HOLES GOES HERE]
4
[DESCRIBE CHILD LANGUAGE]
Make sure that your code completes the following task.
I can definitely do that! Here the code:
...
[LINES 2-6 OF (a)]
(a) Template for prompt in Fig. 2
(b) Template for prompt in Fig.
Figure 4: Partial SPEAC prompt templates for first generation (a) and hole filling (b).
transition relations used a limited set of names, and that methods themselves could be compiled to UCLID5 rather directly. Therefore we defined subset of Python that matches the "object-oriented" category and used that as our child language, C. Essentially, C' is an abstract class that the LLM must extend. For example, the abstract class includes an abstract method called "next" that corresponds to the transition relation. Fig. shows a portion of an example of a Python program in C' and Fig. Tb shows a portion of its corresponding UCLID5 program.
5.2 (Minimal) Prompting
After our synthetic programming elicitation study-once P and C have been selected- we use minimal prompting to interface with LLMs. For example, for UCLID5, we use the prompt template in Fig 4 to create initial programs and the prompt template in Fig. tb fill in holes. More advanced prompting techniques are complementary and could help here. However, for this work, we used minimal prompting as to independently evaluate our contribution.
5.3 Largest Consistent Subtree
Given a program in P, but not in C, our aim is to remove as little as possible from to bring it into the language C. That is, given the AST for p. we wish generate the largest subtree of the AST, possibly containing holes, that is not rejected by the static checks of the language C. For example, the code in Fig. [5b contains some errors, including mismatches between variable and constant types (UCLID5 does not automatically cast constants and so the line self count 1 is interpreted as assigning the integer literal 1 to the bitvector variable self count, which is type error).
We find the largest consistent subtree in three steps. First, we use an error tolerant parser to build an AST, A, for the language P. Second, beginning at the root of A, recursively descend and prune anything that cannot exist in an AST for the language C, placing holes wherever they are needed. This is an aggressive program slice, similar Akhundov et al. 2 who give new AST A'. A' may or may not pass compiler checks, like type checking, or be semantically correct.
The third step finds the minimal number of AST nodes that need to be replaced with holes such that all static checks of the language C' pass, using the approach of Pavlinovic et al. [3]. Specifically, for every static check of the language, for every node of the AST, we generate set of soft clauses. Let S be the the union of all the generated clauses, and let S' be the largest subset of clauses that is sat (the output of MAX-SMT solver). Any clause, that appears in S but does not appear in S' represents a bug: if we add to S", then we will get an unsat set of clauses. So, for every such e, we replace the AST node that generated e with hole.
For cxample, in UCLIDS, the two statements var x: bv32; and x O; would produce a set of clauses corresponding to the assertions that (a) x is bitvector and that (b) x is integer (since 0 is an integer). These assertions, together, are unsat, so MAX-SMT would return a set of clauses that does not include both (a) and (b). One solution would be to remove the bitvector type, producing the partial, but consistent, two statements var x: ??; and x 0;-
We can bias the solver to include one or the other by adjusting the weights on the corresponding clauses. practice, we assign clauses weights that are proportional to the depth of the corresponding node in the AST. This ensures that edits are closer to the leafs of the AST but it breaks syntactic minimality guarantees. In the case where weights are uniform and every node corresponds to exactly one clause, the MAX-SMT approach will make the minimal edit to the AST.
7

---

class TrafficLigh((MModlee
24
def next(self):
class TrafiiCLigh(MMouul)
def types(self))
25
if self.state
def locals(self):
self.state = (2)tor
26
self.sigG False
self = int
3
4
def locals(self):
27
self.sigY Y False
self.count int
4
self.state = (2)
28
self.sigR True
self self.pedcstrian bool 5
self.count Vic
29
self.count
def outputs(sclf):
self.pedestrian Boolean()
30
self.count < 60:
self.sigG
self.sigG = Boolean()
31
self.count +=
selfsigY = bool
self.sigY Boolean()
32
clse:
self.sigR bool def init(self):
10
self.sigR= Boolean()
33
self.state
10
def inputs(self):
34
self.state ??
12
self.pedestrian Boolean()
35
elif self.state == 3:
self.count ??
12
13
def outputs(self):
36
self.sigG False
self.pedestrian =
13
14
self.sigG Boolean()
37
self.sigY False
self.sigG ??
14
15
self.sigY Boolcan()
38
self.sigR False
self.sigY ??
15
16
self.sigR Boolean()
39
self.count < 60:
self.sigR ??
16
17
def isil(::
40
self.count +=
def next(self)):
17
18
self.state (ittooc))))))
41
else:
if self = 0:
18
19
self.count Vector)))
42
self.state
self.siGG False
19
20
sedff.pedstrrian Boolcan()
self. False
20
21
self.sigG Boolcan()
self.sigR Truc
21
22
self.sigY = Boolcan()
self self.count 0
22
23
self.sigR Boolean()
23
(b)
Figure 5: Partial response for task in Fig. using gpt-3.5- ppt-3.5-turbo-01255 (a) and partial first repair (b). Line 5 in (a) declares state as a local variable of bit-vr type; lines 25, 33, and 42 use state as an integer. Line 3 in (b) repairs the type of state to be an integer.
5.4 Model-Based Repair
Once we have a satisfiable set of clauses, the model to repair the partial program. This is where our work most differs from Pavlinovic et al. For example, the partial program clauses is (ss_Ineeeee(?) This clause would be satisfied by setting ?? to integer and so we can repair the partial program be var
generate a corresponding satisfying model and use
32
??; from above would correspond to the set of
integer;
Fig. shows one buggy AST (Fig ba) and the corresponding (Fig. 6b count is declared as an integer in the repaired program because it is used as integer in the buggy program. For repairs that cannot be automatically resolved by the MAX-SMT model, we use
For example, the variable
LLM to generate code to replace the AST holes, shown in Fig.
6 Evaluation
In this section, we implement a prototype of SPEAC for UCLIDS, called Eudoxus, and use it to evaluate the performance SPEAC across three research questions. RQI: Does Eudoxus perform better than LLM baselines on syntactic correctness (passing compiler checks)? RQ2: Does Eudoxus perform better on semantic correctness? RQ3: Does MAX-SMT cost too much computation time? Eudoxus uses the P and C' described in $ and is implemented in Python We use tree-sitter to parse to solve MAX-SMP queries. We allow Eudoxus repeat
and search partial programs, and Z3 [5] the repair loop five times. All MAX-SMT queries are solved locally on a 2.3 GHz Quad-Core Intel Core 17 with 32 GB of RAM. All LLM calls are made through the OpenAl Python API.
We compare Eudoxus against three L.M baselines: few-shot, self-repair, and fine-tuning. All using (GPT4t). Few-shot with and without Mhain-of-Thoughe For the few-shot baseline, we provide examples taken from the UCLIDS GitHub repository the LLM in context. We tried with one context example, and then again with three in context examples. We also combine few-shot prompting with Mfain-of-thoughl 44). Fine-tuning
gpt-3.5-turbo-0125 (GPT3t) and opt-44turbo-2024--444
Available att.:e/s//gt.haa..c////e/rrddddd

---

class Tradicc
class TrafficLighh(
def locals(self):
def lseals(self)):
self.state =
self. self.count = int self, self.pedestrian = bool self.sig bool
3
self.count
self.pedestrian Falsc def outputs(self):
5
self.sigR bool
self.sigG False
self.sigY bool
self.sigY = False
self.state int
8
self.sigR= False def init(self):
9
10
def init(selff):
10
self.state =
self.state
11
12
self.count = 0
self.count =
12
13
self.pedestrian = False
self.pedestrian = False
13
14
self.sigG False
self.sigG False
14
15
self.sigY False
self.sigY False
15
16
self.sigR True
self.sigR True
16
17
17
(a)
(b)
Figure 6: Partial response for Fig. 5a using gpt-3.5-turbo-0125 (a) and partial second repair (b). The outputs method should declare variables and their types but on lines 6-9 of (a) it instead assigns variables to values (i.c., False instead bool). The repair in (b) declares these variables with the appropriate types on lines 5-7.
As with many VLPL, there are very limited number of natural language to UCLIDS examples in the public domain, and certainly not enough for fine-tuning. We do, however, have access 317 regression tests from the open- source code base. For the purposes of fine-tuning, we use self- instruct [43] to first ask the model to summarize the UCLIDS regression tests natural language and then provide this as the natural language description during fine-tuning We fine-tune GPT3t for 284 steps with learning-rate multiplier 0.16. Self-repair. We gave the L.MSs compiler feedback in a self-repair loop starting from zero-shot prompt. We use five iterations to be consistent with Eudoxus.
We use three sets of UCLIDS benchmarks. The first set is a curated set of 33 regression tests with handwritten natural language descriptions. These tests are designed to cover a broad range of UCLIDS features and were used for the synthetic programming elicitation study in $ $5. The second set is a set of 317 regression tests without descriptions taken directly from the UCLIDS GitHub repository. These tests were used for fine-tuning our baseline model, as described above. This set is representative of the quantity and quality of data that user may have available for a VLPL. The third and final set a of 33 exercises and examples taken from three textbooks 24 21 These benchmarks cover formal modeling of concurrent systems, linear-time properties, model checking and systems with discrete dynamics. We used this final set for the end-to-end evaluation below.
6.1 Results
We run two variations of Eudoxus (one using GPT3t, one using GPT4t) and 11 variations of the baselines on all 33 textbook benchmarks. We report the fraction of outputs that pass all compiler checks ("parse," for short) and semantic correctness over all approaches in Table [ Semantic correctness is manually assessed by one author using combination of manual reasoning and hand- written specifications for all programs that compile. Correctness is rated on a scale from from 5. where 1 is entirely wrong, and indicates that the model is correct with only a few minor errors (c.g.. the example output described in $ and Fig. 5). Intuitively, any score > 4 indicates that we believe the output would be useful to text-to-code users.
RQ1: Syntactic Correctness. Eudoxus outperforms all baselines in terms of compiler checks (see "Parse Rate" in Table []] passing all compiler checks on 78% of benchmarks. There are four benchmarks on which Eudoxus hits iteration limit and fails to produce a result, and three benchmarks with small syntax enrors due to bugs in our Eudoxus implementation (e.g., failing to extract code snippets from LLM outputs or printing UCLIDS code incorrectly). In contrast, we find that GPT3t and GPT4t rarely produce UCLIDS models that parse. The best results for GPT3t

---

Semantic Score
Parse Rate
2
5
Eudoxus (GPT41)
24/33
1/24
1/24
3/24
8/24
11/24
Eudoxus (GPT31)
28/33
3/28
6/28
5/28
5/28
9/28
Fine-tuned GPT3t
2/33
0
2/2
0
0
0
One-shot with COT (GPT4))
1/33
0
0
0
1/1
0
One-shot with COT (GPT3t)
One-shot (GPT4t)
One-shot (GPT31)
Three-shot with COT (GPT41)
3/33
0
0
00000
2/3
1/3
Three-shot with COT (GPT31)
1/33
0
0
1/1
Three-shot (GPT4)
4/33
0
0
3/4
Three-shot (GPT3))
2/33
0
0
1/2
1/2
Self-repair (GPT4()
0
Self-repair (GPT31)
Table 1: Eudoxus compared to baselines. We report the semantic score over all correctly parsed models. 1 completely wrong; is fully correct. Eudoxus limited five LLM calls per benchmark, and four benchmarks hit this limit.
come from fine-tuning, but it is only able to produce two programs that parse. The best results for GPT4t come from three-shot prompting, but is only able produce four programs that parse. Given this data, we answer RQ1 in the affirmative: Eudoxus perform better than standard LLM baselines on syntactie correctness. Even more interesting. the two versions of Eudoxus generated programs that passed all compiler checks for 30/33 unique problems; the 11 versions of the baselines together generated programs that passed all compiler checks for only 6/33 unique problems.
RQ2: Semantic Correctness. Every unique problem that the baselines perform well on four unique problems where some baseline scored four or higher- was also solved by Eudoxus. These are likely the easiest problems in the test set. On the other hand, 33/52 programs (24 unique problems) that pass compiler checks produced by Eudoxus scored four or higher. This data suggests that our approach does not negatively impact semantic performance, but it is difficult to draw conclusions since so few the programs generated by the baselines pass compiler checks.
RQ3: MAX-SMT Performance. In terms of execution time, Eudoxus with GPT3t took an average of 0.9 seconds (SD 0.6) repair steps and 7.2 seconds (SD 4.6) in LLM calls. Eudoxus with GPT4t took an average of 1.8 seconds (SD 2.0) in repair steps and 35.1 seconds (SD 24.7) in LLM calls. We conclude that, terms of execution time, LLM calls are more expensive than our static repairs.
6.2 Threats to Validity
While our results are promising, there are three limitations to our evaluation. First, we only evaluated SPEAC one VLPL, UCLID5. It remains be seen if our results can be replicated across different VLPLs. especially those in different domains. Second, we only evaluated SPEAC with two LLMs. It possible that our work will not generalize across different kinds LLMs. Third, only one author evaluated the semantic correctness of programs generated by Eudoxus. While the main takeaway of our work is that we are able generate syntactically correct programs where baselines cannot, possible that we have over or under-estimated semantic correctness.
7 Conclusion
We have presented a synthetic program elicitation and compilation method (SPEAC) that supports natural language code generation for very low resource programming languages (VLPLs). The two key ideas behind SPEAC are (1) to design an interface that is "natural" for LLM "users" and (2) use deductive techniques, which could deemed aggressive for human users, automatically repair LLM outputs when possible. We implemented prototype of SPEAC called Eudoxus that targets the UCLID5 VLPL and evaluated it set of 33 benchmarks from textbooks in the same domain as UCLIDS. Eudoxus performs significantly better than standard LLM baselines on syntactic correctness without sacrificing semantic correctness.
10

---

Acknowledgments and Disclosure of Funding
We would like thank Adwait Godbole, Ameesh Shah, Max Willsey, and the anonymous review- ers for their insightful feedback. We would like to thank Justin Lubin for pointing us to natural programming elicitation. Part of this work was done during the Transfer-to-Excelles Research Program at UC Berkeley in 2023 and part during UC Berkeley's s CS 294-260: Declarative Program Analysis and Optimization in 2024. This work was supported part by a Qualcomm Innovation Fellowship. Royal Academy of Engineering Research Fellowship. DARPA Contract PA8750-23-C-0080 (ANSR), C3DTI, an Amazon Research Award, NSF grant 2303564, by Nissan and Toyota under the iCyPhy center, and by Intel under the Scalable Assurance program.
Summer
References
[1] Lakshya Agrawal, Aditya Kanade, Navin Goyal, Shuvendu K Lahiri, and Sriram Raja- mani. Monitor-guided decoding of code LMS with static analysis of repository context. In Thirty-seventh Conference on Neural Information Processing Systems, 2023. URL
https: //obnree//penr.iee... wtt.pppwwww.i.eeeeoooorotaaiaaaa hett/forumiid-qPuukkiitit
[2] Murad Akhundov, Federico Mora, Nick Feng, Vincent Hui, and Marsha Chechik. Verification by gambling on program slices. In Automated Technology for Verification and Analysis: 19th International Symposium, ATVA 2021, Gold Coast, QLD,, Australia, October 18-22, 2021, Proceedings 19, pages 266-282. Springer, 2021.
[3] Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, et al. Program synthesis with large language models. arXiv preprint arXiv:2 (tti::208..07700 007307 2021.
[4] Christel Baier and Joost- Pooste Katoen. Principles of model checking. MIT Press, 2008
[5] Shraddha Barke, Michael B. James, and Nadia Polikarpova. Grounded copilot: How program- mers interact with code-generate generating models. Proc. ACM Program. Lang., 7(00PSLAI), April 2023. doi: 10. 10.1 145/3386600
WtRLhhttps://ddo otttp:://doo.oor//11.. 100/ 0tt.://.....r01..111////33500000 1145/3586030
[6] Clark Barrett, Aaron Stump, Cesare Tinelli, et al. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK), volume 13, page 14, 2010.
[7] Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, chapter 33, pages 1267-1329. IOS Press, second edition, 2021.
[8] Sahil Bhatia, Jie Qiu, Niranjan Hasabnis, Sanjit A. Seshia, and Alvin Cheung. Verified code transpilation with llms, 2024. (tR.sttss::// http:::://xxvivooooo
/ttppp//./ttpps//rrr...oooo org abs/ /406. 03003
[9] Nikolaj Bjømerr Anh-Dung Phan, and Lars Fleckenstein. v/-an optimizing smt solver. In Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015, Held Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings 21, pages 194-199. Springer, 2015.
[10] Federico Cassano, John Gouwar, Francesca Lucchetti, Claire Schlesinger, Carolyn Jane Anderson, Michael Greenberg, Abhinav Jangda, and Arjun Guha. Knowledge transfer from high-resource to low-resource programming languages for code llms. arXiv preprint arXiv:2308.0995 098955 2023.
[11] Sarah E. Chasins, Elena L. Glassman, and Joshua Sunshine. PL and HCI: better together. Commun. ACM, 64(8):98-106 jul 2021. ISSN 0001-0782. doi: 10.1145/3469279. URL https://doi.orge: httg///..14//348800000 1145/3469279
[12] Fuxiang Chen, Fatemeh H Fard, David Lo, and Timofey Bryksin. On the transferability of pre-trained language models for low-resource programming languages. In Proceedings of the 30th IEEE/ACM International Conference on Program Comprehension, pages 401-412, 2022.
11

---

[13] Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et Evaluating large language models trained on code. arXiv preprint arXiv: 10m.03007733374.. 2021.
[14] Xinyun Chen, Maxwell Lin, Nathanael Schärli, and Denny Zhou. Teaching large language models to self-debug. arXiv preprini arXiv:2304. 0522, 2023.
[15] Leonardo De Moura and Nikolaj Bjørner. 73: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008
[16] Karim Elmaaroufi, Devan Shanker, Ana Cismaru, Marcell Vazquez-Chanlatte, Alberto Vinnaannii-iiinteelli, Matei Zaharia, and Sanjit A. Seshia. ScenicNI.: generating probabilis- tic scenario programs from natural language. In Conference on Language Models (COLM), 2024.
[17] Danicl Fremont, Edward Kim, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Alberto L Sangiovanni- Vincentelli, and Sanjit A Seshia. Scenie: A language for scenario specification and data generation. Machine Learning, I 11(110):305-33849 2023.
[18] Saibo Geng, Martin Josifoski, Maxime Peyrard, and Robert West.
decoding for structured NLP tasks without finetuning. In Houda Bouamor, Juan Pino, and Kalika Bali, editors, Proceedings of the 2023 Conference Empirical Methods in Natural Language Processing, pages (932-10952, Singapore, December 2023. Association for Computational Linguistics. doi: (0.18653/v122023.cor http:////00000mmmmmmmmm......... URL haattps://aacaanhhllgg.. org/ 2023 emnlp-main 674
[19] Barney Glaser and Anselm Strauss. Discovery of grounded theory: Strategies for qualitative research. Routledge, 2017.
[20] Daya Guo, Qihao Zhu, Dejian Yang. Zhenda Xie, Kai Dong, Wentao Zhang, Guanting Chen, Xiao Bi, Y Wu, YK Li, et al. Deepseek-coder: When the large language model meets programming-the rise of code intelligence. arXiv preprint arXiv:2401.14190 2024.
[21] Michael Huth and Mark Dermot Ryan. Logic in computer science modelling and reasoning about systems (2, ed.). Cambridge University Press, 2004.
[22] Naman Jain, King Han, Alex Gu, Wen-Ding Li, Fanjia Yan, Tianjun Zhang, Sida Wang, Ar- mando Solar-Lezama, Koushik Sen, and Ion Stoica. Livecodebench: Holistic and contamination free evaluation of large language models for code. arXiv preprint TBV::2003.07974, 2024.
[23] Edward A. Lee and Sanjit A. Seshia. An introductory textbook on cyber-physical systems. In WESE, page 1. ACM, 2010.
[24] Edward A. Lee and Sanjit A. Seshia. Introduction Embedded Systems: A Cyber-Physical Systems Approach. MIT Press, second edition edition, 2016. URL http::ttttsseshhiiiii org.
[25] K. Rustan M Leino. Dafny: An automatic program verifier for functional correctness. In International conference on logic for programming artificial intelligence and reasoning, pages Springer, 2010.
[26] Raymond Li, Loubna Ben Allal, Yangtian Zi, Niklas Muennighoff, Denis Kocetkov, Chenghao Mou. Mare Marone, Christopher Akiki, Jia Li, Jenny Chim, Qian Liu, Evgenii Zheltonozhskii. Terry Yue Zhuo, Thomas Wang, Olivier Dehaene, Mishig Davaadorj. Joel Lamy-Poirier, João Monteiro, al. Starcoder: may the source be with you!, 2023. URL httptttts///rxi..orrr abs/2305. 06161.
[27] Daniel Melcer, Nathan Fulton, Sanjay Krishna Gouda, and Haifeng Qian. Constrained decoding for code language models via efficient left and right quotienting of context-sensitive grammars. arXiv preprint arXiv:2402. 22..224227799 79888, 2024.
[28] Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, and James Noble. Towards ai-assisted synthesis of verified dafny methods. Proc. ACM Softw. Eng. (FFS)), July 2024. doi: 10.1 145/ 3643763, URL https: / //doii orgo 1145/3643763
12

---

[29] Brad A. Myers, John F. Pane, and Amy J. Ko. Natural programming languages and environments. Commun. ACM, 47(9):47-52, sep 2004. ISSN 0001-0782. doi: 10. 10.1145/10158641001535 101588888
htt.ttttt://....om org/ 1145/1015866 1015888
[30] Theo X Olausson, Jeevana Priya Inala, Chenglong Wang, Jianfeng Gao, and Armando Solar- Lezama. Is self-repair a silver bullet for code generation? In The Twelfth International Conference on Learning Representations, 2023.
[31] OpenAI, Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, llge Akkaya, Flo- rencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, Red Avila, Igor Babuschkin, Suchir Balaji, Valerie Balcom, Paul Baltescu, Haiming Bao, Mohammad Bavarian, , et al. Gpt-4 technical report, 2024.
[32] Zvonimir Pavlinovie, Tim King, and Thomas Wies. Finding minimum type error sources. SIGPLAN Not., (0(0))555422 oct 2014, ISSN 0362-1340. doi: 10. 10.1145/27140444266222 URL httpp://doi...ortt
1145/271166444 2660230
[33] Qiwei Peng, Yekun Chai, and Xuhong Li. Humaneval-xl: A multilingual code generation benchmark for cross-lingual natural language generalization, 2024. URL https://arxiv
[34] Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora, and Sanjit A. Seshia. UCLIDS: multi-modal formal modeling, verification, and synthesis. In CAV (!), volume 13371 of Lecture Notes in Computer Science, pages 538-551. Springer, 2022.
[35] Baptiste Roziere, Jonas Gehring, Fabian Gloeckle, Sten Sootla, Itai Gat, Xiaoqing Ellen Tan, Yossi Adi, Jingyu Liu, Tal Remez, Jérémy Rapin, al. Code llama: Open foundation models for code. arXiv preprint arXiv:2308. 12950, 2023.
[36] Torsten Scholak, Nathan Schucher, and Dzmitry Bahdanau. Picard: Parsing incrementally for constrained auto-regressive decoding from language models. arXiv preprint arXiv:2109.05093, 2021.
[37] Sanjit A. Seshia and Pramod Subramanyan. UCLIDS: integrating modeling, verification, synthesis and learning. In MEMOCODE, pages 1-10. IEEE, 2018
[38] Noah Shinn, Federico Cassano, Ashwin Gopinath, Karthik Narasimhan, and Shunyu Yao. Reflexion: Language agents with verbal reinforcement learning. Advances in Neural Information Processing Systems, 36, 2024.
[39] Klaas-Jan Stol, Paul Ralph, and Brian Fitzgerald. Grounded theory in software engineering research: a critical review and guidelines. In Proceedings of the 38th International Conference on Software Engineering, ICSE 11.. page 220-131, New York. NY, USA, 2016. Association for Computing Machinery. ISBN 9781450339001.
doi: 10.1145/2884781.228888 12884483.... URL
https://doi. orgo 10tg/10..11 11441111811880 78888844877188888333
[40] Artur Tarassow. The potential of 1lms for coding with low-resource and domain-specific programming languages. arXiv preprint arXiv:2307.13018 2023.
[41] Gemini Team, Rohan Anil, Sehastian Borgeaud, Jean- -aantttpt Alayrac Jiahui Yu, Radu Soricut, Johan Schalkwyk, Andrew M. Dai, Anja Hauth, Katie Millican, David Silver, Melvin Johnson, Ioannis Antonoglou, Julian Schrittwieser, Amelia Glaese, Jilin Chen, Emily Pitler, et al. Gemini: A family of highly capable multimodal models, 2024. URL https://arxii...... org. http//axiivvoorrab/////aa/
11805
[42] Bailin Wang, Zi Wang, Xuezhi Wang, Yuan Cao, Rif A Saurous, and Yoon Kim. Grammar prompting for domain-specific language generation with large language models. Advances in Neural Information Processing Systems, 36, 2024.
[43] Yizhong Wang, Yeganeh Kordi, Swaroop Mishra, Alisa Liu, Noah A. Smith, Daniel Khashabi, and Hannaneh Hajishirzi. Self-instruct: Aligning language models with self-generated in- structions. In Anna Rogers, Jordan Boyd-Graber, and Naoaki Okazaki, editors, Proceed- ings of the 6l Annual Meeting of the Association for Computational Linguistics, pages
13

---

13484-13508, Toronto, Canada, July 2023. Association for Computational Linguistics. doi: 2ttp6//////2222...loooooog//3/// URL https::/aclaattollo../ www.l/ooy.o.g///// org. 202//202...r acl -oong.onn....m 754
[44] Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H. Chi, Quoc V. Le. and Denny Zhou. Chain-of-thought prompting elicits reasoning in large language models. In Proceedings of the 36th International Conference on Neural Information Processing Systems, NIPS 222 Red Hook, NY, USA, 2024. Curran Associates Inc. ISBN 9781713871088.
14

---

A NeurIPS Paper Checklist
1. Claims
Question:
Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes],
Justification: the claims concretely supported by results in the evaluation
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
The abstract and/or introduction should clearly state the claims made, including the
contributions made in the paper and important assumptions and limitations. A No
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings. is fine include aspirational goals as motivation long is clear that these goals are not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification: There is limitation paragraph in the evaluation section
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model sell-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested few datasets with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect the factors that influence the performance of the approach.
For example, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-text system might be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms
and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof?
Answer: [NA].
Justification: no theoretical results
Guidelines:
15

---

The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced the statement of any theorems. The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix supplemental material. Theorems and Lemmas that the proof relies upon should properly referenced.
4. Experimental Result Reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Answer: [Yes]
The SPEAC approach is described in sufficient detail to reproduce it. The UCLIDS language and verification tool is open source and publicly available, along with all the regression tests for fine-tuning. The textbooks and code are publicly available.
Justification:
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution a specific model and empirical evaluation, may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often good way to accomplish this, but reproducibility instructions for how to replicate the results, access to a hosted model (e.g.. in the case of large language model), releasing of a model checkpoint, other means that appropriate to the research performed.
also be provided via detailed
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily new algorithm, the paper should make it clear how to reproduce that algorithm.
(b) the contribution is primarily a new model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Question:
Answer: [Yes]
16

---

reproducible, they Justification: In supplementary material.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurlPS code and data submission guidelines (https://nips... cc/
for more details.
While we encourage the release of code and data, we understand that this might not be possible, "No" an acceptable answer. Papers cannot be rejected simply for including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https
/ //ipss.ccppubll... sec/public/guut gwwds// Cowe//oodeeeeeeeeeeeeeeeee isimisssoonn hearbbimsssoooooiiiiiiooo onPolicy) for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing much information possible in supplemental material (appended to the paper) recommended, but including URLs to data and code is permitted.
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: Yes]
Justification: Experiments use openAl LLMs and report the model names and temperature settings used and training details for the baselines.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core the paper to a level of detail that is necessary appreciate the results and make sense of them. The full details can be provided either with the code, in appendix, or as supplemental material.
7. Experiment Statistical Significance
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [NA]
Justification: We do not make claims about statistical significance. We show data for case study.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi-
dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall
run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula,
call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
should be clear whether the error bar is the standard deviation or the standard error of the mean.
17

---

It is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out of range (e.g. negative error rates).
If error bars reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables the text.
8. Experiments Compute Resources Question:
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Answer: [Yes]
Justification: Hardware listed in Sec. 6
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't 't make it into the paper).
9. Code Of Ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics
Answer: [Yes]
Justification:
Guidelines:
The answer NA means that the authors have not reviewed the NeurlPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., there a special consid- eration due to laws or regulations in their jurisdiction).
10. Broader Impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [No]
Justification:
The paper is about getting code to pass compiler checks.
Guidelines:
The answer NA means that there is no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (c.g., disinformation, generating fake profiles, surveillance), fairness considerations (c.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
18

---

The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility ML).
11. Safeguards
Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Answer: [NA]
Justification: We are not releasing any new models. The data we are using not new, and is taken from publicly available textbooks and open source code repositories.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Lieenses for existing assets
Are the creators or original owners of assets (e.g.. code, data, models), used in the paper, properly credited and the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification: UCLID5 is open source and licensed under 3-clause BSD, and cited accord- ingly. Examples taken from textbooks are cited accordingly.
Guidelines:
The answer NA means that the paper does not existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset used and, possible, include URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g., website). the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, pasessswisssi thcode. com datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that re-packaged, both the original license and the license of the derived asset (if has changed) should be provided. If this information is not available online, the authors are encouraged to reach out to asset's ss creators.
13. New Assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
Justification:
All code and documentation is publically available on the GitHub repository.
19

---

Guidelines:
The answer NA means that the paper does not release new assets. Researchers should communicate the details of the dataset/code/mooell as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and Research with Human Subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification: [NA]
Guidelines:
The answer NA means that the paper does involve crowdsourcing nor research with
human subjects.
Including this information the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included the main paper.
According to the NeurIPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: [NA]
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Depending the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
20


Reviews:
[{"review_id": "WrazSxjZY3", "reviewer": "Reviewer_tGyy", "summary": "The paper addresses the challenges of LLMs in generating code for very low-resource programming languages (VLPLs), which are not represented in their pre-training data. Traditional methods to enhance LLM efficacy in this domain include prompting, constrained decoding, and fine-tuning. The authors propose a novel approach called SPEAC, which leverages natural programming elicitation to align with LLMs' tendencies, including their common hallucinations. The technique involves translating a high-resource language (P) into a target VLPL (T) using a subset of P and iterative error repair through LLMs. The largest consistent sub-tree of a generated program in P is identified using a MAX-SMT solver, and errors are iteratively fixed. The approach is demonstrated on the UCLID5 verification language, showing significant improvement in syntactic correctness compared to traditional fine-tuning methods .", "questions": "In the paper, the authors propose using a subset of the high-resource language P, referred to as C, which can be transformed into the target low-resource language T. How is the existence of C determined in general?", "limitations": "Section 5.1 discusses the process of defining the subset C of P at a high level, but it lacks rigorous detail. I would appreciate seeing a more elaborate theory developed around this process in future work.", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "- The idea presented is novel, and the results are impressive, demonstrating significant improvements over traditional methods.\n- The paper is well-written and engaging. The introduction clearly explains the contributions and the problem being addressed. The running example in Section 3 is helpful for understanding the proposed method.", "weaknesses": "I did not find any major weakness in the paper, however, the paper is focused on UCLID5 programs, which consist of a relatively narrow set of use cases, and it is not obvious how well this method will generalize to other VLPLs.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their thoughtful feedback. Please see below for our answers to the question posed.\n\n**tGyy-Q1: How is the existence of C determined?**\n\nDetermining the existence of C is a design process. It is possible that some target languages are so esoteric that no subset of a high-resource language is even remotely compatible. However, showing that UCLID5, a language that is nothing like Python, has a good C in Python is evidence for the existence of a language C for many target languages. \n\nWe described the general process for finding the child language C through grounded theory in Section 5.1 interleaved with the specific process for UCLID5 (mostly on lines 223 to 241) but we omitted some details due to space constraints. We will add detail to the description of the general process by drawing on general guidelines for using grounded theory in software engineering (e.g., Stol et al. 2016) and specific case studies (e.g., Barke et al. 2023). We will add detail to the specific process for UCLID5 by including concrete examples, possibly in the appendix.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "OtFgzHjT3y", "reviewer": "Reviewer_9eZc", "summary": "The paper presents a framework to generate programs given natural language and targeting very low-resource programming languages. They first choose a language well-represented in the training data (in this case Python), and then make the LLM generate in a subset of that language, and then compile the generated program to the target language. When the generated program is checked by formal techniques and found to be inconsistent, some parts of the program are replaced with holes and fixed with LLM again. They apply this method to a very low-resource language VLPL and show that it is able to generate programs that parse (24 out of 33 test problems) and 11 out of 24 have fully correct semantic meaning, while the baseline few-shot prompting and fine-tune methods obtain near zero parsable programs.", "questions": "* Would few-shot prompting baseline methods with more than one example work better?\n* How does constraint decoding compare to the method here to get a parsable program in VLPL instead of Python subset?\n* How does the method compare with reflexion-style methods where iterative prompting is used to fix the problem by including feedback from the parser in the prompt at each iteration?\n* It is mentioned that there is a set of regression tests comprised of 317 tests taken directly from the UCLID5 GitHub repository. How are these tests used? Are they used to evaluate besides the results on the 33 test problems in Table 1?\n* How does the self-instruct with fine-tune method work specifically? How many synthetic programs are generated?\n* Can you provide the full prompt that is used for generation and fixing? Is the code in the appendix A included in the prompt in addition to the prompt template shown in Fig 4?", "limitations": "Limitations are addressed.", "rating": 5, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "* The results are very strong compared to the baseline few-shot prompting and fine-tune methods, which obtain near zero parsable programs.\n* The framework is described in a general way and potentially applicable to other low-resource programming languages as well.\n* The system integrating LLM program generation and formal methods for checking the program is very interesting and demonstrates the effectiveness of the method empirically.", "weaknesses": "A major concern of the paper is that there should be other stronger and popular methods to use as baselines. For example, a common method is iterative fixing of unparsable code by prompting LLM with the parser feedback. Also, many-shot examples (more than one) and including language specification in the prompt may also help, which is also a very standard prompting technique among the community. The method presented here would likely still work better, but it would be more informative to compare with those methods and see how much improvement is made.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their thoughtful feedback. Please see below for our answers to the specific questions posed.\n\n**9eZc-Q1: Would few shot prompting work better?**\n\nAdding more examples improves both the baseline’s performance and Eudoxus’ performance (which currently uses no examples, see Fig. 4). Using few-shot with 3 in-context examples leaves gpt-3.5-turbo's performance with zero successful compilations. For gpt-4-turbo, we find both with and without COT produces successfully compilation for 3/33.\n\n**9eZc-Q2: Comparison with constrained decoding?**\n\nOur work is complementary to constrained decoding in two ways. First, one of the pitfalls of constrained decoding is that it will perform poorly if the external constraints do not align with the underlying vocabulary of the LLM (Beurer-Kellner et al. 2024), i.e., if the desired output is “unnatural” to the LLM then constrained decoding does poorly. Synthetic programming elicitation could help bridge this gap for very low resource programming languages.\n\nSecond, most existing constrained decoding techniques support only context-free languages (Beurer-Kellner et al, 2024) but most programming languages are at-least context-sensitive languages. Our MaxSMT driven repair can be applied after constrained decoding to fix more complicated, context-sensitive errors, like type-checking bugs.\n\n**9eZc-Q3: Comparison with reflection style methods?**\n\nWe gave gpt3.5 and gpt4 compiler feedback in a self-repair loop starting from a zero-shot prompt and found no benefits. Specifically, our repair prompts provided the LLMs with their previously generated code and the corresponding compiler error. We let both LLMs iterate up to five times (same as Eudoxus in our empirical evaluation) but neither LLM was able to successfully repair its own code. We believe this is because the baseline LLM outputs are too far from correct outputs: there are just too many errors to fix. This is consistent with observations from existing work for verification languages, where self-repair alone shows only modest improvements (e.g., Loughridge et al. 2024).\n\nReflection style methods may be more impactful when combined with more advanced techniques (as opposed to a zero-shot starting point), like Eudoxus. Our LLM repair step is currently extremely simple, giving no compiler feedback and doing no self-debugging (see Fig. 4b). Combining our work with complementary reflection style methods is a promising avenue for future work.\n\n**9eZc-Q4: How are the regression tests used?**\n\nThe 317 are used for fine-tuning and for synthetic programming elicitation. See 9eZc-Q5 for more information on fine-tuning. For synthetic programming elicitation, we wrote natural language descriptions for a subset of the regression tests and used these natural language descriptions (without the corresponding regression test) to study the “natural” behavior of the LLMs. We mention this on lines 199-200 but will make it more clear.\n\n**9eZc-Q5: How does self-instruct with fine-tuning work?**\n\nFor self instruct, we took existing tests in UCLID5 and asked the off-the-shelf LLM to create a plausible natural language description. This provides us 317 training pairs of natural language and valid UCLID5 on which to fine-tune. Just as in the self-instruct paper (Wang et al. 2023), the natural language descriptions (questions) are synthetic but the programs (solutions) are not synthetic. We briefly describe this on lines 295-297 but will clarify and add the appropriate citation.\n\n**9eZc-Q6: Providing the full prompt?**\n\nYes and yes! In fact all of this is already included in the supplementary material that we submitted with the paper (but with possibly insufficient documentation, which we apologize for). You can see the full initial prompt in `get_sketch_prompt` of `eudoxus-main/src/eudoxus/llm/prompts.py` and the full hole filling prompt in `get_complete_prompt` of the same file. We are also happy to add the full conversations for every benchmark in the supplementary material along with a few in a new appendix (so that one does not need to execute the code to see a full conversation).", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "DAavXAxqkY", "reviewer": "Reviewer_9mNj", "summary": "In this paper, the authors present a novel approach called SPEAC (Synthetic Programming Elicitation and Compilation) to enable large language models (LLMs) to generate syntactically valid code for very low-resource programming languages (VLPLs). The approach involves creating a hallucinated library within a high-resource language, which can be compiled into the VLPL. The paper includes a case study demonstrating that SPEAC outperforms existing methods in producing syntactically correct programs. Evaluation results demonstrate that SPEAC outperforms all baselines on syntactic correctness (see “Parse Rate” in Tab 1), achieving full syntactic correctness on 78% of benchmarks.", "questions": "The first paragraph in Section 2 is very disorganized. If the authors aim to discuss LLMs for code generation, they should focus on them rather than the benchmarks. It would be beneficial to include more examples of LLMs and either remove the benchmarks discussion or introduce benchmarks in a separate section dedicated to the code generation area.\n\nThe experimental section is weak. Reviewers can only find the experiment results on the eighth page. The authors should present the experimental setup, results, and analysis more prominently and earlier in the paper to support their claims better.", "limitations": "NA", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 1, "contribution": 2, "strengths": "The paper addresses a novel problem of generating code for VLPLs by leveraging LLMs, which is a relatively unexplored area. \n\nThe empirical evaluation demonstrates the effectiveness of SPEAC compared to other baselines.", "weaknesses": "The claims made about the significant improvements achieved by SPEAC are not fully supported by a diverse set of experiments.\n\nThe paper is poorly organized and lacks a clear, logical flow.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their thoughtful feedback. Please see below for our answers to the specific questions posed.\n\n**9mNj-Q1: Reorganization of the paper?**\n\nWe are happy to make all the suggested organization changes under the questions header. Specifically, we are happy to (1) reorganize the first paragraph of Section 2; (2) introduce benchmarks in a separate section; and (3) present the experimental setup, results, and analysis more prominently and earlier in the paper. We estimate these changes should take no more than one day of work.\n\n**9mNj-Q1: More LLMs?**\n\nWe are happy to include more examples of LLMs, as suggested, although our initial experimentation suggests that their performance generating syntactically correct UCLID5 code will be comparable to the OpenAI models (i.e., poor). If there are specific LLMs the reviewer believes we should add, we are happy to follow suggestions.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "x6o7zgNM6u", "reviewer": "Reviewer_6oM2", "summary": "Recent advances in large language models (LLMs) for code applications have demonstrated remarkable zero-shot fluency and instruction following on challenging code-related tasks, ranging from test case generation to self-repair. However, the authors note that these models struggle to compose syntactically valid programs in programming languages that were unrepresented during pre-training, known as very low-resource programming languages (VLPLs). VLPLs are critical in various settings, including domain-specific languages for internal tools and tool-chains, and legacy languages. Inspired by program elicitation, the authors propose creating a hallucinated library within a high-resource language that can be automatically compiled to the VLPL. This library enables the LLM to generate and self-repair code within the syntax of a familiar language. Specifically, the authors introduce Synthetic Programming Elicitation and Compilation (SPEAC), an approach that enables LLMs to generate syntactically valid code even for VLPLs. The authors empirically evaluate the performance of SPEAC in a case study and find that, compared to existing retrieval and fine-tuning baselines, SPEAC produces syntactically correct programs more frequently without sacrificing semantic correctness.", "questions": "Overall, I appreciate the idea presented in this paper. \n\nThe research tackles a critical problem in the field of LLMs for code generation, particularly focusing on VLPLs, which are often overlooked but essential in many applications. The concept of using MAX-SAT to bridge the gap between high-resource and very low-resource languages is innovative and offers a new direction for future research. The empirical results demonstrate that SPEAC outperforms existing baselines in producing syntactically correct programs without losing semantic accuracy.\n\nHowever, the authors need to address some issues.\n\n1. **Missing some details**:\n\nThe authors omit important details about the semantic score. How is the semantic score computed? Is it done automatically or labeled manually? If labeled manually, how many people were involved, and what is the kappa score?\n\n2. **Fail to consider code generation approaches via self-repair or self-debugging**:\n\nWhile the proposed SPEAC approach is promising, the paper does not adequately address how it compares to or integrates with existing methods that leverage self-repair or self-debugging capabilities in LLMs. These approaches are also relevant to this paper.\n\n3. **Only conducted experiments on UCLID5**:\n   \nThe evaluation of SPEAC is limited to a single case study on UCLID5. Broader validation across multiple VLPLs would enhance the generalizability of the findings.", "limitations": "See Questions, thanks.", "rating": 7, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "+ Important area\n+ Novel idea\n+ Good performance", "weaknesses": "- Missing some details\n- Fail to consider code generation approaches via self-repair or self-debugging\n- Only conducted experiments on UCLID5", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their thoughtful feedback. Please see below for our answers to the specific questions posed.\n\n**6oM2-Q1: Details of the semantic score?**\n\nThe semantic scores were manually judged by one professor with experience teaching formal methods (undergraduate and graduate level courses). This small number of judges is definitely a limitation and we will make this explicit in the paper. However, the key takeaway from the results is that Eudoxus lifts the syntactic correctness from 2/33 (Fine-tuned GPT-3.5-turbo) to 28/33 (Eudoxus using GPT-3.5-turbo) while not terribly harming semantic correctness.\n\n**6oM2-Q2: Self-repair or self-debugging?**\n\nPlease see response to reviewer 9eZc question 3 (9eZc-Q3).\n\n**6oM2-Q3: Only UCLID5?**\n\nThe goal of the UCLID5 case study was to conduct an in depth demonstration of our techniques for a very low resource language that looks very different from high resource languages and has a wide range of features. UCLID5 supports software verification, like Boogie (Barnett et al. 2005); hardware verification, like ABC (Brayton and Mishchenko 2010); and can even be used for modeling distributed systems, like P (Desai et al. 2013). We acknowledged that including only one case study is a threat to validity (lines 328-331) but UCLID5’s wide range of features is evidence for the generalizability of our approach.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: This work proposes a method for supporting LLM-based language generation in very low resource programming languages by invoking the LLM to generate code in a hallucinated library in a high-resource language instead, and then translating this program to the low-resource language using an SMT solver and iterative repair.

Reviewers agreed that this is both an important subject and that the proposed technique is quite novel and interesting. The results also highlight that this method can rather substantially improve the quality of the programs generated in a very low resource language.

At the same time, the reviewers noted that the evaluation is rather limited, focusing on just 33 (test) and 317 (fine-tuning) programs in one language (UCLID5). While the results on this set are very strong compared to baselines, this inherently provides limited evidence of the effectiveness and generalizability of the technique. Some reviewers also raised concerns around the limited choice of models and the absence of other prompting strategies as baselines.

As evidenced by the diverging scores, the reviewers weighed the limited evaluation against the technical novelty and positive results in different ways, with the majority opting to accept the work. Given this, and the importance of investigations in this under-studied domain and the significant novelty of this work, we have decided to recommend accepting this work. The authors are encouraged to incorporate the rich feedback from the reviews and to clearly note the limitations in the evaluation in the camera-ready version of the paper.
Decision: Accept (poster)