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
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.
Workflows vs Agents for Code Translation
Compares structured workflows versus agentic approaches for MATLAB-to-HDL translation, showing that agentic methods with the Model Context Protocol increase simulation reach rates by over 20 percentage points on mid-sized models.