Verified Code Transpilation with LLMs

Authors: sahil  bhatia
jie  qiu
niranjan  hasabnis
sanjit a seshia
alvin  cheung
u c berkeley
code  metal
Venue: NeurIPS_cc_2024_Conference
Published: 2024-05-15 19:17:48

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.

Main paper: 
 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 of transforming and compiling code from one programming language to another is called transpilation. The question we 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 a somewhat lower-level, general-purpose 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 accelerators, or network processors. Therefore, significant effort has been dedicated to developing tools aimed at automating the task of lifting. Rule-based approaches rely on traditional pattern-matching techniques [1] ; however, describing these rules can be a complex, human-intensive task. An alternative are search-based techniques that leverage advances in program synthesis (e.g., see [2, 3, 4] ) and formal verification over the last two decades. The use of verified program synthesis for lifting, termed verified lifting, involves searching for a 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, 8] 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-based 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 to 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, target⟩ for ML-based approaches, to enable generalization and scalability for the target DSL.Large Language Models (LLMs) [10, 11] have emerged as a 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 [12, 13, 14] or separately on producing proof annotations (such as invariants) for given code [15, 16] . Additionally, formal verification tools often have their own specialized languages (e.g., SMT-LIB, Dafny) for encoding verification problems and specifications. These languages are 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, we 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 reasoning capabilities of LLMs to translate code from context to an IR. We instruct the model via a prompt to generate code using the operators of the DSL, with Python serving as the IR to 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, we 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. 3) shows that LLMLIFT has significant advantages over traditional search-based symbolic VL-based tools. It solves 7 more benchmarks, requires substantially less effort in terms of LoC (1000×), and is faster in generating verified code and proofs (6× 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 LLMs. 3. Our method eliminates the need for manual encoding of domain-specific heuristics, thus simplifying 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 effectiveness 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 We now give an overview and an end-to-end example of verified lifting (VL) where we use program synthesis to build a compiler. Given a program (S) in the source language (S lang ), VL uses a search procedure to find a program (T) in the target language (T lang ) that can be proved to be functionally equivalent to the given source program. VL comprises of three phases: 1) Search, 2) Verification, and 3) Code generation. The key behind VL is to first transpile S to an user-defined intermediate representation (IR) of the operators in the target language before generating executable code. The IR serves as a functional description of T lang and ignores any implementation details. Hence, during search phase, S is lifted to a sequence of operators expressed using the IR. This expression serves as the program summary (P S) which summarizes S using the IR. Subsequently, P S is verified using a theorem prover to check for semantic equivalence with S for all program inputs. If verification succeeds, P S is then translated into the concrete syntax of the target language using simple patternmatching 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 S lang to T lang , as the P S is already expressed using the operators in the target language.We demonstrate an example of transpiling a sequential C++ to tensor-processing frameworks (such as PyTorch, Tensorflow, NumPy) using VL. Tensor-processing frameworks provide high-level API for performing, large-scale numerical computation on multi-dimensional arrays. Some of the basic tensor operators supported by all the frameworks are elementwise operators (tensor-tensor, tensor-scalar).Fig. 1a shows a 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. 1b , we define the semantics of the tensor operators such as matrix_add and matrix_scalar_sub. These functions abstract the implementation details of the operators in the tensor-processing 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 in VL involve framing it as SyGuS [17] problem. SyGuS is an 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 ∃ T ∈ T lang | ∀ σ. S(σ) = T(σ), where T is a program in the target language. For our program in Fig. 1a , the synthesis phase would return the following P S (i.e., T): matrix_scalar_sub(255, matrix_add(b, a))This expression performs element-wise addition of two matrices a and b, followed by a scalar subtraction of 128 from each element of the resulting matrix. Since S contains a 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, it We next describe how our LLM-based approach can improve VL synthesis problem.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 to other settings. • It is fine to include aspirational goals as motivation as long as it is clear that these goals are not attained by the paper. 
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, vec_elemewise_add would compute the element-wise sum for the first i + 1 elements of base and active, while the source program would push active[i + 1] + base[i + 1] to out, making out equal to vec_elemewise_add(active[:i+1], base[:i+1]), i.e., the RHS for this condition is true.Question: Does the paper discuss the limitations of the work performed by the authors? Answer: Yes Justification: Limitation section (Sec. 7) 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 a 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, a facial recognition algorithm may perform poorly when image resolution is low or 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 it fails to handle technical jargon. • The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size. • If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness. • While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in 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. 
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.The VL problem is characterized by three inputs:1. 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 σ. The overall correctness condition is:EQUATION2. Program Space (G): The program space outlines the set of potential solutions, typically expressed as a context-free grammar G. The language of G includes all sequences of operators ops ∈ T lang applied recursively to terms starting with input variables σ. A target program T is a program summary P S that is a composition of operators ops. An example involving the tensor operators is provided in the previous section. In other words, for each input σ, S (σ) must be expressed using a combination of operators (ops) from T lang . 3. Certificate Space: (G I ) A key part of the VL problem is to generate a certificate of correctness, typically in the form of invariants that a verifier can use to prove that ϕ holds for the generated P S. Synthesis tools typically use a grammar G I to constrain the space of possible invariants to search over; we refer to this as the certificate space.VL Problem: Given the inputs S, ϕ, G, G I , and T lang described above, the VL problem is to generate a correct target program T in T lang represented as the combination (P S, Inv). This is formally expressed in logic as follows:EQUATIONThis states that we aim to find a program summary (P S) and invariants (Inv) from the defined search space G, G I such that the given specification (functional equivalence with S) holds for all possible program states σ.Traditionally, the VL problem has been solved by symbolic program synthesis solvers utilizing methods such as enumerative search, deductive search, and constraint-based approaches [17, 4] . These rely heavily on manually-designed heuristics to make the search over the program and certificate space effective. Unfortunately doing so is resource-intensive and requires domain-specific knowledge.To address these limitations, we take a new approach that leverages LLMs.A naive approach to building a VL-based compiler using LLMs would be to prompt LLMs to translate S lang programs directly into T lang . However, this approach has the following shortcomings:1. VL-based compilers require that the T lang candidates generated during the search phase be functionally equivalent to the input S lang program. This is a strong requirement that current LLMs are unable to satisfy on their own. 2. Unlike widely-used general-purpose languages such as Python, domain-specific 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 to translate the program in Fig. 1a to MLX (Apple's latest tensor processing DSL), and the model fails to generate the expected python MLX code. Instead, the model outputs a completely incorrect solution by hallucinating non-existent MLCompute 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 two key ideas from traditional synthesis to the LLM setting:1. Python as an Intermediate Representation (IR): We adopt VL's key idea of transpiling to an IR rather than directly to the concrete syntax of T lang . Specifically, since Python is highly represented in the training dataset of popular LLMs [12] , these LLMs are effective at generating syntactically-correct Python code. We exploit these observations by leveraging Python as the IR to define semantics of DSL operators. An example is shown in Fig. 1b . 2. Oracle-Guided Inductive Synthesis (OGIS) with LLM oracles: Traditional verified lifting follows the paradigm of counterexample-guided inductive synthesis (CEGIS) [2] , where a Learner that synthesizes from examples interacts with a verifier that checks the Learner's output programs for correctness with respect to a specification. OGIS [18, 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 P S and Inv before invoking a verifier to check correctness. Our queries to the LLM oracles (prompts) follow a few-shot learning approach. Our current verifier provides Boolean feedback to the LLM oracles.In Fig. 2 , we show our LLM-based OGIS approach, where LLMs are applied to generate program summaries and invariants in the IR, using a few-shot learning framework that we describe next.LLMs have demonstrated few-shot reasoning capabilities [11] . Few-shot reasoning allows LLMs to generalize their understanding to new tasks by leveraging a small set of similar examples. Enabling them to extend their reasoning capabilities to tasks without requiring explicit training or fine-tuning 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 T lang . The objective, as defined in Eq. ( 2), is to find P S and Inv expressed using operators from T lang such that ϕ holds. We leverage the few-shot reasoning capability by providing the models with the semantics of operators from the target language (T lang ) using an IR. By exposing the LLMs to these semantics, we enable them to use their reasoning capabilities over code to generate both the P S and invariants in the IR.In Fig. 4 , we illustrate the high-level prompt structure we use to generate the P S and Inv. The prompt consists of the following components:1. Task Instruction. We instruct the model using a natural language to translate S using only the specified DSL operators. 2. DSL Operators. We specify the semantics of all operators from T lang 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 [12] . 3. Specification. While symbolic techniques often rely on approaches like test cases, bounded model checking, and Hoare logic [20] 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 P S and Inv into a two-phase process by first asking the LLM to generate the P S and then inferring invariants corresponding to it. For generating P S, 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 P S for our example code shown in Fig. 1a , representing the S as a combination of DSL operators:matrix_scalar_sub(255, matrix_add(b, a))To ensure that the generated candidates follow the DSL operators defined in the prompt, we use a 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 P S for all program states with S requires loop invariants. In VL, loop invariants typically follow a templated structure:EQUATIONwhere f (i) denotes an expression over loop indexes and e(T lang ) represents an inductive expression constructed using operators from T lang . 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) 2 . 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 P S. This instruction guides the model to produce an invariant corresponding to the generated P S. The invariants are generated as Boolean expressions in Python rather than SMT-LIB, as 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. 1a : The loop invariant states that the loop index row remains within the bounds of the array b (i.e., 0 ≤ i ≤ len(b)). 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 P S generation, the generated loop invariants are also checked using our rule-based parser to ensure they conform to the DSL.Verification. Both the generated P S and Inv are expressed in Python. We use simple patternmatching 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 a 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 new candidates.Code Generation. Once verified, the P S is translated into the concrete syntax of T lang using straightforward rewrite rules that recursively parse the generated P S 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 highly structured syntax. For instance, the generated P S for our running example can be translated into tensor processing frameworks like NumPy, generating the following code:def linear_burn_8_np(b, a): return a + b -255See Appendix F for more details on rule-based code generator. We present our complete algorithm for generating P S and Inv in Appendix A.The termination condition requires that the invariant implies the postcondition. When the loop terminates, i = base.size(), and both the P S and Inv expressions for out will be identical, i.e., the post-condition is satisfied.Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof? Answer: NA Justification: We do not present any theoretical result in the paper. Guidelines:• The answer NA means that the paper does not include theoretical results.• All the theorems, formulas, and proofs in the paper should be numbered and cross-referenced.• All assumptions should be clearly stated or referenced 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. 
experiments: 
 To evaluate the effectiveness of LLMLIFT, we evaluate across four distinct DSLs3 , each targeting a different application domain:1. Distributed Computing: We transpile sequential Java programs into MapReduce implementations written using the Apache Spark [21] API. Spark, an open-source distributed computing framework, provides an interface for programming multiple clusters for data parallelism which helps in large-scale data processing. 2. 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 a recently introduced tensor processing IR called TensIR [24] . TensIR consists of common tensor operations such as elementwise arithmetic operators, reduction operators and transpose, among others. TensIR is designed to enable translation of unoptimized sequential code to tensor operations which can be then executed on 6 different software and hardware backends.In all experiments, we use GPT-4 via their APIs to generate candidates. We set the temperature to 0.7 for all the experiments. For program summary and invariant generation across all domains, we use the same zero-shot P S prompt in Fig. 6 and one-shot prompt in Fig. 7 , respectively. We keep a budget of 50 queries for the P S and a budget of 10 queries for each P S. The parser and logic for invoking the LLMs are implemented in Python with ≈700 LoC.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 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.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 in Appendix G.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 a mapper function to generate key-value pairs. 2. 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 LLMLIFT against MetaLift [25] 4 . MetaLift uses a symbolic solver (Rosette [26] ) to perform the search. We evaluate on 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 a timeout of 1 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 to take an average of 3 minutes to solve. The amount of effort required to build LLMLIFT is also significantly less than MetaLift as it does not require the developers to provide any search-space description for P S and invariants. As MetaLift requires over 1000 LoC for the description of these search-space, LLMLIFT requires only ≈100 lines of prompt.Network packet processing hardware, such as routers and switches, lacks flexibility post-development, preventing experimentation with new data-plane algorithms. Recently, a verified lifting approach [22] was introduced to simplify this process. This compiler offers the developers with two constructs: 1. a packet transaction language (subset of the C language) to express the semantics of these data-plane algorithms 2. a 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 of the atoms in the prompt. We compare the performance of our implementation against MetaLift'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 P S are verified using a SMT solver. MetaLift solves all the 10 benchmarks with an average time of 6 seconds.LLMLIFT is also able to transpile all the 10 benchmarks but with an average time of only 2 seconds. Similar to the Spark case study, we do not require developers to specify the search-space for P S.While MetaLift requires over ≈1100 LoC to describe this search-space, LLMLIFT only uses ≈70 lines of prompt. In summary, LLMLIFT shows similar performance to the existing compiler but can be built using much less effort.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] a search-based lifting tool was proposed to automate the translation of C++ code to TACO.LLMLIFT implementation. In Tab. 1, 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 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 an extended timeout of 1 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 on a 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.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. 5 Tenspiler is able to solve all 23 benchmarks. LLMLIFT also successfully solves all 23 benchmarks, including generation of the correct proofs. 6However, it is important to note that Tenspiler's synthesis algorithm relies on three domain-specific optimizations to achieve scalability. These optimizations require significant effort to implement, with over ≈1200 LoC written by a domain expert. In contrast, LLMLIFT uses ≈320 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 symblioc approach, we remove all the optimizations. Tenspiler, without the optimizations, can only solve 5 out of the 23 benchmarks with a timeout of 1 hour, highlighting the importance of the domain-specific optimizations for its performance. These results highlight the ability of LLMLIFT to solve complex benchmarks without relying on domain-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 seconds.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 P S together in a single step. To test this, we prompt the model in a one-shot setting, providing an example that demonstrates generating the P S and the Inv(s) simultaneously. 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 P S together, LLMLIFT successfully solves 20 out of the total 23 benchmarks. In contrast, the two-phase approach described in Sec. 3 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 P S and the Inv(s) simultaneously. Moreover, the two-phase approach enables the model to leverage the generated P S when constructing the invariant. By having access to the P S, the model can more effectively reason about the necessary conditions and constraints required for the invariant to hold.Question: Does the paper fully disclose all the information needed to reproduce the main experimental 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, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not. • If the contribution is a dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable. • Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution is a 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 to the model. In general. releasing code and data is often one good way to 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 a 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) If the contribution is primarily a new algorithm, the paper should make it clear how to reproduce that algorithm. (b) If the contribution is primarily a new model architecture, the paper should describe the architecture clearly and fully. (c) If the contribution is a 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 be tricky in some cases, in which case authors are welcome to describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results. 
