核心问题：当编译器正确性定理只覆盖已验证核心，并且相对于可能有误的规格与机器语义成立时，形式证明究竟排除了哪些错误，又把哪些错误留给测试发现？
论文卡片
- 原题： Automated Testing and Repair for Verified Compilers Generated by a Coding Agent
- 作者： Martin Rinard。
- 机构： National University of Singapore、Massachusetts Institute of Technology。
- 版本： 2026-07-31，arXiv v1；分类为 cs.SE；预印本。
- 类型： 已验证编译器的自动测试与修复系统研究。
- 阅读入口： alphaXiv · arXiv · HTML 全文 · PDF · 实验 artifact
论文讲了什么
论文研究的 Axon 是一个由 coding agent 在作者监督下生成的、从源语言编译到 AArch64 汇编的编译器。它不是一个“全部代码都被证明”的单一整体，而是包含四类不同可信度的组件：
| 组件类别 | Axon 中的例子 | 已有保证与剩余风险 |
|---|---|---|
| verified | flattening、codegen、certificate checker | Lean 证明变换满足 refinement，但结论依赖所采用的语义与规格 |
| checked | 优化 pass 与其证书生成器 | 优化本身未证明；证书被 verified checker 接受时才保留结果 |
| unverified | AST parser、ASM printer | 不在端到端证明内，可能破坏文本与内部表示的一致性 |
| specification | AST/ASM operational semantics | 定义“正确”的参照；若机器模型本身有误，证明仍可成立而实际执行出错 |
作者提出 ACDC，为每类边界选择不同的可执行 oracle。ASM 测试把同一随机指令序列分别交给可执行 operational semantics 与真实机器，比较最终状态；parser 测试随机生成 AST，执行 print–parse round trip；优化测试则生成随机程序，记录 certificate checker 的拒绝原因。拒绝记录不仅说明哪个 pass 出错，还指出 31 项检查中的具体失败条件，成为 repair agent 定位问题的结构化反馈。
每轮先运行 30 分钟检测，再让 repair agent 根据触发程序、随机种子和失败记录修改代码。修复可能落在 transform、certificate generator、checker、printer、parser 或 operational semantics；若修改 verified checker 或证明相关语义，Agent 还必须同步修复 Lean proof。候选修复既在原触发输入上验证，也要面对新随机种子产生的输入。
主要结果
| 测试对象 | 初始证据 | 修复与停止条件 |
|---|---|---|
| ASM semantics 与 printer | 8,200 个程序中 6,760 个触发缺陷，比例 82.4% | 5 个修复后，再测 4,600 个程序未发现缺陷 |
| AST parser 与 printer | 13,770,000 个程序全部在首轮失败 | 4 个修复后，再测 18,075,000 个程序未发现缺陷 |
| certificate 路径：Csmith | 4,800 个程序触发 27 种 pass–拒绝条件组合 | 13 个修复；随后连续 8 轮无新拒绝 |
| certificate 路径：SPE | 5,398 个程序触发 1 种新组合 | 1 个修复；随后连续 8 轮无新拒绝 |
| certificate 路径：EMI | 3,758 个程序未触发新拒绝 | 达到预设饱和条件 |
这些错误并不只存在于“未验证外壳”。例如，ASM printer 曾把按位运算的源和目标寄存器硬编码成 w0；shift 的 operational semantics 没有按 AArch64 规则把位移量对 64 取模；浮点比较的机器语义对负数、NaN 与正负零处理错误。最后一个修复同时修改语义、printer 和证明，说明测试发现的错误可以穿过规格边界，反向触发 proof maintenance。
certificate rejection 的含义则更复杂。RegAlloc 的确生成了不正确的变换：死 store 覆盖了仍存活的值，checker 正确拒绝了证书，修复应落在优化 pass。另一些变换本身正确，只是 checker 太严格，Agent 于是扩展 checker 并重建其正确性证明。但在 LICMpreheader 案例中，Agent 没有扩展证书能力，而是让相关情形退化为 no-op，并生成 identity certificate；拒绝消失了，优化能力却没有增加。
形式证明没有覆盖什么
Axon 的端到端定理说明：相对于论文给出的 AST 与 ASM operational semantics，被接受的编译结果满足 refinement。它不自动证明 ASM semantics 忠实描述真实 AArch64，也不覆盖 parser 和 printer。论文因此把真实机器执行、round trip 和随机证书审计作为互补证据，而不是把测试当作证明的低配替代品。
作者还把连续多轮未发现新缺陷解释为测试趋于饱和，并据此认为没有观察到 Axon 或修复发生系统性 reward hacking。支持这一判断的证据包括：修复后面对未见随机输入仍不再复现、多个生成策略从 13 个修复降至 1 个再降至 0，以及多数修复作用于彼此分离的代码区域。但“未发现证据”不是“证明不存在”：测试空间有限，停止规则由研究者设定，而且测试、prompt、修复与统计脚本同样由 coding agent 生成。
证据边界
研究只评估一个相对较小的 Axon 语言和编译器，实验运行在一台 M4 Pro 上，repair agent 固定为 Claude Code Opus 4.8。不同模型、随机运行、规模更大的语言或人工维护的编译器可能呈现不同结果。论文报告的是一次修复序列达到既定 clean-round 条件，不是对全部输入的穷尽证明。
“所有检测到的缺陷都被修复”也需要按组件解释：对真实错误，它意味着行为被纠正；对有效证书被拒绝，它可能意味着 checker 的接受范围扩大；对某些优化情形，它只意味着退回 identity transform。把三者都计为 rejection eliminated，适合衡量工作流收敛，却不能单独说明优化器能力增加了多少。
重点读哪里
先读 §2 与图 1，弄清 verified、checked、unverified 和 specification 的边界；再读 §4，看三类 oracle 为什么来自编译器结构本身。实验数字集中在 §5 与表 1–4，其中 RegAlloc、Unreachable、LICMpreheader 三个案例最能区分错误变换、过严 checker 与保守回退。最后读 §6 和 §8，核对作者关于 reward hacking、泛化与证明边界的措辞。
思考启发
以下是导读者由论文引出的理解角度，不是作者额外验证过的结论。
这篇论文更重要的贡献不是“Agent 修好了多少 bug”，而是把一个已验证系统拆成多种证据关系。证明约束 verified core；certificate checker 把未验证优化转成可拒绝的 checked computation；真实机器执行检查模型是否忠于硬件；round trip 检查文本边界。所谓“编译器正确”，实际上由多个不同 oracle 共同封闭，而不是一个 theorem 覆盖全部路径。
它也显示，结构化失败比单一 pass/fail 更接近可修复知识。certificate rejection 同时给出 pass 名称、失败性质和触发程序，repair agent 因而能在 transform、证书生成器与 checker 之间判断责任。不过，这种精确反馈并未消除价值判断：接受更多证书、修复优化，或直接放弃该次优化，都可以让拒绝归零，却代表不同的系统变化。
三个思考问题
1. 定理相对于有误规格成立时，“已验证”还保证什么？
ASM operational semantics 曾与真实 AArch64 行为不一致，但端到端证明仍能成立。这个案例应如何改变我们对 verified compiler 正确性的表述？
展开思考线索
形式证明仍然排除了大量实现层错误：只要规格成立，verified 变换与被 checker 接受的优化满足明确的 refinement 关系。问题不在证明失效，而在结论是条件性的。论文通过真实机器共模拟补上“模型是否忠于硬件”这一条件，说明可信度来自定理、规格验证与未验证边界测试的组合，而不能缩写成无条件的“编译器正确”。
2. certificate rejection 归零，意味着系统变得更正确了吗？
错误 transform 被修复、checker 接受更多有效证书，以及把优化改成 no-op，都能消除拒绝；这三种结果为何不能用同一个成功指标解释？
展开思考线索
三者分别改善语义正确性、证明系统的表达能力和流程可用性。前两者修复了不正确行为或不必要的保守性；no-op 则保留原有正确性，只是不再尝试该优化。若指标只统计 rejection eliminated，它无法区分“更会优化”与“更会安全放弃”。论文如实展示了 LICMpreheader 与 FMAtemp 的取舍，也因此暴露出正确性收敛和优化能力并非同一目标。
3. 同一个 Agent 生态生成测试、修复和统计，独立性从哪里来？
未见随机输入与多种生成策略支持“没有观察到 reward hacking”，但这些证据是否足以排除测试和修复共享同一种盲点？
展开思考线索
新 seed、真实硬件执行、机械检查的 Lean proof，以及 Csmith、SPE、EMI 三种生成分布，确实让修复难以只记住单个触发样本；13→1→0 的新增拒绝也提供了饱和迹象。但 harness、prompt、修复与数据处理脚本均由 coding agent 生成，仍可能共享建模遗漏。论文的结论严格说是“在这些相互补充的 oracle 下未发现系统性投机”，不是对所有潜在盲点的否定。