046 · 简化版被证明，原 kernel 就正确了吗？
RESOLVE 用逐位测试连接原始 kernel 与低并发版本，再证明后者的代数等价性。这条混合证据链扩大了验证范围，也要求分清：哪些连接经过证明，哪些仍依赖有限执行。
Agent-Workflow
029 · 规则能执行，是否就忠实表达了政策？
NOMOS 把书面政策编译为确定性工具调用门控。它能排除自阻塞、参数错绑等结构缺陷，却仍可能把具体授权弱化为‘用户要求过某种操作’。
028 · Agent-Assisted 胜过 Full-Agent，究竟是谁在优化？
论文用评测 harness、性能剖析、工作负载分区和人工筛选约束 GPU kernel Agent；五类算子均优于 Full-Agent，但对照尚不能拆分 harness、专家引导与搜索预算各自的贡献。
027 · 波形变成 SQL，Agent 就会调试芯片了吗？
BTTF 把波形转为 SQLite，再以多 Agent 完成查询、断言检查和 RTL 定位；95.33% 的成绩证明了结构化接口的价值，却不足以单独证明开放式根因调试已经解决。
025 · 返回值被唯一确定，就算规格完整了吗？
SpecAgent 用依赖感知规划、形式验证、跨规格修复与强度审查生成 ACSL 规格；其完备性探针能识别返回值欠约束，但不能单独证明规格已表达全部重要语义。
017 · 人不写 CUDA，就等于 Agent 自主优化吗？
Agentic Kernel Optimization 用多 Agent、性能分析和人工搜索纠偏，在 B200 上为三类 FlashInfer-Bench workload 生成高性能 CUDA kernel；论文证明了代码可由 Agent 完成，却也留下了系统自主性、基线口径与验证边界的问题。
016 · 退回编译器基线，也算优化成功吗？
KernelOPT 尊重 Inductor 已做出的库调用分派，只搜索生成的 Triton 子 kernel，并用四级验证决定替换或回退；250 个 KernelBench 问题上的整体加速来自少数显著收益与大量基线保留的组合，不能等同于每个任务都被优化。
015 · 证据来自不同运行，还能属于同一段程序吗？
Argus 以稳定的语义区域为共同坐标，规划彼此隔离的多次 GPU 测量，并把直接观测、跨视图归因和变体推导的证据明确区分；实验显示更细粒度的反馈能改善多种 kernel 优化 Agent，但跨运行归因仍依赖区域身份与执行可比性的假设。
006 · Agent 变强了，还是编译器更会教了？
CAKE 固定模型与 Agent 脚手架，改用面向 Agent 的硬件显式 IR、校验和局部反馈；实验支持整套编译器环境改善搜索，但尚未分离各组成部分的贡献。