Sahil Bhatia and Jie Qiu and Sanjit A. Seshia and Alvin Cheung

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2024-11

March 14, 2024

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2024/EECS-2024-11.pdf

Domain-specific languages (DSLs) have become integral to various software workflows, offering domain-specific optimizations and abstractions that improve code readability and maintainability. These languages have found applications across diverse domains such as image processing, deep learning, and distributed computing. However, the adoption of these languages often necessitates developers to rewrite existing code using the specific DSLs. Manual rewriting is error-prone and impractical, leading to the development of numerous automated code translation tools. One notably successful approach for addressing this challenge is verified lifting, which relies on program synthesis (search-based) to find programs in the target language that are functionally equivalent to the source language program. While several tools based on verified lifting have been developed for various application domains, they are often specialized for specific tasks or require significant manual effort in terms of domain knowledge or heuristics to scale the search. In this paper, leveraging recent advances in large language models (LLMs) for code, we propose an LLM-based approach to building verified lifting tools. We use the LLM's capabilities to reason about programs by leveraging contextual information to translate a given program into its corresponding equivalent in the target language. This contextual information includes expressing the semantics of the target language using Python as the intermediate language. Additionally, we utilize the LLMs to generate proofs for functional equivalence. We develop lifting-based compilers for three DSLs targeting different application domains. Our approach not only outperforms previous symbolic-based tools but also requires significantly less effort to build.

---

BibTeX citation:

@techreport{Bhatia:EECS-2024-11,
    Author= {Bhatia, Sahil and Qiu, Jie and Seshia, Sanjit A. and Cheung, Alvin},
    Title= {Can LLMs Perform Verified Lifting of Code?},
    Year= {2024},
    Month= {Mar},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2024/EECS-2024-11.html},
    Number= {UCB/EECS-2024-11},
    Abstract= { Domain-specific languages (DSLs) have become integral to various software workflows, offering domain-specific optimizations and abstractions that improve code readability and maintainability. These languages have found applications across diverse domains such as image processing, deep learning, and distributed computing. However, the adoption of these languages often necessitates developers to rewrite existing code using the specific DSLs. Manual rewriting is error-prone and impractical, leading to the development of numerous automated code translation tools. One notably successful approach for addressing this challenge is verified lifting, which relies on program synthesis (search-based) to find programs in the target language that are functionally equivalent to the source language program. While several tools based on verified lifting have been developed for various application domains, they are often specialized for specific tasks or require significant manual effort in terms of domain knowledge or heuristics to scale the search. In this paper, leveraging recent advances in large language models (LLMs) for code, we propose an LLM-based approach to building verified lifting tools. We use the LLM's capabilities to reason about programs by leveraging contextual information to translate a given program into its corresponding equivalent in the target language. This contextual information includes expressing the semantics of the target language using Python as the intermediate language. Additionally, we utilize the LLMs to generate proofs for functional equivalence. We develop lifting-based compilers for three DSLs targeting different application domains. Our approach not only outperforms previous symbolic-based tools but also requires significantly less effort to build.},
}

EndNote citation:

%0 Report
%A Bhatia, Sahil 
%A Qiu, Jie 
%A Seshia, Sanjit A. 
%A Cheung, Alvin 
%T Can LLMs Perform Verified Lifting of Code?
%I EECS Department, University of California, Berkeley
%D 2024
%8 March 14
%@ UCB/EECS-2024-11
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2024/EECS-2024-11.html
%F Bhatia:EECS-2024-11