LLMs just seems to generates loop invariants for validation and then combine them with validators. Compared with traditional VL, does the LLMs-based VL proposed in this paper have any other advantages besides being better in finding IR expression sequences?

To clarify, LLMLift does not directly use LLMs for code validation. Instead, LLMs are used to guess program summaries and loop invariants, which are then passed to a theorem prover to check the validity of the generated program and its proof.

The challenge of finding a correct program summary or an equivalent program in a domain-specific language (DSL) is significant. For example, in our tensor processing domain, the search space for some problems can reach approximately 100,000 expressions for a 20 line input program. Traditional symbolic tools depend on domain-specific heuristics to manage this complexity, whereas LLMLift simplifies the entire search phase by using a straightforward structured prompt, as detailed in the paper.

The program verification community has devoted substantial effort over the years to address the problem of automatically inferring loop invariants. Various approaches have been proposed, including template-based synthesis [1], example-driven methods [2], and machine learning techniques [3]. What sets LLMLift apart is that it bridges two traditionally separate lines of work—program synthesis and formal verification—allowing us to leverage the strengths of both. By integrating LLMs in our iterative framework, we are able to generate candidate loop invariants and program summaries more flexibly and efficiently than traditional methods. To the best of our knowledge, LLMLift is the first approach that can simultaneously solve both the translation and loop invariant generation problems while generalizing across multiple domains.

This capability not only significantly reduces the human effort required to build these techniques but also provides formal guarantees on the output of the LLMs—a task that has traditionally been very challenging.

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?

In LLMLift, there is a possibility that the PS guessing phase might result in an incorrect program summary, as the model initially validates only for syntactic correctness. Since the loop invariants are generated based on this potentially incorrect PS, the generated invariants could also be incorrect. However, these erroneous solutions are caught and rejected during the verification phase of LLMLift. In this phase, a theorem prover is used to check for the semantic equivalence of the generated PS and invariants with the original source program (as described in how we prove equivalence earlier). If the generated PS and its associated invariants do not semantically match the source program, they are discarded. We provide examples of programs rejected by the theorem prover in Figure 10.

Did LLMLIFT make any adjustments after Boolean Feedback?

No, we do not make any adjustments after the Boolean feedback. We just prompt the model with the feedback and the solution if the solution is incorrect.

How to verify correctness if no loops are included in the program.

See general response.

References

[1] Pranav et al. Learning invariants using decision trees and implication counterexamples

[2] Saswat et al. Data-Driven Inference of Representation Invariants

[3] Xujie et al. Learning loop invariants for program verification

How do you produce the target program from the program summary?

Once we have the verified program summary in the IR, the code generation phase uses syntax-driven rules to map IR operators to the concrete syntax of the target DSL. Below we show a snippet of a code generation function that translates a tensor processing IR to PyTorch. This code generation function recursively parses the IR operators and maps them to the corresponding DSL operators.

For instance, the elemwise_add operator in IR translates torch.add in PyTorch, and elemwise_sub translates to torch.subtract. Thus, the IR expression elemwise_add(elemwise_sub(a, b)) becomes torch.add(torch.subtract(a, b)) in PyTorch.

def codegen(expr: Expr):
  if isinstance(expr, Var): return expr.name()
  elif isinstance(expr, Lit): return expr.val()
  elif isinstance(expr, Call): 
    f_name, args = expr.name(), expr.arguments()
    if f_name == "elemwise_add":
      return f"torch.add({codegen(args[0])}, {codegen(args[1])})" 
    elif f_name == "elemwise_sub":
      return f"torch.subtract({codegen(args[0])}, {codegen(args[1])})" 
        ...

Why 0 shot for PS and 1 for invariants:

The task of generating program summaries is relatively easier compared to generating loop invariants. The primary instruction for this task is that the language model should combine operators from the given DSL without introducing any external operators. This constraint is easily expressible in natural language.

Generating invariants, on the other hand, is a more complex task for the following reasons:

1. Specific Template: While LLMs might have encountered loop invariants in their training data, the invariants required for verified lifting often follow a specific template that may not be well-represented in the model's training set. Loop invariants in verified lifting must use a particular syntactic structure. As described in Equation 3 of our paper, they should contain expressions over loop variables and include inductive expressions using the output variable.
2. Language Specificity: The generated invariants are in Python instead of SMT-LIB. This specific format requirement makes it easier to implement a pattern-matching parser for translating the invariants to SMT-LIB later in the process.

Describing these structural and syntactic restrictions accurately in natural language is challenging. Hence we use a one shot prompt for generating the invariants.

LLMLift does not solve significantly more benchmarks than baselines

