LLM 反编译把未知补成可编译代码，行为漂移就藏在编译通过的沉默里

本文要拆掉一个直觉：编译器的绿灯只证明它自己相信这段代码合法，并不证明它和原二进制行为相同。LLM 进入反编译领域时，把传统工具故意留在 UI 上的 undefined 占位符悄悄填平，可编译率被推到 90% 的同时，行为匹配率反向掉到 62%；在 CVE 真实代码上，约一成的参考崩溃被静默"修没"。这一切的发生机制可以用一句话装上名字：测量变目标，就塌缩。 GitHub

下面这条主线贯穿五章：编译器的绿灯只证自洽 → 传统反编译器把未知显式留在 UI 上 → LLM 把这种显式未知平滑成可编译的合理猜测 → 把可编译率当目标，Goodhart 压力把"可诊断的不完整"升级成"沉默的行为漂移" → 工程答案是分层差分验证，原则是奖励保留未知。每章末尾向下一章交出一个被磨利的问题。

一、能跑起来就算移植成功吗？

这一章要把一件听起来反直觉的事讲透：把一段未知代码补成能编译的合法 C 代码，反而会让"绿灯"变得更不可信。它讲的不是 LLM 不聪明，也不是 LLM 不努力，而是"未知被填平"这一动作本身就把"信不过"的证据一起埋掉了。

要理解这件事，三件证据要先摆在一起：编译器只证自洽、传统反编译器把"信不过"显式留在 UI 上、LLM 把这种显式未知平滑成可编译的合理猜测。这三件事本来互不相关，但合起来就拼出了"为什么把未知补成可编译代码会让绿灯失真"这道命题。下面先把这三要素的最小版本各给一段，再走到具体证据。

先说第一件。一段 C 源码喂给编译器，编译器只回答一件事：这段代码在它的内部模型里是不是合法。这叫"自洽"，不是"等价"。把两个完全不同的程序扔给同一个编译器，编译器可能都为它们亮绿灯——绿灯证的是它自己相信这两段代码都合法，不证这两段程序在所有输入下行为相同。绿灯的沉默不是证据，沉默是因为这道题本来就不是编译器要回答的题。

第二件是说反编译器故意把这种"信不过"摆到台面上。在 Ghidra 这种主流反编译工具里，undefined、undefined4、undefined8 不是缺陷标记，而是它主动放出的"我不知道"信号。维护者在社区 Issue 里说得直接：undefined 类型被设计成允许变量在后续分析 pass 中"漂浮"（float）到更合适的类型——任何具体类型一旦被锁定，即便后续证明它错了，反编译器也不会再修正它。undefined 永远是浮动的，是分析员可以随时改写回退的占位符Issue #2225。类型恢复阶段的代码注释也自承：在某些情况下反馈环路无法收敛，工程师主动放弃再传播一次，而不是强行收敛——这样 decompiling 才能终止，并把"放弃"以 typerecovery_exceeded flag 暴露在 UI 上funcdata.hh。

第三件才轮到 LLM。LLM 进入反编译不是来"更聪明地读汇编"，而是来填这道传统工具的痛点：Ghidra 的输出看着像 C、但通常编不动也跑不动。LLM4Decompile（Tan et al. 2024）直接把 DeepSeek-Coder 微调成反编译专用模型，目标函数是"让 LLM 输出的 SRC' 接近原始 SRC 的 next-token likelihood"LLM4Decompile。看下面这张图，输入是汇编，输出是 C 源，损失在 SRC 与 SRC' 之间计算： LLM4Decompile

图注：End2end 路径的自上而下流程：源码先编译成二进制，再反汇编成 ASM，最后由 LLM4Decompile-End 直接从 ASM 生成 C 源 SRC'。虚线回传的 Loss 在 SRC 与 SRC' 之间计算，是模型微调的目标函数。End2end 走的是 ASM → SRC' 的序列到序列映射。

LLM4Decompile 的成功数据非常亮：把 Ghidra 在 HumanEval-Decompile 上平均约 20% 的可执行率推到 45–52%（6.7B 模型），22B 版本推到 64%。但要注意，它的训练目标只是"让 SRC' 看起来像 SRC"——既没有验证 SRC' 是否在所有输入下与原二进制行为一致，也没有验证时序、寄存器副作用等深层契约。换句话说，它优化的就是 LLM4Decompile 自己写在损失函数里的那个代理指标。绿灯拿到一个全新的维度：之前是"代码看着像 C 编不动"，现在变成"代码编得动但语义可能悄悄漂了"。

