Research map / Large language models / Agents, code and math
Verified Code Transpilation with LLMs
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes LLMLift, which uses GPT-4 to generate Python-IR program summaries and loop invariants for verified lifting, translating code into four DSLs (Spark, P4/Domino, TACO, tensor IR) with SMT-based verification.
Problem
Automated code transpilation into domain-specific languages with functional correctness guarantees; existing verified lifting tools are symbolic, DSL-specific, and require heavy domain-specific search heuristics, while plain LLM transpilation offers no guarantees.
Approach
Use an LLM to lift source code into a Python-based intermediate representation that defines DSL operator semantics, generating both program summaries and loop invariants via prompting, then verify equivalence with an SMT theorem prover and map the verified summary to DSL syntax with rewrite rules.
Key results
- On 45 MetaLift Spark benchmarks, LLMLift solves 44 versus MetaLift's 40, averaging under 1 minute per benchmark versus about 3 minutes.
- On 60 C2TACO TACO benchmarks, LLMLift solves all 60 with average 2 seconds versus C2TACO's 57 solved at 41 seconds on average.
- On 23 Tenspiler benchmarks, LLMLift solves all 23 with average 95.89 seconds versus Tenspiler's 115.14 seconds, without domain-specific optimizations.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| use LLMLift instead of MetaLift | Spark lifting · Spark (45 benchmarks) | benchmarks solved: 40 -> 44 | Helped |
| use LLMLift instead of MetaLift | Spark lifting · Spark | average solving time: 3 minutes -> less than 1 minute | Helped |
| use LLMLift instead of MetaLift | Domino lifting · Domino (10 benchmarks) | benchmarks solved: 10 -> 10 | No clear effect |
| use LLMLift instead of MetaLift | Domino lifting · Domino | average solving time: 6 seconds -> 2 seconds | Helped |
| use LLMLift instead of C2TACO | TACO lifting · TACO (60 benchmarks) | benchmarks solved: 57 -> 60 | Helped |
| use LLMLift instead of C2TACO | TACO lifting · TACO | average solving time: 41 seconds -> 2 seconds | Helped |
| use LLMLift instead of Tenspiler | tensor processing lifting · Tensor processing (23 benchmarks) | benchmarks solved: 23 -> 23 | No clear effect |
| use LLMLift instead of Tenspiler | tensor processing lifting · Tensor processing | average solving time: 115.14 seconds -> 95.89 seconds | Helped |
| generate program summary and invariants together in one step instead of using the two-phase approach (ablation) | LLMLift · Tensor processing (23 benchmarks) | benchmarks solved: 23 -> 20 | Hurt |
| remove all three domain-specific optimizations (ablation) | Tenspiler · Tensor processing (23 benchmarks) | benchmarks solved: 23 -> 5 | Hurt |
| use LLMLift instead of C2TACO | TACO lifting · TACO scalability (10 synthetic benchmarks) | benchmarks solved: C2TACO: any of the 10; LLMLift: 10 | Helped |
Surprising findings
- Generating program summary and invariants in a single combined prompt solved only 20 of 23 tensor benchmarks versus 23 for the two-phase approach.
- Direct end-to-end LLM translation to the DSL hallucinated non-existent TACO functions, motivating the Python IR design.
Limitations
- Relies on GPT-4 API with a fixed budget of queries and temperature 0.7, so results depend on a closed model.
- Some generated candidates use unsupported Python constructs or are semantically wrong, requiring parser filtering and verifier rejection.
- Single-phase combined generation of summaries and invariants performed worse than the two-phase approach.
Experimental setup
Datasets: MetaLift Spark benchmarks Domino benchmarks C2TACO benchmarks Tenspiler benchmarks
Benchmarks: MetaLift Spark benchmarks (45) Domino (10) C2TACO TACO benchmarks (60) Tenspiler tensor benchmarks (23)
Metrics: number of benchmarks solved solving time lines of code effort
Baselines: MetaLift C2TACO Tenspiler Casper Mold
Builds on: verified lifting Metalift C2TACO Tenspiler SyGuS
Closest papers by meaning
- Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages (NeurIPS 2024 · similarity 0.88)
- Lemur: Integrating Large Language Models in Automated Program Verification (ICLR 2024 · similarity 0.88)
- CRAFT: Customizing LLMs by Creating and Retrieving from Specialized Toolsets (ICLR 2024 · similarity 0.87)
- Evaluating Program Semantics Reasoning with Type Inference in System $F$ (NeurIPS 2025 · similarity 0.87)
- CoRe: Benchmarking LLMs’ Code Reasoning Capabilities through Static Analysis Tasks (NeurIPS 2025 · similarity 0.87)
- How efficient is LLM-generated code? A rigorous & high-standard benchmark (ICLR 2025 · similarity 0.86)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.