related work: 
 Code Transpilation for DSLs. Several approaches have been proposed for automating the task of translating legacy or unoptimized code to DSLs. These range from symbolic rule-based approaches [1] to search-based verified lifting approaches [7, 5, 27, 8, 25, 6] and neural approaches [9, 28] . Most of these tools are either optimized for a 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 [29] , where an IR is designed for low-resource languages and then combination of LLM and compiler techniques is used to reliably generate code for these languages.Code Translation for Mainstream-to-Mainstream Languages. The closest work to ours is by Roziere et al. [28] on a sequence-to-sequence model to 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 is to map functional programs to the operators of a DSL in a semantics-preserving 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-mainstream translation, such as [28] , 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.LLMs for Code. LLMs are trained on massive amounts of code from various sources, leading to impressive performance on programming tasks such as code generation [12, 13] , repair, testing, and transpilation. While the use of learning to synthesize proof artifacts, specifications, and models in formal methods is not new [18] , recently LLMs have been successfully employed in such tasks (e.g., [15, 16, 29] ). However, generating reliable code from LLMs remains challenging due to the stochastic nature of these models and the difficulty in creating a verification oracle for complex specifications. With LLMLIFT, we demonstrate the first approach to verified code generation with LLMs, albeit in the limited setting of transpilation for side-effect-free 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. • Providing as much information as possible in supplemental material (appended to the paper) is recommended, but including URLs to data and code is permitted. 
