Verified Code Transpilation with LLMs
Authors: Sahil Bhatia
Jie Qiu
Niranjan Hasabnis
Sanjit A. Seshia
Alvin Cheung
Venue: NeurIPS 2024 poster (2024)
Keywords: Program Synthesis
Compilers
Formal Methods
LLMs
Primary area: machine_learning_for_other_sciences_and_fields

Abstract: Domain-specific languages (DSLs) have become integral to various software workflows. Such languages offer domain-specific optimizations and abstractions that improve code readability and maintainability.  However, leveraging these languages requires developers to rewrite existing code using the specific DSL's API. While large language models (LLMs) have shown some success in automatic code transpilation, none of them provide any functional correctness guarantees on the rewritten code. Another approach for automating this task is verified lifting, which relies on program synthesis to find programs in the target language that are functionally equivalent to the source language program. While several verified lifting tools have been developed for various application domains, they are specialized for specific source-target languages or require significant expertise in domain knowledge to make the search efficient. In this paper, leveraging recent advances in LLMs, we propose an LLM-based approach (LLMLift) to building verified lifting tools. We use the LLM's capabilities to reason about programs to translate a given program into its corresponding equivalent in the target language. Additionally, we use LLMs to generate proofs for functional equivalence. We develop lifting-based compilers for four DSLs targeting different application domains. Our approach not only outperforms previous symbolic-based tools in number of benchmarks transpiled and transpilation time, but also requires significantly less effort to build.

Verified Code Transpilation with LLMs
Sahil Bhatia
Jie Qiu
Niranjan Hasabnis Sanjit A. Seshia'
Alvin Cheung'
'CC Berkeley jieq, sseshia, akcheung){berrkeley)
Code Metal
(sahilbhatia,
niranjan@codemetall
Abstract
Domain-specific languages (DSLs) are integral to various software workflows. Such languages offer dopain-specific optimizations and abstractions that improve code readability and maintainability. However, leveraging these languages requires developers rewrite existing code using the specific DSL's API. While large language models (LLMs) have shown some success in automatic code transpilation, none of them provide any functional correctness guarantees on the transpiled code. Another approach for automating this task is verified lifting, which relies on program synthesis find programs the target language that are functionally equivalent to the source language program. While several verified lifting tools have been developed for various application domains, they are specialized for specific source-target languages require significant expertise in domain knowledge to make the search efficient. this paper, leveraging recent advances in LLMs, we propose LLM- approach (LLMLIFT) to building verified lifting tools. We use the LLM's capabilities to reason about programs to translate given program into its corresponding equivalent in the target language. Additionally, use LLMs to generate proofs for functional equivalence. We develop lifting-basee compilers for four different DSLs targeting different application domains. Our approach not only outperforms previous symbolic-he based tools in both the number benchmarks transpiled and transpilation time, but also requires significantly less effort build.
Introduction
Domain-specific languages (DSLs) have gained popularity due to their ability to provide optimizations and abstractions that improve code readability and performance in specific domains. Examples of recent DSLs include Spark (distributed computing), NumPy (array processing). TACO (tensor processing), and P4 (network packet processing). With new DSLs emerging for diverse application domains and programming languages, developers often face the task of manually rewriting existing code to incorporate these languages into their existing workflows. This manual rewriting process can be tedious, may introduce bugs into the code, and may fail to preserve the semantics of the starting code. This problem transforming and compiling code from one programming language to another called franspilation. The question address in this paper is: can large language models (LLMs) correctly and automatically perform code transpilation?
A particularly useful form of code transpilation, termed lifting. involves translating code in somewhat lever-level, purepee language to equivalent code in a DSL. Lifting allows developers to port code to DSLs from which efficient code can be generated for special-purpose hardware, such as GPUs, machine learning accelcrators, or network processors. Therefore, significant effort has been dedicated to developing tools aimed at automating the task of lifting. Rule-basee based approaches rely on traditional
techniques [ however, describing these rules can be a complex,
Work was done while at Intel Labs.
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

numan-intensive task. An alternative are search-based techniques that leverage advances in program synthesis (c.g.. see 3 and formal verification over the last two decades. The use of verified program synthesis for lifting, termed verified lifting, involves searching for program in the DSL and subsequently formally verifying its semantic equivalence to the source program. Verified lifting has been successfully applied in building compilers [5] 6 7 g for DSLs like Spark, SQL, Halide, and TACO. Contemporary program synthesis approaches can be broadly classified into two categories: symbolic and neural. Traditionally, symbolic techniques such as enumerative, deductive, and constraint-basee synthesis strategies have been used for implementing the search. More recently, neural networks [9] have been trained and leveraged to accelerate the search process. Despite their successes, both symbolic and neural approaches have common drawbacks: 1) The synthesizer is customized for each DSL, making them challenging adapt for new DSLs, and 2) Significant effort is required to design the synthesizer, including domain-specific heuristics for symbolic approaches and the generation of parallel corpora (source, larget) for ML--based approaches, to enable generalization and scalability for the target DSL..
Large Language Models (LLMs) 1O have emerged promising approach for tackling complex programming tasks, including code generation, repair, and testing. However, generating reliable code with formal correctness guarantees with LLMs remains challenging. Most work on LLMs either focuses on generating code without correctness guarantees [2] [2] [4] or separately on producing proof annotations (such invariants) for given code [6). Additionally, formal verification tools often have their own specialized languages (c.g.. SMT-LIB, Dafny) for encoding verification problems and specifications. These languages typically low-resource in the training datasets of LLMs, making it challenging for the models to generate code in these formal verification languages directly. To leverage LLMs for building verified lifting compilers, must address two key constraints: generalization to new DSLs and providing correctness guarantees for the generated code.
In this work, we investigate the use of LLMs for verified lifting (VL). Our approach, called LLMLIFT, takes inspiration from the core technique of VL, which involves translating the source program to a higher-level intermediate representation (IR) that describes the semantics of the DSL operators. Once the synthesized code is verified, it is then translated to the concrete syntax of the DSL using rewrite rules. We leverage the reasoming capabilities of LLMs to translate code from context to IR. We instruct the model via a prompt to generate code using the operators of the DSL, with Python serving as the IR encode the semantics of these operators. Python's significant representation in the training datasets of LLMs makes it a suitable choice for this purpose. In addition to generating the DSL program, also prompt the model to generate a proof of correctness for the program. To the best of our knowledge, our approach is the first to leverage LLMs to generate both code and proof annotations together. To verify the functional equivalence of the generated program to the given source program for all program states, we translate both the generated program and the proof to the syntax of an automated theorem prover. This step ensures that the synthesized code is formally verified and can be trusted to be correct. Our evaluation (section Sec. 33 shows that LLMLIFT has significant advantages over traditional search-based symbolic VL-bbaed tools. It solves 7 more benchmarks, requires substantially less effort in terms of LoC (1000x), and is faster in generating verified code and proofs (6x on average).
In summary, this paper makes the following novel contributions
1. We introduce the first technique for formally-verified code transpilation using LLMs.
2. Our approach uses Python as an IR for code generation, thus eliminating the need for specialized DSL-specific training data or fine-tuning of L.MMs.
3. Our method eliminates the need for manual encoding of domain-specific heuristics, thus simplify- ing the process of verified lifting by reducing the human effort required in traditional techniques.
4. We propose an approach to generate not only the lifted code but also a proof of correctness for the generated code. This integration of LLMs with verification oracles guarantees the correctness of the generated code, a crucial aspect that sets our approach apart from other work on LLM--based code generation.
5. We show the effectivvness of our approach (Sec. 4 by constructing compilers for four DSLs spanning various application domains. In terms of accuracy, our LLM-based compilers achieve comparable performance to existing tools and, in some domains, outperforms the prior approaches.
2 Background
2

---

def matrix_and(a: ListDList[int]), by Listiisst(int]))
List(List[int]]: 3 return
[]]
if len(a) <
or not len(a) len(b)
or vec_add(a[3). b[0]) ==[]
8
else
vec_add(a(o), b[o]),
vector<vector<intte test( vecter<vector<intt>
10
metrrik_ett(al1:..01112
})
vectorsvactercint>
12
def matrix_scalar_se int, be List[List[ine]])
vectersvectorcints out; for (int row 8; row b.size(); rowts) { vector<int> rec_vec;
13
-> List(List(int]]:
return
15
[]
(int col 8; col b(e))size(); col+))
if len(b)
int pixel = b[row][col] a[row][col] 255;
17
else [
row_vec. veec.push_bar push_bacck(ixx))); out (arh_baac(roo__ee)) return out;)
vec_scalar_sutt.. b[0]).
10
matrik,,sallrr.suu.. b[1:1)
11
])
(a) Source Code (S).
(b) Target Language (Taang).
Figure 1: Sequential source code in C++ and semantics of DSL in IR.
We now give overview and an end-to-end example of verified lifting (VL) where synthesis to build a compiler. Given a program (S) in the source language (Stang), ) VL uses a search procedure find program (T) in the target language (Tiang) that can be proved to be functionally equivalent to the given source program. VI. comprises of three phases: 1) Search, 2) Verification, and 3) Code generation. The key behind VL is first transpile S to user-defined intermediate representation (IR) of the operators in the target language before generating executable code. The IR serves as a functional description of Tang and ignores any implementation details. Hence, during search phase, S is lifted to sequence of operators expressed using the IR. This expression serves as the program summary (PS) which summarizes using the IR. Subsequently, PS is verified using theorem prover to check for semantic equivalence with S for all program inputs. If verification succeeds, PS is then translated into the concrete syntax of the target language using simple pattern- matching rules provided by the user to generate executable code. These rules are notably simpler to write compared to a rule-based translator that directly compiles from Stang to Tiangs as the PS already expressed using the operators in the target language.
program
We demonstrate example of transpiling a sequential C++ censor-processing frameworks (such as PyTorch, Tensorflow, NumPy) using VL. Tensor-pre sannoo-processing frameworks provide high-level API for performing, large-scale numerical computation on nulti-dimensional arrays. Some of the basic tensor operators supported by all the frameworks are elementwise operators (tensor-tensor, tensor-scalar).
Fig. la shows sequential source program (S) performing the linear burn blending operation in image editing. The given source program takes as input two images (represented as 2D vectors) and processes each pixel from both the images by first adding them and then subtracting by integer 255.
In Fig. we define the semanties of the tensor operators such as matrix_ade and serriixscalar_sbbb These functions abstract the implementation details of the operators in the censor-processe frameworks while only capturing the high-level semantics of the operators. Our goal is to find an IR expression sequence of these operators such that it is semantically equivalent to S. Traditional approaches to solving this search problem VL involve framing it as SyGuS [77 problem. SyGuS is approach for solving program synthesis problems by specifying constraints and searching for solutions within a defined space. Specifically, a SyGuS problem involves defining a search space that syntactically restricts the space of possible solutions, thereby making the search tractable. Formally, this objective can be stated as 3 T Thang V a. S(a) T(a), where T is a program in the target language. For our program in Fig. Ta the synthesis phase would return the following PS (i.e., T): Matrix_scalar_su((22 matrix_add(b, a))
This expression performs element-wise addition of two matrices and b. followed by a scalar subtraction of 255 from each element of the resulting matrix. Since S contains loop, proving equivalence with the generated program requires another predicate called the "loop invariant." A loop invariant is a logical statement that must hold before and after each iteration of a loop. Intuitively,

---

Tagget Desor piio
ge Lang agg
Paser
Paasrr
Verifar
Code Generator
Source
Target
P5 Prompt
Invariant Prompt
Rediran Fxedbaok
Figure 2: A high-level overview of our LLMLIFT framework for building verified lifting-based tools.
captures the essential properties that are preserved while the loop executes. During VL's synthesis phase, generate both the program summary and any required loop invariant for verification. Verification is done by sending the program summary and loop invariant(s) to a theorem prover. Verifier checks the semantic equivalence between and the generated program summaries. VL currently uses cve5 and z3 for this purpose. Once verified, we translate the generated program summary the conerete syntax of the DSL (NumPy) using simple mittehn- rules, resulting in the following executable code:
def linear_buree wwwbbuur_n__nnn_ (b: np.ndarray, a: np.ndarray) -> np. ndarray: return b 255
We next describe how our LLM-based approach can improve VL synthesis problem.
3 LLM-Based Verified Lifting
We now describe our LLM-based approach for verified lifting. We begin by formalizing the VL problem. Then we give details of how we use LLMs to improve over the traditional VL approach.
3.1 Problem Formulation
The VL problem is characterized by three inputs:
Specification (Φ): The specification (ø) defines the property that the target program (T) should satisfy. For VL considered in this paper, the source and target programs are side-effect free functions of their inputs. Thus, & encodes the semantic equivalence of T and the source program (S) for each program input state a. The overall correctness condition is:
Ya Φ0 T) = V S.o) T(a)
Program Space (G): The program space outlines the set of potential solutions, typically expressed context-free frre grammar G. The language of G includes all sequences of operators ops E Tiang applicd recursively to terms starting with input variables a. target program T is program summary PS that is composition of operators ops. An example involving the tensor operators is provided in the previous section. In other words, for each input a, (a) must be expressed using combination of operators (ops) from Tiang-
Certificate Space: (G,) A key part of the VL problem to generate a certificate correctness, typically in the form of invariants that verifier can PS. Synthesis tools typically use a grammar Gy to constrain the space of possible invariants to search over; refer this as the certificate spuce.
prove that holds for the generated
VL Problem:
Given the inputs S, o, G. Gr, and Tiang described above, the VL problem is to generate correct target program in Tiang represented as the combination (PS, Inv). This is formally expressed in logic as follows:
PS E G 3In E Gj Vo δ(a, (PS, Inw),
This states that aim to find program summary (PS) and invariants (Inv) from the defined search space G, G, such that the given specification (functional equivalence with S) holds for all possible program states
Traditionally, the VI problem has been solved by symbolic program synthesis solvers utilizing methods such enumerative search, deductive search, and constraint-based approaches [7.4. These

---

gueen Test per
using spple ferray processinn ing penntically equivaient Kiceat Furction
sicompute: :ffeeer tuttestoopate: :Terer
<Instructiona>
alcatane (tfeeer a)
(fTask Desoraption)
vectarsoer/anstee iendette rertwereeee cestinee h.
aata on eloompannt 21901
vesto westo voster eats
Semantines>
Hie for cant lne plunl (ofra]]loa)] afrad]teal]; con.beee
(toperators in DSL)>
ball stant); codret
eSpecification
([Source Progran))
return cxtt)
Figure 4: Prompt Structure.
Figure 3: End-to-End Lifting Example.
rely heavily Hanually-designee heuristics to make the search over the program and certificate space effective. Unfortunately doing so is resource- -intensve and requires domain-specifie knowledge. To address these limitations, take new approach that leverages LLMs.
3.2 LLM-based Verified Lifting
naive approach to building a VL-based compiler using LLMs would be to prompt LLMs to translate Stang programs directly into Tiang. However, this approach has the following shortcomings:
VL-based compilers require that the Tiang candidates generated during the search phase be functionally equívalent to the input Stang program. This is strong requirement that current LLMs are unable to satisfy on their own.
Unlike widely-used general-purpose languages such Python, domain- specifii languages (DSLs) are used only in their niche applications. Unsurprisingly, we find that LLMs struggle to generate code in languages that are insufficiently represented in their training data.
In Fig. 3] we show an example of LLMs struggling to generate code reliably in new DSLs. We instruct GPT-4o translate the program in Fig. Ta MLX (Apple's latest tensor processing DSL), and the model fails to generate the expected python MLX code. Instead, the model outputs completely incorrect solution by hallucinating non-existent MLComput header file. This problem is even more prominent for new DSLs that the model might have never seen in the training dataset.
Our Approach: To address these challenges, we propose an approach that adapt key ideas from traditional synthesis to the LLM setting:
1. Python Intermediate Representation (IR): We adopt VL's key idea of transpiling an IR rather than directly to the concrete syntax of Thang- Specifically, since Python is highly represented in the training dataset of popular LLMs [12]. these LLMs are effective at generating syntactically-corred Python code. We exploit these observations by leveraging Python as the IR to define semantics of DSL operators. An example is shown in Fig. [b
2. Oracle-Guided Inductive Synthesis (OGIS) with LLM oracles: Traditional verified lifting follows the paradigm of counterexample-guieee synthesizes from examples interacts with verifier that checks the Learner's output programs for correctness with respect to a specification. OGIS [88 19 is a generalization of CEGIS with a richer oracle interface that allows for more expressive oracles and interactions. Our LLM Lifting approach instantiates OGIS with LLM oracles that synthesize PS and Inv before invoking a verifier check correctness. Our queries the LLM oracles (prompts) follow few-shot learning approach. Our current verifier provides Boolean feedback to the LLM oracles.
inductive synthesis (CEGIS) (2), where a Learner that
In Fig. we show our L.M- OGIS approach, where LLMs applied generate program summaries and invariants in the IR, using a few-shot learning framework that we describe next.
3.3 Few-Shot Learning Approach
Few-shot reasoning allows LLMs to generalize their understanding new tasks by leveraging a small set of similar examples. Enabling them to extend their reasoning capabilities to tasks without requiring explicit training fine-tuning
LLMSs have demonstrated few-shot reasoning capabilities [1].
5

---

for those specific tasks. We propose leveraging the few-shot reasoning capabilities of LLMs for verified lifting as fine-tuning existing LLMs for each new DSL is often infeasible due to the lack of extensive training data and the rapid pace at which new DSLS are developed. The effort required to collect, annotate, and preprocess DSL.-specific training data for fine-tuning can be substantial, making it impractical to adapt LLMs to each new DSL.
As described in Sec. 2 in VL, we generate candidates in an IR that abstracts away low-level implementation details of the operators in Tiong- The objective, as defined in Eq. (2) is to find PS and Inu expressed using operators from Tiong such that & holds. We leverage the few-shot reasoning capability by providing the models with the semantics of operators from the target language (Tiang) using an IR. By exposing the LLMs these semantics, we enable them to use their reasoning capabilities over code to generate both the PS and invariants in the IR.
In Fig. 4 we illustrate the high-level prompt structure we use to generate the PS and Tnu. The prompt consists of the following components:
1. Task Instruction. We instruct the model using natural language to translate S using only the specified DSL operators.
2. DSL Operators. We specify the semantics of all operators from Tiang using Python and include it in the prompt. Python is chosen as our IR due to (a) its widespread use across domains, (b) its concise and expressive nature, making the representation readable and straightforward and, (c) its significant representation in code datasets used for training LLMs [2].
3. Specification. While symbolic techniques often rely on approaches like test cases, bounded model checking, and Hoare logic (0) for defining specifications, the natural language interface of LLMs offers flexibility in using various specifications and combining different forms. Given that LLMs are primarily trained on raw source code and may not have encountered other forms of specification during training, we directly use the source program (S) as the specification in our prompt.
We next describe the end-to-end workflow for our LLM-based verified lifting.
PS Guessing. We split the generation of PS and Inv into two-phase process by first asking the LLM to generate the PS and then inferring invariants corresponding to it. For generating PS, we prompt the model in zero-shot setting. Due to space constraints, we show an instantiation of the prompt structure shown in Fig. 4 in Appendix B When prompted, the model generates the following PS for our example code shown in Fig. la representing the as a combination of DSL operators:
srrri__saala__uu(2555
matrix_add(b, a))
To ensure that the generated candidates follow the DSL operators defined in the prompt, we use rule-based parser to reject any candidates that do not satisfy this constraint, i.e., those that use constructs outside the DSL operators (see Appendix D for examples).
Inv Guessing. Next, if S contains loops, establishing the functional equivalence of the generated PS for all program states with S requires loop invariants. In VL., loop invariants typically follow a templated structure:
Inu - f() A e(Tiang)
where f(i) denotes expression over loop indexes and e(Tiang) represents an inductive expression constructed using operators from Than- This structured nature simplifies the invariant generation process compared to solving general loop invariant synthesis problems. To facilitate the generation of loop invariants, we use one-shot learning (unlike the zero-shot approach for program summaries). This is needed: 1. to familiarize the model with the concept and structure of invariants in the VL context and, 2. generating program summaries is relatively easier than loop invariants, as the model's primary instruction is simply to combine operators from the given DSL without introducing external ones-a constraint that is easily expressed in natural language (due to space constraints we illustrate the prompt in Appendix B The prompt for invariant generation closely resembles that used for generating program summaries, including S with an additional assertion stating the equality of the return variable with the previously generated PS. This instruction guides the model to produce an invariant corresponding to the generated PS. The invariants are generated as Boolean expressions in Python rather than SMT-LIB, we found that LLMs encounter difficulties in generating SMT-LIB (standard format for SMT solvers) code due to its limited representation in training datasets. When prompted, model generates the following invariant for the code shown in Fig.
We evaluate LLMLIFT with zero-shot invariant prompt in Appendix K

---

def invariant_outer col, b, a, out): return row >= and row <= len(b) and out matriaaaa mmetrrx_scalar_suu(255
matrix_add(bEil), a[:i]))
The loop invariant states that the loop index row remains within the bounds of the array b (i.e., 0 S i len(6)). Additionally, the invariant expresses out as a tensor DSL expression over the first i elements of the inputs b and a, which helps verify that the invariant holds in each iteration of the loop. Similar to PS generation, the generated loop invariants are also checked using our rule-based parser ensure they conform to the DSL
Verification. Both the generated PS and Inu are expressed in Python. We use simple pattern- matching rewrite rules to translate these expressions into syntax compatible with the verification oracle, which checks for functional equivalence. The objective is to verify that the given S and generated T are equivalent for all possible inputs to the S program. In Appendix E we provide proof demonstrating how we establish this functional equivalence using an SMT solver. If the verifier cannot establish validity, we start the process again to generate
candidates.
Code Generation. Once verified, the PS translated into the concrete syntax of Tiang using straightforward rewrite rules that recursively parse the generated PS and translate it into the concrete operators of the DSL, leveraging the syntactic nature of Python. The translation process is simplified due to Python's 's highly structured syntax. For instance, the generated PS for our running example can be translated into tensor processing frameworks like NumPy, generating the following code:
def @irear_burn___nee return a b 255
a):
See Appendix F for more details on rule-based code generator. We present our complete algorithm for generating PS and Inv in Appendix
4 Experiments
To evaluate the effectiveness of LLMLIFT, we evaluate across four distinct DSL each targeting a different application domain:
1. Distributed Computing: We transpile sequential Java programs into MapReduce implemen- tations written using the Apache Spark (2I) API. Spark, open-source distributed computing framework, provides an interface for programming multiple clusters for data parallelism which helps in large-scale data processing.
Network Packet Processing: We transpile sequential network processing algorithms in C to the operators of programmable switch devices [22] with its own ISA. This translation enables the exploration of novel algorithms, such as congestion control and load balancing, on programmable switch devices.
3. TACO: We transpile sequential C++ programs into TACO 23 's API. TACO is a tensor processing compiler for generating highly optimized GPU code for performing tensor computations.
4. Tensor Processing. We transpile sequential C++ programs to recently introduced tensor processing IR called TensIR 241 TensIR consists of common tensor operations such element- wise arithmetic operators, reduction operators and transpose, among others. TensIR is designed to enable translation of unoptimized sequential code tensor operations which can be then executed on 6 different software and hardware backends.
Implementation Details: In all experiments, We set the temperature to 0.7 for all the experiments. For program summary and invariant generation across all domains, respectively. We keep budget of 50 queries for the PS and a budget of 10 queries for each PS. The parser and logic for invoking the LLMs are implemented in Python with sc700 LoC.
GPT-4 via their APIs generate candidates.
the same zero-shot PS prompt in Fig. 6 and one-shot prompt in Fig. 7
Note. LLMLift currently only supports a subset of the C/C++ and Python language in the source programs. In particular, it does not support any code that uses pointers objects verifying programs with these constructs is challenging. That said, we did not encounter the use of these constructs in any of the benchmarks in all the four domains that we evaluated on.
? All the benchmarks used for evaluation can be found at:
7

