VERT: Verified Equivalent Rust Transpilation with Large Language Models as Few-Shot Learners

Rust是一种编程语言，它结合了内存安全和低级控制，提供类似于C的性能，同时默认保证不存在未定义的行为。Rust的日益流行促使人们研究如何将现有代码库安全正确地转换为Rust。现有的研究可分为两类：基于规则和基于大型语言模型(LLM)。虽然基于规则的方法理论上可以产生正确的转换，保持与原始代码相同的输入输出等效性，但它们通常会产生不可读的Rust代码，使用Rust语言的不安全子集。另一方面，虽然基于LLM的方法通常可以生成更易读、易维护和安全的代码，但它们不提供任何关于正确性的保证。在这项工作中，我们提出了VERT，一种可以产生具有正确性形式保证的易读Rust转换的工具。VERT的唯一要求是源语言需要有Web Assembly编译器，这对大多数主要语言来说是正确的。VERT首先使用Web Assembly编译器获取一个oracle Rust程序。同时，VERT使用LLM生成一个易读的候选Rust程序。该候选程序会与oracle进行验证，如果验证失败，我们将重新生成新的候选转换，直到验证成功为止。我们通过转换一套从竞争式编程基准测试中获取的1,394个程序来评估VERT。将Anthropic的Claude-2和VERT结合使用，与仅使用Claude相比，Rust转换的基于属性的测试通过率从31%提高到54%，基于有界模型检查的通过率从1%提高到42%。此外，我们还评估了VERT在使用指针的实际C项目中生成非平凡安全Rust的能力。我们的结果提供了有关LLM编写安全Rust的限制的见解。

论文旨在解决如何正确且可读地将现有代码转换为Rust语言的问题，同时保证正确性和安全性。

VERT是一种工具，它可以使用Web Assembly编译器和大型语言模型来生成可读的Rust转换，并通过与原始代码的Oracle比较来验证正确性。这种方法结合了规则和LLM方法的优点，并提供了正确性保证。

论文使用VERT工具转换了来自竞争编程基准测试的1,394个程序，并评估了VERT在实现属性测试和有界模型检查方面的性能。此外，还使用VERT在使用指针的真实C项目中生成了安全的Rust代码。论文的方法提供了一种新颖的方法来转换现有代码，并提供了正确性保证。

现有的工作主要分为基于规则和基于LLM的方法。基于规则的方法可以产生保持输入输出等价性的正确转换，但通常会产生难以阅读的Rust代码。基于LLM的方法通常可以产生更易读、易维护和安全的代码，但无法提供正确性保证。