conclusion: 
 We presented a principled approach to leverage LLMs for code transpilation. Unlike prior LLM-based transpilers, our transpiled code is provably equivalent to the input, while also takes significantly less time to generate as compared to prior non LLM-based approaches with correctness guarantees, as demonstrated in transpiling to 4 DSLs used across a range of application domains.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. 
limitations: 
 While LLMLIFT demonstrates impressive performance across four DSLs, there are few opportunities for future improvements. Currently, our approach generates a 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 of a solution. Providing more granular feedback, such as counter-examples from the theorem prover or compiler error messages, can possibly help guide the LLM towards generating correct solutions more efficiently. for _ in range(num_iters):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 be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions). • The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.) • The assumptions made should be given (e.g., Normally distributed errors). • It should be clear whether the error bar is the standard deviation or the standard error of the mean. • It is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have a 96% CI, if the hypothesis of Normality of errors is not verified. • For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out of range (e.g. negative error rates).• If error bars 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. 
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 to reproduce the experiments? 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 of 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 it into the paper). 
code of ethics: 
 Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics https://neurips.cc/public/EthicsGuidelines? 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 circumstances that require a deviation from the Code of Ethics. • The authors should make sure to preserve anonymity (e.g., if there is a special consideration due to laws or regulations in their jurisdiction). 10. Broader Impacts Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed? Answer: 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.• If 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 societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations. • The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster. • The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology. • We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution. • For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review. 
 
 Appendix: # Gets `n`PS solutions from LLM for the given `source_code`.# Assuming all solutions in `seen_ps_sols`are incorrect, `get_ps_sols7 # tells the LLM to not generate any solution in this set. 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.Your task is to rewrite the given test C++ Function. You need to use only the set of provided functions and constants to achieve this. The rewritten program should be semantically equivalent to the test function. Please do not generate any explanations. #Instructions # 1. Do not use for/while loops for rewriting the function. # 2. The rewritten program should just be a single return statement of the form return_var = provided_function(...) # 3. Inline all the expressions. Do not use intermediate variables. In this section, we evaluate the scalability of symbolic solvers in the context of verified lifting-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 on domain-specific 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. 8a where the source performs an in-place operation on an array arr of length n and raises each element of the array to the power of 4. C2TACO enumerates candidate expressions using tensor operators and index variables in increasing order of expression length. C2TACO enumerates ≈30k candidates. We illustrate some of the incorrect expressions in Fig. 8a .To test the scalability of C2TACO, we randomly generated a set 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 of 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 10 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 the source code. To further test the capabilities of LLMLIFT, we evaluated it 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 In this section, we provide a qualitative analysis of the mistakes made by LLMs while generating code and proofs. In LLMLIFT, we use Python as the IR and the P S and Inv(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 in the solutions and rejects any candidates that do not comply with the theorem prover's syntax.One common source of syntactic errors is the use of Python-specific constructs that are 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. 10 uses a for loop, which is not supported by SMT solvers. Similarly, the second and third solutions utilize Python'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(1, []).Semantic errors occur when the generated code is syntactically correct but is semantically not equivalent to the given S. In the context of the screen blend benchmark (shown in Fig. 9 ), Fig. 11 illustrates two examples of semantically incorrect programs generated by GPT-4. The first program incorrectly subtracts a term from the base matrix instead of subtracting it from the sum of base and active matrices. The second program suffers from a similar issue. It subtracts an incorrect term from the active matrix. Specifically, the term being subtracted is matrix_elemwise_div(matrix_elemwise_mul(base, active), matrix_scalar_mul(32, matrix_elemwise_mul(base, active))), which is different from the one in the given program.We use Floyd-Hoare Logic (FHL) to establish the validity of generated programs [30] . In FHL, verification problem is represented as a Hoare triple {A}P {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 is {x = 0} x := x + 1{x > 0}. The Hoare triple states that if x = 0 before executing x := x + 1, then after executing the program, x will be greater than 0. 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 (V C) 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 V C is true given pre-condition, i.e., A → V C(P, B). Standard techniques exist to generate verification conditions from a given source program [31] . 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 solvers. This encoding allows for the mechanical checking of any Hoare triple's validity. In Fig. 13 , we show the V Cs generated for the source program in Fig. 12 Since i = 0, the vec_elemewise_add operation is applied to an empty list, resulting in an empty list. Therefore, the invariant holds in the initial state.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 an IR expression, the code generation function parses its operators and operands and translates each of 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 are mapped to their values (lines 4-5), and function calls are mapped to their corresponding PyTorch operators (lines 6-11).For instance, the elemwise_add operator in IR translates torch.add in PyTorch, and elemwise_sub translates to torch.subtract. As a result, the IR expression elemwise_add(elemwise_sub(a, b)) becomes torch.add(torch.subtract(a, b)) in PyTorch.Similarly, if we want to translate the code to another DSL, such as TensorFlow, we can simply change the specific operator rules to generate TensorFlow code. For example, the elemwise_add operator in IR would be translated to tf.add (line 9), and the elemwise_sub operator would be translated to tf.subtract (line 11). Thus, the same IR expression elemwise_add(elemwise_sub(a, b)) would become tf.add(tf.subtract(a, b)) in TensorFlow. 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.1× (NumPy) and 167.71× (PyTorch) compared to sequential C++ implementations when compiled with GCC -O3. 2. Distributed Computing: The generated Spark implementations achieved an average speed-up of 15.6× 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 3. TACO: The TACO compiler generates optimized GPU code. Translating programs to the TACO IR results in a performance gain of 24× 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 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.Python is one of the most widely represented programming languages in the training data of these models. This ensures that the model can generate Python code reliably with minimal prompting, reducing the likelihood of hallucinations. Python's highly syntactic nature facilitates easier parsing. This is beneficial as 1. it allows for the development of syntax-driven parsers that can efficiently 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. 3 ). 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 to 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.To evaluate if our prompts generalize across models, we evaluated LLMLIFT's performance using GPT-4o [32] , Claude 3.5 Sonnet [33] , and Gemini-1.5-Pro [34] . We used the exact same setting as described in Sec. 4 (zero-shot for P S and one-shot for Inv) 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.5-Pro solved 21 benchmarks (failed to guess the correct P S for the 2 unsolved benchmarks). The results show that our prompts are robust and generalize well across models, even without prompt engineering.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 [35] and Mistral Nemo 12.2B [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 finetuning, for the following two reasons:1. Instruction Following: Larger models are better at following the instructions to generate programs strictly with the defined DSL operators. 2. Handling Long-Context: With prompts that can grow in size to include all DSL operators and feedback, larger models manage long-context tasks more effectively.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 a 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 [32] , Claude 3.5 Sonnet [33] , and Gemini-1.5-Pro [34] . We used the exact same prompts for generating P S, 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 as this domain has the most complex DSL. In 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 a 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 P S for 2 benchmarks and correct Inv for 1).# of benchmarks solved GPT-4 11 GPT-4o 23 Claude 3.5 Sonnet 23 Gemini-1.5-Pro 20 Table 2 : Zero-shot performance of various proprietary models on tensor benchmarks.Your task is to generate the loop invariant 'Inv' such that it is true at all the locations it is defined at. Generate only a single 'Inv' expression which holds at all the locations. The invariant needs to be generated using only the functions defined below. Write the loop invariant as a python boolean formula. #Instructions: 1. You can use the defined functions to write the loop invariant. Do not use any for loops or any other python construct. NeurIPS Paper ChecklistWe evaluate LLMLIFT with a zero-shot invariant prompt in Appendix K.All the benchmarks used for evaluation can be found at: https://github.com/metalift/metalift/tree/llmlift/llmlift/benchmarksCasper[5] is not functional and Mold[1] is not open-sourced.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 I. 