把"看着像 C 编不动"改成"编得动、但可能悄悄漂"，这件事的后果可以被一篇 2026 年的系统化实验具体测出来：在 291 个 GitHub 真实函数上，LLM4Decompile 让 Ghidra 的可编译率从 75% 推到 90%，行为匹配率却从 74% 反向掉到 62%——这组 90% / 62% 的数字来自 Liu、Raff、Micinski（2026）的 Decompile-Diverge，他们对参考二进制做 AFL++ 差分执行、用 bounded observable post-state 做行为比对才得到这个分裂（McNemar 配对检验 p=0.002）。同一条崩塌曲线在 287 个 CVE 函数上还表现为"参考崩溃被悄悄修没"——8.7%，25 个原本会触发的崩溃不见了。这个 90%/62% 由谁、以何种参考二进制差分得出，下一步会先解释为何绿灯会误导。 DecLLM

把 LLM 请进场之后，工程界也意识到"只看可编译"这条目标太软，于是又给系统挂上几道行为 oracle。DecLLM（Wong et al. ISSTA 2025）正是这条思路的代表：它以可编译率为入口，但已经加入有限行为 oracle 形成闭环——给定 IDA Pro 伪代码，循环里每次让 LLM 重写、GCC 编译失败回灌、ASAN 跑测试用例报内存错误回灌、AFL++ fuzzing 报语义不一致回灌；任一 oracle 报错都触发下一轮修复，最长 15 轮DecLLM。

图注：DecLLM 的迭代修复闭环。LLM 生成伪代码 → GCC 编译 → 编译错误回灌给 LLM；ASAN 跑测试用例 → 内存错误 / 输出不一致回灌；AFL++ fuzzing → 语义不一致回灌。每条红色反馈箭头都把"可编译 / 可运行"的反馈信号压回 LLM。

这条闭环在 IDA Pro + GPT-3.5/GPT-4 上把 Code Contest 的可重编译率从单次问询的 32% 拉到 74% / 78.3%，整体上限约 70%。与一次性生成的 LLM4Decompile 不同，DecLLM 已经把"行为 oracle 报红"这条反馈接进了循环——这是它在 SOTA 路线里被反复拿来对比的关键改进，但它的 oracle 覆盖范围也仍然有限：编译错误 + ASAN 内存错 + AFL++ 在官方测试集上的语义不一致，缺少跨 oracle 覆盖范围的输入生成和 bounded observable post-state 比对。换句话说，DecLLM 是"以可编译率为入口、但已加入有限行为 oracle 的闭环"——它比纯 prompt 修复更接近行为等价，但它的闭环仍然没有能力捕捉"在它没覆盖的输入上悄悄改变语义"那一类漂移。DecLLM 自己在 §7 直接引用 Rice 定理承认"checking equivalence is inherently undecidable"——他们清楚知道这条目标不是行为等价，但只能拿到这条目标。下一章要追问：把可编译率当目标、把行为 oracle 当闭环里的反馈项之后，那些原本会暴露的失败，到底藏到了哪里。

二、把可编译率当目标后，错误被推去了哪里

把一个原本用于观察或区分的测量改造成优化目标，参与者会围绕它行动，测量本身就会失去判别力。Strathern 在 1997 年把这条机制写在关于英国大学审计制度的论文里：当考试表现成为预期，作为区分个体表现的指标就会变差。她的原句已经成为这条机制最广为人知的现代表述——"When a measure becomes a target, it ceases to be a good measure."Strathern 1997。术语由 Hoskin 1996 提出，源头是 Goodhart 关于货币控制的观察，但 Strathern 把这条机制从货币政策搬到教育评价、审计问责、工程评测，是 Goodhart 定律在跨域引用中成为通用框架的关键节点。

理解了这层机制再看 LLM 反编译的崩塌曲线，数字就变得清晰。Liu、Raff、Micinski 在 2026 年的 Decompile-Diverge 论文里做了一件关键的事：他们没有沿用"shipped tests 通过"作为判定标准，而是构建了一个独立的行为 oracle——对每个函数自动合成 driver，用 AFL++ 在参考二进制上 fuzzing 生成 corpus，把反编译候选重新编译后跑同一批输入，比对返回值、内存写、.data/.bss 范围内的 bounded observable post-stateDecompile-Diverge。看下面的 oracle 流水线：

