Verified Code Transpilation with LLMs

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.

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

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.

Rating

4

Confidence

4

Soundness

2

Presentation

2

Contribution

3

Limitations

Are there DSLs that are hard to define with Python as IR?

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.

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

Please consider addressing the points raised in the “Weakness” section.

Rating

3

Confidence

4

Soundness

2

Presentation

2

Contribution

3

Limitations

The paper has sufficiently addressed the points concerning limitations and societal impact.

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.

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

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?

Rating

7

Confidence

3

Soundness

3

Presentation

3

Contribution

3

Limitations

The authors have not adequately discussed the limitations of this 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.

Strengths

1. Timely problem considering the emergence of different accelerators. 2. Automated transpilation with integrated feedback and verifier makes the process independent and self-contained. 3. Use 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. 4. Zero-shot approach requires no retraining, but this could lead to issues as well. See weakness and detailed comments.

Weaknesses

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

See the part marked using (***) below.

Rating

3

Confidence

3

Soundness

3

Presentation

3

Contribution

2

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.

Thanks for the rebuttal

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.