Verifiers in the Loop: Decoding Time Verification for Code Translation¶

会议: NeurIPS 2026
arXiv: 2605.17626
OpenReview: https://openreview.net/forum?id=7RvjiiRX0n
代码: https://github.com/qsdrqs/dtv-translation
领域: 代码智能
关键词: 代码翻译, 测试时验证, 解码期验证, 结构感知回滚, 编译器反馈

一句话总结¶

提出解码期验证框架 DTV，将确定性验证器引入自回归生成内循环，在语句和代码块等结构边界进行局部渲染、验证、结构感知回滚与诊断反馈增强，在同等 Token 预算下大幅提升代码翻译编译通过率。

研究背景与动机¶

近年来，通过在推理阶段分配额外计算资源（如重复采样、搜索、自反思优化等测试时计算扩展）来提升大语言模型的生成质量，已成为超越单纯扩大预训练规模的重要路径。然而，现有的测试时计算扩展方法大多针对数学或开放性自然语言推理设计，依赖模型自身的概率置信度或学习得到的奖励模型（PRM）进行指导。这种软性打分在编码任务中往往表现脆弱：代码具备极其严格的离散句法与语义正确性约束，模型极易为看似合理但实际存在编译/类型错误的代码赋予高概率，且代码奖励模型跨语言迁移成本极高。

与开放领域不同，软件开发任务天然具备编译器（如 rustc）、静态类型检查器（如 tsc）以及自动化测试等确定性外部验证器，能够提供确定性的通过/失败判定与丰富的诊断定位信息。传统的验证方式多为事后验证（outcome-only），即在完整程序生成完毕后再调用验证器进行过滤、重排序或多轮修复。这种机制的核心痛点在于无法干预生成轨迹本身：一旦前缀中引入了可通过验证器检测的早期错误（如变量所有权转移或类型不匹配），后续的自回归解码就会在受污染的上下文条件下持续展开，模型往往会顺着错误继续推演而非主动纠错，造成极大的生成算力浪费与累积错误蔓延。

为了打破事后验证在自回归语境下的滞后性，亟需一种让确定性验证信号直接参与自回归内循环的解码范式，在错误发生之处即时阻断并纠偏。核心 idea：构建解码期验证框架（DTV），将代码结构边界作为元步骤，在生成过程中交替执行前缀局部渲染与确定性验证，通过结构感知回滚与诊断反馈提示增强，确保自回归生成仅在经过验证的合法前缀上延伸。

方法详解¶

整体框架¶

DTV 将代码生成过程抽象为一个显式的确定性状态机控制器，与冻结参数的预训练代码生成模型协同工作。在生成目标程序时，基础采样器按词元逐步生成，直到遇到语句（statement）、代码块（block）、函数（function）或完整程序（program）等结构边界，此时控制器暂停生成触发“元步骤（meta step）”。在元步骤中，渲染器将当前不完整的代码前缀转换为验证器可解析的合法工件，并触发适用的验证器套件进行检验；若全部通过则提交该前缀为安全检查点，若存在失败则提取结构化诊断信息并依据升级策略执行局部回滚与反馈增强重试。

%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
    A["源程序与未验证前缀"] --> B["结构边界生成与合法前缀渲染"]
    B --> C["多粒度验证器套件检验"]
    C -->|全体验证器通过| D["检查点提交与前缀冻结"]
    C -->|存在验证错误| E["诊断反馈状态更新与提示增强"]
    E --> F["结构感知回滚与范围逐级升级"]
    F -->|回滚至上层结构| B
    D -->|未达终止边界| B
    D -->|程序级全部通过| G["输出已验证目标代码"]

关键设计¶

1. 结构边界验证与合法前缀渲染：在语法节点处维护合法前缀不变性

部分生成的代码在语法上通常是不完整的（如未闭合的括号、缺少后继声明），而编译器或类型检查器通常要求完整的代码单元才能执行检查。DTV 建立了一套嵌套层次结构 \(\mathcal{G}=\{\texttt{stmt}\preceq\texttt{block}\preceq\texttt{func}\preceq\texttt{program}\}\)，并通过流式解析器维护的作用域栈在结构闭合符号处触发暂停。渲染器 \(\mathsf{Render}:(S,Y_{\leq i})\mapsto A_{i}\) 负责将当前前缀补齐为验证器可识别的代码工件，例如为语句补全局部包装函数或临时占位闭合。每个验证器 \(O_j\) 配备适用谓词 \(F_j(A)\)，仅在工件满足最低粒度时介入。只有当当前作用域下所有适用验证器均判定通过（\(q_j=1\)）时，控制器才执行 Commit 操作，将前缀固化为检查点 \(\mathcal{C}\)，从而严格维持“合法前缀不变性（legal prefix invariant）”——即所有已提交的检查点均可保证在语法与静态语义上无已知矛盾，为后续回滚提供可靠基准。

