生成式编译：让编译器在 AI 生成代码过程中实时给出反馈 Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code
用 sealor 把部分代码补全为可编译程序，让编译器在生成中途就反馈
前置知识
Sealor（封闭器）
本文提出的核心概念，是一个轻量级、语法主导的变换 $S : \Sigma^* \to \Sigma^*$，把未完成的「部分程序」补成一个完整、可被标准编译器检查的程序。它通过保留已生成的代码、在缺失处插入良类型占位符（如 $\varepsilon$、holeval()、holediv()）来工作。设计上要求「完备性」：凡是能补全为合法程序的部分程序，封闭后也必须是合法程序；同时尽量做到「可靠性」：让真正的死胡同前缀被编译器拒掉。
整个方法的核心就是 sealor——它让现有编译器（rustc）无需重写就能检查部分程序，是把编译器反馈从「生成后」提前到「生成中」的关键技术装置。
Rust 借用检查（Borrow Checking）
Rust 通过所有权（ownership）和借用（borrowing）规则在编译期保证内存安全：一个值在同一时段要么有多个不可变共享借用 &T，要么有一个独占的可变借用 &mut T，两者不能共存。借用检查器在编译期静态分析变量的生命周期与借用重叠，违反就报错（如 E0502：在不可变借用仍存活时尝试可变借用）。这种严格静态语义让 Rust 程序更安全，但也让 AI 生成的代码极难一次编译通过。
本文的核心动机就是：Rust 这类静态语义丰富的语言能提供强保证，但其严格性让 LLM 生成合法代码非常困难，正是编译器反馈最能发挥作用、又最难实现的场景。
约束解码（Constrained Decoding）
约束解码是另一条让 LLM 生成合法代码的路线：在自回归采样时，每生成一个 token 都用一个前缀检查器 $P : \Sigma^* \to \mathbb{B}$ 过滤候选 token，只保留 $P(c \circ t) = \text{true}$ 的 token（即当前部分程序还能扩展成合法程序）。它要求白盒访问模型的下一个 token 分布，并且要为每种约束（语法、类型、借用）重新实现一套语言语义。对于 Rust，编译器前端就有约 60 万行代码，完整重写几乎不可行。
约束解码是本文最主要的对比对象。理解它的两条硬伤——需要白盒访问、需要重写语义——才能看懂生成式编译为什么是更实用的折中方案。
生成后编译器反馈（Post-Generation Compiler Feedback）
目前最主流的做法：让模型生成完整文件后再用编译器检查，把诊断信息（错误位置、原因、建议）拼回 prompt，让模型重新生成或修改。优点是与黑盒 API 兼容、直接复用编译器、错误信息丰富；缺点是反馈延迟——错误往往在第几行就出现了，但要等整个文件生成完才能发现，期间后续代码可能基于错误假设「滚雪球」式积累更多错误。
这是生成式编译要改进的基线（论文里简称 PC）。理解它的延迟和错误雪球问题，才能理解为什么需要在生成中途就反馈。
Featherweight Rust（FR）
Pearce 提出的一个受 Rust 借用系统启发的精简演算，遵循 Featherweight Java 的哲学：用最小化的语法给出类型健全性证明，同时保留 Rust 的核心特性（copy/move 语义、可变/不可变借用、词法生命周期）。本文在 Lean 中完整机械化实现了 FR 的语法、类型规则、操作语义和类型/借用安全性证明，并修正了原始工作的若干处类型规则错误。
FR 是本文用来形式化定义和证明 sealor 性质的核心演算。先在 FR 上证明完备性和选择性可靠性，再迁移到真实 Rust，是论文的技术路线骨架。
研究动机
AI 生成的代码仍然容易出错，这对下游软件系统的正确性和安全性构成威胁。在 Rust 这类静态语义丰富的语言里问题尤其突出：所有权与借用规则虽然能在编译期提供内存安全保证，但严苛的编译期约束让合法代码比 C 这种宽松语言难生成得多。现有两条路线各有硬伤。「生成后编译器反馈」（PC）要等到整个文件生成完才跑编译器，错误往往在第几行就发生了（如论文 Fig. 1 的例子中，借用冲突在第 4 行就出现），却要等到第 8 行文件结束才反馈；这期间后续 token 都基于错误假设生成，一个核心错误会滚雪球式地衍生出几十甚至上百条诊断信息（论文实测 PC 平均每条错误消息含 13.8 条诊断，CRUST-Bench 上有时达数百条），让模型难以定位根因。「约束解码」则要在采样时逐 token 过滤，对真实 Rust 来说要重写约 60 万行编译器前端代码，几乎不可行；它还需要白盒访问模型，无法用于闭权重的 frontier 模型；并且只是「静默过滤」token，不告诉模型为什么被拒、也无法修改已生成的前缀。
本文的目标是本文要在两者之间开辟第三条路：让编译器风格的诊断反馈在生成过程中（而非生成完成后）就可获得，且同时满足三个硬性目标——(1) 兼容黑盒 LLM API，不需要白盒访问模型的 token 分布；(2) 直接复用现有编译器基础设施（rustc），不做大规模语义重写；(3) 提供编译器风格的文字诊断而非静默拒绝，让模型能理解错误并主动修改前缀。可量化的目标是：在仓库级 Rust 编码任务上，相对 PC 进一步降低编译错误率、提升功能正确性，并把错误报告时机从「文件末尾」提前到「错误源附近」。
与已有工作不同的是，已有的工作要么从「采样策略」角度改进约束解码（如局部/全局约束采样），要么在生成后用编译器迭代修复。本文抓住了被两边都忽视的一个点：编译器只能检查完整程序，而 LLM 生成的是部分程序——只要有一个轻量变换能把部分程序「补全」成编译器能消化的完整程序，就能让现成编译器直接当「前缀检查器」用，且仍带丰富诊断。这个视角的关键洞见是：完备性和可靠性这对性质，在生成式编译里优先级和约束解码正好相反——不完备（误拒可补全的前缀）比不可靠（漏掉死胡同）更有害，因为误拒会浪费已生成的好前缀；而漏掉的死胡同还能靠后续检查兜底。这个优先级翻转，让一个轻量、语法主导的 sealor 就足够实用。
核心方法
打个比方：PC 像「写完整篇作文再批改」，约束解码像「每个字都让老师盯着改」；生成式编译则是「写半句就交给老师，老师把半句补成一个完整句子再判对错」。技术路线分三层。最底层是抽象定义：把编译器建模为 $C : \Sigma^* \to \mathbb{B} \times \Sigma^*$，生成式编译器 $G : \Sigma^* \to \Sigma^*$ 接口相同但做前缀检查；中间用 sealor $S : \Sigma^* \to \Sigma^*$ 把部分程序 $c$ 变成完整程序 $S(c)$，诱导出的生成式编译器定义为 $G_{C,S}(c) := C(S(c))$。中间层是性质：证明 sealor 的完备性/可靠性会「提升」到生成式编译器（定理 3.2）。最上层是两个具体实例：FR 上的语法主导 sealor $S_{FR}$（Lean 机械证明全局完备、语句边界处可靠），以及真实 Rust 上的 sealor $S_{RS}$（约 5k 行 Rust，委托 rustc 做语义检查）。
全文最核心的洞见是：要让编译器检查部分程序，并不需要重新实现类型系统，只需要一个轻量、几乎只跟语法走的 sealor。具体做法是保留已生成的代码原封不动，仅在「未完成边界」插入良类型占位符——FR 用单位值 $\varepsilon$，Rust 用两个互补占位符：holediv()（即 panic!()，类型为永不类型 !，可强转为任意类型且发散，让控制流路径在 borrow checker 眼里「不存在」从而保完备性）和 holeval()（泛型函数 `const fn holeval()() -> T { panic!() }`，类型为推断出的 T，保持 borrow checker 开启）。关键创新点是把完备性/可靠性这对矛盾的目标重新排优先级：以全局完备为主、可靠性只在语句边界 $X_{stmt}$ 这类便宜可得处追求。这和约束解码（必须全局可靠、token 级完备）恰好镜像对称。这种优先级翻转 + 占位符设计，使得 sealor 不碰类型系统就能复用 rustc，5k 行代码 vs. 编译器前端 60 万行，差距两个数量级。
方法步骤详情
完整流程分四步。步骤1（部分语法解析）：LLM 流式吐 token 时，用 rust-analyzer 解析当前前缀 $c$ 为部分 AST，识别出哪一段是已完成结构、哪一段是「正在生成的边界」（如未闭合的块、部分变量名、部分字段访问 `e.b_f`）。步骤2（封闭）：sealor 按规则递归封闭边界——块规则 `{s; S^s_{RS}(b_e); holediv()}`、条件分支缺失侧用 holediv()、函数调用先查 rustc 拿到元数 $n$ 再用 holeval() 补齐缺失参数、字段访问 `e.b_f` 只取 `&e` 避免移动语义、let/赋值只递归右子树而丢弃左侧绑定。步骤3（编译 + 抑制）：把封闭后的程序 $S_{RS}(c)$ 喂给 rustc，但用「预期错误」机制抑制「未来依赖错误」（如「缺失 trait 方法」「需要类型标注」「未定义名」）——这些错误只在未来补全代码后会消失，必须抑制才能保完备性；抑制范围严格限定（如「缺失 trait 方法」只在封闭部分 trait impl 内抑制）。EOS 到达后清空所有抑制。步骤4（诊断回投）：维护封闭程序到原部分程序的字符位置映射，把 rustc 报告的错误高亮重新渲染到原前缀 $c$ 上；纯由占位符引入的错误直接丢弃。然后两个并发模块（生成器 + 生成式编译器）通过纯文本通信，采用「最新优先」策略：编译慢时不阻塞生成，拒绝时把 $c \circ err$ 拼回 prompt 重启生成，最多 $k$ 次重启后再退回 PC 的 $n-k$ 轮。
技术新颖性
和已有技术的本质区别有三点。与约束解码相比：(1) 它不碰采样过程，只观察流式输出，因此天然兼容黑盒 frontier 模型；(2) 它返回编译器风格的文字诊断而非静默过滤，模型能理解为何被拒并主动改前缀（约束解码无法修改已生成 token）；(3) 它复用 rustc 而非重写语义，实现量是约束解码的零头。与 PC 相比：它在部分程序上就反馈，错误离源头近（论文实测中位数只比理论下界晚 3 行）、诊断少（平均 5.5 条 vs PC 的 13.8 条）、避免 66.7% 的不可恢复代码被白白生成。与 typed holes 相比：typed holes 需要扩展语言本身、把洞变成类型系统的一等公民；本文的占位符借用语言既有元素（panic!()、泛型函数），不修改类型系统。形式化层面，本文是首个把「部分程序封闭 → 编译器检查」这件事用 Lean 完整机械证明其完备性/可靠性提升关系的工作，并顺手修正了原始 FR 的若干类型规则。
实验结果
论文在两个仓库级 Rust 任务上评测：Translation（CRUST-Bench 子集，20 个 C 转 Rust 实例）和 UpdatedAPI（用最近变更的库 API 实现命令行工具），跨 7 个模型（Opus 4.8、GPT 5.3 Codex、Gemini 3.5 Flash、Kimi K2.7、GLM 5.2、Qwen 3.5 397B/9B）。Table 1 的核心数字：LLM 平均编译错误率 65.9%，PC 降到 20.7%，GC 再降到 13.1%；14 个模型-任务配置中 GC 在 13 个取得最佳编译错误率（一个并列），其中 9 个相对 PC 统计显著（$\alpha = 5\%$ 配对检验）。最亮眼：Opus 4.8 在 UpdatedAPI 上把错误率从 PC 的 6.7% 降到 0.0%，GPT 5.3 从 13.3% 降到 3.3%。功能正确性上 GC 在 11/14 配置最佳，最大提升是 GLM 5.2 在 UpdatedAPI 上从 PC 的 53.3% 升到 71.7%，Kimi K2.7 在 Translation 上从 39.9% 升到 53.9%。运行时间反直觉地下降：平均开销从 PC 的 +283%（233 秒）降到 GC 的 +170%（135 秒），因为 GC 在第一个不可恢复错误就中断生成，不再反复补完不可能编译的文件；Qwen 9B 在 Translation 上从 879 秒降到 357 秒/样本。Fig. 12 三个子图分析机制：(a) 65% 的 GC 错误报告只含 ≤2 条诊断（平均 5.5 条），PC 只有 40% 这么精简（平均 13.8 条，Translation 上偶达数百）；(b) GC 报错中位数只比理论下界 Oracle 晚 3 行，1/4 情况完全对齐，而函数级变体 GCfn 晚 14 行、PC 晚 89 行；(c) GC 平均在文件 33.3% 位置就检出错误，几乎贴合理论上限 32.7%，即避免了 66.7% 的不可恢复代码被生成。错误种类上类型不匹配（E0308）占 1/3 以上，还能提前检出借用冲突（E0502）和移出借用值（E0507）。85.3% 任务在前 $k=10$ 次重启内完成、不再退回 PC，55.4% 任务在早期反馈阶段就被正确解决。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| Translation（C 转 Rust，CRUST-Bench 子集）— 编译错误率 | 编译错误率（↓） | GC 平均约 12.6%（Opus 4.8: 2.6%, GPT 5.3: 1.8%, Kimi K2.7: 11.0%） | PC 平均约 18.6%（Opus 4.8: 7.5%, GPT 5.3: 3.9%, Kimi K2.7: 38.6%） | Kimi K2.7 从 38.6% 降至 11.0%，绝对降 27.6 个百分点 |
| UpdatedAPI（适配新库 API）— 编译错误率 | 编译错误率（↓） | GC 平均约 12.1%（Opus 4.8: 0.0%, GPT 5.3: 3.3%, GLM 5.2: 16.7%） | PC 平均约 22.8%（Opus 4.8: 6.7%, GPT 5.3: 13.3%, GLM 5.2: 45.0%） | Opus 4.8 降至 0.0%，GLM 5.2 从 45.0% 降至 16.7% |
| Translation — 功能正确性 | 通过单元测试比例（↑） | Kimi K2.7: 53.9%, Qwen 9B: 33.3% | PC Kimi K2.7: 39.9%, PC Qwen 9B: 30.3% | Kimi K2.7 绝对提升 14.0 个百分点 |
| UpdatedAPI — 功能正确性 | 通过单元测试比例（↑） | GLM 5.2: 71.7%, Kimi K2.7: 83.3%, Opus 4.8: 86.7% | PC GLM 5.2: 53.3%, PC Kimi K2.7: 76.7%, PC Opus 4.8: 85.0% | GLM 5.2 绝对提升 18.4 个百分点 |
| 端到端运行时间 | 相对 LLM 的平均额外开销（↓） | GC +170%（135 秒） | PC +283%（233 秒） | Qwen 9B 在 Translation 上从 879s 降到 357s/样本 |
| 错误报告位置（961 个错误文件回放） | 首报错中位数延迟（相对 Oracle 行数，↓） | GC 中位数 3 行 | GCfn 14 行，PC 89 行 | 比 PC 早约 86 行 |
局限与改进
作者明确承认三点。第一，形式化只覆盖 ok 这个布尔判定，不建模诊断 err 本身——没有形式化保证「err 描述的是原部分程序的真实缺陷而非封闭引入的伪影」，只靠经验观察 + 抑制机制兜底（§8）。第二，sealor 规则全部手写：FR 和 Rust 的每条规则都是人工推导、人工论证完备/可靠，扩展到新语言或语言演进需要重做。第三，可靠性是「选择性」的——只在语句边界 $X_{stmt}$ 处成立，其他位置可能漏掉死胡同（虽能被后续或最终检查兜底）。我自己的观察：(1) 评测任务都聚焦 Rust 这一种语言且都是「填骨架」式任务，未验证自由生成、跨文件重构、宏 heavy 代码等场景；(2) CRUST-Bench 子集仅 20 个实例，UpdatedAPI 规模也有限，统计显著性靠配对检验但样本量本身不大；(3) GC 相对 PC 的提升在强模型上很温和（如 Opus 在 Translation 功能正确性 61.0%→62.3%），主要红利集中在弱模型和 UpdatedAPI 这类「API 漂移」场景；(4) 错误检测延迟分布是重尾（均值 27.7 行 vs 中位数 3 行），90.5% 的尾部延迟来自未来依赖项（未解析名/导入 63.8%、缺失方法 26.7%），这部分本质上仍要等文件接近完成。
独立分析的弱点
弱点一：sealor 的可扩展性瓶颈。每加一个 Rust 特性就要手写一条封闭规则并人工论证，作者自己也把这列为开放问题。改进方向是「自动化 sealor 构造」——从语言规范或参考实现（如 rustc 行为）合成规则，在「完备 + 尽量可靠」约束下做搜索。弱点二：在「未来依赖错误」（前向引用、缺失方法）面前延迟退化。这些错误当前要等到文件接近完成才报，因为 sealor 谨慎容忍未定义项。改进方向是引入轻量的「作用域最终化」机制——当模型明确表示某个块/impl 结束时，触发一次更严格的检查，把那些可解除的未来依赖提前钉死。弱点三：诊断质量未优化。论文直接复用 rustc 的错误格式，假设模型训练语料里见过最多这种格式；但面向 agent 的诊断格式（带修复建议、带上下文）是另一个开放问题（§8）。改进方向是结合 He et al. 面向 AI 的错误消息研究，做诊断的二次改写。弱点四：当前调用策略是硬编码的「编译完就检查、被拒就重启」。改进方向是把「何时调用生成式编译」交给 coding agent 自主决策（像调工具一样），让 agent 学会在大改写后多查、小修补后少查。弱点五：评测只覆盖 Rust 一种语言、且是骨架填充任务。改进方向是把方法论迁移到其他静态语义丰富的语言（Haskell、OCaml、TypeScript strict mode、Verilog），并在自由生成 agent 场景下验证。
未来方向
作者明确提出五个方向：(1) 形式化诊断 err 的「真实性」——证明 err 描述的是原部分程序的缺陷而非封闭伪影，可借鉴类型错误定位的形式化工作；(2) 解耦调用策略——研究调用频率、把调用决策交给 agent、探索白盒访问能否带来额外收益；(3) 用诊断 err 作训练信号，在训练阶段而非仅推理阶段利用编译器反馈；(4) 自动化 sealor 构造，让方法随语言演化和新语言设计一起扩展；(5) 把生成式编译推广到任何「可被自然语言引导、产出中间代码」的生成方法（不限于 LLM）。基于本文成果可延伸的方向：把 sealor 思路和 constrained decoding 结合——用 sealor 做「粗筛」避免大规模重写、用 token 级约束做「精筛」；把生成式编译嵌入 IDE 实时编程（live programming）场景；研究 sealor 在程序合成（synthesis from spec）里作为 type-guided search 的轻量替代；把诊断回投机制扩展成「部分程序的反事实补全可视化」帮助人类开发者理解 AI 生成过程。
复现评估
复现性非常好。作者公开了完整的机械化证明（Lean）、代码实现、benchmark 和评测结果，仓库地址 https://github.com/eth-sri/generative-compilation。代码量明确：sealor 约 5k 行 Rust（用 rust-analyzer 解析部分 AST，对 rust-analyzer 做了少量补丁以更好处理部分 AST），LLM 接入层约 3k 行 Python，外加约 8k 行 Python 用于 API wrapper、数据集和评测编排，共 329 个 Rust + Python 测试覆盖 sealor 和推理行为。模型侧覆盖 7 个模型（3 个 frontier 黑盒 + 4 个开源权重），用固定控制流的 agent harness（类似 Agentless）以保证可比性。关键超参数明确：Translation 上 $n=20$（PC 反馈轮数），UpdatedAPI 上 $n=15$，两者 $k=10$（GC 重启数），temperature 0.6，并对预算 $n,k$ 做了消融。算力需求论文未单列但实测端到端每样本数百秒级，对 frontier API 调用成本是不小的开销；自建 rustc 调用 + rust-analyzer 部署需要一定工程投入。主要复现难点不在算力而在工程：要稳定地复现「部分 AST 解析 + 位置映射 + 错误抑制」这套机制，并对接各家 LLM 的流式 API。整体评估：原理可复现、代码开源、benchmark 可得，属于这一批论文里复现友好的水平。
论文图表
展示一个 LLM 生成的 Rust 函数 fmt_msg：它先在第 2 行用 `let tag = &msg[..HEADER_SIZE]` 不可变借用 msg，第 3 行又调用 `msg.drain(...)` 可变借用 msg，而 tag 在第 4 行还要用，于是不可变借用与可变借用重叠，违反借用规则无法编译。这是贯穿全文的「跑通例子」。
这是论文的动机锚点，让读者直观看到「LLM 生成的 Rust 代码常常一次编译不过」这个具体问题，后续 Fig. 2/3/4/5 都围绕它展开。
展示 rustc 对 Fig. 1 程序返回的错误信息 E0502：详细指出第 2 行发生不可变借用、第 3 行发生可变借用、第 4 行不可变借用仍在使用，并给出代码高亮。这种丰富的诊断正是论文想保留并提前利用的。
这张图说明「编译器反馈质量很高但来得太晚」——错误信息极有价值，这正是生成式编译想复用的资产，也是 PC 模式下「等文件结束才反馈」的核心痛点。