---

Tensors form the key construct in machine learning and tensor compilers play an important role in optimizing these operations. TACO 23 is one such compiler which can automatically generate highly optimized code tailored to CPUs and GPUs. TACO's language represents the operations in a concise einsum like notation. Recently, C2TACO 6 search-based lifting tool was proposed to We present the results in the sections below and defer the error analysis to Appendix D We also provide an analysis on the performance of the generated code Appendix G
4.1 Distributed Computing
MapReduce, a programming model for parallel processing of large datasets across distributed clusters, simplifies parallel computation by abstracting away distributed system complexities. A MapReduce program comprises two phases: 1. Map: Input data is partitioned into smaller chunks, each processed by mapper function to generate key-value pairs. Reduce: Intermediate key-value pairs are shuffled, sorted based on keys, and then processed by reducer functions to aggregate associated values.
LLMLIFT implementation. We compare the performance of LLMLIFF against MetaLift 25 MetaLift uses symbolic solver (Rosette (26)) perform the search. We evaluate the same 45 benchmarks as MetaLift. All the benchmarks have loops and require loop invariants to prove the functional equivalence of the source and the generated program. MetaLift solves 40 out of 45 with timeout of hour. LLMLIFT is able to solve 44, i.e., generate the correct translation as well as the required invariants to prove the correctness. LLMLIFT solves 4 additional benchmarks on which MetaLift times out. In addition to solving more benchmarks, LLMLIFT solves them much faster. It takes less than 1 minute on average to solve each benchmark when MetaLift has take an average of 3 minutes to solve. The amount of effort required to build LLMLIFT is also significantly less than Metalift as does not require the developers to provide any search-space description for PS and invariants. As Metal.ff requires over 1000 LoC for the description of these search-space, L.MLIFFT requires only 100 lines of prompt.
4.2 Network Packet Processing
Network packet processing hardware, such as routers and switches, lacks flexibility post-development, preventing experimentation with new data-plane algorithms. Recently, verified lifting approach [22] was introduced to simplify this process. This compiler offers the developers with two constructs: 1.
packet transaction language (subset of the language) to express the semantics of these data-plane algorithms 2. compiler [22 that translates the packet processing algorithms to the instruction set of programmable switch devices. Atoms are introduced as an instruction set of the hardware to represent the atomic operations supported by the hardware. Compiler translates the packet transaction algorithm to a sequence of atoms resulting in a different programmable switch configuration.
LLMLIFT implementation. We implement the Domino compiler using LLMLIFT by defining the semantics the atoms in the prompt. We compare the performance of our implementation against MetaLift's 's implementation. All benchmarks in Domino are imperative C programs without any loop constructs, so no loop invariants are required for these benchmarks. The generated PS are verified using SMT solver. MetaLift solves all the 10 benchmarks with average time of 6 seconds. LLMLIFT is also able to transpile all the 10 benchmarks but with an average time of only seconds. Similar to the Spark case study, we do not require developers to specify the search-space for PS. While MetaLift requires over 100 LoC to describe this search-space, LLMLIFT only uses R.70 lines of prompt. In summary, LLMLIFT shows similar performance to the existing compiler but can be built using much less effort.
4.3 TACO
automate the translation of C++ code to TACO.
LLMLIFT implementation. Tab. [ we compare the performance of C2TACO and LLMLIFT for all the benchmarks. We use the same 90 mins timeout for each benchmark that was used in the original C2TACO evaluation [6. C2TACO solves 57 out of the total 60 benchmarks, while LLMLIFT successfully solves all 60 benchmarks. The 3 benchmarks that C2TACO fails to solve
'Casper [5] is not functional and Mold is not open-sourced.
8

---

Tool
BLAS
DSP
DSPStone
makespeare
mathfu
simpl_ array
UTDSP
darknet
C2TACO
100%
100%
100%
100%
91.6%
90%
100%
92.8%
LLMLIFT
100%
100%
100%
100%
100%
100%
100%
100%
Table I: Accuracy on various benchmarks for TACO.
require expressions of depth greater than 4. Due to its enumerative approach, C2TACO struggles to find solutions for these cases. We attempted to run these 3 challenging benchmarks with extended timeout of day, but the C2TACO was still unable to find a solution. C2TACO uses over 1000 LoC for implementing the heuristics to scale the symbolic search. In contrast, LLMLIFT relies simple 100 lines of prompt (task instruction + DSL semantics) to achieve better performance than C2TACO. C2TACO takes an average of 41 seconds while LLMLIFT average solving time is 2 seconds. We also perform an experiment to test the scalability of C2TACO enumerate apporach with more complex benchmarks than the ones used in the original evaluation. We include the results in Appendix C
4.4 Tensor Processing
Many domains, such as image processing, signal processing, and deep learning, have legacy code written in high-level languages that operate on individual values of the input and perform specific operations. To leverage the optimizations provided by deep learning frameworks or hardware backends like GPUs, this code needs to be lifted to the operators supported by these languages. Prior work 24 introduced a tensor IR that can translate sequential programs to six different hardware and software backends automatically using a verified lifting approach.
LLMLIFT implementation. We evaluate LLMLIFT against Tenspiler (24] on the 23 benchmarks from the image processing and ML kernel domain Tenspiler is able to solve all 23 benchmarks. LLMILIFT also successfully solves all 23 henchmarks, including generation of the correct proofs 6 However, is important to note that Tenspiler's 's synthesis algorithm relies on three domain-specitn optimizations to achieve scalability. These optimizations require significant effort to implement, with over Rs 1200 LoC written by a domain expert. In contrast, LLMLIFT uses R320 lines of prompt to solve these benchmarks. It does not rely on any user-defined heuristics, which showcases its ability to generate correct solutions without the need for domain-specific optimizations. To check the scalability of Tenspiler's s symblioc approach, we remove all the optimizations. Tenspiler, without the optimizations, can only solve out of the 23 benchmarks with a timeout of hour, highlighting the importance of the domain-speciftr optimizations for its performance. These results highlight the ability of LLMLIFT to solve complex benchmarks without relying on domain cemainn-peccife specific heuristics. Moreover, LLMLIFT solves these benchmarks faster than Tenspiler with all its optimizations enabled. LLMLIFT takes an average time of 95.89 seconds to solve each benchmark, whereas Tenspiler takes 115.14 14 seconds.
4.5 Two-phase Approach for LLMLIFT
In this section, we evaluate an alternative approach to the two-phase method described in Sec. 3 where we generate the Inv(s) and the PS together in single step. To test this, we prompt the model in one-shot setting, providing example that demonstrates generating the PS and the In((s) simultancously. We merge the prompts described in Fig. 6 and Fig. 7 to create a unified prompt for this experiment.
Due to budget constraints, we limit this experiment to the tensor processing domain, which represents our most complex DSL with 37 operators. We use the same query budget as the two-phase approach. When prompted to generate the invariant and PS together, LLMLIFT successfully solves 20 out of the total 23 benchmarks. In contrast, the two-phase approach described in Sec. Bec.Esslvver solves all 23 benchmarks. We hypothesize that the reduced performance of the single-phase approach may be attributed to the increased complexity of generating both the PS and the Twv(s) simultaneously. Moreover, the two phase approach enables the model to leverage the generated PS when constructing the invariant. By having access to the PS, the model can more effectively reason about the necessary conditions and constraints required for the invariant to hold.
'We refer the readers to the paper 24 for more details on these benchmarks. We also evaluate LLMLIFT on these benchmarks using other LLMs and present the results in Appendix

---

Related Work
Code Transpilation for DSLs. Several approaches have been proposed for automating the task of translating legacy unoptimized code to DSLs. These range from symbolic rule-based approaches []] to search-based verified lifting approaches 7 27 25 and neural approaches p 28 Most of these tools are either optimized for specific domain or require domain expertise to scale. In contrast, LLMLIFT simplifies the process of building lifting tools by leveraging LLMs. Closely related to our work is 20) where IR is designed for low-resource languages and then combination of LLM and compiler techniques used to reliably generate code for these languages.
Code Translation for Mainstream -awereamttt--Maieeaeaaaaa Mainstreamtt Languages. The closest work to ours is by Roziere et [28] on sequeence-t--sequene model translate code between C++, Java, and Python. Our work differs in two key respects: we target lifting to DSLs, and our LLM based approach produces formally verified code. The objective of verified lifting to map functional programs the operators of a DSL in a semantics prenttiiiip manner. Translating between mainstream languages has its own set of challenges: 1. Different languages support various constructs, making direct mapping challenging: 2. Disparities in type systems across languages must be handled, and, 3. Generating accurate verification conditions and formal proofs for equivalence checking across diverse language constructs is complex. Due to these challenges, prior work in mainstream-to-mann to-manstreamm translation, such as (88) often relies on test-case- based approaches demonstrate semantic equivalence, rather than formal verification. Such approaches do not provide any correctness guarantee in the generated code, and hence are risky to deploy in practice.
LLMs for Code. LLMs are trained on massive amounts of code from various sources, leading to impressive performance on programming tasks such code generation [2 13, repair, testing, and transpilation. While the use of learning to synthesize proof artifacts, specifications, and models in formal methods not new [8]. recently LLMs have been successfully employed in such tasks (e.g., [5 16 ). However, generating reliable code from LLMs remains challenging due to the stochastic nature of these models and the difficulty in creating verification oracle for complex specifications. With I.MLIFF, we demonstrate the first approach to verified code generation with LLMs, albeit in the limited setting of transpilation for side-effect- code.
Conclusion
We presented principled approach to leverage LLMs for code transpilation. Unlike prior L..--based transpilers, our transpiled code is provably equivalent to the input, while also takes significantly less time generate compared to prior non LLMM-baed approaches with correctness guarantees, as demonstrated in transpiling to DSLs used across range of application domains.
7 Limitations
While LLMLIFT demonstrates impressive performance across four DSLs, there are few opportunities for future improvements. Currently, our approach generates program summary and checks only for syntactic correctness, ensuring that the generated expressions are compatible with the SMT solver. We then generate invariants corresponding to the program summary, which are formally verified for correctness. However, incorporating a semantic filtering step using test cases could potentially eliminate some spurious program summaries. Another limitation of our current approach is that we use Boolean feedback to check the correctness a solution. Providing more granular feedback, such counter-examples from the thcorem prover or compiler error messages, can possibly help guide the LLM towards generating correct solutions more efficiently.
10

---

Acknowledgments and Disclosure of Funding
We would like thank Federico Mora Rocha, Elizabeth Polgreen, Rishabh Singh and the anonymous reviewers for their insightful feedback.
This work was supported in part by DARPA Contract FA8750-23-C-0080 (ANSR), a Google BAIR Commons project, C3DTI, NSF grants 115-1955488, IIS IIS-2027575, ARO W91 INF21 10339, ONR N00014-21-1-2724, and DOE award DE-SC0016260, DE-SC0021982, and the Sloan Foundation.
References
[1] Cosmin Radoi, Stephen J. Fink, Rodric Rabbah, and Manu Sridharan. Translating imperative code to mapreduce. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA '14, pages 909-927, New York, NY, USA, 2014. ACM.
[2] Armando Solar-Lezama Liviu Tancau, Rastislav Bodik, Sanjit A. Seshia, and Vijay A. Saraswat. Combinatorial sketching for finite programs. Proceedings of the 12th International Confer- ence Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 404-415 ACM Press, October 2006.
[3] Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, and Ashish Tiwari. Oracle-guided component- based program synthesis. In Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering (ICSE), pages 215-224, May 2010.
[4] Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. Program synthesis. Found. Trends Program. Lang., 4(1-2):1-119 2017.
[5] Maaz Bin Safeer Ahmad and Alvin Cheung. Automatically leveraging mapreduce frame- works for data-intensive applications. In Gautam Das, Christopher M. Jermaine, and Philip A. Bernstein, editors, Proceedings of the 2018 International Conference on Management of Data, SIGMOD Conference 2018, Houston, TX, USA, June 10-15, 2018, pages 1205-1220. ACM, 2018.
[6] José Wesley de Souza Magalhães, Jackson Woodruff, Elizabeth Polgreen, and Michael F. P. O' O'Boyle. C2taco: Lifting tensor code to taco. In Proceedings of the 22nd ACM SIGPLAN International Conference Generative Programming: Concepts and Experiences, GPCE 2023, page 42-56, New York, NY, USA, 2023. Association for Computing Machinery.
[7] Alvin Cheung, Armando Solar-Lezama and Samuel Madden. Optimizing database- backed applications with query synthesis. ACM SIGPLAN Notices, 48(6):3-14. 2013.
[8] Maaz Bin Safeer Ahmad, Jonathan Ragan-Kelley, Alvin Cheung, and Shoaib Kamil. Automati- cally translating image processing libraries to halide. ACM Transactions on Graphics (TOG), 38(6):1-13, 2019.
[9] Benjamin Mariano, Yanju Chen, Yu Feng, Greg Durrett, and Işil Dillig, Automated transpilation of imperative functional code using neural-guided program synthesis. Proc. ACM Program. Lang., 6(0PSSLA), April 2022.
[10] Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. Bert: Pre-training of deep bidirectional transformers for language understanding. In North American Chapter of the Association for Computational Linguistics, 2019.
[11] Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan. Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert- Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei. Language models are few-shot learners. In Proceedings of the 34th International Conference on Neural Information Processing Systems, NIPS'20 20, Red Hook, NY, USA, 2020. Curran Associates Inc
11

---

[12] 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 I Lamy-Poirier, João Monteiro, Oleh Shliazhko, Nicolas Gontier, Nicholas Meade, Armel Zebaze, Ming-Ho Yee, Logesh Kumar Umapathi, Jian Zhu, Benjamin Lipkin, Muhtasham Oblokulov, Zhiruo Wang, Rudra Murthy, Jason Stillerman, Siva Sankalp Patel, Dmitry Abulkhanov, Marco Zocca, Manan Dey, Zhihan Zhang, Nour Fahmy, Urvashi Bhattacharyya, Wenhao Yu, Swayam Singh, Sasha Luccioni, Paulo Villegas, Maxim Kunakov, Fedor Zhdanov, Manuel Romero, Tony Lee, Nadav Timor, Jennifer Ding, Claire Schlesinger, Hailey Schoelkopf, Jan Ebert, Tri Dao. Mayank Mishra, Alex Gu, Jennifer Robinson, Carolyn Jane Anderson. Brendan Dolan-Gavitt, Dan- ish Contractor, Siva Reddy, Daniel Fried, Dzmitry Bahdanau, Yacine Jemnite, Carlos Muñoz Ferrandis, Sean Hughes, Thomas Wolf, Arjun Guha, Leandro von Werra, and Harm de Vries. Starcoder: may the source be with you!, 2023.
[13] Yujia Li, David Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser, Rémi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, Thomas Hubert, Peter Choy, Cyprien de Masson d' Autume, Igor Babuschkin, Xinyun Chen, Po-Sen Huang, Johannes Welbl, Sven Gowal, Alexey Cherepanov, James Molloy, Daniel J. Mankowitz, Esme Sutherland Robson, Pushmeet Kohli, Nando de Freitas, Koray Kavukcuoglu, and Oriol Vinyals. Competition-level December 2022.
code generation with alphacode. Science, 378(6624):1092-1120
[14] Baptiste Rozière, Jonas Gehring, Fabian Gloeckle, Sten Sootla, Itai Gat, Xiaoqing Ellen Tan, Yossi Adi, Jingyu Liu, Romain Sauvestre, Tal Remez, Jérémy Rapin, Artyom Kozhevnikov, Ivan Evtimov, Joanna Bitton, Manish Bhatt, Cristian Canton Ferrer, Aaron Grattafiori, Wenhan Xiong, Alexandre Défossez, Jade Copet, Faisal Azhar, Hugo Touvron, Louis Martin, Nicolas Usunier, Thomas Scialom, and Gabriel Synnaeve. Code llama: Open foundation models for code, 2024.
[15] Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin. Can large language models reason about program invariants? In Andreas Krause, Emma Brunskill, Kyunghyun Cho, Barbara Engelharrdt, Sivan Sabato, and Jonathan Scarlett, editors, Proceedings of the 40th International Conference on Machine Learning, volume 202 of Proceedings of Machine Learning Research, pages 27496 27520, PMLR, 23-29 Jul 2023.
[16] Saikat Chakraborty, Shuvendu K Lahiri, Sarah Fakhoury, Madanlal Musuvathi, Akash Lal, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, and Nikhil Swamy. Ranking llm-generated loop invariants for program verification. arXiv preprint 11X0022310.09342, 2023.
[17] Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In 2013 Formal Methods in Computer-Aided Design, pages 1-8, 2013.
[18) Sanjit A. Seshia. Combining induction, deduction, and structure for verification and synthesis. Proceedings of the IEEE, 103(1 1):2036-200 20501 2015.
[19] Susmit Jha and Sanjit A. Seshia. A Theory of Formal Synthesis via Inductive Learning. Acta Informatica, 54(7):693-726, 2017.
[20] C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576- 580, 1969.
[21] Matci Zaharia, Mosharaf Chowdhury, Tathagata Das, Ankur Dave, Justin Ma, Murphy Mc- Cauley, Michael J. Franklin, Scott Shenker, and Ion Stoica. Resilient distributed datasets: A fault-tolerant abstraction for in-memory cluster computing. In Proceedings of the 9th USENIX Conference Networked Systems Design and Implementation. NSDI'12, 2012.
[22] Anirudh Sivaraman, Alvin Cheung, Mihai Budiu, Changhoon Kim, Mohammad Alizadeh, Hari Balakrishnan, George Varghese, Nick McKeown, and Steve Licking. Packet transactions: High-level programming for line-rate switches. In Proceedings of the ACM SIGCOMM 2016 Conference, Florianopolis, Brazil, August 22-26, 2016, pages 15-28, 2016.
[23] Fredrik Kjolstad, Shoaib Kamil, Stephen Chou, David Lugato, and Saman Amarasinghe, The tensor algebra compiler. Proc. ACM Program Lang., L(00PSLA):7:1-77:22,, October 2017.
12

---

[24] Jie Qiu, Colin Cai, Sahil Bhatia, Niranjan Hasabnis, Sanjit A. Seshia, and Alvin Cheung. Tenspiler: verified lifting-based compiler for tensor operations, 2024.
[25] Sahil Bhatia, Sumer Kohli, Sanjit Seshia, and Alvin Cheung. Building Code Transpilers for Domain-Specific Languages Using Program Synthesis. In Karim Ali and Guido Salvaneschi, editors, 37th European Conference on Oriented Programming (ECOOP 2023). volume 263 of Leibniz International Proceedings in Informatics (LIPlcs), pages 38:1-38:30, Dagstuhl, Germany, 2023. Schloss Dagstuhl Seiinizz-Zentrun für Informatik.
[26] Emina Torlak and Rastislav Bodik. Growing solver-aided languages with rosette. In Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Progrumming & Software, Onward! 2013, pages 135-152, New York, NY, USA, 2013. ACM.
[27] Shoaib Kamil, Alvin Cheung, Shachar Itzhaky, and Armando Solar-Lezama. Verified lifting of stencil computations. In Chandra Krintz and Emery Berger, editors, Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 711-726. ACM, 2016.
[28] Baptiste Roziere, Marie-Anne Lachaux, Lowik Chanussot, and Guillaume Lample. Unsu- pervised translation of programming languages. Advances in neural information processing systems, 33:20601-20611, 2020.
[29] Federico Mora, Justin Wong, Haley Lepe, Sahil Bhatia, Karim Elmaaroufi, George Varghese, Joseph E. Gonzalez, Elizabeth Polgreen, and Sanjit A. Seshia. Synthetic programming elicitation for text-to-code in very low-resource programming and formal languages. In Thirty-Eighth Annual Conference Neural Information Processing Systems (NeurIPS), 2024.
[30] C. A. R. Hoare. An axiomatic basis for computer programming. 12(10):576 -800 oct 1969.
Commun. ACM,
[31] Mike Barnett and K. Rustan M. Leino. Weakest-precondition of unstructured programs. In Proceedings of the 6th ACM SIGPLAN-SIGSOF Workshop on Program Analysis for Software Tools and Engineering, PASTE '05, page 82-87, New York, NY, USA, 2005. Association for Computing Machinery.
[32] OpenAl. GPT 4o. httppsr//oeeaaaaoocw/w/eeeelllla 2024.
[33] Anthropic. Claude 3.5 Sonnet. 2024.
[34] Google. Gemini 1.5 Pro
2024.
[35] Meta. Llama 3.1 8B. http:///uugiiiifeecoooocmmmmmmmr 2024.
[36] Mistral AI and NVIDIA. Llama 3.1 8B. Mistral-Nemo- Instruct-2t4rt 2024.
https://wuginngfcee.c//mttttaaa
13

---

Appendix
A
Algorithm
The transpile_com _ode algorithm shown in Fig. 5 translates the source code of a program into a target language using LLM. The cource_code parameter represents the code to be transpiled, and num_iters and n specify the number of rounds to generate PS and Invs and the number of PS and Trus to generate in each round, respectively.
The seen_ps_son _s_sls set keeps track of all PS that have been processed by the algorithm. The algorithm operates in a loop that runs for num_iters iterations (line 4). In each iteration, the algorithm calls get_pss_sols (line 8) to generate n different PS solutions for the given source_code from LLM, and tells LLM to not generate any PS in the seen_ps__s0 _p__solss set. This is because PS solutions are processed in previous iterations and did not yield verifiable translations, so we deem them incorrect. For each generated PS, the algorithm first checks if it has been seen before by looking it up in the seen_ps_soli set (line 11). If the PS has been encountered previously, the algorithm skips it to avoid redundant processing. If it is new, the algorithm parses it to check for syntactic validity using the parse function (line 19). If the summary has invalid syntax, it is discarded, and the algorithm moves on to the next summary. If the PS is syntactically correct, the algorithm proceeds to generate (s)(s) for it. It maintains a set called seen_iny aree_iiv_soll__eee www_ssslsfooooo of invariants that have been processed for the current PS to avoid redundant processing. It also checks each generated /no(s) syntactic validity and discards it if it is not.
that keeps track
If both the PS and the Inc(s) pass the syntactic validation, the algorithm proceeds to verify their correctness using the verify function (line 44). If the verification succeeds, the algorithm returns the PS (ps_sol) as the final transpiled code (line 45).
The algorithm continues this process of generating PS and Ines and verifying their correctness until a valid solution is found or the maximum number of tries is reached. If no valid solution is found within the given number of tries, the algorithm returns None (line 48), indicating that the transpilation was unsuccessful.
B Prompts
In this section, we present an instantiation of the prompt structure shown in Fig. The prompt shown in Fig. [connssst of several components designed to guide the language model in generating semantically equivalent code using a restricted set of functions and constants. The prompt begins with clear task description that instructs the model that its goal is to rewrite the given C++ function using only the provided functions and constants while maintaining semantic equivalence. Next, the prompt includes set of instructions. These constraints are designed make the generated code easier to parse and translate into format suitable for theorem provers. The prompt then provides a set of defined functions in Python. These functions define all DSL operators that the model can use to rewrite the given C++ function. Finally, the prompt includes the test function in C++ which the model should rewrite using the provided functions and constants.
In Fig. 7 we present a one-shot prompt designed to guide the language model in generating loop invariants for the given test function. This prompt is similar in structure the program summary guessing prompt: it provides a clear task description, set of instructions, and examples to guide the model in generating the desired output. The prompt instructs the model to prove the assertion in the test function by finding a loop invariant using the defined functions. It includes specific constraints on the generated loop invariant, such as using only the defined functions, avoiding loops, using a single return statement, inlining expressions, and generating separate invariants for each loop in the test function. These constraints are intended to simplify the parsing of the generated invariants into SMT formulas, making it easier to integrate them into automated theorem provers. Additionally, the prompt provides a template for the invariant structure, guiding the model in constructing the loop invariant as a Python function that takes the loop variables and relevant data structures as input and returns a boolean expression. The invariant should involve comparisons the loop variables using operators and expressions, and an equality check for the loop-dependent variable using the defined functions. The prompt also includes an example to demonstrate the expected format and structure of the loop invariant. Example I shows a test function that performs element-wise subtraction of two
14

---

def seen_ps_sols: set[str] set()
str, nin_iters: int, n: int) >> str:
in range iters):
Gets "n" PS solutions from LLM for the given "source_code"
Assuning all solutions seen_ps_.oos" incorrect, "et_.s__ools"
tells the LLM to not generate any solution in this set.
ps_sols: list[str] = got_ps_sols(n, source_code, seon_ps_sols)
For ps_sol in ps_sels: 10
ps_sal seen__s__ools
12
# No have processed this PS before. continue
13
14
else:
15
Otherwise, we add it to the set of seen Ps solutions. seen_ps_.oos. (pd
17
18
this invalid syntax if not (prse(ps_)))): continue
19
20
22
Generate invariants for this PS
seen Lnvss for_ps: set[str] set()
24
Gets "n" Iny solutions from LLM for the given PS solution "ps_sol".
25
inv_sals: list[str] get__in__sols_forre for inv_sol in inv_sols:
ps_sel)
26
27
inv_sol in have
this Inv solution for this PS before.
29
continue
else:
31
Otherwise, we add it to the set of seen Inv solutions for this PS.
32
seen_inv_sols__ ps. (id(iv__so)))
33
34
this Iny has invalid syntax. if not porse(inv_sol): continue
36
38
a Verify Inv and PS. In this call, convert all PS and Inv solutions syntax an solver. The solver then checks senantic equivalence between the solution and the source progran, using the generated invariants as proofs.
39
60
41
'verify" returns True and only if the PS solution is equivalent to the source program. verify(inv_sdl, ps_sol): return ps_sol
43
45
46
solution has been Found. return None
48
Figure 5: LLMLIFT's algorithm for generating PS and Ines.
matrices and provides two loop invariants. Example 2 shows the test function for which we need to generate the loop invariants.
To avoid regenerating the same incorrect solutions, the prompt also includes all the syntactically correct solutions that have been generated so far, along with a message saying These generated programs are incorrect. Do not generate the same. Please generate another program.
PS Guessing Prompt
Your task is rewrite the given lest C++ Function. You need use only the set provided lunctions and constanis to achieve this. The rewritten program should be semantically equivalent the function. Please do not generate any explanations.
#Instructions
# Do for/hiile loops rewriting function.
# 2. The rewritten program should just be a single return statement of the form return_ var provided functionn(..)
Inline expressions, not internediate
#defined functions
from typing isport Any, Callable, List
def ite(cond:
bool, if_ then: Any, if-else: Any) +> Any: return if_then else if_else
reduce_sun(x: Listlint]) int:
15