图注：Decompile-Diverge 的 oracle 流水线。参考 C 函数先编译成二进制 → AFL++ 在该二进制上 fuzzing 生成 corpus → 反编译得到候选 → 重新编译候选成二进制 → 对同一批输入在两边重跑 → 比对 bounded observable post-state，输出 Matched / Diverged / Crash Absence 三种判定。关键：corpus 是从参考二进制 fuzzing 出来的，不是从 shipped tests 给的。

这条 oracle 给出的数字触目惊心：在四个公开语料库上（HumanEval-Decompile n=161、ExeBench valid_real n=1538、AnghaBench n=215、MBPP C n=597），12,133 个通过全部 shipped tests 的候选里，仍有 4.9% 在生成的 corpus 上行为分歧；Nova 在 HumanEval 上单系统最差达到 13% 的 Divergence-given-Pass。在 291 个 GitHub 真实函数上，LLM4Decompile 把 Ghidra 的可编译率从 75% 推到 90%——但行为匹配率从 74% 反向掉到 62%，匹配率掉了 12 个百分点。配对 McNemar 检验 p=0.002，可编译率排名把 LLM4Decompile 排在 Ghidra 前面，行为匹配率排名把 Ghidra 排在 LLM4Decompile 前面。

更严重的是 CVE 函数：LLM4Decompile 让 25 个原本会触发的参考崩溃被悄悄"修没"——Crash Absence 25/287 = 8.7%，95% 置信区间 6.0%–12.5%。Ghidra 自身 0%、Hex-Rays 仅 1%（3/287）、DeGPT-Qwen 0%。在崩溃这种最容易发现的故障类型上，激进重写让大约一成的崩溃悄悄消失——开发者失去的不是"一些误报"，而是"这个 bug 曾经存在"这条信息本身。

源级归因指向一类高风险的改写特征，但需注意，这一层分析识别的是相关模式，不能单独证明前面 Goodhart 因果链中的哪一环是驱动因素。在 40,345 个 candidate pair 上，refiner 类系统移除了 40%–98% 的前端词汇——把 *(_DWORD*)(a1+40) 翻译成 C 迫使模型"创造"一个原二进制里没有的字段、类型或 callee。引入字段 / 类型 / callee 的输出行为分歧率是不引入的 4.6 倍（Fisher 精确 p<10⁻⁶），这一关联提示"凭空造出原二进制里没有的符号"是与行为漂移显著共变的高风险改写动作；12% 被标记的 token 是纯粹编造，其余大部分是把标准库调用替换为项目宏或包装器。SK2Decompile 最激进：引入 843 个字段、773 个类型、170 个 callee、481 个编译失败，但在真实代码上可编译率却只有 Hex-Rays 的一半。"凭空引入"和"漂移加剧"在同一批系统上同时出现，并不等于"前者就是后者的因"——这是相关，不是因果；但它足以把这类改写动作标记为需要单独控制的高风险变量，而不是默认安全的填充。

这条"优化掉不确定"的模式在反编译之外的代码生成领域同样存在。Dasu、Kundu、Tan 2026 年的代码幻觉分类研究在 12 个开源模型 × 270 个对抗性 prompt × 4332 个响应上系统测量了"模型在面对不可满足任务时倾向于做什么"Code Hallucination Taxonomy。结果是：综合幻觉率 0.60、拒绝率仅 0.27——面对"不存在的 npm 包"这种最容易识破的请求，模型幻觉率高达 0.98；面对"分布式系统不可能三角"这种需要推理才能识别的请求，幻觉率反而降到 0.46–0.73。模型拒绝的依据是请求"看起来可不可能"，不是请求"真的可不可能"。看下面这张按子类别排序的幻觉率分布：

图注：幻觉率按 24 个子类别排序的横向条形图。右侧高幻觉率（接近 0.98）是红色——不存在的 npm 包、虚构的系统集成、虚构的 Rust crate、伪造的编译开关，这些"看起来像真但其实不存在"的请求；中间（0.46–0.73）是橙色——分布式系统不可能三角、矛盾约束、复杂度近似；左侧低幻觉率（0.08–0.30）是蓝色——改字的老题、打字近似的名字、跨生态安装这种有真名的请求。拒绝率跟随表面可信度走，不跟随真实不可能性走。

