Program Skeletons for Automated Program Translation

Xanadu132025年9月26日大约 61 分钟

Program Skeletons for Automated Program Translation

论文来自 2025 Proceedings of the ACM on Programming Languages (PLDI) 的《Program Skeletons for Automated Program Translation》。

摘要

将软件在不同编程语言之间进行翻译是一项具有挑战性的任务，目前自动化技术依然难以奏效，且很难扩展到大型程序。跨语言翻译的关键难点在于：需要把源程序的预期行为重新表达为目标语言中符合其“习惯用法”（idiomatic）的构造。这个过程必须抽象掉源语言的细节，同时保持整体功能不变。

本文提出了一种新颖且系统的方法，使这类翻译更易于自动化——基于我们称之为“程序骨架（program skeletons）”的框架。程序骨架通过抽象并有效汇总较低层次的具体代码片段，保留源程序的高层结构；这些片段随后可以机械化地翻译到目标编程语言。按设计，骨架允许对片段的具体实现以多种方式进行填充，并且可以与现有的数据驱动代码合成器配合工作。更重要的是，骨架在概念上支持可靠的分解（sound decomposition）：也就是说，只要每个独立片段都被正确翻译，再结合机械化翻译得到的骨架，最终的译后程序即可被视为整体上正确。

我们实现了一个原型系统 Skel，将骨架式翻译的思想用于从 Python 到 JavaScript 的转换。与以往工作相比，我们的结果显示出可喜的可扩展性：在 9 个真实世界的 Python 程序上（其中一些超过约 1k 行代码），其中约 95% 的代码片段可以自动翻译，约 5% 需要人工处理。基于整程序测试套件，所有最终翻译的程序均被验证为正确。

1. Introduction

自动代码翻译要求将用一种编程语言编写的源代码翻译成另一种。将遗留代码库迁移到新语言和平台的任务自然会出现在许多环境中[1,25]。旧的语言和库依赖关系变得过时，不再被积极维护，这通常导致迫切需要转向一个维护良好的库更受欢迎的平台。代码迁移也有助于通过将流行的库移植到缺少类似功能的语言来填补软件生态系统之间的空白。

尽管这一课题至关重要，但要实现令人满意的自动化翻译一直是长期挑战，即便是在相近语言之间也是如此 [48]。从理论上看，一个“天真”的想法是为一对语言构建一个跨语言编译器，但这种做法往往站不住脚——此类翻译器产出的代码质量通常既不可读也不可维护。要想在自动化代码迁移上取得实用且现实的进展，方案必须满足三个基本要求：其一，不能牺牲正确性——译后代码在行为上应与源程序等价；其二，能够随真实世界程序的规模扩展；其三，产出的翻译应当可被人类阅读与理解，从而为后续维护铺平道路。同样地，方案还必须遵循目标语言中常见或“惯用”（idiomatic）的编程风格，例如合理使用目标语言的 API 与库；若违背惯用性，迁移就很可能失去脱离源语言的初衷。

以现代大型语言模型（LLMs）为代表的数据驱动方法在满足第三条“惯用性”要求方面显示出希望 [20, 23, 27, 44, 54, 55]。然而，基于 LLM 的代码翻译技术在满足前两条——正确性与可扩展性——方面仍举步维艰 [2]，并且大多局限于规模很小的基准程序（仅几十行代码） [2, 38, 51]。随着程序规模增大，多个相互关联函数中错误的复合效应会显著加剧，使得最终的翻译难以修复。

本研究关注如何扩展（scaling up）自动化代码翻译的能力。我们的出发点是：要想切实应对这一挑战，可以通过系统性地把核心任务分解为更小、更简单的子任务来实现，例如把源代码拆分为更小的片段。这样的方案天然便于利用现有技术（如面向代码的 LLMs），因为这些技术通常在较小尺度的翻译任务上工程化良好。当然，简单地“拆分后各自独立翻译” 并不可行：即便每个小片段单独看都是正确的，它们的译文也可能无法良好拼合，从而导致整体程序不正确。

本文的核心贡献是一个称为程序骨架（program skeleton）的框架，它支持对翻译任务进行可扩展且模块化的分解。程序骨架捕获了源程序中可以机械化翻译到目标语言的那一部分；它把剩余实现细节抽象掉，用目标语言中的若干占位符（placeholders）来替代，之后再分别用具体实现将这些占位符具体化（concretize）。最终目标是：得到的目标程序是正确的，即能够通过给定的一组 整程序（whole-program） 测试。

理想情况下，程序骨架应具备两个鲜明特性。其一，骨架应当支持可靠的分解（sound decomposition）：只要把骨架中的占位符以任何正确的方式具体化，便能保证得到的整体程序是正确的。其二，不含占位符的骨架代码应当能够自动从源语言翻译到目标语言。因此，骨架必须对源语言与目标语言之间的相似性与差异有足够的认知与把握。

笔者注：大模型负责做骨架中占位符（小片段）的具体翻译，不含占位符的骨架代码由传统算法自动翻译。

在这项工作中，我们通过我们的工具 Skel 展示了基于骨架的分解方法的有效性。Skel 被设计用于将代码从 Python 翻译到 JavaScript——这是当今最流行的两种语言。Skel 在两种语言共享的语义模型上进行推理，仅保留两种语言之间可以直接对应的那部分结构，并将其余实现细节抽象掉。对于每个给定的 Python 程序及其配套测试，Skel 会分析其执行，并用占位符（placeholders）替换被省略的源代码片段。每个占位符都携带一个局部语义约束（local semantic requirement），其具体实现应满足该约束。将生成的骨架以完全机械化的方式翻译到目标语言 JavaScript 之后，Skel 可以与现有的代码合成器协同工作（包括基于大型语言模型的合成器），分别为每个占位符直接寻找 JavaScript 实现。若合成器缺乏“可靠性（soundness）”而导致错误，我们可以局部地修正各个占位符的实现，使之满足相应的局部语义约束。

我们在生成骨架与检验其正确性这两个环节都使用了程序测试。虽然也可以借助形式化规约来刻画正确性，但本文所涉及的源语言与目标语言都属于动态脚本语言，在这类语言之间进行跨语言的功能等价性检验向来十分困难。基于务实考量，我们因此选择用一种纯测试驱动的方法来展示骨架这一概念。

笔者注：大模型非常擅长写js、python，但本文工作在c/c++、rust等强类型编程语言上的可移植性未必好

我们在近期工作所采用的一个基准集上评估了 Skel 在 Python→JavaScript 翻译任务上的性能（见 [51]）；与更早的工作 [50] 相比，该基准包含更大规模的程序，并且我们还进一步扩展，引入了接近 2k 行代码的程序。在 9 个被翻译的程序中，有 4 个无需任何人工介入即可直接通过整程序测试。其余程序由于我们用于占位符合成的现成 LLM 能力有限，需要对少量代码片段进行人工修复。总体而言，95% 的代码片段无需人工干预即可得到符合测试用例的正确译文；在对剩余 5% 片段进行人工修复之后，所有翻译得到的程序均通过了给定测试用例。由此我们得出结论：Skel 为实现从 Python 到 JavaScript 的大部分自动化翻译提供了一条颇具前景的路径。

2. 程序骨架：预览

我们先用一个具体示例来说明“骨架（skeleton）”的概念。图 1(a) 给出了一个需要被翻译成 JavaScript 的 Python 源程序。图 1(b) 展示了为该 Python 程序生成的程序骨架，但骨架已被翻译为符合 JavaScript 语法的形式。这个骨架是一个不完整（部分）的 JavaScript 程序，包含若干占位符（placeholders），并为每个占位符给出了局部语义要求。占位符用来替换原先 Python 代码中的部分具体实现。随后可以通过一个独立的片段合成步骤来完成该骨架：该步骤会生成具体的 JavaScript 代码片段，最终替换骨架中的占位符。填充某个占位符的片段应当满足该占位符的局部语义要求。经过这样的片段合成之后，得到的最终结果是一个可运行的 JavaScript 程序，如图 1(c) 所示。