We compare LLMLift against symbolic implementations that were evaluated on a small, diverse set of benchmarks designed to showcase the effectiveness of their specific approaches. As a result, these tools achieve high accuracy on these benchmarks. To demonstrate the scalability of our approach, we created a set of 10 synthetic benchmarks for C2TACO, which are far more complex than those in the original set of benchmarks (see Appendix C). Our experiments show that LLMLift easily scales to handle these more challenging benchmarks, solving all 10 benchmarks in under 2 seconds. In contrast, C2TACO is unable to solve any of the 10 synthetic benchmarks with a 90 minute timeout.

LLMLift reduces development effort compared to prior rule-based approaches

One of the key strengths of LLMLift is its ability to scale the search process for VL without relying on domain-specific heuristics. This significantly reduces the human effort required to build VL based compilers, making the technology more accessible across various domains. As detailed in our experimental section, symbolic search techniques heavily rely on domain-specific heuristics for scalability. For instance, C2TACO uses over 1000 lines of code solely to describe these heuristics, which are specific to the TACO IR and cannot be easily reused for other domains. Even with these heuristics, their search fails to scale to more complex benchmarks beyond those used for evaluation in the paper (see Appendix C). In contrast to domain-specific heuristics, the development effort for LLMs is a one-time investment that can be leveraged across multiple domains and tasks. Once trained, these models can be applied to various VL tasks with minimal additional development.

Main obstacles and efforts needed to extend LLMLift to transpilation between mainstream languages

The objective of VL is different from translating programs between mainstream languages. Our approach focuses on mapping functional programs to the operators of a DSL in a semantics-preserving manner. As described in the paper, this problem of mapping to DSL is important as a) DSLs often provide a more concise way of expressing the same program compared to imperative implementations, enhancing maintainability and b) DSLs typically offer domain-specific optimizations that can significantly improve performance. However, there are several challenges in this mapping problem. In addition to the search space being huge, LLMLift must not only find a correct translation but also generate a proof of equivalence. This adds another layer of complexity.

Translating between mainstream languages has its own set of challenges:

1. Different languages support various constructs, making direct mapping challenging,
2. 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 TransCoder[1], often relies on test-case-based approaches to demonstrate semantic equivalence, rather than formal verification. Such approaches do not provide any correctness guarantee in the generated code, and hence are risky to deploy in practice. On the other hand, LLMLift formally verifies the code which is generated and proves the semantic equivalence with the source program.

References

[1] Baptiste Roziere et al. Unsupervised translation of programming languages.

Why use GPT-3.5?

The use of GPT-3.5 in Figure 3 was to illustrate a key challenge in applying LLMs to the task of verified lifting: the difficulty these models face in generating correct code for DSLs, even when the DSL is not particularly new. Our experiments with GPT-3.5 showed that despite TACO being introduced in 2017, which is well within the training cutoff date for GPT-3.5 (2021), the model still struggled to generate correct TACO code when used as-is.  This issue persists even with more recent and advanced models. For instance, when we tested the same prompt with GPT-4, which presumably has been trained on a larger corpus potentially including more TACO programs, it still produced an incorrect solution. Specifically, the generated program contained an incorrect usage of the get function in the final return statement.

int mag_array(int *a, int n) {
    Tensor<int> A({n}, Format{Dense}); Tensor<int> result(ScalarType::Int);
    for (int i = 0; i < n; ++i) { A.insert({i}, a[i]); }
    A.pack(); IndexVar i;
    result() = sum(i, A(i) * A(i)); result.compute();
    return result.getStorage().getValues().get<int>(0);
}

Similarly, when we tested Claude 3.5 Sonnet, one of the latest models from Anthropic, with the same prompt, it also returned incorrect code, misusing the sum function.

int mag_array(int* a, int n) {
    Format csr({Sparse, Dense}); Format dense({Dense});
    Tensor<int> A({n}, csr); Tensor<int> B({n}, dense); Tensor<int> result({}, dense);
    for (int i = 0; i < n; i++) { A.insert({i}, a[i]); }
    A.pack(); IndexVar i; B(i) = A(i) * A(i);
    result() = sum(B(i)); result.compile(); result.assemble(); result.compute();
    return result.at({});
}

These results show that even the largest and most advanced LLMs struggle to reliably generate correct code for new DSLs when directly prompted to do so. This highlights the inherent difficulty of generating code reliably in new DSLs and illustrating that LLMLift is solving a challenging problem.

How does the approach handle complex features in source languages that do not have direct counterparts in the target DSLs?

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. Moreover, we currently support commonly-used data structures including arrays, tuples, maps, vectors and tensors, and that was enough for us to show good experimental results.

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.

The average number of tries to get to the correct PS solution is 4.3 and the median is 1, which means that most benchmarks generate the correct PS in the first try. Given a correct PS, it takes an average and a median of 1.77 and 1.74 tries, respectively, to generate the correct invariant.