更进一步的跨域证据是：同一组模型在 91 个可解对照 prompt 上没有一例 over-refusal，也就是说"模型不会因为不敢拒绝而拒绝能答对的"——它拒绝得不对、编造得自信。面对一个"不可能"的任务，模型的默认动作是自信地编造，不是诚实地标注未知。

把"可编译率 / 通过率"作为评测指标的塌缩在 LLM 评测文化里是系统性的。Bean 等 29 位研究者 2025 年对 445 个 LLM benchmark 的系统审查发现：81.3% 的 benchmark 至少部分使用 exact matching（40.7% 独家使用），只有 16.0% 使用统计检验或不确定性估计；53.4% 的 benchmark 没有给出"分数 → 真实能力"的论证链条Measuring what Matters。可编译率塌缩与 exact matching 塌缩是同一类结构：单一可机器判定的二元信号被默认当作"能力"或"等价性"的代理。 Measuring what Matters

这些数字拼起来说的是同一件事：把"看起来对"当目标去优化，系统不会真的变好；它会把"可诊断的不完整"升级成"沉默的行为漂移"，并在崩溃这种最容易发现的故障上把它悄悄修没。下一章要用两组独立证据（系统化实验 + 真人工程）来追查：漂移长什么样。

三、漂移长什么样：系统实验与 1993 真人在同一机制上相遇

前面已经看到 Decompile-Diverge 在 4.9% 的整体行为分歧率里给出了统计证据。但统计数字远不如一个具体例子来得直观。Liu、Raff、Micinski 给出了一个 worked example：ExeBench 函数 decode6 把线性 index 映射成 6 列 band，最后一列更窄。它附带的 10 个 shipped IO pair 都在一个有限区间内，在这个区间里"最后一列较窄"恰好不会被触发，因此所有 shipped tests 通过。SK2Decompile 把固定步长 6 与可变 final-band 宽度 D 混用，结果在 (100, 16, 8) 输入上写出 (8, -2) 而参考输出是 (12, 6)——只在测试范围外才暴露。LLM4Decompile 把商检查换成 n ≥ maxcol·height·6，这个等价只在有符号约束与不溢出条件下成立，在 (0, 10¹⁰, 10⁹) 上输出 (10¹⁰, −2×10¹⁸)，而参考是 (0, ~10⁹)。两个模型在 100 个生成输入上分别只匹配 70 / 66 个，原生 Ghidra / Hex-Rays 匹配 100/100。这正是"re-executability 不等价于行为等价"的完整标本。

与系统实验并列的是 1993 年的一份真实工程记录。Babylonian Twins 是 1993 年在巴格达用 68000 汇编写就的 Amiga 游戏，作者 Rabah Shihab 与他的团队在 2026 年用 LLM 辅助把它移植到 Godot 引擎Porting my 1993 Amiga game to Godot。移植过程中，作者不仅把所有代码通过 vasm 工具链重编一遍——做到与 shipped binaries 字节相同才算通过——还让 LLM 同时处理汇编阅读、地图数据反汇编、关卡结构还原、字节 diff 比对与发布材料生成。这套工作流的最大价值在于：作者本人就是 1993 年原始代码的程序员，移植中出现的每一个 bug 都能追到原代码的具体位置。

其中最有教育意义的 bug 出现在关卡 2：玩家站在一层走廊上，没有任何敌人接近，却挨了一下。打人的是 13 个 tile 之上、岩石之间、棕榈树旁的持矛卫兵。原 68000 汇编是：

sub.w   d1,d4           ; d4 = vertical distance to the kid
cmp.w   #4,d4
bpl     Sg.Far          ; 4 or more rows below? not my problem
cmp.w   #-2,d4
bmi     SG.far          ; too far above? also not my problem

bpl（branch if positive，下界）拒绝"4 行以下不在攻击范围"，bmi（branch if negative，上界）拒绝"−2 行以上不在攻击范围"。这两个守卫一起把卫兵的攻击范围框死在脚下三行。LLM 移植版本保留了 bpl、丢失了 bmi——也就是说，LLM 看到一段"if / cmp / range"里包含两段方向相反的守卫时，把上界那一半整段漏掉、只把下界那一半原样留下，让原代码故意设计的不对称守卫被无声地删成只剩一边的残缺形式。LLM 并不是把它补成了"对称且完整"，它把本来就不对称的守卫进一步截成了"只剩单边"的残缺。看下面的现场图：