因此，程序骨架的方法在翻译流程的两部分之间实现了清晰的关注点分离：骨架生成与骨架完成。如图 1(b) 所示，生成的骨架代码可由一个基于规则的系统机械地生成；而最终的完成步骤则可以使用任何现成的片段合成器，包括 LLM 等。

接下来，我们形式化给出骨架的概念及其理想性质。可以将骨架看作一种中间表示，概念上由两部分组成：一个语法表示，以及对各个占位符之语义要求的注解。

程序骨架：语法层面

一个语法骨架是带有“空洞（holes）”或“占位符”的程序。形式化地，针对一种语言 $\mathcal{L}$ ，一个语法层面的程序骨架是带孔洞的部分程序 $K$ ，其孔洞集合为

\mathrm{Holes}(K)=\{h_1,\ldots,h_n\}.

对骨架 $K$ 的一个 完成（completion） 就是一个映射

\Gamma:\ \mathrm{Holes}(K)\to \mathcal{L}.

我们用 $\Gamma(K)$ 表示由该完成 $\Gamma$ 所诱导得到的完整程序。

程序骨架：带注解

显然，并非所有的完成都是理想（可取）的。限制可能的完成的一种自然方式，是为每个占位符指定独立的需求。因此，我们为骨架 $K$ 中的每个占位符 $h$ 添加一个局部语义要求 $\varphi\subseteq \mathcal{L}$ 。形式化地，若对每个占位符 $h_i$ 都满足

\Gamma(h_i)\in \varphi_i,

则称完成 $\Gamma$ 与这些局部语义要求集合 $\{\varphi_i\}_i$ 相容。我们记

\tilde{K}=\langle K,\varphi_1,\varphi_2,\ldots,\varphi_n\rangle

为一个带注解的程序骨架，并且在后文中常将其也简称为程序骨架。

一个理想的骨架应当支持可靠的分解（sound decomposition）。直观地说，这意味着：如果每个占位符都被正确地合成，那么最终完成的骨架就会产生一个正确翻译的程序。我们将这一目标形式化为源程序与目标程序之间的抽象正确性概念，分别记为 $\ell_{\mathrm{src}}$ 与 $\ell_{\mathrm{tgt}}$ 。需要注意的是，某次翻译是否被视为正确，取决于目标语言中的哪些程序被认为与给定源程序行为等价。我们假设跨语言的这种行为等价概念是存在的，并将其编码为一个二元关系：

\mathrm{Eq}_{(\mathrm{src},\mathrm{tgt})}\ \subseteq\ \mathcal{L}_{\mathrm{src}}\ \times\ \mathcal{L}_{\mathrm{tgt}}\, .

可靠分解（Sound Decomposition）

令 $\mathrm{Eq}_{(\mathrm{src},\mathrm{tgt})}$ 为一个关系，用来刻画源语言与目标语言程序之间的某种等价概念。我们称一个骨架 $\hat{K}_{\mathrm{tgt}}$ 对于关系 $\mathrm{Eq}_{(\mathrm{src},\mathrm{tgt})}$ 与某个源程序 $\ell_{\mathrm{src}}\in \mathcal{L}_{\mathrm{src}}$ 是可靠的（sound），当且仅当：对 $\hat{K}_{\mathrm{tgt}}$ 的每一个完成 $\Gamma_{\mathrm{tgt}}$ ，都有

\bigl(\,\ell_{\mathrm{src}},\ \Gamma_{\mathrm{tgt}}(\hat{K}_{\mathrm{tgt}})\,\bigr)\ \in\ \mathrm{Eq}_{(\mathrm{src},\mathrm{tgt})}\, .

备注。 上述可靠性的概念是抽象的——它并未给出 $\mathrm{Eq}_{(\mathrm{src},\mathrm{tgt})}$ 的具体定义（例如程序等价或正确性的精确定义）。在通篇工作中，我们采用的具体“等价”概念是经验性的：要求源程序与目标程序在一组用户自定义测试上表现一致。我们给出的最终方案以“可靠性”作为指导原则，我们的实现只是对“骨架”概念的一种尽力而为的阐释。具体而言，我们既没有提供一个关于跨语言等价关系的完整规格说明，也不声称我们的实现可以对所有程序及其所有可能输入在普遍意义上保证可靠性。

我们的系统 Skel 旨在成为一个实用的原型。为此，Skel 定义了一种中间表示，称为 SkelCR，它抓取了源语言 Python 与目标语言 JavaScript 的共性，并且适合于用机械的、基于规则的方式进行翻译。该表示在设计上的主要实践挑战在于：如何取得表达能力的恰当水平。一个过于受限的中间表示可能会让现成的合成器难以为各个占位符找到符合习惯用法（idiomatic）的实现；反过来，若骨架允许更大的完成空间，就能在选择（即合成）具体实现时拥有更多自由，从而为“符合习惯的翻译”留出空间，并在整体效用上更好。我们在第 6 节的评估中以实验方式展示了这种效用：Skel 能够在很大程度上自动化地成功翻译真实世界的基准程序。

笔者注：没有形式化证明，可以说自己比较“实用” 😄

回到示例（Example Revisited）

在 SkelCR 中表示的骨架承载了目标程序的高层语法结构，并包括词法作用域与函数签名。此类抽象在源语言与目标语言之间高度相似，因此可以用一套固定的规则机械地翻译。例如，图 1(b) 展示了由图 1(a) 中的 Python 程序导出的 JavaScript 程序骨架。可以观察到，函数与类定义的词法作用域和嵌套结构在 Python 程序（图 1(a)）到翻译后的骨架（图 1(b)）之间都被保留了。

此阶段的骨架是一个不完整的 JavaScript 程序，带有若干占位符（虚线矩形）。每个占位符都携带一个局部语义要求。在我们的设定中，这些要求被编码为一段段 I/O 序列，用以指定实现该占位符的代码片段必须产生的可观测效应（细节见第 3 节）。图 1(b) 以标记为 $h^{\mathrm{tgt}}_2$ 的占位符为例，突出显示了其语义要求。非正式地说，图中的语义要求可以理解为：当从某个初始状态（@Init {…}）执行该代码片段时，应当首先以特定实参调用名为 unpack_binary 的函数（@Call {…}），随后在获得该调用结果后，完成剩余计算并返回一个特定的值（@Return {…}）。这类语义要求反映了相应片段既要与骨架交互，也要彼此协作的方式。

骨架翻译的可组合性在该示例中十分明显。图 1(c) 给出了由现代 LLM 生成的对骨架中占位符的一次完成。对于实现 $h^{\mathrm{tgt}}_2$ 的各种不同方式，只要它们对所要求的 $\varphi^{\mathrm{tgt}}_2$ 是有效的，就应该能够与对其他占位符（如 $h^{\mathrm{tgt}}_1$ ）有效的完成很好地组合。换句话说，如果各个占位符的片段分别满足其局部语义要求（以注解 $\varphi^{\mathrm{tgt}}_i$ 的形式编码），那么整个翻译的完成就应当自动满足全局语义要求——在本文的设定中，这对应于通过测试。

这种可组合性的一个重要结果是：我们可以局部地检查某个候选代码片段是否具有与其占位符要求相一致的期望行为。也就是说，一个占位符完成中的错误会在本地被捕获，而不会以不可预期的方式影响其他占位符的语义。能够隔离并局部化完成中的错误，使得我们可以利用那些表达力强但并不保证可靠性的合成器——这正是现代数据驱动方法的典型做法。

笔者注：有点类似基于数据流式的编程？

3. Skel：骨架生成与完成的概览

本节概述我们在骨架生成与骨架完成上的关键设计选择。从宏观层面看，骨架生成受两种语言在高层结构上的相似性所引导。第 3.1 节说明我们如何利用这种相似性，从源程序中确定语法骨架；第 3.2 节讨论我们如何通过对源程序各片段的可观测行为进行建模与提炼，从而得到各占位符的局部语义要求；最后在第 3.3 节，我们给出获得完整翻译的实用方案。

3.1 确定骨架的语法结构