2. 结构感知回滚与范围逐级升级：自适应平衡上下文保留与上游错误根因清除

当验证失败时，直接在当前语句简单重采样往往无法解决深层语义矛盾。例如在 C 转 Rust 任务中，后续打印语句触发的借用检查错误（E0382 所有权转移），其根源往往是数行之前的参数消费未调用 .clone()；若仅回滚当前打印语句，无论如何重试都必然失败。为此，DTV 提出了基于层次结构的逐级升级回滚策略（Escalation）。控制器默认从最小的语句级（\(\texttt{stmt}\)）开始回滚；若在同一诊断锚点上重试仍报告相同错误，则自动将回滚范围扩大至外层代码块（\(\texttt{block}\)）乃至函数签名起始点（\(\texttt{func}\)），截断并丢弃受影响的作用域栈帧，释放更大的编辑窗口让模型重写上游绑定逻辑。同时引入脱困机制（Bailout），当特定诊断锚点的访问频次达到预设上限时，主动终止内循环回退给外层自反思流程，避免在不可行路径上耗尽 Token 预算。

3. 诊断反馈提示增强：将结构化报错注入条件上下文以消除盲目重采样

若回滚后仅依靠温度采样重新生成，模型极易落入相同概率分布并复现相同错误模式。DTV 设计了反馈状态管理机制 \(\mathcal{F}_{k+1}=\mathsf{Update}(\mathcal{F}_k,o_k)\)，维护未解决的编译器报错、行号锚点及诊断日志。在启动重试前，控制器将反馈状态编码为文本块 \(\phi_{k+1}=\mathsf{Encode}(\mathcal{F}_{k+1})\)，并将原条件上下文 \(S\) 动态替换为增强上下文 \(\widetilde{S}_{k+1}=\mathsf{Augment}(S,\phi_{k+1})\)。重试支持两种具体模式：行内继续（Inline Continuation，将编译器诊断以代码注释形式追加在回滚前缀末尾，模型在同轮次中继续补全）和补丁修复（Patch-based Repair，开启新的对话轮次，向模型呈现结构化诊断并要求其针对回滚作用域返回最小修改补丁 diff）。通过这种定向反馈，模型在自回归重试时明确知晓此前违反的静态规则，显著提高了单次重试的修复成功率。

一个完整示例¶

以 C 转 Rust 中的所有权转移为例： 1. 模型首先生成函数头及中间语句：consume(message);，该语句在语句级验证时通过编译并被提交为安全检查点； 2. 随后模型生成下一句：println!("{message}");，此时流式解析器检测到分号触发验证，rustc 介入编译检测到错误 E0382: borrow of moved value: message； 3. 控制器首先尝试语句级回滚，在行内添加注释 // rustc error: E0382 borrow of moved value 并重新生成当前语句，但由于 consume(message) 已移走所有权，重试依然触发 E0382； 4. 控制器检测到相同错误代码停滞，触发作用域升级（Escalation），将回滚目标扩大至整个函数体起始，撤销此前已提交的 consume(message); 检查点； 5. 模型在携带 E0382 诊断提示的增强上下文中重新生成函数体内部逻辑，成功输出 consume(message.clone());，随后继续生成 println!("{message}");，验证器全票通过并顺利提交。

实验关键数据¶

主实验¶

在同等单样本 Token 预算（上限为源码 Token 数的 16 倍）约束下，以 Qwen3-4B-Instruct 为主模型，在 C 转 Rust（300 个 CodeNet 程序，rustc + 差异化测试）与 JS 转 TS（150 个 TypeWeaver 程序，tsc + ESLint）两项任务上对比 DTV 与基线。

任务	评估配置	编译通过率 (%)	均耗 Token 倍率 \(k\)	每次通过均耗 Token [95% CI]
C → Rust	naive / one-shot	16.3%	1.55	360 [309, 415]
C → Rust	naive / self-refine	72.3%	7.18	1903 [1548, 2339]
C → Rust	DTV / one-shot	47.0%	2.00	596 [499, 714]
C → Rust	DTV / self-refine	82.0%	5.28	1654 [1345, 1990]
JS → TS	naive / one-shot	4.7%	1.10	435 [310, 567]
JS → TS	naive / self-refine	33.3%	11.48	1648 [1071, 2497]
JS → TS	DTV / one-shot	21.3%	2.77	715 [547, 960]
JS → TS	DTV / self-refine	46.0%	10.11	2103 [1470, 2856]