图注：关卡 2 的 doorman bug 现场还原。上层岩石平台右侧有一个红框标注"GUARD stands here (155,90)"，一条黄色箭头从红框垂直向下穿过整片岩石地形，箭身中段写"BUG: shoe reached down this column"。下层岩石平台标签"where you got hurt (y103-108)"，一条蓝色线条水平指向卫兵原本不该打到的那一格。LLM 把 bpl 下界保留但丢了 bmi 上界，导致卫兵的"脚下三行"攻击范围被拉成"贯通整列"——穿过岩石、穿过他不存在的走廊。

同一类"对称化补全"的错误还有：trampoline 的更新顺序差一个 tick 触发双跳；门需要的四个 palm key 被读成一个奇怪的"单 key"导致教程出口永远打不开；立体声 → 单声道的声循环长度算错，每段音效中途被截断重启；1993 年要求的"远距离换位"proximity 检查被简单拿掉，闲置 twin 是被 stamp 到 map 里的 statue，两个 statue 叠在一起会互相吃 tile。

这些 bug 都符合同一个指纹：LLM 看到占位符 / 守卫 / 边界，就用"看起来合理"的方式去改写——有时是补出一个对称版本（如 trampoline / 门 / 声循环 / proximity），有时是把原本就不对称的守卫进一步截成只剩一边的残缺（如 doorman）。Decompile-Diverge 在 CVE 上看到的是"崩溃被悄悄修没"，Babylonian Twins 在游戏上看到的是"守门员突然穿过地板打你"。doorman 是"激进改写导致漂移"的一个具体实例，它把"下界保留 / 上界丢失"这条改写动作翻到了表面；而 Decompile-Diverge 报告的 OR 4.6 表明"凭空引入原二进制里没有的字段 / 类型 / callee"是与行为分歧显著共变的相关风险信号。把"统计相关"和"个案显形"摆在一起读，更稳妥的表述是：激进引入是分歧的相关风险信号；个案暴露了它在真实代码里能让守卫缺边的具体形态。两者都不足以单独证明 Goodhart 因果链中哪一环是驱动因素。下一章要问的是：既然不能靠"通过编译 + 通过测试"判定等价，那怎么验收？

四、差分验证的金字塔：从字节到时序手感

既然编译器的绿灯和 shipped tests 的绿灯都不能证明等价，工程上能拿到的是什么？答案是分层 oracle——从最严到最弱，每一层在它能成立的范围内给出独立证据。

最严的一层是字节级 byte-identical。Babylonian Twins 在 Step 2 重编 68000 汇编时，vasm 工具链对每条 ASM 重新汇编，与 shipped binaries 做 SHA 级 diff——字节相同才算通过。这一步在 14:49 首次通过，拦下了后续所有的"代码看起来对、跑起来画面差不多、但其实语义已经漂了"。字节 diff 把这种沉默错位翻到表面的一个经典例子：当 org 重绕（ASM-One 允许 location counter 倒退，vasm 不允许）的 ds.b 800 被当作"零字节写入"而不是"跳过 800 字节"时，重编字节从某点起整体偏移 944 字节。铜列表挪位、游戏照常启动、画面看起来正常，但整片天空的颜色没出来。看下面的字节差异掩码：

图注：关卡 2 字节级差异掩码。黑色 = 两个版本相同的像素，白色 = 不同像素。顶部与右上方有大面积连续白色（整片天空被刷白）、中下部成排小单元（动画水面差异）。可见轮廓：矩形平台、棕榈树、带尖顶的小型建筑、底部带栏杆的水平带、一排相同的低矮剪影。这是 byte-identical oracle 的输出——画面看起来对，但字节 diff 把整片天空与水面翻到了表面。