Python 与 JavaScript 在高层上相似，而在低层上差异明显。两者在高层设计中有许多共同点，例如都提供类似的控制流结构（循环、条件语句等），并且都有相近的词法作用域规则与用于捕获非局部变量的闭包机制。两种语言都是动态类型，且都拥有许多语义相近的常用数据类型；例如，Python 的 List 与 Dict 分别类似于 JavaScript 的 Array 与 Object。两者也都支持面向对象的封装，允许定义带有方法的类。

然而，在语句层面的程序表示细节上，两种语言差异很大。最显著的差别体现在可用的标准库 API 及其语义上；这会迫使“符合习惯用法”的翻译在目标程序中以不同的一组 API 与运算符来表达源程序的逻辑。

Skel 生成的程序骨架统一了源程序与其翻译结果在高层语法结构上的一致性——即函数/词法作用域以及每个作用域的符号表。Skel 假定这类函数级或类级的结构已由源程序完全指定。如果期望采用与源程序不同的高层结构来进行翻译，我们期望用户在使用 Skel 之前先调整源程序结构。这种在源与目标之间统一高层程序结构的做法，可以简化之后对各占位符局部语义要求的分析：因为 Skel 可以把源程序视为源语言中的“已完成骨架” $\,\Gamma_{\mathrm{src}}(K_{\mathrm{src}})\,$ ，从而得到骨架中占位符与源程序代码片段之间的对应关系——把

(h^{\mathrm{src}}_0,\ldots,h^{\mathrm{src}}_n)

映射为

(g^{\mathrm{src}}_0,\ldots,g^{\mathrm{src}}_n)\,.

我们将在下一小节说明如何确定这些占位符的语义要求。

3.2 用可观测效应刻画语义要求

从宏观层面看，我们的语义要求是从原始程序中提取的，形式为各个代码片段的输入—输出行为。当然，必须谨慎决定这些 I/O 行为需要刻画到什么细节层级；理想状态下，我们希望捕捉到保证骨架可靠性所必需的关键细节，同时尽量去除对目标语言中“符合习惯用法”的实现并不重要的细枝末节。

难点在于：真实的 Python 与 JavaScript 程序的语义往往“很乱”。代码片段的语义远比在基本值上的纯函数复杂得多。一旦出现闭包、共享数据引用，以及与数量众多、可能是高阶的库 API 交互时，究竟应把什么视作输入与输出就会变得不清晰。

一个天真的做法是：为了精确刻画某个代码片段的输入—输出行为，可以尝试捕捉底层语言运行时的全部状态变化。这种做法不会漏掉细节，但对我们的骨架生成任务并无裨益，因为它捕捉到的状态变化会牵涉大量与具体语言相关的细节。此类低层细节的例子包括：迭代器的内部实现、库 API、临时闭包、特殊的控制流状态等；这些都很难在目标语言中直接翻译成符合习惯的构造。另一方面，如果分析过于粗粒度而忽略了低层细节，则会带来分解时出错的风险：也就是说，满足这类粗粒度语义要求的代码片段，在被合并回骨架后，未必能得到一个可运行且正确的目标程序。

为应对如何选择合适抽象层级（在跟踪输入—输出行为时）的挑战，Skel 采用如下关键设计原则作为指导：

不可区分性原则（Indistinguishability Principle）： 任何满足同一占位符语义要求的两个代码片段，应当在占位符之外不可被区分。

该原则反映了：为某占位符合成得到的片段能否与程序其余部分正确组合。更具体地说，上述原则并不是询问“语言解释器能否区分该占位符的不同完成”，而是询问“除了该占位符对应的片段之外，程序的其他片段是否能从所观察到的行为中区分出这两个候选片段”。我们用可观测效应（observable effects）来描述这种从外部可观察到的行为。

“不可区分性原则”是一种务实的放宽：与前述天真的方案相比，它允许在骨架完成中拥有更大的灵活性。基于可观测效应来规定代码片段，并不要求源程序与目标程序之间达到完整状态等价。

笔者注：也就是说，Skel采用较宽松的占位符代码段，只要求其满足输入输出约束

共同模型的必要性

准确地从代码片段中提取可观测效应并不容易。区分“内部的”与“对外可观测的”效应并无统一做法——这取决于我们如何建模程序语义，以及该建模能否同时映射到源语言与目标语言。对此，我们首先确定一个通用的程序语义模型，称为 ProcEmu，它把可观测效应显式化。该公共模型的要点在于：任何两个语义完全相同的程序，必然具有不可区分的代码片段（即同样的可观测效应）。Skel 将 Python 与 JavaScript 中的具体语义都映射到这个公共模型；直观地说，当这两种语言中的程序 $\ell_{\mathrm{src}}$ 与 $\ell_{\mathrm{tgt}}$ 在 ProcEmu 中被映射为语义等价的程序时，我们就可以把它们视为等价。下面我们以高层方式介绍 ProcEmu（细节见第 4 节）。

ProcEmu 模型

我们提出一个名为 ProcEmu 的公共模型，把代码片段的执行视作独立的“进程”。程序的执行因此变成一组“相互通信的进程”，而不是语言解释器中的单一进程。各个进程是隔离的，它们只能通过消息通信，这与进程代数中的典型概念相似（除了这里不存在并行执行）。代码片段之间的交互被映射为若干类型的“通信消息”。

一个（Python 或 JavaScript）程序，在抽象为 ProcEmu 模型后，会把每一次对代码片段 $g_i$ （它填充占位符 $h_i$ ）的调用仿真为一个单独的有状态“进程”。在这个意义上，ProcEmu 对带有骨架 $K$ 的完整程序 $\ell$ 的“执行”就是如下进程间通信序列：

\rho \;=\; \mathrm{ProcEmu}(\ell)\;=\; \mathcal{K} \;\xRightarrow{\text{Init}_1}\; P_0 \;\xRightarrow{\text{Call}_2}\; \mathcal{K} \;\xRightarrow{\text{Init}_3}\; P_1 \;\cdots\; \;\xRightarrow{\text{Res}_{m-1}}\; P_0 \;\xRightarrow{\text{Ret}_m}\; \mathcal{K}

其中，每个 $P_i$ 是一个进程，对应于某个占位符的一次调用，而 $\mathcal{K}$ 是与骨架 $K$ 对应的唯一进程。一个进程在执行序列 $\rho$ 中可以被多次中断与恢复；这些转换对应于控制流的转移，在 $\rho$ 中以箭头（如 $\xRightarrow{\mathrm{Res}_{m-1}}$ ）表示。每一次控制流转移都伴随数据交换，我们用“消息”来刻画这种交换。例如，在上面的序列 $\rho$ 中，进程 $\mathcal{K}$ 首先通过消息 $\mathrm{Init}_1$ 与进程 $P_0$ 通信，随后 $P_0$ 以消息 $\mathrm{Call}_2$ 响应并发送给 $\mathcal{K}$ 。

决定可观测效应

在 ProcEmu 确立之后，从具体程序执行中获取可观测效应的问题就转化为：从执行序列 $\rho$ 中提取通信序列。尽管骨架结构澄清了进程的边界，但决定跨进程消息中应包含哪些信息仍需谨慎。目标是让传递的信息既 (1) 最小 又 (2) 足够。理想地，我们只应包含“刚好足够”的信息：使得相关代码片段在一个隔离进程中可以被正确仿真（充分性），同时一旦再删去任何信息，就会使这种仿真失败或偏离真实执行（最小性）。我们在第 4 节给出 ProcEmu 的细节，使其尽可能贴合该目标；这些细节还可能依赖具体语言（本文中为 Python 与 JavaScript）。

理想与实现

我们指出，ProcEmu 模型自然导向一个跨语言程序精确定义的等价概念，从而为可靠分解铺平道路。更具体地说，由 ProcEmu 诱导的（理想的）观测等价关系为

\mathrm{Eq}^{\mathrm{Ideal}}_{(\mathrm{src},\mathrm{tgt})} =\bigl\{\,(\ell_{\mathrm{src}},\ell_{\mathrm{tgt}})\ \big|\ \mathcal{F}\bigl(\mathrm{ProcEmu}(\ell_{\mathrm{src}})\bigr) = \mathrm{ProcEmu}(\ell_{\mathrm{tgt}}),\ \ell_{\mathrm{src}}\in\mathcal{L}_{\mathrm{src}},\ \ell_{\mathrm{tgt}}\in\mathcal{L}_{\mathrm{tgt}} \,\bigr\},