References

[1] Maaz Bin Safeer Ahmad et al. Automatically leveraging mapreduce frameworks for data-intensive applications.

Why GPT-4

With LLMLift, our objective was to demonstrate that LLMs can be effectively used for the task of VL without requiring fine-tuning. We needed a model that was good in two things:

1. Instruction Following: The model needed to generate programs strictly using the defined operators in a DSL.
2. Handling Long-Context: The prompt can grow in size when incorporating all DSL operators and feedback, so the model needed to manage long-context tasks effectively. GPT-4 was the best model available that met both of these requirements.

To explore whether LLMLift could leverage open-source models or if larger models were necessary, we evaluated LLMLift using two recent open-source models (Llama3 8B and Mistral Nemo 12.2B) and another proprietary model (Claude-sonnet-3.5). Due to budget constraints, we used a subset of benchmarks from the tensor processing domain, which is the most complex among all the DSLs we evaluated. Specifically, we used 12 image processing blend benchmarks. We use the same budget of queries and temperature settings.

Open-source models, Llama3 and Mistral, did not solve any of the benchmarks. Their solutions use Python constructs outside of the defined IR, causing them to immediately fail our syntactic parser. Claude, on the other hand, successfully solved 9 out of the 12. Llama3 and Mistral are significantly smaller than proprietary models like Claude and GPT-4. The results suggest that larger models are better suited for VL.

Complexity of source programs

Lines of code (LOC) are often used as a proxy for evaluating program complexity. In the benchmarks, the average LOC is 14. As described in the paper, our aim is for LLMLift to translate functional programs, and we observe that 10-20 lines of code are typical for these programs in the real world.

RAG is more feasible solution

To clarify, LLMLift does not depend on the presence of specific DSLs in the training data of large language models to perform code translation. In fact, we demonstrate that LLMLift can reliably generate code in DSLs that the model may have never encountered during training, for instance our tensor processing DSLs and the TACO IR. With LLMLift, we introduce a structured prompting approach that explicitly includes the semantics of the DSL operators using an IR. The model's task is then to generate a program using only the operators defined in the prompt. Once we have a verified solution in the IR, we apply syntax-driven rules to translate the program into the concrete syntax of the DSL.

RAG-based approaches rely on the source and target programs having similar representations in the encoding space. However, in the context of VL, the source and target languages often have completely different syntactic structures. For example, in the tensor processing domain, the source programs are written in vanilla C++, while the target language involves tensor operations like tensor-tensor arithmetic and tensor-scalar arithmetic. Moreover, multiple lines of code in the source language can be mapped to a single operator in the target (e.g., a loop adding corresponding elements of two vectors can be mapped to element-wise addition operator), and lifting-based transpilation is rarely one-to-one token-wise between the source and target languages. This significant syntactic difference makes it challenging to use a RAG-based implementation for generating a program summary in the DSL.

That said, we believe RAG could be beneficial in LLMLift in a different way—specifically, in selecting examples for few-shot prompting. RAG could be used to retrieve the most relevant examples for a new program, which could then be used to prompt the model. This approach might help reduce the sample complexity of LLMLift.

For large code bases we see KV cache management to be a problem

We apologize, but we don't fully understand how KV cache management would be a significant issue in the context of VL. In the VL scenario, we're dealing with individual programs which are just a few hundred lines rather than large codebases, so the issues of KV cache management are not a concern for our current approach.

Why python as IR?

Python is the most widely represented language in the training data. This ensures that the model can generate Python code reliably with minimal prompting. Python's highly syntactic nature facilitates easier parsing. This is beneficial as a) it allows for the development of syntax-driven parsers that can efficiently translate the IR to theorem prover languages and b) It simplifies the process of translating the IR to the target DSL's concrete syntax.

Direct conversion to a DSL is challenging because many DSLs may not be well-represented in the model's training data (see Figure 3). Moreover, it is also challenging to verify DSL programs using theorem provers as they do not provide support for these languages and it is not trivial to translate the DSL directly to the language supported by them. On the other hand, many theorem provers have existing libraries for handling Python-like syntax, making the verification step of LLMLift easier.

Why is accuracy the right metric?

Accuracy is the most critical metric for evaluating a transpiler, as the translated program must be semantically equivalent (checked by a formal verifier) to the given source program. Another important metric is the performance of the translated code. Currently, the code generated by LLMLift significantly outperforms its corresponding program in the source language across all domains.

Why 0.7 as the temperature?

At lower temperatures, these models generate more deterministic outputs, which limit their ability to explore diverse solutions. Due to budget constraints, we only experimented with temperature 0.7, which is close to the optimal temperature found for code generation in recent paper[1].

References

[1] Evaluating Large Language Models Trained on Code. https://arxiv.org/abs/2107.03374