---

return 8 if len(x) else X[o] reduce_sum(x([::]
def vec vec_elermieenullg List[int], y: List[int]) => List[int]:
return
[]
len(x) < or not len(x) len(y)
else [x[0] y[e], vve__elemiise.ml y[1:3)
def reduce_naxte List[int]) -> int:
return
x[0]
len(x)
else (x[0] x[6] reduuc__nax(((:3) else :))
def vec (ec_elemmisn.odi(:: List[int], y: List[int]] -> List[int]:
return
[]
len(x) < or not len(x) len(y)
else [x[0] y[ol, vec_.elemiise.eddidtl..... y[1:3)]
def vec_elemisn_sau(Cr List[int], y: List[int]] >> List[int]:
return
[]
len(x) < 1 or not len(x) len(y)
else [x[0] y[ol, vec__elamise_suub([11.... y[1:3)]
def vec_elemmisnddiv(t List[int], y: List[int]] >> List[int]:
return
[]
if len(x) < 1 or not len(x) == len(y)
else [x[0] y[o], wer_ellmwis__iiv((l. y[::])]
//test function kinclude <vector> using nanespace
tast (vector<int> input, max_pos)
int nax_val input[e];
for (int 1; nax_pos; i+t) if (input[i] nax_val)
nax_val input[i]; max_val;;
}
Figure 6: Prompt for guessing the PS.
16

---

Invariant Guessing Prompt
Your Lask is to prove that "assertion" true in "lest' function. The ussertion can be proved by finding loop invariant using the delined functions, Write the loop invariant python booleun formula.
#instructions:
defined functions 2. Do not use foz/while loops for rewriligg the function.
need
loop invariont.
rewritten program should just be single return
return yar provided__uunctionn function((..)
4. Inline all the expressions. Do not use intermediate variables.
5. Generate separate loop invariants for each loop test function.
6. invariant structure
def invarianti: int, input: List[int), ss. int, weight: List[int]) -> bool: return op exprO and op exprt) and ss = operation over defined functions
Examplel:
Adefined Functions
def rrc_elermise_subCe list[int], y: list[int.) list[int]:
return
[] if len(X) < or not len(x) == len(y)
else LX[9] yl8l, wwweemise.suuttiiiieeeeeeeeeeeee y[1:])]
def matrix_nlnwise wwrrxy/lmwis...uanerri... list[list[int],, matrixu:: listDlistDint]) listDlist[int]]:
[]
len(natrix_x) or not len(matrix_x) len(matrix.y)
else [
secemisse_uunnatrix.co netrixcy(e)),
matrrik.lleemmsssssuuttaak..... matrix.((::3),
//tast function
vectorswectoruuint... to rest/eetoorsvettoruunnt..t base, vectorsvectorrunnt..... active)
vectorivectermuits..ee out;
uint8_t t base size();
uint8_t base[0].sizen
for (uint8_t row 8; row n; row++) [
vectorsuint8_t: row_vee;
for (uint8_t col 8; col col++)
uint8_t pixel base[row] active[row][col)
(ackipxi
out bash.vec
assert out = matrix_elumisse_uattta active);
}
def invarianti (row, col, base, active, out):
return row >e and row <= base. and out matrrx_elmmise__ubhhaae (baseI: active[:rowl) def invariant2(row, col, base, return row >0 8 and rew (éseesize(() and col >- and col <s [ase[e].sizeg) and row_vec vec_elenwise_eee rrrc_elenwis__uubbuueee sub(blse(row[[[ccol], active[roo][:col]) and out == wttp:ellewiseeeuhhhhaeeeee :row] active[:raw])
out):
Exaplee2:
#defined functions
from typing import Callable,
def sub((: int, matrixx:: List[List[intt]) >> List[List[int]]: return
[]
if (en(natrix_x) <
else [vec_stalar_subee matri smatrix_scalar_sub6.. motrix_X(1:11
natrix_scalar (a: int, motrixx: List[list[ine])) List[List[int]]: return
[]]
if len(natrix_x) <
else vec_sscaar__mlle natrix,x())), <matrix_scalar.mule matrixx(1::11
def satrixascallr..divaa: int, matrix.x: List[List[in:]] >> List(List(int]):
return (
[]
if len(natrix_x) <1
(vec_stalar_dies div(e, me0)) mmatrix_scaar. div(a. metrix
17

---

def baalar_nttrix_subff int, netrix_x: List(List(int]) List(List(int]):
return <
[]
if len(natrix_x) <.1
else [scalar_vec_subte natrix_x(e)),, "scalar siralarr metrix_x(1:11
//tast function #include <vector> using namespace std;
int masoorn input, vectorsint> weight) {
for (int = 8; i input. siput.size(;; i++)
56 input[i] input[i];
assert = reduce stt.eeeeeeeeeeeeeeeelle.e.eeeeee input))
Figure 7: Prompt for guessing the loop invariant(s).
C Scalability
void Dourth_in.placeiint arr, int for (int 8; ++1 {
arrlij arrLi] amrlll; arrtil arrtil arr[il;
void tast1 (intk arr, int n)
expression
2
for (int i 8; < n; +-1) { arr[i] arr(i] arr[i] arr(i] arr(i] arr(ll;
out[i] arr[i]] arr[i] arr[i] arr[i]
4
//Incorrect TACO expressions
5 )
11
aut(i) air(i) arr(i) out(1) Const arr(1.1) out(k) Consl arr(l.k,1)
//TACO expression
7
out[i] = arr[i] arrtij arrtil arrtil arrtil
13
(b) Example of synthetic benchmark with expression length 5.
(a) Benchmark on which C2TACO fails.
Figure 8: Scalability evaluation of symbolic solvers using synthetic benchmarks.
In this section, we evaluate the scalability of symbolic solvers the context of verified lifting-basse based tools. The benchmarks used in the evaluation of these tools are often carefully selected and limited in scope, allowing the tools to perform well within their intended domain. However, in this experiment, we aim to demonstrate that symbolic tools relying domain-specift heuristics can be brittle and fail to scale when the complexity of the benchmarks increases beyond a certain threshold.
We begin by evaluating C2TACO. Upon careful analysis of the benchmarks on which C2TACO struggles, we observed that the tool often times out when tasked with generating expressions of length greater than 4 One such example is illustrated in Fig. 88 where the source performs an in-place operation on an array arr of length and raises each element of the array to the power of C2TACO enumerates candidate expressions using tensor operators and index variables in increasing order of expression length. C2TACO enumerates =33k candidates. We illustrate some the incorrect expressions in Fig. 8al
To test the scalability of C2TACO, randomly generated of 10 benchmarks with expressions of varying lengths, ranging from 5 to 10, incorporating various arithmetic operations (see Fig. 8b for an example). We used a timeout 90 minutes for C2TACO, as reported in the original evaluation. C2TACO was unable to solve any of the 10 benchmarks within the timeout. In contrast, LLMLIFT, was able to solve all benchmarks correctly in less than 2 seconds. This performance can be attributed to the ability of language models to identify patterns and learn from the context provided in source code. To further test the capabilities of L.I.I. we evaluated on a variation of the benchmark shown in Fig. 8a where each element of the array is raised to the power of 20 instead of
18

---

vectar<vactor<intt> screen_blend_ wwremn.ieen.Kyecttovvvettrrrsss base, vecter<vector<intt active) {
vecter<vector<intt> out; int m (ase.size();
base(0).size();
for (int row = row rou-t) {
vectorcint> row_vec;
for (int col = 8; col col+)) {
int pixel = baseIrow][cal]
active[row][col] (base[row]]cool] active[row[Ccol)) 255;
row_vec.pusil pt..ccpppsshbbac(peeel).)
10
out bash_bbc((row_e))
12
13
return out;
14
Figure 9: screen screen_blend blend benchmark source code.
Despite the increased complexity of the expression, LLMLIFT was able generate the correct solution efficiently.
D Qualitative Analysis of the Errors
In this section, we provide a qualitative analysis of the mistakes made by LLMs while generating code and proofs. In LLMLIFT, we use Python the IR and the PS and Inw(s) are generated in Python. The errors encountered can be classified into two categories: syntactic and semantic.
Syntactic errors occur when the generated code constructs are not compatible with the theorem prover. To mitigate this issue, we use a syntactic parser that translates the generated solutions to the language supported by the theorem prover. The parser ensures that only supported constructs are present the solutions and rejects any candidates that do not comply with the theorem prover's syntax.
One common source of syntactic errors is the of Python-specific constructs that not supported by SMT solvers. Although we prompt the model to generate solutions using only the constructs provided in the prompt's scope, controlling the exact code generated by the model can be challenging. Fig. 10 illustrates examples of program summaries generated by GPT-4 for the screen blend benchmark that contain unsupported constructs. For instance, the first solution in Fig. [O] uses a for loop, which is not supported by SMT solvers. Similarly, the second and third solutions utilize Python's 's list comprehension syntax, which is also not directly supported by SMT solvers. List comprehension are supported in SMT solvers using empty lists and append functions, such as append (]).
Semantic eπrors occur when the generated code is syntactically correct but is semantically not equivalent to the given S. In the context the screen blend benchmark (shown in Fig. ( examples of semantically incorrect programs generated by GPT-4. The
Fig- [1 illustrates first program incorrectly subtracts term from the base matrix instead of subtracting it from the of base and active matrices. The second program suffers from similar issue. It subtracts an incorrect term from the active matrix. Specifically, the term being subtracted m__mlllle (base, active), matrix_scai
matrix elemwise _eediieediiiiiiii matris el elemwise seawwss_mmull se_mulll____eeee (base, active))), which is different from the one in the given program.
mul (32,
E Proof of Equivalence
We use Floyd-Hoare Logic (FHL) to establish the validity of generated programs [30]. In FHL, verification problem is represented
Hoare triple ((B), where: 1. A is the pre-condition. 2. P is the program to be executed, and 3. B is the post-condition. An example of a valid Hoare Triple {z = 0} == 1(x 0}. The Hoare triple states that if x 0 before executing x := + then after executing the program, will be greater than 0. To establish the validity of a Hoare triple, we prove that executions starting from states satisfying A, after executing program P. result in states satisfying B. This involves finding Boolean predicate called the verification condition (VC) that characterizes the set of pre-conditions from which every execution of P leads a state satisfying B. Formally, we need to prove that the VCC is true given pre-condition, i.c., A + VC,P,B).
19

---

def screan_ blend 8base:: List[List[int]], active: List[list[intt]) >> ListLlis([int]]: serrix.elewsse_addd
batrix_elemmise_ubby base,
nntrix.llemise_dee div(
natrix_eleme se (base, active),
vec_scalar_ (32,, (1 for rbns)
)
10
active
def 3lend_8(base, List[List(int]], active: List(List[int]] List[List[int]]: return matrix_elowisee.ne
natrix_elemiis su.
base,
natrix_el porrx_eelewiisee se_iv(
elemwise_mull active).
(ec_scalar_mi(CC [L1]Herr(base(88))eeetttees)))
),
11
def screan_blemt blend_ baetr_llee___bbeeee 8(bas:: List[list[int]], active: List[List(intt)) List[List[int]]: elwerieeeeewsseddd
vatrix.elemise_subee base, natrix.olemise_die
natrix_eleman se_ se_ne, active),
vec_scalar (32, (UD==leemcbasse)))))eeeeeesss))
).
10 active
Figure 10: Programs rejected by LLMLIFT's syntactic parser.
def screen bleeed_bbeeddeee b(bae_ List[List[int]], active: List[List[int]]) >> List[List[int]]: return natrix_elamise_adde natrix_elemise.ce base,
Axrrixeeeemise_div
matrix_elemit se mel (base, active),
scalar_natrix_dii base)
).
10 active
11
screen, 8(base: List[List(int]], active: List[List(int]]) List[List[int]]: return matrix_elemwsseadee base,
antrix_elemisee.uu
active,
natrix_elemiiee se_div
perix_elemmise. (base, active).
natrix_scalar (32, natrix_elemise aaaaiiiieenuuubbeeeeeeeeee (buse, active))
10
Figure 1I: Programs rejected by theorem prover for semantic incorrectness.
Standard techniques exist to generate verification conditions from given source program B1. For programs containing loops, an additional predicate called loop invariant is required. This invariant helps prove that the post-condition remains valid regardless of the number of loop iterations. The inference rules provided by FHL can be encoded into format that can be fed into automated theorem provers or SMT solvers. This encoding allows for the mechanical checking any Hoare triple's
validity. In Fig. [3 we show the VCs generated for the source program in Fig I2
20

---

vectarcints test(vectorsint> base, vactor<int> active) vectorcint> out; for (int i = 8: base. sise:size(); ++1) put.push. push return out;
out
back baselil);
Figure 12: Source Code (S) for proof.
Initial Condition
Tnu(i 0, out 0. active, base)
Ineli, out, active, base) A (i < base.size()) + Inv((i + 1) out.push back back(actiuell + baselil) active, base)
Preservation
Termination
Inv(i, out, active, base) < base.size()) + PS active, base)
Figure 13: Verification conditions for the source code in Fig. 12
def invariant i): return >= 0 and <= size( and out
base[:i])
def PS(out, aS active,
return out
base)
Figure 14: PS and Inw for the source code in Fig. 12
Proof:
1. Initial Condition: Before the loop executes, O and out []. The loop invariant expresses out as the result of a pre_eeleeeiss se_add operator over the first elements of active and base. Since i 0, the rec_elemewise _dd operation is applied to empty list, resulting in empty list. Therefore, the invariant holds in the initial state.
Preservation Condition: The preservation condition ensures that the invariant holds throughout all iterations of the loop. This can be shown by induction. Assume the invariant holds at the i-th iteration. In the + 1)-th iteration, vec_elemewiss _e_ would compute the element-wise sum for the first + 1 elements of base and active, while the source program would push activeli + + baseli + 1] to out, making out equal to lec__elleeisss__dddeeeeee (activee i+]]] base[: i.e the RHS for this condition is true.
Termination Condition: The termination condition requires that the invariant implies the post- condition. When the loop terminates, i buse.sizz(), and both the PS and Tre expressions for out will be identical, i.e., the post-condition satisfied.
F
Code Generation
Once we have the verified program summary in the IR, the code generation phase uses syntax-driven rules to translate IR programs into the target DSL's concrete syntax. Given IR expression, the code generation function parses its operators and operands and translates each them recursively. Below, we show a snippet of a code generation function that translates IR programs to PyTorch. In this function, each IR expression type is matched against a translation rule: variables are mapped to their names (lines 2-3), literals mapped their values (lines 4-5), and function calls mapped to their corresponding PyTorch operators (lines 6-11).
For instance, the elemwise_ad operator in IR translates torch. add in PyTorch, and elemwise_su translates to subtract.. As a result, the IR expression b)) becomes torch. add(torch. subtract b)) in PyTorch.
Similarly, we want to translate the code another DSL, such as TensorFlow, we can simply change the specific operator rules to generate TensorFlow code. For example, the elemwise_ add operator
21