其中，ProcEmu 所用的 $\ell_{\mathrm{src}}$ （及 $\ell_{\mathrm{tgt}}$ ）的骨架是由 Skel 构造的唯一骨架。这里， $\mathcal{F}$ 是一个跨语言类型映射，把源语言中的“复刻/适配（retrofit）”对象映射到目标语言中的对应对象（详见第 4.2.2 节）。

原则上，理想的 Skel 会把给定程序翻译为某个 $\ell_{\mathrm{tgt}}$ ，并在理想检查

\mathcal{F}\bigl(\mathrm{ProcEmu}(\ell_{\mathrm{src}})\bigr) \;=\; \mathrm{ProcEmu}(\ell_{\mathrm{tgt}})

通过时宣告成功。然而，我们的 Skel 实现是尽力而为的：在实践中，由于诸多现实考量（例如浮点误差、API 的不精确建模、比较大型对象时的时间开销等），我们的等价性检查只能做到近似。因此，实现不可避免地偏离理想，在绝对意义上可能无法保证可靠性。与此同时，我们的实证评估表明这种偏离并不严重：每当观察到翻译的错误时，我们总能把问题精确定位到产生错误的具体代码片段。

3.3 代码片段合成

一旦我们为骨架得到了语义要求（通过执行源程序和目标程序，并在 ProcEmu 中提取序列 $\rho$ ），就可以用一种朴素方法来完成每个占位符 $h_i$ ：——把所有涉及代码片段 $g_i$ （待合成）的进程实例的消息汇总成一个单一的语义规格 $\varphi_i$ ，然后用该规格去一次性查询合成引擎。不幸的是，这种做法会给合成器带来巨大负担，因为这样“朴素编码”的规格往往非常大，包含来自同一片段多个进程实例的许多轮消息。在这种场景下，数据驱动的合成器（也就是 LLM）很可能会犯许多难以调试的复合性错误。

在 Skel 中，我们采用了另一种方法——带抽查的逐步细化（gradual refinement with spot-checking）。具体地，对于某个占位符 $h_i$ 对应的代码片段 $g_i$ ，我们使用一条逐渐更为完备的规格序列

\varphi_i^{(1)},\ \varphi_i^{(2)},\ \ldots,\ \varphi_i^{(j)}

对其进行增量细化。操作上，我们按照序列 $\rho$ 所诱导的顺序遍历代码片段。在序列的第 $m$ 步，若遇到的是占位符 $h_i$ ，则考虑对其进行合成。若这是第一次遇到 $h_i$ ，我们以规格

\varphi_i^{(1)}=\psi_m

查询合成器并在成功后继续；此处的 $\psi_m$ 编码了在第 $m$ 步观察到的那对输入—输出消息。另一方面，如果我们之前已经为 $h_i$ 合成过某个代码 $g_i$ （满足到目前为止的规格 $\varphi_i^{(j)}$ ），则按如下方式处理：如果 $g_i$ 已经满足由新的输入—输出对在第 $m$ 步所诱导出的附加规格 $\psi_m$ ，我们就直接进入下一步，并保持 $\varphi_i^{(j)}$ 不变；否则，我们把规格更新为

\varphi_i^{(j+1)}=\varphi_i^{(j)}\land \psi_m

然后用该更新后的规格再次查询合成引擎（即逐步细化）。如前述，若合成成功就前进到下一步；然而若检查失败，我们会立即对当前片段 $g_i$ 重新发起一次合成（这就是抽查，spot checking）。

这种方法带来两点关键收益，使得 Skel 更加实用。首先，逐步细化的设计只会在过程中真正出现的新输入—输出对上增加规格（而不是一开始就把所有 I/O 对都纳入），从而让实践中的规格规模保持合理；这在精神上与 CEGIS 方法相似。其次，与“先把一切都合成完再统一检查”的标准做法不同，抽查会在继续进行更多合成之前主动发现并修正由合成器（例如 LLM）引入的错误，从而使得后续其他占位符的合成也能顺利进行。更多细节见第 4.3 节。

笔者注：也就是说，不是一次性要求满足所有语义要求，而是一步步来

4. Skel 的设计细节

Skel 通过分析源程序来生成程序骨架的两个主要部分：语法结构与语义要求。在此之后，它会按照执行顺序为各个占位符合成并逐步细化代码片段。

4.1 程序骨架的语法结构

Skel 通过镜像（复写）源程序中的函数签名以及跨越词法作用域可见的符号，来确定骨架的语法结构，同时将低层的实现细节留作占位符。沿用我们的运行示例，图 2（左）中的 Python 程序是一个典型的带有闭包的多函数程序。该程序包含四个词法作用域：一个全局作用域和三个不同函数的作用域。入口位于全局作用域中的代码片段，该片段同时也作为程序的单元测试。程序中会创建闭包，并在不同地方作为值传递。函数 compute 内部有一个闭包 _update，它会在（第 8 行）被作为实参传给另一个函数 multi。图 2（右）给出了这个 Python 程序的一个符合习惯用法且正确的 JavaScript 翻译。该示例突出了 Python 源程序与 JavaScript 翻译之间的如下相似与差异：

高度相似：词法作用域。 源程序与翻译在函数声明与词法函数作用域的嵌套结构上高度相似（图 2 中用绿色标注）。如果忽略那些不会“逃逸”的若干闭包（例如 JavaScript 中的 i => a[i] *= n），我们的程序骨架会保留这类词法作用域信息，从而基本可以原样翻译到 JavaScript。
¹

部分相似：符号表。 源程序与翻译的符号表相似但不完全相同。源程序中的一些符号会在翻译中保留，而另一些会被消除。例如，变量 asum 会被保留，而 compute 函数中的变量 x 会被消除，改用表达式 arr[i] 代替。类似的消除也发生在 multi 中变量 y 上。被消除变量的共同特征是：它们在其作用域之外并不会被访问。Skel 会静态地消除这类符号，并在不包含它们的情况下生成骨架。

不相似：API 使用与编码风格。 尽管两种语言在高层结构上相似，但在语句层面常常不同。语义上相近的语句，通常需要使用不同的 API、运算符与编码风格来表达。这些差异进一步影响了程序逻辑的组织方式。举例来说，Python 的 range 与 zip（图 2 中橙色标注）常用于编写循环；然而在 JavaScript 中并没有与 range 或 zip 自然对应的 API。对这类循环的符合习惯用法的 JavaScript 翻译，往往会使用不同类型的 API，例如 keys 和 forEach。正因为存在这些语言差异，Skel 将语句层的细节在骨架中保留为占位符，并在目标语言中用语义方式对其加以重建。

¹ 注意：该示例并未展示某些特性，例如 Python 的关键字参数，这在 JavaScript 中没有直接对应。我们在第 5 节会说明如何处理它们。

Skel 旨在生成一种程序骨架：在保留源程序与翻译之间相似性的同时，抽象掉它们的差异。因此，它把源程序看作是对源骨架 $K^{\mathrm{src}}$ 的一次完成，完成片段为 $g^{\mathrm{src}}_0,\ldots,g^{\mathrm{src}}_3$ 。随后，JavaScript 程序的语法骨架就可以通过参照 $K^{\mathrm{src}}$ 来生成。图 2 右上角标注为 $K^{\mathrm{tgt}}$ 的代码行表示该骨架的一部分。

