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
The Trust Problem Has Shifted: What Formal Verification Can and Cannot Guarantee About AI-Generated Code
A clear-eyed technical assessment of formal verification for AI-generated code: which approaches are credible, what barriers remain, and where the market will emerge first.
The Real Cost of Leaving NVIDIA
What Automated Transpilation Actually Costs, and What It Doesn't