为什么字节相同在理论上就是最严的 oracle？因为字节相同等价于寄存器 + 内存 + frame 在出口完全相同——这正是 translation validation 理论里的 functional / observational refinement 的充分条件。Pnueli 1998 提出的 ≤ 关系定义为"若 c1 有定义良好语义且以可观察结果 R 终止，则 c2 也以 R 终止"；Tristan-Leroy 2008 在 Coq 里把这一形式化推到块级 symbolic execution 验证，块出口只需满足 m2 = m1 ∧ s2 ⊆ s1（寄存器 / 内存 / 帧映射相同 + 良定义约束集满足）——能区分 x := 1 与 x := x / 0 这种语义等价逃逸Tristan-Leroy POPL 2008。Leroy 2009 在 CompCert 后端把这一观察拆成 forward / backward simulation 两类可操作证明义务——forward simulation 加上目标语言确定性就能推出 specification preservationCompCert back-end。Gourdin 2023 把 block-level simulation 推广到 loop optimization，用 BTL 中间语言 + oracle 提供的 invariant 注释实现跨循环验证。 LOC

但字节匹配不是所有函数都能做到。fireemblem8j 项目在 16 个原本不字节匹配但机器检查等价的函数上展示了完整的分层 oracle 体系fireemblem8j equivalence_proving。三层 oracle：

第一层 bounded SMT 符号执行（Z3）：把 JP ROM 字节与重建代码在同一符号初始状态下分别执行，断言可观察状态相同（返回值 + callee-saved + sp + 数据内存写 + 有序 call / MMIO trace），用 ARMv4T THUMB 语义 + 有界循环展开。结果：12/16 PROVEN-BOUNDED(N)。

第二层 concrete differential testing（Unicorn THUMB）：当 SMT 不可达（非线性运算、间接 callback、栈混叠、超大函数）时，在模拟器里跑 JP 字节 vs 重建版本，比对返回值 + 内存写。结果：+2 = 14/16 machine-checked equivalent。

第三层 live game-state harness（mGBA 真机 capture）：当函数读 ~30 个 live 全局（如 sub_8057F80，1248 条指令 / 149 分支 / 58 calls）无法用合成输入驱动时，boot 真 ROM、按键快进到战斗中、single-step 抓现场、EWRAM+IWRAM dump、replay_diff.py 比对。结果：sub_8057F80 115/115 writes+ret 匹配。

三层组合给出 16/16 machine-checked equivalent，但严格分层（强→弱）：字节匹配 > unbounded-proven > bounded-proven > differential / dynamic。这里有几个关键边界必须点破：

• MMIO 必须建模为有序事件 trace，不是普通内存。GBA I/O（0x04000000–0x040003FF、palette / VRAM / OAM）的一次被后写覆盖的写入仍有硬件效应，读也可以有副作用或返回变化中的状态位。所以"最终寄存器 / RAM 相同但 MMIO trace 不同"的两个函数不是观察等价。
• 计时无法被 functional / observational equivalence 单独保证。fireemblem8j 文档直接承认：instruction count 不是 GBA timing model（wait-states、seq / non-seq、prefetch、DMA / IRQ、alignment 都不在其中）。时序敏感的例程（IRQ / HBlank / DMA / 串口 / 音频混频、任何依赖 raster / DMA 效果的）不能被 functional 或 observational 等价接受。字节匹配仍是唯一实际保证。

差分执行 / 差分模糊测试本身有一个更老的方法论根。McKeeman 1998 在 Digital Technical Journal 上把"差分测试"凝成一句："如果同一个测试被喂给多个可比较的程序（例如多个 C 编译器），有一个程序给出不同结果，那可能就暴露了一个 bug。"McKeeman 1998。差分测试的三种常见策略（多编译器作 oracle、旧 vs 新、跨优化等级）虽是后世（Chen 2018 / Chen CSUR 2019 / Sharma 2022）从 McKeeman 原文的三段叙事中总结出来的命名，但核心方法论从 1998 年定型。看下面的方法论概念图： McKeeman

图注：差分测试的操作骨架。Code Generator 生成测试 → 喂给 N 个 Compiler（Compiler #1 / #2 / ⋯ / #N）→ 每个 Compiler 旁挂 Execute → 所有 Execute 输出进入 Diff. Comparison 决策菱形 → 分叉为 All Okay（绿）/ Bug Found（粉）。差分测试的工程化范式从 1998 年的 McKeeman 起就是把"多个等价系统在同输入上比对、出现差异就是 bug"。

McKeeman 的方法论从 1998 年到 2026 年一脉相承：Decompile-Diverge 是它在 LLM 反编译场景的 2026 实例，把参考二进制与候选二进制放在同一批 AFL++ fuzzing corpus 上做差分 oracle，fireemblem8j 是它在 GBA 重构场景的 2026 实例（多 oracle 层级叠加）。同一根方法论在不同场景的不同形态——但它能告诉你的仍然是"在我有的 oracle 覆盖范围内没有证据"，不是"已证明等价"。