Decision: 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.

Reviews: review: paper_summary: paper_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.
strength_weakness: strength_weakness: 1.	DSLs have less representation in the present LLM training dataset (more so lacking correct and efficient codebases). 
2.	Limited 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. 
3.	Underutilization of the GPT4 model which has a huge memory and compute footprint. 
4.	The 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.
5.	The 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. 
6.	 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. 
7.	Although 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.
questions: questions: See the part marked using (***)  below.
limitations: 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. 

The 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. 

There 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. 

(***) The paper does not include the rationale behind many of their assumptions like:
a.	Why 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. 
b.	Why 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. 
c.	Why was a temperature of 0.7 chosen and what is the impact of varying the same?
d.	Why was GPT 4 specifically chosen given its huge size? And how would the design fair against self correcting models and AutoGPT kind of models? 
e.	The paper overall misses sensitivity and ablation studies making it difficult, if not impossible, to understand the impact of each of the design components.
paper_summary: paper_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.
strength_weakness: strength_weakness: - 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
questions: 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?
- How does the approach handle complex features in source languages that do not have direct counterparts in the target DSLs?
- What are the common factors in tests that failed, and how can the approach be adjusted to address these issues?
- Why use GPT-3.5 other than the latest version of GPT in Figure 3?
limitations: limitations: The authors have not adequately discussed the limitations of this paper.
paper_summary: paper_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.
strength_weakness: strength_weakness: 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.