---

in IR would be translated to tf. add (line 9), and the elemwise_sub operator would be translated tf. subtract (line 11). Thus, the same IR expression (tw.iieeeeaddeeeiiiieeeeeeeee b)) b)) in TensorFlow.
would become tf. af. aod(tf.subtractee
def cexegen(expr: Expr):
if isinstance Var): return expr name
elif isinstance(expr, Lit):
return expr. v)
elif isinstance Call): f_name, args expr. name(), expr.arguments() if f_name == "elemwise_adee =_ddddd
return add (cdodegee((arr))())))) (codegen(args((1))))
10
elif f_name == "elemwise_suv s__b__sub return f"torch. "ttoorc.subtract(ee Subtract((codeeen((rrstt
{codegen(args((1333)
Figure 15: Code for translating IR expression to concrete syntax of DSL (PyTorch).
G Performance of Generated Code
The primary objective of verified lifting is to generate semantically equivalent programs in the target DSL from the source. DSLs are inherently designed to offer -omaiin-peccffic optimizations, and the performance gains observed post-tran cossttranlltiinn attributable to the implementation of operators within the DSL rather than the translation process itself.
In LLMLIFT, our aim was to replicate the existing VL-based compilers. We performed a manual verification of LLMLIFT'S output against the corresponding symbolic tools, confirming output equivalence of the two tools. Given this equivalence, the performance gains reported by the original symbolic tools are directly applicable to LLMLIFT's translations. Performance numbers for some of the domains are following:
Tensor Processing: The objective this domain is to generate tensor programs executable on tensor processing backends. Translations to this intermediate representation (IR) yield performance gains of 2.1x (NumPy) and 167.71 x (Py (PyCo) compared to sequential C++ implementations when compiled with GCC -03.
2. Distributed Computing:
The generated Spark implementations achieved an average speed-up of 15.6x compared to the sequential Java implementations. Additionally, when compared to manually written code by expert, the generated outputs performed competitively. For more details on the user study, we refer the reader the paper
3. TACO: The TACO compiler generates optimized GPU code. Translating programs the TACO IR results in a performance gain of 24x compared to sequential C++ programs when compiled with GCC-O3
It is important to note that finding a program with optimal performance on the target backend would require performing the search phase with specific cost (objective) functions. While finding an equivalent program in the target DSL is already challenging task, incorporating an optimization function into the search adds another layer of complexity. In addition, defining these cost functions is non-trivial in itself, as they must accurately capture the performance characteristics of the target backend. Currently, even without using cost functions, LLMLIFT is still able to generate performant code, described earlier.
H Python as IR
Python one the most widely represented programming languages in the training data these models. This ensures that the model can generate Python code reliably with minimal prompting, reducing the likelihood hallucinations. Python's highly syntactie nature facilitates easier parsing. This is beneficial 1. it allows for the development of drivax-driven parsers that can efficiently
22

---

translate the IR to the language supported by theorem provers and 2. It simplifies the process of translating the IR to the target DSL's concrete syntax.
Direct conversion to a DSL is challenging because many DSLs may not be well-represented in the model's training data (as illustrated in Fig. B}. In addition, it is also challenging to verify DSL programs using theorem provers as they do not provide support for these languages and it is not trivial to translate the DSL directly the language supported by them. On the other hand, many theorem provers have existing tools or libraries for handling Python-like syntax, making the verification step of LLMLIFT more reliable.
I LLMLIFT's Performance with Other Large Models
To evaluate if our prompts generalize across models, we evaluated LLMLIFT's performance using GPT- Claude 3.5 S3nnet[33], and Gemini-1.5-Pro(33.
We used the exact same setting as described in (zeroshht for PS and one-shot for Invv for this evaluation. We evaluated on the 23 benchmarks from the tensor processing domain. GPT-4o and Claude 3.5 Sonnet were able to solve all the benchmarks while Gemini-1.3 1.5-Pro solved 21 benchmarks (failed to guess the correct PS for the 2 unsolved benchmarks). The results show that prompts robust and generalize well across models, even without prompt engineering.
LLMLIFT's Performance with Smaller Models
To explore whether LLMLIFT could leverage smaller open-source models or if larger models like Claude and GPT-4 were necessary, we evaluated LLMLIFT using two recent open-source models, Llama3 8B 335 and Mistral Nemo 12.28 (36,, using Hugging Face's ' serverless inference API. We used the benchmarks from the tensor processing domain, which is the most complex among all the DSLs we evaluated. We use the same budget of queries and temperature settings.
Neither Llama3 and Mistral solved any of the benchmarks. Their solutions used Python constructs outside of the defined IR, which caused them to immediately fail our syntactic parser. Our results suggest that larger models can be more effectively used for the task of VL without requiring fine- tuning, for the following two reasons:
1. Instruction Following:
Larger models are better following the instructions to generate programs strictly with the defined DSL operators.
2. Handling Long-Cou Context:: With prompts that can grow in size to include all DSL operators and feedback, larger models manage long-context tasks more effectively.
K LLMLIFT'S Performance With Zero-Shot Prompt
At the time of writing, GPT-4 was the most advanced model, and we used one-shot prompting, as shown in Fig. 7 to generate loop invariants. Recently, with further improvements in the models, we experimented with simplified prompt to test whether zero-shot prompting could effectively infer invariants. Note that this prompt is zero-shot but includes some natural language instructions to guide the model on the structure of the loop invariant. We evaluated LLMLIFT'S performance using GPT-4o (2 Claude 3.5 Sonnet (33), and Gemini-1.5. 1.5- 34 We used the exact same prompts for generating PS, and the prompt described in Fig. 16 for inferring loop invariants. We used the same temperature settings and query budget for this experiment. We queried these models using their API endpoints. We evaluated on the 23 benchmarks from the tensor processing domain this domain has the most complex DSL. addition, all of them have loops and require loop invariants for proving equivalence of the translated programs with the source programs.
As shown in Tab. 2 we observe that GPT-4, the model used for all experiments in Sec. 4 does not perform well with zero-shot invariant prompt. A one-shot prompt, shown in Fig. 7 was necessary for generating accurate guesses of loop invariants. However, more recent models like GPT-4o and Claude 3.5 Sonnet were able to solve all 23 benchmarks even under the zero-shot setting. We also observed that Claude used the least number of queries to generate the correct solutions. Gemini did not solve 3 out of 23 benchmarks (failed to generate correct PS for 2 benchmarks and correct Inw for 1).
23

---

Model name
of benchmarks solved
GPT-4
GPT-4o
23
Claude 3.5 Sonnet
23
Gemini- 1.5-Pro
20
Table Zero-shot performance various proprictary models on tensor benchmarks.
Invariant Guessing Zero-Shot Prompt
Your task is generate the loop invariant "Inv' such that it is all the locations defined Generate single "Inv' expression which holds at all the locations. The invariont noods to be generated using only the functions defined below, Write the loop invariant as python boolean formula. ilnstructions:
any loops any python construct. Generale sepurate loop invariants for each loop test function. Retum loop invariant single boolean expression. Only
use
loop invariant.
return the invariant and na other code in code block.
def ieeeond:: bool, if_ then: Any, if_else: Any) +> Any: return th_then cond else if_else
def reduce_sumie List(int]) +> int: return if len(x) else x[O] reduce_suunX[1..
def rec_elermise_nee List[int), y: List[int]) List[int):
return []]
if len(K) < or not len(x) =* len(y)
else [x[o] * y[ol, pooccelemmsemmmllteeee y[I:3)]
def reduce_nax(e List[int]) +> int:
return
x[8]
if len(x)
else (x[o] x[e] reduca_nax(x(I:)) else reluce_nax(xI1:))
def vec_ vec_elermise List[int), y: List[int)) List[int]:
return
[]
if len(x) len(x) len(y)
else [x[9] + y[e], eed(eleeeeeeee((([ y(1:D)]
def rec_elemissnssbbee List[int], y: List[int]] List[int]:
return {
[]
if len(x) < 1 or not len(x) e- len(y)
[x[o] y[el, meee_eleemiee_su((tte y[1:3)]
def vec_elemiieeddivce List[int], y: List[int]) + List[int]:
return
[]
if len(x) len(x) len(y)
else [xto] // y[ol, sew.ellllwie__iiivdeeeee y(1:1)1
//test function #include <vector> using namespace std;
rnsnorn_part1 (yeetorrrty input, vectorsint> weight)
int ss 8;
size(: ie)
ss input[i] input[il;
assert ss aeduce_sun(ve__ell (input, input));

---

Use the following template to generate the loop invariant
* strong loop invariant should have the following properties:
# It should have boolean expressions over the loop index variable "1" to describe the valid range "1"
$ 2. It should have inductive expression describing the output variable "ss using the defined functions.
def invariant(1: int, input: List[int].
weight: List[int]] bool:
return expression over loup index variable and ss operation over defined Functions
Figure 16: Zero-shot prompt for guessing the loop invariant.
25

---

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 experiment section (Sec. 4 reflects all the claims made in the introduction.
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 or 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 other settings.
is fine to include aspirational goals motivation long as is clear that these goals are not attained by the paper.
Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: Yes
Justification:
Limitation section (Sec. is included in the paper.
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 in 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 well-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 on a few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low images are taken in low lighting. Or a speech-to-text system might not be used reliably to provide closed captions for online lectures because 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 grounds for rejection, worse outcome might be that reviewers discover limitations that aren't I acknowledged in the paper. The authors should use their best judgment and recognize that individual actions favor of transparency play an important role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: NA
Justification: We do not present any theoretical result in the paper.
Guidelines:
26

---

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 clearly stated or referenced in 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 or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main experi- mental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Answer: Yes
Justification:
Yes, included all the prompts and experimental details in the paper.
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, No answer 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 not.
the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible 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, if the contribution is specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access the model. In general. releasing code and data is often one good way accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of a large language model), releasing of model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require all submissions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) the contribution primarily new algorithm, the paper should make it clear how to reproduce that algorithm.
(b) If the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is new model (e.g., a large language model), then there should either be a way to access this model for reproducing the results or a way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may tricky in some cases, in which case authors welcome to describe the particular way they provide for reproducibility. In the case of closed-souse source models, it may be that access to the model is limited in some way (e.g.. to registered users). but it should be possible for other researchers to have some path to reproducing or verifying the results.
Open access data and code
Question: Does the paper provide open access to the data and code, with sufficient instructions to faithfully reproduce the main experimental results, as described in supplemental material?
Answer: Yes
Justification:
We are releasing all the benchmarks used for evalutation.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
27

---

Please see the NeurlPS code and data submission guidelines guides/CodeSubmi ssionPolicy) for more details.
While we encourage the release code and data, we understand that this might not be possible, "No" is acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for a new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurlPS code and data submission guidelines (https://nipg cttpssccccppccccccccc guides/Codeeubmi ssi onnolicy for more details.
The authors should provide instructions data access and preparation, including how 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. only subset of experiments are reproducible, they 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 as much information as possible in supplemental material (appended to the paper) is recommended. but including URLs data and code is permitted.
Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits. hyperparameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: Yes
Justification: All the hyperparameters (temperature, candidates) are included in the experiment section.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to a level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, or as supplemental material.
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: Yes
Justification:
The experimental evaluation is deterministic given a specific version of LLM and
verifier
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, confidence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should 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 mean.
It is OK to report 1-sigma error bars, but should state it. The authors should preferably report 2-sigma error bar than state that they have a 96% CI, if the hypothesis of Normality of errors 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 (c.g. negative error rates).
28

---

If eтrоr bars are reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments Compute Resources
Question: For each experiment, does the paper provide sufficient information on the computer resources (type of compute workers, memory, time of execution) needed reproduce the experi- ments?
Answer: Yes
Justification:
We just rely on the API calls to the language model.
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 compute required for each of the individual experimental runs as well as 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 make into the paper).
9. Code Of Ethics
Question: Does the research conducted in the paper conform, every respect, with the NeurIPS Code of Ethics https: ips. hccppbblccc/hhiicssiieeeleeeeeee
Answer:
Yes
Justification:
Reviewed the ethics and were followed for all the stages for this paper.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special cireumstances that require a deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., ., if there a special consideration due to laws 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: Yes
Justification: The goal of this paper is to improve code transpilation efficiency and we do not expect any negative societal impact.
Guidelines:
The answer NA means that there is no societal impact of the work performed.
the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negative socictal impacts include potential malicious unintended uses (c.g.. disinformation, generating fake profiles, surveillance), fairness considcrations (c.g., deploy- ment 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 par- ticular applications, let alone deployments. However, if there 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 generate deepfakes for disinformation. On the other hand, it is not needed to point out that generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used intended and functioning correctly, harms that could arise when the technology is being used intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
29

---

If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of MI.).
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 (c.g.. pretrained language models, image generators, scraped datasets)?
Answer: NA
Justification:
No misuse anticipated.
Guidelines:
The answer NA means that the paper poses such risks.
Released models that have high risk for misuse 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 access the model 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 a best faith effort.
12. Licenses for existing assets
Question: Are the creators original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Answer: Yes
Justification: Yes, all data sources and tool used for evaluation are cited.
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version the asset used and, possible, include a 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.
assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, swaeerswi thcode. com/ datasets has curated licenses for some datasets. Their licensing guide can help determine the license of a dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
If this information not available online, the authors are encouraged reach out the asset's 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:
We are releasing datasets as part of this submission.
Guidelines:
The answer NA means that the paper does not release assets.
Researchers should communicate the details of the dataset/code/model as part of their sub- missions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset used.
30

---

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, applicable, as well as details about compensation (if any)?
Answer: NA
Justification:
No human case study was performed for this paper.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribution of the paper involves human subjects, then as much detail as possible should included in the main paper.
According 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 Sub- jects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed 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: No human case study was performed for this paper.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Depending on the country in which research conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and expect authors 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 applica- ble), such as the institution conducting the review.
31


Reviews:
[{"review_id": "tmsG9R2EQj", "reviewer": "Reviewer_2Wxn", "summary": "The paper aims to solve the problem of conversion of source code from one language to any domain specific language (DSL) leveraging LLMs eliminating manual intervention. The primary contribution lies in the domain of automating the transpilation along with providing functional correctness proof simultaneously. Their technique LLMLift converts source language to an intermediate representation (IR, python in this work), generates program summary and invariants, uses program summary to check the functional correctness using a verifier and finally converts to a DSL. They have evaluated multiple benchmarks across domains: distributed computing, network packet processing, tensor processing and TACO (tensor processing compiler for GPU code). Their evaluations set them apart by improving on latency (6x on average) and having high semantic accuracy.", "questions": "See the part marked using (***)  below.", "limitations": "Leveraging generative models to solve the problem of transpilation and providing quantitative estimates of functional correctness simultaneously seems to be a timely and much needed solution in today’s tech diaspora. But usage of a model like GPT4 seems to be an overkill considering the resource requirement that it entails. Using a smaller model, that is trained to do sequence to sequence conversion along with target language library as a database in case of RAG can be thought of as a more efficient way to achieve the same. In the suggested method, there is dependency/ sole reliance on the model only to do the conversion to IR and then the target language, but not all DSLs would find the same degree of contribution in the training dataset of the models. Using RAG here gives the user more freedom. \n\nThe writing does not make it easy for the readers to understand the underlying sub-components and the handshake thereby. For instance, we do not know how the verifier works, the criteria on which it works and its logical complexities. \n\nThere seems to be a scalability issue for bigger codebases which would overshoot the supported prompt length of the model. We do not know how the code base is broken down into cohesive pieces and each forms a prompt. Also, for large code bases we see KV cache management, storage and communication to different compute nodes to be a serious problem. \n\n(***) The paper does not include the rationale behind many of their assumptions like:\na.\tWhy python was chosen as the IR, and how much of a benefit (in terms of correctness/ latency) it provides compared to a direct conversion without an IR. \nb.\tWhy is accuracy the right metric? Given we do not have much knowledge about the length, functionality and complexity of the source and the target languages. The authors fail to provide a comparison between the transpiled code and the DSL implementation designed by an expert. \nc.\tWhy was a temperature of 0.7 chosen and what is the impact of varying the same?\nd.\tWhy was GPT 4 specifically chosen given its huge size? And how would the design fair against self correcting models and AutoGPT kind of models? \ne.\tThe paper overall misses sensitivity and ablation studies making it difficult, if not impossible, to understand the impact of each of the design components.", "rating": 3, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "1.\tTimely problem considering the emergence of different accelerators.\n2.\tAutomated transpilation with integrated feedback and verifier makes the process independent and self-contained. \n3.\tUse of python as an IR improves user readability and is more probable to be accurate given the huge online corpus and training data on the same. \n4.\tZero-shot approach requires no retraining, but this could lead to issues as well. See weakness and detailed comments.", "weaknesses": "1.\tDSLs have less representation in the present LLM training dataset (more so lacking correct and efficient codebases). \n2.\tLimited novelty, as there already exists work, and the authors confirm the same, which use LLMs to transpile from one language to another and produce proof annotations separately. The effort in the current work is largely automating and integrating these two steps. \n3.\tUnderutilization of the GPT4 model which has a huge memory and compute footprint. \n4.\tThe zero-shot approach might not yield very good results if the LLM does not have sufficient training data on the DSL. On the other hand, a solution like RAG is more feasible as it can be finetuned and made context aware with minimum information on the DSL.\n5.\tThe end-to-end process of transpilation is not very clear. Although it sounds intuitive, the fine-grained steps are missing in the explanation, leading to a belief that the paper majorly contributes towards an efficient prompt-engineering for doing transpilation rather than having an innovative approach. \n6.\t The evaluation metrics are poorly chosen. Using LoC as a metric of effort is not fair where the model and the framework (GPT4, and it’s API along with the implementation platform) doing the transpilation work has a resource (compute, memory, LoC, energy etc.) requirement of many orders of magnitude higher than any of the conventional tools like C2TACO. \n7.\tAlthough the evaluation consists of many benchmarks, we are missing comparisons for many important DSLs like HDLs, GPU programming, OpenCL etc. These languages form the foundation of most of the new generations of the domain specific accelerators design framework.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Why GPT-4**\n\nWith LLMLift, our objective was to demonstrate that LLMs can be effectively used for the task of VL without requiring fine-tuning. We needed a model that was good in two things:\n1. Instruction Following: The model needed to generate programs strictly using the defined operators in a DSL.\n2. Handling Long-Context: The prompt can grow in size when incorporating all DSL operators and feedback, so the model needed to manage long-context tasks effectively.\nGPT-4 was the best model available that met both of these requirements.\n\nTo explore whether LLMLift could leverage open-source models or if larger models were necessary, we evaluated LLMLift using two recent open-source models (Llama3 8B and Mistral Nemo 12.2B) and another proprietary model (Claude-sonnet-3.5). Due to budget constraints, we used a subset of benchmarks from the tensor processing domain, which is the most complex among all the DSLs we evaluated. Specifically, we used 12 image processing blend benchmarks. We use the same budget of queries and temperature settings.\n\nOpen-source models, Llama3 and Mistral, did not solve any of the benchmarks. Their solutions use Python constructs outside of the defined IR, causing them to immediately fail our syntactic parser. Claude, on the other hand, successfully solved 9 out of the 12. Llama3 and Mistral are significantly smaller than proprietary models like Claude and GPT-4. The results suggest that larger models are better suited for VL. \n\n**Complexity of source programs**\n\nLines of code (LOC) are often used as a proxy for evaluating program complexity. In the benchmarks, the average LOC is 14. As described in the paper, our aim is for LLMLift to translate functional programs, and we observe that 10-20 lines of code are typical for these programs in the real world.\n\n**RAG is more feasible solution**\n\nTo clarify, LLMLift does not depend on the presence of specific DSLs in the training data of large language models to perform code translation. In fact, we demonstrate that LLMLift can reliably generate code in DSLs that the model may have never encountered during training, for instance our tensor processing DSLs and the TACO IR. With LLMLift, we introduce a structured prompting approach that explicitly includes the semantics of the DSL operators using an IR. The model's task is then to generate a program using only the operators defined in the prompt. Once we have a verified solution in the IR, we apply syntax-driven rules to translate the program into the concrete syntax of the DSL.\n\nRAG-based approaches rely on the source and target programs having similar representations in the encoding space. However, in the context of VL, the source and target languages often have completely different syntactic structures. For example, in the tensor processing domain, the source programs are written in vanilla C++, while the target language involves tensor operations like tensor-tensor arithmetic and tensor-scalar arithmetic. Moreover, multiple lines of code in the source language can be mapped to a single operator in the target (e.g., a loop adding corresponding elements of two vectors can be mapped to element-wise addition operator), and lifting-based transpilation is rarely one-to-one token-wise between the source and target languages. This significant syntactic difference makes it challenging to use a RAG-based implementation for generating a program summary in the DSL.\n\nThat said, we believe RAG could be beneficial in LLMLift in a different way—specifically, in selecting examples for few-shot prompting. RAG could be used to retrieve the most relevant examples for a new program, which could then be used to prompt the model. This approach might help reduce the sample complexity of LLMLift.\n\n**For large code bases we see KV cache management to be a problem**\n\nWe apologize, but we don't fully understand how KV cache management would be a significant issue in the context of VL. In the VL scenario, we're dealing with individual programs which are just a few hundred lines rather than large codebases, so the issues of KV cache management are not a concern for our current approach.\n\n**Why python as IR?**\n\nPython is the most widely represented language in the training data. This ensures that the model can generate Python code reliably with minimal prompting. Python's highly syntactic nature facilitates easier parsing. This is beneficial as a) it allows for the development of syntax-driven parsers that can efficiently translate the IR to theorem prover languages and b) It simplifies the process of translating the IR to the target DSL's concrete syntax.\n\nDirect conversion to a DSL is challenging because many DSLs may not be well-represented in the model's training data (see Figure 3). Moreover, it is also challenging to verify DSL programs using theorem provers as they do not provide support for these languages and it is not trivial to translate the DSL directly to the language supported by them. On the other hand, many theorem provers have existing libraries for handling Python-like syntax, making the verification step of LLMLift easier.\n\n**Why is accuracy the right metric?**\n\nAccuracy is the most critical metric for evaluating a transpiler, as the translated program must be semantically equivalent (checked by a formal verifier) to the given source program.  Another important metric is the performance of the translated code. Currently, the code generated by LLMLift significantly outperforms its corresponding program in the source language across all domains. \n\n**Why 0.7 as the temperature?**\n\nAt lower temperatures, these models generate more deterministic outputs, which limit their ability to explore diverse solutions. Due to budget constraints, we only experimented with temperature 0.7, which is close to the optimal temperature found for code generation in recent paper[1].\n\n### References\n[1] Evaluating Large Language Models Trained on Code. https://arxiv.org/abs/2107.03374", "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": "Cbt2K9X6bG", "reviewer": "Reviewer_KVm8", "summary": "The authors propose an approach named LLMLift, which utilizes large language models (LLMs) to achieve verified code transpilation. LLMLift not only translates a given program into its corresponding equivalent in the target language but also generates proofs for functional equivalence. The paper claims that this method outperforms previous symbolic-based tools in both the number of benchmarks transpiled and transpilation time, while requiring significantly less effort to build.", "questions": "- Why is there no performance comparison given in the experimental evaluation? Is it because the task is merely to translate DSLs and is not related to performance issues, or does performance remain similar as long as the DSL is generated?\n- How does the approach handle complex features in source languages that do not have direct counterparts in the target DSLs?\n- What are the common factors in tests that failed, and how can the approach be adjusted to address these issues?\n- Why use GPT-3.5 other than the latest version of GPT in Figure 3?", "limitations": "The authors have not adequately discussed the limitations of this paper.", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The paper is highly innovative. It fully explores and leverages the generalization capability, few-shot learning capability, and inherent domain knowledge of LLMs. Additionally, it transforms the code translation task from end-to-end generation into generating PS and INV with LLMs, which cleverly reduces task difficulty and enhances the utilization of LLMs. \n\n- The evaluation is thorough, covering multiple DSLs and comparison against a tensplier proposed in 2024, which fully demonstrates the capability of the method.", "weaknesses": "- The paper mentions a budget of 50 queries for the program synthesis (PS) and a budget of 10 queries for each PS, but it lacks an analysis of the success rate and the number of queries used. Providing this information would offer a clearer picture of the efficiency and effectiveness of the approach", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Why use GPT-3.5?**\n\nThe use of GPT-3.5 in Figure 3 was to illustrate a key challenge in applying LLMs to the task of verified lifting: the difficulty these models face in generating correct code for DSLs, even when the DSL is not particularly new. Our experiments with GPT-3.5 showed that despite TACO being introduced in 2017, which is well within the training cutoff date for GPT-3.5 (2021), the model still struggled to generate correct TACO code when used as-is.\n&emsp;This issue persists even with more recent and advanced models. For instance, when we tested the same prompt with GPT-4, which presumably has been trained on a larger corpus potentially including more TACO programs, it still produced an incorrect solution. Specifically, the generated program contained an incorrect usage of the get function in the final return statement.\n```\nint mag_array(int *a, int n) {\n    Tensor<int> A({n}, Format{Dense}); Tensor<int> result(ScalarType::Int);\n    for (int i = 0; i < n; ++i) { A.insert({i}, a[i]); }\n    A.pack(); IndexVar i;\n    result() = sum(i, A(i) * A(i)); result.compute();\n    return result.getStorage().getValues().get<int>(0);\n}\n```\nSimilarly, when we tested Claude 3.5 Sonnet, one of the latest models from Anthropic, with the same prompt, it also returned incorrect code, misusing the sum function.\n```\nint mag_array(int* a, int n) {\n    Format csr({Sparse, Dense}); Format dense({Dense});\n    Tensor<int> A({n}, csr); Tensor<int> B({n}, dense); Tensor<int> result({}, dense);\n    for (int i = 0; i < n; i++) { A.insert({i}, a[i]); }\n    A.pack(); IndexVar i; B(i) = A(i) * A(i);\n    result() = sum(B(i)); result.compile(); result.assemble(); result.compute();\n    return result.at({});\n}\n```\nThese results show that even the largest and most advanced LLMs struggle to reliably generate correct code for new DSLs when directly prompted to do so. This highlights the inherent difficulty of generating code reliably in new DSLs and illustrating that LLMLift is solving a challenging problem.\n\n\n**How does the approach handle complex features in source languages that do not have direct counterparts in the target DSLs?**\n\nLLMLift currently only supports a subset of the C/C++ and Python language in the source programs. In particular, it does not support any code that uses pointers or objects as verifying programs with these constructs is challenging. That said, we did not encounter the use of these constructs in any of the benchmarks in all the four domains that we evaluated on. Moreover, we currently support commonly-used data structures including arrays, tuples, maps, vectors and tensors, and that was enough for us to show good experimental results. \n\n**The paper mentions a budget of 50 queries for the program synthesis (PS) and a budget of 10 queries for each PS, but it lacks an analysis of the success rate and the number of queries used. Providing this information would offer a clearer picture of the efficiency and effectiveness of the approach.**\n\nThe average number of tries to get to the correct PS solution is 4.3 and the median is 1, which means that most benchmarks generate the correct PS in the first try. Given a correct PS, it takes an average and a median of 1.77 and 1.74 tries, respectively, to generate the correct invariant.\n\n### References\n[1] Maaz Bin Safeer Ahmad et al. Automatically leveraging mapreduce frameworks for data-intensive applications.", "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": "c6S4pA4tUd", "reviewer": "Reviewer_ZcXM", "summary": "This work proposes LLMLift that leverages large language models (LLMs) to perform program transpilation. It first uses a prompt to lift the source program into an intermediate representation of the operators in the target language, called a program summary. Then, it prompts the LLM to generate loop invariants if necessary. The generated program summary and loop invariants are used to verify the equivalence of the source program and the program summary. This process is repeated until a correct program summary is found or the computation budget is reached. Finally, the program summary is rewritten into code in the target language using simple rules. The evaluation was performed on four tasks: distributed computing, network packet processing, TACO, and tensor processing. The results show that LLMLift can correctly transpile more benchmarks, spend less time, and require less effort to develop.", "questions": "Please consider addressing the points raised in the “Weakness” section.", "limitations": "The paper has sufficiently addressed the points concerning limitations and societal impact.", "rating": 3, "confidence": 4, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "Code transpilation is an interesting and important problem for both research and industry. The paper has demonstrated a nice combination of LLMs and verification to obtain provably correct transpiled code. The evaluation is performed on a diverse set of four scenarios. Moreover, I think the approach can have good potential even for translation between mainstream programming languages.", "weaknesses": "My main concern for this paper is poor writing, in both syntactic and semantic level. The writing needs significant improvement in general. I also have some other concerns about the evaluation.\n\n### 1. Syntactic Writing Issues\nI found the following syntactic issues:\n- Typos: Line 135 program program, Line 175 Contarary. There might be other typos so I suggest the authors run spell checks.\n- The number of arguments received by $\\phi$ are different in Equations (1) and (2).\n- It is visually difficult to separate the citations from normal text. I suggest to add a pair of parentheses like the ICML format.\n\n### 2. Semantic Writing Issues\nThe general idea of the approach is easy-to-understand, the paper lacks many technical details:\n- How do you verify the equivalence of the source program and the program summary? The paper provides hardly any details on this, but I think this is a non-trivial task.\n- How do you produce the target program from the program summary? Again, the paper mentions that this can be done using simple rules without giving any technical details.\n- How difficult are the four tasks considered in the evaluation? Providing some end-to-end examples would be helpful.\n- Why do you use one-shot prompting for generating program summaries but zero-shot for generating loop invariants?\n\n### 3. Concerns about Evaluation\n- LLMLift’s benefit lies mostly in speed. However, it does not solve significantly more benchmarks than baselines. Why is it the case?\n- The paper claims that LLMLift reduces development effort compared to prior rule-based approaches. I am not sure if this is a fair comparison, because the development of LLMs, such as GPT-4 used in the paper, requires significant development effort and computation resources.\n- The paper targets only transpilation from mainstream languages to DSLs. What are the main obstacles and efforts needed to extend LLMLift to transpilation between mainstream languages?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**How do you produce the target program from the program summary?**\n\nOnce we have the verified program summary in the IR, the code generation phase uses syntax-driven rules to map IR operators to the concrete syntax of the target DSL. Below we show a snippet of a code generation function that translates a tensor processing IR to PyTorch.  This code generation function recursively parses the IR operators and maps them to the corresponding DSL operators.\n\nFor instance, the `elemwise_add` operator in IR translates `torch.add` in PyTorch, and `elemwise_sub` translates to `torch.subtract`. Thus, the IR expression `elemwise_add(elemwise_sub(a, b))` becomes `torch.add(torch.subtract(a, b))` in PyTorch.\n```python\ndef codegen(expr: Expr):\n  if isinstance(expr, Var): return expr.name()\n  elif isinstance(expr, Lit): return expr.val()\n  elif isinstance(expr, Call): \n    f_name, args = expr.name(), expr.arguments()\n    if f_name == \"elemwise_add\":\n      return f\"torch.add({codegen(args[0])}, {codegen(args[1])})\" \n    elif f_name == \"elemwise_sub\":\n      return f\"torch.subtract({codegen(args[0])}, {codegen(args[1])})\" \n        ...\n```\n\n**Why 0 shot for PS and 1 for invariants:**\n\nThe task of generating program summaries is relatively easier compared to generating loop invariants. The primary instruction for this task is that the language model should combine operators from the given DSL without introducing any external operators. This constraint is easily expressible in natural language. \n\nGenerating invariants, on the other hand, is a more complex task for the following reasons:\n1) Specific Template: While LLMs might have encountered loop invariants in their training data, the invariants required for verified lifting often follow a specific template that may not be well-represented in the model's training set. Loop invariants in verified lifting must use a particular syntactic structure. As described in Equation 3 of our paper, they should contain expressions over loop variables and include inductive expressions using the output variable.\n2) Language Specificity: The generated invariants are in Python instead of SMT-LIB. This specific format requirement makes it easier to implement a pattern-matching parser for translating the invariants to SMT-LIB later in the process.\n\nDescribing these structural and syntactic restrictions accurately in natural language is challenging. Hence we use a one shot prompt for generating the invariants.\n\n**LLMLift does not solve significantly more benchmarks than baselines**\n\nWe compare LLMLift against symbolic implementations that were evaluated on a small, diverse set of benchmarks designed to showcase the effectiveness of their specific approaches. As a result, these tools achieve high accuracy on these benchmarks. To demonstrate the scalability of our approach, we created a set of 10 synthetic benchmarks for C2TACO, which are far more complex than those in the original set of benchmarks (see Appendix C). Our experiments show that LLMLift easily scales to handle these more challenging benchmarks, solving all 10 benchmarks in under 2 seconds. In contrast, C2TACO is unable to solve any of the 10 synthetic benchmarks with a 90 minute timeout.\n\n**LLMLift reduces development effort compared to prior rule-based approaches**\n\nOne of the key strengths of LLMLift is its ability to scale the search process for VL without relying on domain-specific heuristics. This significantly reduces the human effort required to build VL based compilers, making the technology more accessible across various domains. As detailed in our experimental section, symbolic search techniques heavily rely on domain-specific heuristics for scalability. For instance, C2TACO uses over 1000 lines of code solely to describe these heuristics, which are specific to the TACO IR and cannot be easily reused for other domains. Even with these heuristics, their search fails to scale to more complex benchmarks beyond those used for evaluation in the paper (see Appendix C). In contrast to domain-specific heuristics, the development effort for LLMs is a one-time investment that can be leveraged across multiple domains and tasks. Once trained, these models can be applied to various VL tasks with minimal additional development. \n\n**Main obstacles and efforts needed to extend LLMLift to transpilation between mainstream languages**\n\nThe objective of VL is different from translating programs between mainstream languages. Our approach focuses on mapping functional programs to the operators of a DSL in a semantics-preserving manner. As described in the paper, this problem of mapping to DSL is important as a) DSLs often provide a more concise way of expressing the same program compared to imperative implementations, enhancing maintainability and b) DSLs typically offer domain-specific optimizations that can significantly improve performance. However, there are several challenges in this mapping problem. In addition to the search space being huge, LLMLift must not only find a correct translation but also generate a proof of equivalence. This adds another layer of complexity.\n\nTranslating between mainstream languages has its own set of challenges: \n1. Different languages support various constructs, making direct mapping challenging, \n2. Generating accurate verification conditions and formal proofs for equivalence checking across diverse language constructs is complex. \n\nDue to these challenges, prior work in mainstream-to-mainstream translation, such as TransCoder[1], often relies on test-case-based approaches to demonstrate semantic equivalence, rather than formal verification. Such approaches do not provide any correctness guarantee in the generated code, and hence are risky to deploy in practice. On the other hand, LLMLift formally verifies the code which is generated and proves the semantic equivalence with the source program.\n\n\n### References\n[1] Baptiste Roziere et al. Unsupervised translation of programming languages.", "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": "IV7o7I28t6", "reviewer": "Reviewer_9szn", "summary": "This paper proposes an LLM-based approach (LLMLIFT) to building verified lifting tools. LLMLIFT leverages LLMs to generated both code and proof annotations together. For four real-world DSLs, LLMLIFT not only outperforms previous symbolic-based tools in both the number of benchmarks transpiled and transpilation time, but also requires significantly less effort to build.", "questions": "1. Compared with traditional VL, does the LLMs-based VL proposed in this paper have any other advantages besides being better in finding IR expression sequences? For example, what are the specific advantages of generating loop invariants compared with traditional methods?\n2. It is mentioned that the model uses PS to generate invariants, then whether it will lead to the error of the invariant due to the error of PS generation?\n3. Did LLMLIFT make any adjustments after Boolean Feedback?\n4. How to verify correctness if no loops are included in the program.", "limitations": "Are there DSLs that are hard to define with Python as IR?", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "For the important task of automatically code transpilation for DSLs, this paper domonstrate a novel approach to generating and verifying the generated code using LLMs. While using LLMs, the key idea of VL is combined: Python is used as IR, which solves the shortcomings of direct translation based on LLMs. The experimental results are improved compared with the existing methods.", "weaknesses": "Some statements are not clear and accurate:\n1. An important contribution and innovation of this paper is that generating and verifying the generated code using LLMs. However, to be precise, LLMs just seems to generates loop invariants for validation and then combine them with validators. \n2. Contributions should be distinguished from strengths.\nThe experiment does not seem to well illustrate the advantages of using LLMs to validate generated code as proposed in this paper. For example, to what extent did this LLMs-based validation phase improve the experimental results?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**LLMs just seems to generates loop invariants for validation and then combine them with validators. Compared with traditional VL, does the LLMs-based VL proposed in this paper have any other advantages besides being better in finding IR expression sequences?**\n\nTo clarify, LLMLift does not directly use LLMs for code validation. Instead, LLMs are used to guess program summaries and loop invariants, which are then passed to a theorem prover to check the validity of the generated program and its proof.\n\nThe challenge of finding a correct program summary or an equivalent program in a domain-specific language (DSL) is significant. For example, in our tensor processing domain, the search space for some problems can reach approximately 100,000 expressions for a 20 line input program. Traditional symbolic tools depend on domain-specific heuristics to manage this complexity, whereas LLMLift simplifies the entire search phase by using a straightforward structured prompt, as detailed in the paper.\n\nThe program verification community has devoted substantial effort over the years to address the problem of automatically inferring loop invariants. Various approaches have been proposed, including template-based synthesis [1], example-driven methods [2], and machine learning techniques [3]. What sets LLMLift apart is that it bridges two traditionally separate lines of work—program synthesis and formal verification—allowing us to leverage the strengths of both. By integrating LLMs in our iterative framework, we are able to generate candidate loop invariants and program summaries more flexibly and efficiently than traditional methods. To the best of our knowledge, LLMLift is the first approach that can simultaneously solve *both* the translation and loop invariant generation problems while generalizing across multiple domains.\n\nThis capability not only significantly reduces the human effort required to build these techniques but also provides formal guarantees on the output of the LLMs—a task that has traditionally been very challenging.\n\n\n\n**It is mentioned that the model uses PS to generate invariants, then whether it will lead to the error of the invariant due to the error of PS generation?**\n\nIn LLMLift, there is a possibility that the PS guessing phase might result in an incorrect program summary, as the model initially validates only for syntactic correctness. Since the loop invariants are generated based on this potentially incorrect PS, the generated invariants could also be incorrect. However, these erroneous solutions are caught and rejected during the verification phase of LLMLift. In this phase, a theorem prover is used to check for the semantic equivalence of the generated PS and invariants with the original source program (as described in how we prove equivalence earlier). If the generated PS and its associated invariants do not semantically match the source program, they are discarded. We provide examples of programs rejected by the theorem prover in Figure 10.\n\n**Did LLMLIFT make any adjustments after Boolean Feedback?**\n\nNo, we do not make any adjustments after the Boolean feedback. We just prompt the model with the feedback and the solution if the solution is incorrect.\n\n**How to verify correctness if no loops are included in the program.**\n\nSee general response.\n\n### References\n[1] Pranav et al. Learning invariants using decision trees and implication counterexamples\n\n[2] Saswat et al. Data-Driven Inference of Representation Invariants\n\n[3] Xujie et al. Learning loop invariants for program verification", "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:
We thank the reviewers for their helpful comments and suggestions. We will incorporate all suggestions and clarify the confusion in our next version. Below, we address some of the common  concerns that the reviewers raised.

**How do you verify the equivalence of the source program and the program summary?**

We use Floyd-Hoare Logic (FHL) to establish the validity of generated programs[1]. In FHL, verification problem is represented as a Hoare triple $\{A\} \, P \, \{B\}$, where:
- $A$ is the pre-condition
- $P$ is the program to be executed
- $B$ is the post-condition

To establish the validity of a Hoare triple, we prove that all executions starting from states satisfying $A$, after executing program $P$, result in states satisfying $B$. This involves finding a Boolean predicate called the verification condition ($VC$) that characterizes the set of pre-conditions from which every execution of $P$ leads to a state satisfying $B$. Formally, we need to prove that the $VC$ is true given pre-condition $A$, i.e., $A \rightarrow VC(P, B)$. 


Standard techniques exist to generate verification conditions from a given source program[2]. For programs containing loops, an additional predicate called a loop invariant is required. This invariant helps prove that the post-condition remains valid regardless of the number of loop iterations. The inference rules provided by FHL can be encoded into a format that can be fed into automated theorem provers or SMT (Satisfiability Modulo Theories) solvers. This encoding allows for the mechanical checking of any Hoare triple's validity.

Following are the VCs generated for our running example (Figure 1a) in the paper:
_Verification conditions:_
1. Initial: $$Inv(i=0, sum=0, data)$$
2. Preservation: 

$$
\begin{gather}
Inv(i, sum, data) \land (i < size(data))
\rightarrow \\\\
Inv(i+1, ite(data[i] < 100, sum = sum +  data[i], sum = sum), data)
\end{gather}
$$

3. Termination: 
$$
\begin{gather}
Inv(i, sum, data) \land \lnot(i < size(data)) \rightarrow \\\\
PS(sum, data)
\end{gather}
$$


_Generated program summary ($PS$) and $Inv$:_

\begin{align}
S &= sum \\\\
  &= reduce(map(data, \lambda j : ite(j < 100, i, 0)), \lambda a, b : a + b) \\\\
Inv &= (i \geq 0) \land (i \leq size(data)) \land sum \\\\
    &= reduce(map(data[:i], \lambda j : ite(j < 100, j, 0)), \lambda a, b : a + b) \\\\
\end{align}


_Proof:_
1. Initial Condition:
Before the loop executes, $i = 0$ and $sum = 0$. The invariant expresses sum as the result of a map followed by a reduce operation over the first $i$ elements. Since $i = 0$, the map-reduce operation is applied to an empty list, resulting in a zero sum. Therefore, the invariant holds in the initial state.
2. Preservation Condition:
The preservation condition ensures that the invariant holds throughout all iterations of the loop. This can be shown by induction. Assume the invariant holds at the $i$-th iteration. In the $(i + 1)$-th iteration, map-reduce would compute the sum for the first $i + 1$ elements, incrementing sum with the $(i + 1)$-th element of the input list data if it is less than 100.
3. Termination Condition:
The termination condition requires that the invariant implies the $PS$. When the loop terminates, $i = size(data)$, and both the $PS$ and $Inv$ expressions for sum will be identical, meaning the postcondition is satisfied.

**Why is there no performance comparison given in the experimental evaluation?**

The primary objective of verified lifting is to generate semantically equivalent programs in the target DSL from the source. DSLs are inherently designed to offer domain-specific optimizations, and the performance gains observed post-translation are attributable to the implementation of operators within the DSL rather than the translation process itself.

In LLMLift, our aim was to replicate the existing VL-based compilers. We performed a manual verification of LLMLift's output against the corresponding symbolic tools, confirming output equivalence of the two tools. Given this equivalence, the performance gains reported by the original symbolic tools are directly applicable to LLMLift's translations. Performance numbers for some of the domains are following:
1. Tensor Processing: The objective in this domain is to generate tensor programs executable on tensor processing backends. Translations to this intermediate representation (IR) yield performance gains of 2.1x (NumPy) and 167.71x (PyTorch) compared to sequential C++ implementations when compiled with GCC -O3.
2. TACO: The TACO compiler generates optimized GPU code. Translating programs to the TACO IR results in a performance gain of 24x compared to sequential C++ programs when compiled with GCC -O3.
3. Distributed Computing: The generated Spark implementations achieved an average speed-up of 15.6x compared to the sequential Java implementations. Additionally, when compared to manually written code by an expert, the generated outputs performed competitively. For more details on the user study, we refer the reader to the paper[1].

It is important to note that finding a program with optimal performance on the target backend would require performing the search phase with specific cost (objective) functions. While finding an equivalent program in the target DSL is already a challenging task, incorporating an optimization function into the search adds another layer of complexity. In addition, defining these cost functions is non-trivial in itself, as they must accurately capture the performance characteristics of the target backend. Currently, even without using cost functions, LLMLift is still able to generate performant code, as described earlier.

### References
[1] C. A. R. Hoare. An axiomatic basis for computer programming.

[2] Mike Barnett et al. Weakest-precondition of unstructured programs.

Meta-review: The authors propose LLMLift: a technique using LLMs toward verified lifting. First, the LLM transforms the source program $S$ into a program summary $PS$ (in Python with the constraint that it only uses provided Python functions representing the DSL). The LLM then predicts constraints (like loop invariants $Inv$) which are passed to an automated theorem prover which attempts to prove that $PS$ is equivalent to $S$. Once verified, since $PS$ only uses DSL operators expressed as Python functions, it can be transformed with straightforward rewrite rules into a program $T$ in the target DSL. LLMLift is shown to outperform prior approaches in 4 DSLs.

Reviewers had different opinions about this paper and were not convinced by each other during discussion.
* For strengths, reviewers mentioned the problem was "timely" and "important"; LLMLift is "highly innovative", a "novel approach", and "independent and self-contained"; the approach "improves user readability" and "requires no retraining"; and the evaluation is "thorough" on a "diverse set of four scenarios" and "fully demonstrates the capability of the method".
* For weaknesses, reviewers mentioned limited novelty in combining transpilation and producing proof annotations which have been explored separately, syntactically poor writing quality, missing details about the approach and experiment results, concerns about LoC metrics to measure engineering effort, and a desire for even greater performance increase.
* The author rebuttals provide important clarifications about the missing details (verifying equivalence of $S$ and $PS$, transforming $PS$ into $T$, benchmark difficulty, reasoning behind design choices in the approach) and extra experiment results (performance of generated code, insufficiency of models weaker than GPT-4, stats on accuracy of the two steps). Although reviewers’ opinions generally did not change based on the rebuttals, I think the content of the rebuttals would greatly improve the paper if included.

Because reviewers took very different stances and did not agree, I read the entire paper myself. I wrote down my opinions and some notes as if I were providing a new review, shown after the horizontal line below.

Here are my opinions about the strengths and weaknesses listed above:
* I agree with all of the strengths.
* Although the novelty is somewhat limited, I still think it is sufficient because this is the first work to apply LLMs to transpilation and verification in one end-to-end system. The most important design consideration here is the choice of IR which enables the LLM to directly predict of $PS$, generate $Inv$, and statically transform $PS$ into $T$. I don’t think it was obvious a priori that this choice would be as effective as it was, so this counts toward novelty in my view.
* I agree that the writing quality does not yet meet the bar for publication. However, I am hopeful that the authors can improve this, especially since the rebuttals seem to have much more polished writing.
* The paper was indeed missing important details, but they have now been provided in the rebuttals.
* I do think the LoC comparisons are suspect since some details are still missing and it is hard to make the comparisons fair. Perhaps this can be resolved with more details, or reworded to be more conservative in claims. But either way, the LoC comparisons are minor compared to the main experiment results of solving more benchmarks in less time.
* In contrast to some reviewers’ opinions, I don’t think the amount of engineering for LLMLift should include any amount of the engineering of GPT-4, because GPT-4 already exists with many use-cases beyond LLMLift. It is normal and expected to build upon general-purpose tools.
* Although the reviewers provide reasonable suggestions for further experiments, I think LLMLift’s performance increase over prior approaches is already sufficient for publication.

I think the technical contribution of this paper meets the bar for publication at NeurIPS, so I recommend to **accept**. _The only concern in my view is about the writing_: there are numerous grammatical and formatting issues, and missing details must be incorporated from the rebuttals into the paper.

**To the authors:** The paper's writing very clearly needs improvement, both syntactically (grammar and formatting) and semantically (covering all important details). As it is right now, the paper's writing quality is _well below the bar for publication_. But, I recognize that you (authors) have the _ability_ to improve the writing. Specifically, it is immediately obvious that the rebuttals are written much better and contain important details that were missing from the paper. If the paper could reach a similar level of polish and detail, it would be significantly improved. I also recognize your engagement during the discussion period with lengthy rebuttals and new experiments/analyses, so I feel that you are invested in improving how your work is perceived. So, by recommending acceptance, I am generously providing you an opportunity to improve the paper without needing another round of review at a later conference. **Please do not take this for granted.** If the paper is accepted, **it is necessary to spend time adding details and improving the writing**, consulting a native English speaker and someone proficient in LaTeX as needed.

---
# My "review" of the paper

**Strengths:**
* _Most important_: there are impressive results on multiple domains compared to multiple prior approaches
  * I would not have expected an LLM to perform these tasks (generating semantically-correct Python subject to the constraint of only using provided operations, and generating invariants sufficient for formal verification) as successfully as was demonstrated, so the experimental results seem very impressive to me.
  * LLMLift outperforming multiple prior approaches on their own benchmarks is very compelling to me, especially if those benchmarks highlight the strengths of the prior approaches and not LLMLift.
  * But, contextualizing these results is very important. I suggest (below) that the authors do this by providing end-to-end examples of LLMLift’s predictions on real benchmarks.
* Verified lifting is an important topic
* Using LLMs in the proposed way is intuitive

**Weaknesses:**
* _Most important_: writing quality needs much improvement
* Important details/examples are missing
  * The rebuttals significantly reduce this weakness. The remaining portion of this weakness is the lack of end-to-end examples of LLMLift compared to prior approaches, and the uncertainty around whether details/examples will be incorporated into the paper with clear writing.
* Directly asking an LLM to perform these tasks is not particularly novel without clever prompting strategies

Questions:
* Line 79: Where does the 1000x LoC comparison come from? Section 4 mentions LoC used in prior approaches for specific goals, but we additionally need info about the total LoC (for prior approaches and LLMLift including prompt templates).
* Line 223: why zero-shot for PS and one-shot for Inv, after praising the few-shot abilities of LLMs (line 194)?
  * The reasoning provided in the rebuttal to ZcXM is satisfactory, but should be added to the paper
* Readers need more details about proving correctness and translating PS into target program
  * Extra details provided in rebuttals are satisfactory, but definitely should be added to the paper
* Table 1: The caption says “tensor processing domain” but the compared approach is C2TACO which is only mentioned in Section 4.3 (for the TACO domain). Section 4.4 (for the Tensor Processing domain) does not mention C2TACO. There must be some inconsistency.

Suggestions for improvement:
* Throughout: fix citation style and grammar issues (too numerous to list individually)
* Fig 1: this implementation of reduce seems wrong, for example, should reduce([], f) == 0? This is true for reduce with sum, but not always
* Be consistent with notation style. For example, there are at least 4 styles used for the target program T, on lines 97, 123, 124, 146.
* Line 246: == instead of =
* Appendix A: the transpile_code algorithm should be made into a numbered figure. And, `incorrect_ps_sols` and `seen_ps_sols` seem to be identical (they always contain the same elements)
* Figures 5 and 6: provide text instead of screenshots
* Table 1 is not referenced anywhere in the text, and besides, it seems not an efficient use of paper space. More important summary information can be provided instead, such as a graph or table summarizing the most important results on all 4 domains.
* It would help to provide figures (in an appendix) showing, for each of the 4 domains, a benchmark for which LLMLift outperforms the compared approaches, and the exact results (S, PS, Inv, T, generation time) produced by LLMLift and the compared approaches.

**My rating: 6** (Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.)

In terms of technical contribution, I would say my confidence is 4/5. However, I am unsure about how much we can trust the authors to improve the writing and incorporate new details.
Decision: Accept (poster)