把这一章的所有证据拼起来，结论是：单一 oracle 永远不够。字节匹配在最严的位置，但它只在你真能拿到字节时才成立；可观察状态差分 + fuzzing 是大多数代码能拿到的第二档；时序手感要靠真机 capture 或 cycle-exact 模拟、且 fireemblem8j 已经证实对 IRQ / HBlank / DMA 等场景"字节匹配是唯一实际保证"。分层 oracle 不是工程妥协，是"可观察类从强到弱"的语义梯度——每放松一层 oracle，你都在接受某一类未检测到的行为漂移。下一章要把这套验证金字塔反过来用到 LLM 辅助反编译 / 重构工作流的取舍上：保留未知为什么是工程能力，而不是缺陷。

五、保留未知，是一种工程能力

激进重写的安全代价在 CVE 上看得最清楚。Decompile-Diverge 在 287 个 CVE 函数上记录到 LLM4Decompile 让 25 个原本会触发的参考崩溃被悄悄"修没"（8.7%，95% CI 6.0%–12.5%）Decompile-Diverge。崩溃消失的代价不是"少了一个误报"——开发者失去的是"这个 bug 曾经存在"这条信息。原始崩溃是 bug 报告的最强证据：当一段代码在原始二进制上崩溃，开发者知道问题在那里；当 LLM 把守卫的下界补了、上界丢了，崩溃不再复现，开发者既不知道 bug 存在，也不知道 bug 已被"修复"——这种沉默改义比一个明显失败的测试更危险，因为它把"曾经存在的 bug"从证据链里抹掉了。

行为漂移不是"AI 偶发 bug"，它有可识别的指纹：LLM 看到占位符就补一个看起来合理的对称版本、把 shipped tests 没覆盖的输入悄悄改变语义。这种漂移在 CVE 安全代码上表现为"崩溃被悄悄修没"，在 1993 游戏上表现为"守门员突然穿过地板打你"，同一种机制在两种语境里显形——LLM 引入字段 / 类型 / callee 后行为分歧率翻倍（OR 4.6，p<10⁻⁶），与 doorman bug 的"下界保留 / 上界丢失"在统计与个案两个尺度上指向同一件事。

代码生成领域的同向证据来自"保留未知 = 工程能力"的实证测量。Dasu 等 2026 年的代码幻觉分类研究在 12 个开源模型上系统测量了"模型在面对不可满足任务时倾向于做什么"，结果是：面对"不存在的 npm 包"（HR 0.98）模型几乎必然编造；面对"分布式系统不可能三角"（HR 0.46–0.73）模型有更多识别；面对"可解的对照题"模型几乎没有 over-refusalCode Hallucination Taxonomy。换句话说，模型的"合法行为"是分两段的：在可解任务上答对、在不可解任务上明确拒绝。"保留未知"不是模型能力不足，它是模型在面对"我无法保证语义等价"时应当采取的可被测量的合法动作。

那么，高保真迁移的工作流应当怎么组织？三条原则可以收束：

奖励保留未知。当 LLM 反编译器遇到它无法从二进制推断出的字段、类型、callee、守卫边界时，输出"unknown"或"无法判定"应当比输出"看起来合理的猜测"获得更高的工程评分。把"未发现分歧"严格表述为"在我有的 oracle 覆盖范围内没有证据"——明确写出 oracle 的覆盖范围（哪些函数 / 哪些输入 / 哪些时序假设），而不是默写"已证明等价"。这与传统反编译器把 undefined 留在 UI 上是同一原则的延续：宁可让分析员看到"我不知道"，也不要替他锁死一个未经证实的类型。

奖励最小改写。当 LLM 反编译器必须在"补一个看起来合理的字段"与"保留 undefined 让后续 pass 处理"之间选择时，应当偏向后者。SK2Decompile 引入 843 个字段 / 773 个类型 / 170 个 callee / 481 个编译失败，却在真实代码上可编译率只有 Hex-Rays 的一半——激进改写的代价已经在统计上坐实。最小的改写动作把"我必须为这一行假设负责"的范围缩到最小，让人类分析员在后续 pass 里有机会补完未知的部分。