### 1. Syntactic Writing Issues
I found the following syntactic issues:
- Typos: Line 135 program program, Line 175 Contarary. There might be other typos so I suggest the authors run spell checks.
- The number of arguments received by $\phi$ are different in Equations (1) and (2).
- It is visually difficult to separate the citations from normal text. I suggest to add a pair of parentheses like the ICML format.

### 2. Semantic Writing Issues
The general idea of the approach is easy-to-understand, the paper lacks many technical details:
- 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.
- 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.
- How difficult are the four tasks considered in the evaluation? Providing some end-to-end examples would be helpful.
- Why do you use one-shot prompting for generating program summaries but zero-shot for generating loop invariants?

### 3. Concerns about Evaluation
- LLMLift’s benefit lies mostly in speed. However, it does not solve significantly more benchmarks than baselines. Why is it the case?
- 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.
- 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?
questions: questions: Please consider addressing the points raised in the “Weakness” section.
limitations: limitations: The paper has sufficiently addressed the points concerning limitations and societal impact.
paper_summary: paper_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.
strength_weakness: strength_weakness: Some statements are not clear and accurate:
1. 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. 
2. Contributions should be distinguished from strengths.
The 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?
questions: 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?
2. 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?
3. Did LLMLIFT make any adjustments after Boolean Feedback?
4. How to verify correctness if no loops are included in the program.
limitations: limitations: Are there DSLs that are hard to define with Python as IR?

Comments: title: Thanks for the rebuttal
comment: Thanks for submitting the rebuttal. I have read it but I believe the paper needs a major revision to reach the bar of NeurIPS. Therefore, I will keep my score. Below I provide a list of suggestions that might be helpful for the next iteration of the paper:
- Improve writing and formalization.
- Include the verification method and the way of generating target programs from program summaries into the appendix.
- Design and present benchmarks that can better demonstrate LLMLift’s advantages, especially in solving more test cases.
- Include ablation studies on important hyperparameters.