图 3 右侧展示了我们在 SkelCR 中骨架语法结构的图表示。它包含四个词法作用域及其各自的符号表，同时省略了语句层面的细节。父子关系对应于词法作用域的嵌套结构。每个符号表罗列了所在词法作用域中的所有声明，包括变量与嵌套函数（闭包）的标识符。生成器与类在概念上类似于闭包。当前作用域之外不会被访问的符号会被消除。闭包 _update 虽然嵌套在 compute 中，但可能会逃逸（escape），因此会保留在骨架里以便正确建模其语义。骨架的语法结构在 SkelCR 中形式化为图 4 所示的两部分：各作用域上的可观测符号（Scopes），以及跨作用域的符号映射关系（Relations）。每个作用域都有一个符号表。例如，图 3 中四个符号表里的可观测符号，对应于图 4 中每个作用域的符号表（记为 $\mathrm{Id}^{\mathrm{Scope}}$ ）。符号可以跨作用域相关联：图 3 中的虚线箭头表示非局部符号所引用的目标，绿色箭头表示作用域的父子关系。这些关系在图 4 中分别对应于 $\mathrm{Map}^{\mathrm{nonlocal}}$ 与 $\mathrm{Map}^{\mathrm{Closure}}$ 。

到目前为止的示例解释了 Python 与 JavaScript 中的一些通用语言特性，它们与 SkelCR 的对应关系如图 4。我们支持的其他语言特性（如类声明与装饰器）的处理在我们的技术报告 [53] 中有进一步说明，其中还详述了源代码规范化的细节。

4.2 语义要求的抽取

第 3 节提到的 ProcEmu 模型为 Python 源程序与 JavaScript 翻译的具体语义提供了统一表示。Skel 以两步法为占位符构造语义要求：首先，在具体的程序输入下记录每个源片段的可观测效应；然后，将这些可观测效应直接映射为相应占位符的语义要求。

4.2.1 获取可观测效应

我们构建了一个动态分析器 ProcEmu analyzer，用来监控真实的程序执行，并抽取与 ProcEmu 执行模型相对应的消息——在该模型中，每次对某个代码片段的调用就是一个“进程”。于是，每个代码片段的可观测效应就是这些“进程”之间的相关消息。

以图 2 的运行示例为例，Skel 将源 Python 程序建模为 9 个相互通信的进程（如图 5）。整个消息序列 $\rho$ 被可视化为进程之间的箭头。在这一语义模型中，由 $K^{\mathrm{tgt}}$ 创建的“骨架进程” $\mathcal{K}_{\mathrm{tgt}}$ 负责编排其他 8 个“片段进程” $P_0,\ldots,P_7$ 。某些代码片段（例如 $g^{\mathrm{tgt}}_3$ ）会被多次调用，因而会对应多个进程（如 $P_2$ 与 $P_5$ ）。

在我们特定的 ProcEmu 设计下，程序执行可概括如下：任意时刻只有一个进程在执行。执行从骨架进程 $\mathcal{K}$ 开始，它会立即启动与入口片段对应的“代码片段进程”（该片段也可以是整个程序的测试）。当某个代码片段进程把控制流转交给程序的其他部分时，它会在发送一条消息后暂停，这条消息会唤醒中央协调者——即骨架进程。骨架进程决定下一步执行，要么恢复一个现有进程（例如处理返回或抛出），要么创建一个新进程（例如进行调用）。通信仅在控制流转移时发生；所传递的消息不仅转移控制流，还包含后续执行所需的数据。关于骨架（在我们的 ProcEmu 执行模型中）的语义细节，请参见技术报告 [53]。

捕获到的行为（Behaviors Captured）：为了做到正确，分析应捕获足够细的细节，以便之后能够区分不同的执行。什么级别的细节才算“足够”，取决于语言中可能出现的程序行为。Skel 支持 Python 与 JavaScript 的子集（分别记为 $\mathcal{L}_{\mathrm{src}}$ 与 $\mathcal{L}_{\mathrm{tgt}}$ ），其中代码片段之间的所有交互可归为三类控制流交互（调用、返回、异常）以及三类数据共享（参数/数据传递、共享变量、共享引用）。每个闭包值被建模为一对唯一的 Id 组成的元组：该闭包自身所在作用域的 Id 与创建该闭包的进程 Id。通过这样的元组，我们的 ProcEmu 模型就能正确“仿真”对闭包的调用。对于共享引用，需要特别小心，因为它们可以出现在嵌套的数据对象之中；我们接下来会解释其处理方式。

省略的行为（Behaviors Left Out）：我们的模型把某些程序行为与状态视为单个“进程”的内部细节，因此不会在 ProcEmu 语义中捕获。例如（第 4.1 节提到的）被消除的局部变量的绑定变化、被消除且不会逃逸的闭包的调用，以及在同一片段内抛出并捕获的异常对象。最棘手的是共享数据引用：在一个代码片段中创建的变量与对象，可能通过多种方式在其他片段中被访问——例如闭包逃逸、堆上的共享引用，或是高阶库 API 将它们传给不同的片段。我们的 ProcEmu 分析器为每个进程动态维护一组“可能可达的对象”，以跟踪每个进程能够访问的对象；我们把这样的对象集合称为可观测集合（observable set）。每个进程的可观测集合会在控制流转移时更新：从可观测符号/对象可达的对象会被加入集合，并在该进程结束前一直保持可观测。其他对象不会加入该集合，例如大多数临时对象或某些库 API 实现中的内部对象。当某个进程的当前状态不再被其他进程访问时，分析会把与之相关的通信消息从记录中移除。

API 的副作用（Side Effects of APIs）：程序中的 API 调用同样会对代码片段的可观测效应做出贡献，并在 ProcEmu 中建模。正如第 4.1 节所述，许多 API 在 Python 与 JavaScript 之间缺乏清晰的一一对应。因此，我们尽量在可能的情况下把它们抽象掉，而不是都作为调用（Call）效应显式建模。具体而言，我们把非纯 API 调用的副作用分为两类：透明（transparent）副作用与不透明（opaque）副作用。当 API 会修改或创建可从其输入或输出对象间接引用到的数据对象时，我们把其影响视为“透明”的——此时只需让 ProcEmu 分析器跟踪可观测对象上的变化即可捕捉其效应。相反，“不透明”效应来自与外部环境交互或修改隐藏程序状态的 API；典型例子是 Python 中的 print 与 random。我们的 ProcEmu 分析器把这类不透明效应建模为发送给骨架“进程”的一种特殊调用消息，并由该骨架进程直接处理。在实际实现里，我们通过 手写垫片（shim） 来处理此类 API；这既繁琐又容易出错，从而在一定程度上会影响可靠性。更多建模细节见我们的技术报告 [53]。

笔者注：手写垫片（shim）不太靠谱吧

通信消息格式（Communication Message Format）：基于上述分析，我们可以把“进程间通信”作为每个代码片段的可观测效应记录下来。用于表达这些通信消息的文法列在图 6 中。整份记录（图 6 中的 Semantics）由针对每个代码片段（通过 $\mathrm{Id}^{\mathrm{Scope}}$ 标识）的一组消息序列（记为 $\overrightarrow{\mathrm{MsgSeq}}$ ）组成。每个 $\mathrm{MsgSeq}$ 表示某个片段的一次执行过程中的消息序列（ $\mathrm{IOStep}$ ），包含进入与离开该进程的消息。对每个片段进程，消息分为三类输入消息与三类输出消息。每条消息都携带相关数据，包括一个简洁的上下文 $\mathrm{CTX}$ （由前述“可能可达对象”的分析及控制流相关的数据传递共同决定，例如调用消息中的 $\mathrm{ARGS}$ ）。

图 7 展示了我们在 ProcEmu 模型中记录的、对示例程序中代码片段 compute 的一次执行的可观测效应；这次执行对应于前面图 5 中与进程 $P_1$ 相关的那条路径。图 7 中部给出了 $P_1$ 与概念性 ProcEmu 设计里的骨架进程 $\mathcal{K}_{\mathrm{src}}$ 是如何通信的。对可观测效应的分析，等价于在执行中部所示的伪代码时记录消息。以相同的方法分析其他片段，我们的分析器即可收集到图 7 右侧所示的整程序可观测效应。

4.2.2 将可观测效应迁移到目标端（Transferring the Observable effects to the Target）

从源端的 Python 程序获得可观测效应之后，下一步就是把这些可观测效应转换成目标骨架中各占位符的语义要求。