在对比其他测试时扩展基线方面，DTV 亦展现出显著帕累托优势： - 相比 Best-of-N（\(N \in \{1, 2, 4, 8, 16, 32\}\)）：在 C 转 Rust 上 BoN 在 \(N=32\) 时通过率仅达 44.5%，而在 JS 转 TS 上 BoN 通过率全程停滞在 7.0% 且消耗大量 Token，显示单纯重采样难以摆脱缺乏类型注解的局部陷阱。 - 相比带有编译反馈的搜索基线 S：S 在 C 转 Rust 和 JS 转 TS 上分别取得 75.5% 和 33.0% 通过率，但每题平均 Token 消耗达到 DTV 的 4.7 倍与 2.0 倍；DTV 通过结构边界的即时回滚避免了全量程序重跑。

消融实验¶

在 C 转 Rust 前 100 个样本上，固定外层 self-refine 循环与 Token 预算，逐一剥离 DTV 的核心机制：

配置	编译通过率 (%)	\(\Delta\) (pp)	均耗 Token 数	\(\Delta\) Token	说明
DTV-full	85.0%	–	3580	–	完整 DTV 机制
DTV-no-feedback	74.0%	-11.0	4138	+558	仅回滚但不注入报错诊断反馈
DTV-no-escalation	79.0%	-6.0	3623	+43	仅在语句级回滚，禁止向上升级
DTV-detect-and-abort	70.0%	-15.0	4417	+837	遇错即终止内循环，完全退化为外层重试

关键发现¶

内循环修复是最大增益来源：禁用内循环恢复（DTV-detect-and-abort）导致编译通过率剧降 15.0 个百分点，且外层自反思轮次从 3.1 轮激增至 13.5 轮（增加约 4 倍），表明及早截断局部错误远胜于生成整段错误程序后再从头修补。
诊断反馈对单次成功率至关重要：剥离诊断反馈使一轮单次通过率（inner-1shot）下降 23.0 个百分点；缺乏具体错误信息的重采样极易重复踩坑。
范围升级有效解决非局部依赖：在细粒度分析中，DTV 的修复成功率在本地错误（Local，编辑行即报错行）上最高（C 转 Rust 50.0%，JS 转 TS 29.3%），在非本地错误（Nonlocal）上有所衰减；作用域升级机制使模型得以回滚修改更早的变量定义与声明，挽救了相当一部分跨语句依赖问题。
跨模型架构与规模表现稳健：切换至 Gemma-4-E4B 后 DTV 同样保持领先；在参数量更大的混合专家模型 Qwen3-30B-A3B 上，DTV 将 C 转 Rust 通过率由 92% 推高至 97%，JS 转 TS 由 57% 推高至 66%。

亮点与洞察¶

将编译器内化为解码期的状态机守门员：传统方法要么将验证器置于生成后的外循环，要么试图训练易过拟合的神经 PRM；DTV 巧妙利用代码天然的语法结构边界，以极小开销调用未经修改的现有工业级编译器，实现了离散符号世界与连续自回归模型的有机结合。
合法前缀不变性与结构化回滚机制：通过维护已验证检查点，DTV 避免了全局重启，在保证已生成前缀绝对可靠的前提下，让错误局限在最小语法单元内被就地消化。
可泛化的解码拦截架构：DTV 解耦了控制器调度逻辑、特定语言语法渲染器与具体验证器驱动，这一设计思路可直接复用至带有形式化约束验证（如 Dafny、Coq）、SQL 语法合规性检查或 API 接口契约调用的其他代码生成领域。

局限与展望¶

依赖具有行级定位能力的结构化诊断：DTV 依赖验证器输出具备精确行号定位与可解释错误信息的诊断结果；若验证器仅能返回全局布尔值（如黑盒执行超时或测试失败未指明断言位置），结构化回滚与反馈增强将难以发挥最大效力。
长距离非局部错误修复难度较大：对于跨模块类型不一致或深层架构重构需求，仅在函数/代码块级别的回滚仍然受限，极端情况下可能会出现重复尝试同一报错而耗尽预算的情况。
真实运行耗时的工具链开销：在 JS 转 TS 任务中，由于 Node.js / tsc / ESLint 每次启动与扫描的串行开销较大，DTV 在生成 Token 减少的同时端到端物理耗时有所上升；未来需探索常驻编译器后台服务或增量编译接口以加速验证。

评分¶

新颖性: ⭐⭐⭐⭐☆ 提出在结构边界交替执行局部渲染与确定性验证的状态机解码框架，设计了结构感知回滚与升级机制。
实验充分度: ⭐⭐⭐⭐⭐ 涵盖 C-Rust 与 JS-TS 两大任务、三类主流开源模型，提供了详尽的成本匹配帕累托对比、消融分析及错误类型穿透分析。
写作质量: ⭐⭐⭐⭐⭐ 概念形式化清晰，问题与机制定义严密，实验图表信息量极其丰富。
价值: ⭐⭐⭐⭐⭐ 为大模型测试时计算扩展在代码与高形式化领域的工程落地提供了极其扎实的范式参考。