一句话：结合大语言模型与模型检测，将任意可编译到 WebAssembly 的语言转译为等价且地道的 Rust。
Rust 兼具内存安全与底层控制，将既有代码库正确且地道地转译为 Rust 已成为研究热点。现有方法分为基于规则和基于大语言模型（LLM）两类：前者理论可靠，但输出常不地道且不安全，且仅支持少数源语言；后者多语言且输出更地道安全，却缺乏正确性保证。VERT 提出一种形式正确、多语言且输出更地道的 Rust 转译器。它支持任何可编译到 WebAssembly 的语言：先用 Wasm 编译器得到 oracle Rust 程序，再由 LLM 生成地道的候选 Rust 程序，最后通过模型检测验证候选与 oracle 等价。摘要未报告具体实验数据，但作者声称该方法同时获得正确性与地道性。
Rust is a programming language that combines memory safety and low-level control, providing C-like performance while guaranteeing the absence of undefined behaviors by default. Rust’s growing popularity has prompted research on correct and idiomatic transpiling of existing code-bases to Rust. Existing work falls into two categories: rule-based and large language model (LLM)-based. While rule-based approaches are theoretically sound, they often yield unidiomatic and unsafe Rust code, and are limited to few source languages, which hinders maintainability and industrial application. By contrast, LLM-based approaches, while providing no guarantees, are polyglot and typically produce more idiomatic and safe Rust code. In this work, we present VERT, a formally correct, polyglot Rust translator with more idiomatic outputs. VERT supports any language that compiles to Web Assembly. Using the Web Assembly compiler, VERT obtains an oracle Rust program. Leveraging the LLM, VERT generates an idiomatic candidate Rust program. This candidate is verified against the oracle with model-checking to ensure equivalence.
DOI 原文 ·
@inproceedings{paperbot9349,
title = {VERT: Polyglot Verified Equivalent Rust Transpilation with Large Language Models},
author = {Aidan Z.H. Yang and Yoshiki Takashima and Brandon Paulsen and Josiah Dodds and Daniel Kroening},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00123}
}