  Domain-specific languages (DSLs) are integral to various software workflows.
Such languages offer domain-specific optimizations and abstractions that
improve code readability and maintainability. However, leveraging these
languages requires developers to rewrite existing code using the specific DSL's
API. While large language models (LLMs) have shown some success in automatic
code transpilation, none of them provide any functional correctness guarantees
on the transpiled code. Another approach for automating this task is verified
lifting, which relies on program synthesis to find programs in the target
language that are functionally equivalent to the source language program. While
several verified lifting tools have been developed for various application
domains, they are specialized for specific source-target languages or require
significant expertise in domain knowledge to make the search efficient. In this
paper, leveraging recent advances in LLMs, we propose an LLM-based approach
(LLMLift) to building verified lifting tools. We use the LLM's capabilities to
reason about programs to translate a given program into its corresponding
equivalent in the target language. Additionally, we use LLMs to generate proofs
for functional equivalence. We develop lifting-based compilers for {\em four
different} DSLs targeting different application domains. Our approach not only
outperforms previous symbolic-based tools in both the number of benchmarks
transpiled and transpilation time, but also requires significantly less effort
to build.