转换的主要目标。 转换的核心目标是映射数据类型。SkelCR 中的大部分表示（对应于图 6 的 Semantics）在转换时都保持不变；唯一需要改变的是数据对象表示中的数据类型名（即 $\mathrm{Id}^{\text{type}}$ ，对应 VAL 中的类型）。例如，我们会把所有 $\mathrm{Id}^{\text{type}}=\text{"List"}$ （Python 中的一种类型）改为 $\mathrm{Id}^{\text{type}}=\text{"Array"}$ （JavaScript 中的一种类型）。数据对象的语义内容与相互关系不变。

类型映射（Type Mapping）。 在目标语言中选择映射到哪种数据类型是 Skel 需要处理的一项重要问题。符合习惯用法的翻译通常会使用语义上相近的类型，但对每一种源端数据类型来说，不存在一种在所有翻译任务中都最优的单一目标类型。举例而言，图 8 展示了同一个 Python 代码片段（compute）及一个 JavaScript 翻译的细节。在图 8 左侧的 Python 代码执行期间，变量 arr 指向类型为 List[int] 的对象（这一点可从图 8 标注出的可观测效应看出）。在右侧的翻译代码片段中，arr 指向类型为 Array<number> 的对象——这是 JavaScript 中常用的类型。然而，也存在许多其他选择，例如 Array<BigInt> 或 BigInt64Array，它们可以支持更大的整数值，或更高效的内存操作。

Skel 采用一个默认的类型映射 $\mathcal{F}$ （部分示意见图 8 中部），在把可观测效应转化为骨架中的语义要求时做到对上下文不敏感。类型一致性由 $\mathcal{F}$ 来保证：例如，我们可以据此确定，凡是 Python 中类型为 List[int] 的对象，在 JavaScript 中对应对象就必须是 Array<number> 类型。必要时可以覆写这份默认映射，以便针对具体翻译任务做定制。至于如何自动决定最佳类型映射（可能依赖上下文）属于与 Skel 正交的问题，是一条有价值的后续研究方向。

笔者注：说白了也就是不管怎么决定最佳类型映射

翻译的灵活性（Translation Flexibility）。 通过用可观测效应来抽象细节，Skel 得以支持更灵活的翻译。例如，图 8 中 Python 代码片段里的 zip(mat, arr) 调用会创建一个有状态的迭代器对象，在调用 multi 之前会被多次更新。然而，这个在 compute 中使用的迭代器对象并不会被程序的其他部分访问，因此被省略在可观测效应之外。相应的 JavaScript 翻译在实现循环的方式上拥有自由度——只要可观测效应一致（比如具有同样的 Call 消息序列等）。例如，图 8 右侧的 JavaScript 翻译中，Python 里的 zip 迭代器对象已经不存在；该循环改用 JavaScript 标准库中的 forEach API 来表达（其内部同样是有状态的）。

4.3 代码片段合成（Code Fragment Synthesis）

在获得程序骨架之后，Skel 会为占位符合成代码片段。图 2 的 JavaScript 翻译中，以四个虚线框高亮的片段就是这样合成出来的，对应 $g^{\mathrm{tgt}}_0,\ldots,g^{\mathrm{tgt}}_3$ 。这些片段与目标语言中的程序骨架 $K^{\mathrm{tgt}}$ 组合后，就得到完整的翻译。在这一步中，Skel 使用外部合成器（例如 LLM）。

Skel 按照程序的执行顺序逐步合成并细化这些代码片段。每个片段都由代码合成器生成。我们提出一个称为按执行顺序翻译环（Execution-Order Translation，简称 EOT）的算法来处理整个过程。EOT 环在每一步之后都利用 ProcEmu 对不完整的翻译进行检查：如果当前将要执行的代码片段尚不存在，EOT 环就向合成器发出查询以获取一个初始片段；否则，若该处已存在片段，EOT 环就在其上应用“检查—细化”（check-and-refine）策略。已经通过检查的执行步骤会被跳过，只有那些未通过的步骤（即反例）会被提供给合成器，用以细化相应的代码片段。EOT 环终止时，最终翻译自然会通过用于派生语义要求的所有测试。下面我们用一个例子详细说明 EOT 环；该算法的精确定义见技术报告 [53]。

EOT 示例（EOT Illustration）

图 9 展示了 EOT 环的一次示例运行，其目标是在目标骨架中补齐各片段，使得最终完成体能够实现先前图 5 中的执行序列 $\rho$ 。为简明起见，图中省略了涉及骨架进程 $\mathcal{K}$ 的中间步骤。对每个步骤，处理时可能出现三种情形：“缺失片段”（Missing Fragment）、“步骤出错”（Step Error）与“步骤通过”（Step Pass）。

“缺失片段”意味着此步所对应的概念性进程 $P_i$ 背后的代码片段还未实现（如图中与进程 $P_1$ 相关的第 2 步）。EOT 环会构造一个合成查询来生成该片段。此处所谓“规格”（specification）指的是提供给合成器的若干输入—输出步骤，它们是针对每个代码片段的语义要求中的一个子集，与其他片段无关。当出现“缺失片段”时，EOT 环会选取与该片段相关联的第一个输入—输出步骤作为初始规格；该初始规格与源端（Python）中对应的代码片段一起，作为提示共同发送给合成器（即 LLM）。
第二与第三种情形发生在图中那些已有对应代码片段的“进程”上：若现有片段在该步表现符合期望，则记为“步骤通过”，EOT 环继续处理 $\rho$ 中的下一步；否则就是“步骤出错”。对于“步骤出错”，EOT 环要么细化规格（例如将该错误作为反例加入），要么修复已有代码片段（即带着错误信息重试）。

例如，图 9 倒数第二步在执行 $P_1$ 时出现了错误步骤，从而触发了对片段 compute 的细化。细化—修复过程的目标，是迭代地更新该代码片段，使其通过出错步骤，同时不破坏先前已经通过的步骤。概念上，这与程序中其他片段无关，因为错误的根因一定位于当前片段之内。为修复该错误，EOT 环首先将该错误步骤作为反例加入规格，然后基于更新后的规格重新合成一个代码片段，并重新执行与该片段相关的全部执行步骤予以校验；若全部校验通过，视为该错误已被解决，EOT 环继续前进。以图 9 为例，该错误通过给片段 compute 的规格新增一个反例得到解决。

还可能出现这样的情况：当某个代码片段被更新后，之前与同一片段相关的一些步骤又报告了错误。若此前的该步骤尚未被选作反例，则会将其纳入并进一步细化该片段的规格。另一种可能是：该片段的行为直接违反了迄今为止为它累积的规格。在这种情况下，Skel 会高亮该不匹配并指示合成器去修复其已生成的代码；更具体地，Skel 会把语义不匹配的描述与当前片段一并提供给 LLM，以便其在代码中修复错误。该过程会反复迭代，直至错误被解决，或达到预设的修复重试上限。在后者情形下，EOT 环会暂停并等待外部协助（因为合成器可能无法独立修复）。最终，当 $\rho$ 中所有步骤都被处理完成时，我们将得到一个在测试上正确的完整翻译（如图 2 所示的那样）。

5. 实现（Implementation）

本节说明遵循第 4 节设计而实现的 Skel 原型。

支持的语言子集。 我们的 Skel 原型聚焦于满足以下性质的 Python 与 JavaScript 的子集，使其适合在特定的 ProcEmu 模型中建模。首先，这些子集中的程序是确定性的且单线程。其次，对这些程序而言，运行时不能创建或修改词法作用域，也不能在不通过符号表中的变量的情况下访问词法作用域（例如排除反射，如 eval(..)）。第三，我们假定这些程序中使用的大多数库 API 与运算符要么是纯的，要么只产生透明副作用（见 4.2 节）。在我们的实验基准中，超过 90% 的 API 满足这些标准。对少数带有不透明副作用的 API（如 random 与 print），我们在 ProcEmu 下实现了 API shim，把它们的影响计算为进程通信消息。目前这类 shim 的实现仍是尽力而为，可能并不完整。更多细节见技术报告 [53]。

笔者注：仅适用于单线程、无反射（eval）、低副作用代码

