核心问题：简化程序的形式化证明，能给原始 GPU kernel 多强的正确性保证？
论文卡片
- 原题： RESOLVE: Language-Agnostic Validation of GPU Kernels Through Testing, Reduction, and Proof
- 作者： Ashkan Vedadi Gargary、Guido Martínez、Sebastian Burckhardt、Gabriel Ebner、Abhinav Jangda、Madan Musuvathi、Tyler Sorensen；UC Riverside、Math, Inc. 与 Microsoft Research。
- 日期与版本： 2026-10-05，arXiv v1，14 页；cs.PL / cs.DC / cs.LG；系统与实证研究预印本。
- 定位： AI 生成 GPU kernel 的验证，结合并发测试、Agent 改写和 F*/Pulse 证明。
- 入口： arXiv · HTML 全文（v1） · PDF（v1） · alphaXiv
简短导读：把难以证明的部分留给测试
高性能 kernel 使用的异步复制、流水线和同步机制，往往超出验证器的语义覆盖。RESOLVE 不要求先形式化全部硬件特性，而是把问题拆开。
首先，在二进制层扰动执行时序，寻找同一输入产生不同结果的情况。接着，让 Agent 将候选与参考程序分别改成低并发版本，用逐位一致的测试检查改写；再转成 Kuiper 程序，继续测试翻译前后的逐位一致性。最后，证明两份 Kuiper 程序满足共同的实数代数规格。
图 4 的纵向连接靠测试，底部共同规格靠证明。 证明不会自动把前面的测试升级为全输入保证。这里的“语言无关”主要来自二进制测试接口；后续证明仍受 Kuiper 所支持的语义限制。
证据与限制
实验使用 H100、CUDA 13.0，Agent 通过 Copilot CLI 使用 GPT-5.6。RKB 将 KernelBench Level 1 的 100 个问题与生成候选配对，候选都已通过原基准的容差测试。§6.2、表 1 的分母需要分开看：
| 检查范围 | 结果 | 能说明什么 |
|---|---|---|
| 初步测试可分类的 17 个候选 | 15 个逐位匹配参考；2 个是没有内存访问的空 kernel | 原容差测试会放过错误；15 个并非获得形式化证明 |
| 进入完整流程的 14 个候选 | 11 个完成；2 个缺少 Kuiper 特性；1 个使用不同数值近似 | 支持流程的可行性，不能写成“100 个全部验证” |
| 143 个可运行的同步故障变体 | 检出 92 个，其中 90 个无需时序扰动就会暴露 | 扰动的增量收益不能算作全部 92 个 |
未检出的变体包括不影响最终结果的竞争，以及工具无法扰动的 warp 内冲突。因此，确定性测试既不是完整的 race 检测，也不是无竞争证明。表 2 中，14 个完整流程案例的总耗时中位数约 143 分钟，说明证明环节仍然昂贵。
还有两道边界。其一，共同规格只描述代数计算，不提供浮点误差界；不同阶数的 Taylor 近似即使足够接近，也可能无法证明等价。其二，规格必须足够强：两个程序都满足一个宽松规格并不意味着它们等价。作者人工检查了规格，这部分尚未自动认证。以上为原文报告，未独立复现。
重点阅读章节
- §3 与 §6.2： 区分确定性、数据竞争和扰动测试的实际覆盖范围。
- §4–5、图 4： 沿每条连接辨认其依据是测试还是证明，以及证明中的数值语义。
- 表 1–2、§6.4： 分清完成完整流程的案例与只通过修复后确定性测试的案例，避免把不同强度的证据合并。
思想启发：证明对象也需要被验证
以下是导读者的理解。
这里最有意思的不是“测试加证明更可靠”这句笼统判断，而是证明对象本身由 Agent 构造。简化让证明成为可能，也增加了一个问题：这个更容易证明的对象，是否仍忠实代表原程序？精确到每一位的比较消除了单次比较的容差选择，却没有消除输入与调度覆盖的缺口。
混合方法的价值可以成立，而端到端形式化保证仍不成立。它扩大了能获得有效证据的程序范围；理解这一贡献，不需要把证据链中所有环节称为证明。
三个开放性思考问题
1. 逐位一致比容差一致更严格，为什么仍不能替代改写正确性的证明？
参考思路
比较标准的严格程度与覆盖范围是两件事。一次逐位匹配能精确回答这次执行是否一致，但未测试的分支、特殊输入或调度仍可能破坏关系。更强的单次判据不自动扩大被检查的输入集合。
2. 一个含竞争但始终输出相同结果的 kernel，应该被接受吗？
参考思路
答案取决于规格要求的是可观察结果，还是还包含内存模型与同步规则。当前平台上看似稳定的竞争，可能依赖尚未被扰动的执行条件；但把所有竞争都视为可观察错误，又会混淆两种不同性质。论文主动区分二者，也限制了自身的检测主张。
3. 两个程序满足同一实数规格，何时仍不足以说明优化可接受？
参考思路
规格可能遗漏数值误差、特殊值行为，或本来就没有唯一限定输出。代数等价允许某些浮点重排，却不回答这些重排的误差能否被应用接受；反过来，实数表达式不等价的近似，也未必不可接受。证明与应用要求之间的距离，取决于规格选择。