SpecTra: Enhancing the Code Translation Ability of Language Models by Generating Multi-Modal Specifications

TL;DR

SpecTra tackles the problem of improving LLM-based code translation by generating and validating multi-modal specifications (static, IO, and NL) from source code and using them to constrain translations. It introduces a self-consistency-based validation pipeline to ensure specification quality and employs a staged translation workflow that uses one spec from each modality in sequence. Empirical results show up to 46% relative improvements across multiple language pairs and models, with a case study demonstrating applicability to full-project translation. The work suggests that high-quality specifications are a promising direction for enhancing real-world LLM-driven code translation and points to future work on formalizing specs and extending to other tasks.

Abstract

Large language models (LLMs) are increasingly being used for the task of automated code translation, which has important real-world applications. However, most existing approaches use only the source code of a program as an input to an LLM, and do not consider the different kinds of specifications that can be extracted from a program. In this paper, we propose SpecTra, a multi-stage approach that uses a novel self-consistency filter to first generate high-quality static specifications, test cases, and natural language descriptions from a given program, and then uses these along with the source code to improve the quality of LLM-generated translations. We evaluate SpecTra on three code translation tasks - C to Rust, C to Go, and JavaScript to TypeScript - and show that it can enhance the performance of six popular LLMs on these tasks by up to a relative improvement of 46%. We also present a case study on extending this approach to handle translation of a full C project to Rust. Our research suggests that generating high-quality specifications could be a promising and efficient way to improve the performance of LLMs for code translation.

Figures (6)

• Figure 1: An overview of SpecTra.
• Figure 2: Our different specification modalities are complementary. This diagram shows how many out of the 300 C to Rust translations are solved using each individual specification modality. All results are with gpt-4o. Diagrams of other language pairs are in the Supplementary Material.
• Figure 3: The first step of our approach involves generating multiple candidate specifications from a given program. This is the actual output of gpt-4o on our motivating example from \ref{['sec:motivating']}.
• Figure 4: Filtering out incorrect specifications. We re-generate C code using each specification, and pick the specifications corresponding to re-generated C programs that pass the test case.
• Figure 5: Using different modalities of specifications to perform specification-augmented translation. These are the actual prompts and specifications generated by SpecTra.