重写 Python 语言特性。 在 SkelCR 的设计里，我们只对闭包与位置参数进行建模。为支持包含类、装饰器、关键字参数等结构的程序，我们的 Skel 原型会先通过一个简单的规范化步骤，把它们重写为嵌套闭包与位置参数。类的继承与类方法也通过该规范化步骤处理。有关规范化策略的细节见技术报告 [53]。

骨架生成。（以 SkelCR 表达的）语法结构通过对源程序进行轻量分析而提取：解析符号定义与引用，并消除那些未在其他位置被引用的局部符号，以及确定不会逃逸的小型嵌套闭包的符号表。对于骨架的语义要求，我们在每个代码片段的入口与出口上插桩所有可能的控制流转移。动态分析器还会记录共享对象与闭包的元数据，如 4.2.1 节所述。

6. 评估（Evaluation）

我们从两个方面评估 Skel 在将程序从 Python 翻译到 JavaScript 这一任务上的表现：

有效性（第 6.1 节）：Skel 能否在合理正确性的前提下，基本自动地把真实世界的 Python 程序翻译到 JavaScript？
消融研究（第 6.2 节）：Skel 的各个组成部分分别贡献了多少？

笔者注：原文为5.1节和5.2节，应该为笔误

基准（Benchmarks）.我们期望基准中的每个样例程序都是带测试的独立 Python 程序。已有一个满足此要求的基准，来自以往关于调试神经翻译的工作 [51]：它包含 5 个真实世界的 Python 模块（不含测试），规模在 121～882 行代码（LOC）之间。除该基准外，我们还从 GitHub 上选取了至少 700 颗星的流行仓库中更长、更多样的 4 个程序，组成表 1 所示的基准。共计 9 个程序，规模从 121 LOC 到 2400 LOC 不等，既涵盖经典算法的实现，也包含用于生产的标准库或第三方模块。我们报告每个程序的静态调用图的最大深度 $h_{\mathrm{CG}}$ ；可以看到，程序越长，通常 $h_{\mathrm{CG}}$ 越大，说明其结构复杂度更高。

为降低外部 LLM 合成器的难度，我们将单个代码片段的最大大小限制为 100 行。基准中只有 5 个函数超过 100 行；我们对这 5 个函数的函数体做了语法层面的重构，拆分为更短的（<100 LOC）的小函数。该步骤较为直接，可用现成的 IDE 工具自动化完成。若样例含多个文件，我们将其合并为单文件的可独立运行的 Python 程序。表 1 中的统计均基于此类预处理后的程序，既用于评估 Skel，也用于与基线方法对比。

单元测试与全局数据。 基准中的每个 Python 程序都自带测试套件。我们对其中部分测试套件做了扩充以提高覆盖率，并用扩充后的套件进行评估；最终覆盖率见表 1。按照既有工作 [27, 51]，我们用简单的字符串替换将 Python 测试转为 JavaScript 测试；这已足够，因为测试通常是例行的调用序列与数值比较，不需要“符合习惯用法”的代码合成。我们手动检查这些测试以确保其正确性，同时 Skel 也帮助确认它们在源端与目标端表现一致。我们对程序中的全局常量（如可能很大的数组初值或查找表）也做了类似的转换，它们体量虽大但转换直接。

Skel 的设置（Skel Setup）。我们为所有程序配置 Skel 使用相同的默认类型映射。Skel 的 EOT 环的“修复”最大重试次数设为 3；即若某一步在 3 轮重试后仍失败，EOT 环就会暂停并等待外部帮助。用于 LLM 合成与基于提示的修复的模型为 “GPT-4-turbo” 与 “GPT-3.5-turbo”²（当时最先进的 LLM 之一）。我们将解码温度设为 0 以降低输出噪声，并为所有程序固定一套提示模板；提示细节见技术报告 [53]。

笔者注：

对比的翻译器（Compared Translators）。我们与两类基线进行对比：一类基于 LLM，另一类基于编译器规则。

LLM 基线：我们实现了一个简单的语法层“分而治之”策略，使用与 Skel 相同的模型、超参数与相近的提示。该方法把源代码顺序分割成片段，每个片段对应全局作用域中的一个完整函数或类定义，然后逐段请求 LLM 翻译并串接结果。
规则基线：采用一个生产可用、基于编译器规则的现成翻译器 Transcrypt [42]。它是 Python→JavaScript 最成熟的规则式翻译器之一，在 GitHub 上约有 3k 颗星。

评估指标（Evaluation Metrics）。我们使用两种不同粒度的正确性指标：

整体正确性：看最终翻译是否通过测试。
外部修复量：当不能自动得到正确翻译时，我们用“需要外部协助（如用户）修复的函数个数”量化，简称 #UserFix。
- 对 Skel，#UserFix 指 EOT 环卡住（达到重试上限）时，需要用户提供的正确代码片段的函数数，以便 Skel 能继续完成剩余翻译。
- 对基线方法，由于没有像 Skel 那样的逐步自动验证，很难严格定义 #UserFix。我们采取“尽力而为”的方式：开始调试并修正最明显的错误（如类型错误、缺失 API 等）。若修复发生在某个函数内部，则把该函数计入 #UserFix。我们对每个程序投入 1–2 小时 人工修复，得到 #UserFix 的下界：若修了 $k$ 个函数后程序仍不正确，则记为 $(k+)$ 。

6.1 整体有效性（Overall Effectiveness）

我们首先评估将 GPT-4-turbo 或 GPT-3.5-turbo 作为代码合成器时 Skel 的整体有效性。由于只要 EOT 环成功终止，Skel 就保证能通过测试，因此我们的评估流程是：让 Skel 翻译这 9 个程序；当 Skel 在某个代码片段上“卡住”时再进行人工介入。我们统计需要介入的函数个数（记为 #UserFix）。最终（按设计预期），所有翻译都会通过测试。我们同时报告无需人工介入、由 Skel 自动翻译并验证通过的函数个数（记为 #Auto）。表 2 给出了 #Auto 与 #UserFix 的数值。我们还使用自动化比例：