让假设可追溯。每一处 LLM 引入的字段 / 类型 / callee / 守卫都应当能被追回到"这条假设的依据是什么"——是寄存器使用模式？是调用约定？是某种 libc 包装？如果依据消失或被推翻，这处假设应当能被反向回退为 undefined 而不是被默默保留。这与传统反编译器 descend2Undef() 把一个具体类型"沉"回 undefined 是同一机制——只是 LLM 流水线里需要把这一动作做成显式可触发、可审计的工作流步骤。

1993 年的 Babylonian Twins 在 2026 年的 Godot 移植中完整展示了"保留未知"作为正向工程能力的一面。同一拱门在 1993 Amiga 与 2026 Godot 中都被保留：

图注：左侧"BAGHDAD, 1993"：4:3 块状低分辨率石砖，两座拉马苏雕像立于深色拱门两侧，赤膊角色从拱门走出，台阶前有一排金属尖刺陷阱。右侧"2026"：宽屏高细节重绘版，雕像鬃毛 / 鳞片 / 胡须清晰可见，角色戴帽 / 红色腰带，新增石碑浮雕与青绿色陶罐。拱门位置、雕像两侧、尖刺陷阱完全对应——隐式规范被保留下来，渲染被重新构建。

上面这张图只能作为"视觉重建仍对齐原作布局"的示意来读：拱门位置、雕像两侧、尖刺陷阱这些几何要素在 1993 与 2026 两版之间看上去是对应的。图中没有任何游戏名 / 平台名 / 引擎名 / URL 出现——读者看到的是一张布局对照图，它本身不构成"行为被保留"的证明。能不能断言行为等价，要看前文列出的证据：铜列表天空那 24 个色字索引的字节差分要在重编后保持相同、隐藏层在开门时显形的状态差分要在两个版本上各跑一遍得到一致、sprite 双朝向要按"两行一朝向"逐项对照、门的空洞要靠 map 数据之外那 18 字节 object record 的逐字段比对来确认、50 Hz 与 60 Hz 双时钟要各自保留手调常数的字节差分。这种胜利的代价是逐项确认：铜列表天空的 24 个色字索引必须保留、隐藏层必须在开门时显形、sprite 双朝向必须按"两行一朝向"理解、门的空洞必须在 map 数据之外另用 18 字节 object record 补、50 Hz 与 60 Hz 双时钟必须各自保留手调常数。每一项都需要 LLM 主动问出来或主动保留未知——这不是模型能力的缺失，这是模型在面对"我无法保证语义等价"时该采取的可被测量的合法动作。

把这一切收束成一句：奖励保留未知，奖励最小改写，让每一个改写背后的假设可追溯，把"未发现分歧"严格表述为"在我有的 oracle 覆盖范围内没有证据"——而不是"已证明等价"。这是 LLM 辅助反编译 / 重构工作流中唯一一个把 Goodhart 压力反向利用的工程原则。

参考文献

1. When LLM Decompilers Recompile More and Preserve Less (Liu / Raff / Micinski 2026) — arXiv:2609.05370
2. LLM4Decompile: Decompiling Binary Code with Large Language Models (Tan et al. 2024) — arXiv:2403.05286
3. "Improving Ratings": Audit in the British University System (Strathern 1997) — PDF mirror
4. Refusing the Impossible: A Taxonomy and Benchmark for Code Hallucination in LLMs (Dasu / Kundu / Tan 2026) — arXiv:2609.03267
5. Ghidra undefined signaling mechanism — Ghidra funcdata.hh (commit 134f5394)
6. DecLLM: LLM-Augmented Recompilable Decompilation (Wong et al. ISSTA 2025) — DOI 10.1145/3728958
7. Porting my 1993 Amiga game to Godot, with an LLM reading the 68000 assembly (Shihab / bithunch 2026) — babyloniantwins.com
8. Differential Testing for Software (McKeeman 1998) + fireemblem8j equivalence_proving — McKeeman PDF · fireemblem8j docs
9. Measuring what Matters: Construct Validity in LLM Benchmarks (Bean et al. NeurIPS 2025) — arXiv:2511.04703
10. Translation Validation (Pnueli et al. 1998) + Formal Verification of Translation Validators (Tristan / Leroy POPL 2008) — POPL'08 PDF · CompCert back-end (ar5iv 0902.2137)