Verified Code Transpilation with LLMs
LLMLift uses large language models (LLMs) to automate code translation between domain-specific languages (DSLs), ensuring functional correctness and outperforming traditional tools in speed and efficiency.
Abstract
This research proposes LLMLift, an innovative approach to code transpilation using large language models. The work addresses the challenge of converting code written for one language into functionally equivalent code in another target language, particularly for domain-specific languages (DSLs). LLMLift combines LLM-powered translation with proof generation to create formal proofs establishing functional equivalence. The team developed lifting-based compilers for four different DSLs across various application domains. Their approach surpasses earlier symbolic tools in both the quantity of successfully transpiled benchmarks and the speed of transpilation, while requiring significantly less development effort to implement.
Related Research
AI-generated code that works — and proves it
How Code Metal combines AI with formal methods to build trusted code translation systems, and welcoming Prof. Loris D'Antoni as our first Code Metal Scholar.
UniPar: A Unified LLM-Based Framework for Parallel and Accelerated Code Translation in HPC
Introduces UniPar, an evaluation framework for assessing how large language models translate between parallel programming languages, achieving 69% compilation success and 33% functional correctness through fine-tuning and compiler-guided repair.