\text{Automation Ratio}\;=\;\frac{\#\mathrm{Auto}}{\#\mathrm{Auto}+\#\mathrm{UserFix}}\, .

我们发现，使用 GPT-4 的 Skel 能在无需人工介入的情况下，自动翻译 9 个真实程序中的 4 个（文中以绿色高亮）。更具体地，Skel+GPT-4 能自动翻译 466 个函数中的 443 个，整体自动化比例约 95%。当代码合成器较弱（GPT-3.5）时，Skel 只能自动翻译 1 个程序，但总体自动化比例仍约 85%。所有最终翻译均通过测试。

更强的合成器带来更好的效果：配备 GPT-4 的 Skel 能自动正确翻译约 95% 的函数，所有最终翻译都通过测试。

随后我们将 Skel 与两类基线翻译器比较：一种基于 LLM，另一种基于编译器规则。这里将 GPT-4 作为 LLM 基线。表 3 展示了每个基准的 #UserFix（0 表示无需任何人工介入即可正确）。按“评估指标”所述，若在有限时间内仍未通过测试，我们报告 #UserFix 的下界，记为 $k+$ 。

由表 3 可见，LLM 基线无法正确翻译 9 个基准中的任何一个；从 #UserFix 看，其翻译中需要修复超过 93 个函数。这一过程既耗时又繁琐，尤其是对两份超过 1k LOC 的程序——作者为修复它们投入了数十小时，但仍未能让其中 2 个程序全部通过测试。规则式翻译器 Transcrypt 能正确翻译 2 个程序，但对另 5 个程序无法运行（记为 NA），原因在于这些程序使用了 Transcrypt 不支持的 API 与语言特性。修复 Transcrypt 的翻译也并不容易：其结果依赖模拟的库与依赖项，可读性较差。相比之下，要让 9 个程序全部正确，Skel+GPT-4 所需的 #UserFix 约为基线方法的 1/4。同时，得益于 Skel 的逐步检查，我们可以把错误精确定位到单个代码片段的范围，便于人工介入。值得注意的是，即便 Skel 配备较弱的 GPT-3.5，其表现仍优于配备 GPT-4 的基线方法。

与其他翻译器相比，Skel 的翻译需要的 #UserFix 明显更少；Skel 的逐步检查也让人工介入时“该修哪里”一目了然。

6.2 消融研究（Ablation Study）

我们进行了消融实验，以评估 Skel 的代码合成机制中每一项设计选择对其自动化水平（从而减少人工工作量）的贡献。举例来说，填充程序骨架的最基础做法，可能只提供对应的源端代码片段以满足语法，而不提供用于验证每个代码片段的语义要求。我们通过实证验证了两项关键选择对最终自动化比例的必要性：（a）在源端代码片段之外，额外提供一步语义要求作为规格（specifications）；（b）check-and-refine（检查—细化），它旨在当合成器（LLM）首次未能得到正确实现时，自动地对每一步进行验证、细化并修复代码。

我们分别用 $\text{Skel}_{\text{base}}$ 、 $\text{Skel}_{\text{spec}}$ 与 $\text{Skel}_{\text{spec+chkrfn}}$ 表示三种变体：仅提供源端代码片段（不含上述两点）、在合成中使用语义规格、以及完整的 Skel（既含语义规格、又含逐步的 check-and-refine）。我们使用 GPT-4 作为代码合成器，对每个变体进行测试，并报告每个变体的 $\#\mathrm{UserFix}$ （需要人工修复的函数数）。结果见表 4。

没有语义规格与迭代细化帮助时， $\text{Skel}_{\text{base}}$ 在翻译过程中产生了 89 个错误函数。将语义规格加入 Skel 后，约有 1/3 的 $\#\mathrm{UserFix}$ 被消除，仍剩 61 个——这表明语义规格能帮助 LLM 更清晰地理解任务，但合成代码仍易出错。在此基础上再加入迭代细化，又可自动化处理额外 38 个 $\#\mathrm{UserFix}$ 。在 check-and-refine 的帮助下，LLM 在大多数情况下最终能够合成正确的代码片段。关于剩余 $\#\mathrm{UserFix}$ 的进一步讨论，见技术报告 [53]。

7. 局限性与开放问题（Limitations and Open Problems）

我们发现 Skel 作为“骨架”概念的一个有前景的原型，能够把 最多约 2k 行 的 Python 程序自动翻译为 JavaScript。若要扩展到更长的程序，我们预见主要有三大挑战，未来工作可着力解决：

类型映射的自动化（Automated type mapping）。 较长的程序通常使用更广泛的数据类型。若能自动建模数据类型、自动选择类型映射，并允许为程序的不同部分灵活更换映射，将能显著减少人工工作量，尤其在需要翻译来自第三方库的数据类型时。
具有不透明副作用的 API 建模（API modeling with opaque side effects）。 对于带有不透明副作用的 API（如 print(...)），目前我们的做法是手动为其编写 shim（见第 5 节）。更长的程序往往包含更多此类 API，甚至包含目标语言中没有对应项的 API。手工建模既繁琐又易错。将这类 API 建模自动化，有望把 Skel 的适用范围扩展到更大的程序族。
面向语言结构的自动重构（Automatic refactoring for language constructs）。 更长的 Python 程序可能使用更多语言特性，其中一些（如多重继承）是源语言独有的，这会导致源程序在高层结构上无法直接映射为目标语言中的合法程序。我们认为，在翻译开始前对源程序的高层结构做自动化重构是一个可行方向；这方面可借鉴既有的代码迁移经验报告 [48]。

除上述实现层面的挑战之外，追求完整的函数等价性（functional equivalence）在翻译长程序时也是一个开放问题。Skel 目前聚焦于基于测试的等价性，这并不能保证在所有可能输入上都等价。另一条可能的道路是：针对自动推断得到的函数规格，采用形式化验证来证明等价。

本文聚焦于自动化的程序翻译，目标是生成满足基于测试的正确性要求的代码。这个问题与代码迁移、程序合成以及规格推断密切相关。

代码迁移（Code Migration）

人们已经探索了多种自动化代码迁移的方法。一条路线是构建规则驱动的系统。领域特定语言 TXL [15] 与 StringTemplate 工具 [40] 等，都是用于编写代码变换的通用工具。工程上也有针对特定语言的转译器，例如 Transcrypt（将 Python 翻译为 JavaScript）[42]。理论上，这类方法可以扩展到长程序，但在实践中，往往需要大量工程投入才能构建足够完备的系统来翻译真实世界的程序。与此同时，这些规则工具经常会生成不可读的代码，它们只是在最低层面模拟源程序 [22, 24, 42, 50]。

另一条路线是利用数据驱动方法。神经网络可以在无需手写规则的情况下翻译代码 [12, 14, 28]。随着近年 LLM 的发展，短程序的翻译性能取得了显著进步 [13, 37, 56, 59]。在数百万行真实代码的训练下，它们常能生成符合目标语言习惯、可读性高的翻译。不过，在代码翻译中 LLM 依然容易出错；随着源程序长度增加，任务很快超出 LLM 的能力范围，生成的代码也很难正确 [30, 51]。本文提出一种基于骨架生成的两阶段方案：对任务做清晰的分解，既支持规模化翻译，又能保留“习惯用法”的代码风格。我们也注意到有并行工作同样在探索对长程序翻译的任务分解 [23, 58]，但它们面向的是辅助人类开发者的部分翻译，并不以通过整程序测试为目标。

笔者注：说明一下我们工作的独特性

程序合成（Program Synthesis）

代码翻译也与程序合成密切相关。程序合成旨在根据规格，在目标语法中生成实现；规格形式包括输入/输出示例 [41]、逻辑公式 [6]、参考实现 [26]、内联断言 [45] 等。近来，LLM 成为合成程序的另一条重要路径，出现了大量针对编码任务构建或专门化的模型 [7, 11, 31, 35, 43, 60]。

在代码翻译方面，已有工作尝试用合成技术在不同语言间转换代码。例如，Kamil 等将 Fortran 的 stencil 计算编码为可由 SMT 求解的正确性翻译 [26]；此法适用于领域特定语言，但难以扩展到大程序。Wang 等从用户片段合成翻译规则，并搜索规则组合来翻译程序 [50]；然而该方法因指数级搜索空间而可扩展性有限。我们的做法把代码翻译正式化为一种合成任务：合成器得到每个占位符的输入/输出规格以及对应的源端片段作为参考。其可扩展性的关键在于对任务的干净分解：按执行顺序把整体问题拆成子任务。即便片段级合成会失败，未来的自动化技术也可以为特定片段引入更专业的合成器。

规格推断（Specification Inference）

自动化规格推断在程序分析与验证中已有大量研究 [4, 5, 8–10, 16, 18, 21, 29, 34, 47]。最常见的技术之一是双向溯因（bi-abduction） [10]，其目标是在分离逻辑中自动推断程序的前/后置条件 [9, 17]。尽管前景可期，现有成功多局限于简单性质，而非函数正确性规格。近期的 Quiver 技术 [46] 通过人写注释来引导溯因推断，从而缓解歧义并确定合适的抽象层级。除形式化技术外，数据驱动的规格推断也在兴起 [19, 32, 36, 39, 49, 57]。虽然这些技术有望推断出完整的函数规格，但对结果规格的自动验证仍然是一个挑战 [32]。

9. 结论（Conclusion）

我们针对高层构造相似的语言，提出通过骨架生成来解决代码翻译问题。我们的方法 Skel 通过为代码片段生成来自测试的输入/输出规格，把 Python 翻译为 JavaScript。核心思路是把两种语言的程序语义抽象到一个共享的通信进程模型中：既捕获可观测效应，又省去低层、语言特定的细节，以支持习惯用法的翻译。我们还提出了一个按执行顺序填充骨架的实用算法。在真实世界程序上的评估显示了 Skel 的有效性。

仍有若干挑战：包括超越测试的正确性、更广的数据类型映射的自动化、更多 API 的建模，以及更多语言结构的支持。我们认为，解决这些问题的后续工作将进一步提升 Skel 翻译更复杂程序的能力。

10. 数据可用性声明（Data Availability Statement）

本论文所用的代码与基准数据所组成的工件已在 Zenodo 提供 [52]。该工件的最新版本可在此处获得 [3]。