核心问题：对任意超越函数解释都成立的等价证明，为什么仍不能直接保证两个真实后端等价？
论文卡片
- 原题： Proving LLM-Generated GPU Kernels Correct and Safe: Floating-Point Verification in Lean and VerCors
- 作者： Archibald Browne、Eugene Lee、Cristopher Salvi（Imperial College London、Logos Research）。
- 日期与版本： 2026-10-17 提交，arXiv v1；cs.PL；验证框架与案例研究预印本。
- 定位： AI 生成 CUDA 的浮点语义等价与并发安全验证；研究重点是证明能力，没有评测 kernel 加速。
- 阅读入口： arXiv · HTML 全文（v1） · PDF（v1） · alphaXiv
简短导读：给未知函数同一个名字
论文用确定性翻译器把 PyTorch 规格与有限 CUDA 子集转成 Lean 表示，以 Float32 推理语义等价，再用 VerCors 检查内存与线程安全。证明 Agent 补充自动化未解决的推理，生成 Agent 根据反馈修改候选代码。
最有意思的是 exp：系统不证明硬件指数函数如何舍入，而把它保留为不透明函数。若两边都计算 1 / (1 + exp(-x))，并执行相同的 Float32 运算，就能在共同解释下证明一致。但真实参考实现与 CUDA 必须把这个符号实现成逐点相同的函数；不同后端不能仅凭函数同名满足该条件。§5.1 中，__expf 与 expf 被建模为不同符号，替换因此未获证明。
证据与限制
§4 在翻译器支持范围内选择了 30 道 KernelBench 题，每题最多五个有效回合；导入失败的回合可重试。两种模型在同一框架中的成绩如下，列名沿用表 2：
| 指标（通过题数） | GPT-5-fast | Opus-5-fast |
|---|---|---|
| Lean 语义轴 | 18/30 | 30/30 |
| VerCors 安全轴 | 23/30 | 23/30 |
| 联合通过 | 11/30 | 22/30 |
每种模型仅运行一次，没有波动估计；这也不是与其他验证系统的同预算对照。单轴通过不能代替同一候选同时通过两项检查。
证明对象仍是翻译后的模型。CUDA 到 Lean 的翻译被信任，并在安全假设下将并行代码顺序化。§3 还明确说当前配置信任 SMT 求解器结果，因此不能把整条链概括成“只需信任 Lean 内核”。超越函数的共同解释、规格与翻译的忠实性，以及前置条件，仍限定着结论。
以上为论文报告；本导读未独立运行其验证框架。
重点阅读章节
- §3 的 Transcendental Functions 与 CUDA AST Extraction： 看共同函数解释和顺序化分别引入什么条件。
- §4、表 2： 分开理解语义轴、安全轴与联合通过率，以及有效回合的计数方式。
- §5.1、§5.2 与 §6： 看不透明函数的成功案例、负零引发的语义差异，以及定理用于真实执行时的边界。
思想启发：普遍性也有共同前提
以下是导读者的理解。
“对任意函数都成立”容易被听成“不需要关心函数实现”。它实际表达的是：任取一个函数，把它同时放进等式两边，关系成立。这没有允许左边任选一个函数、右边再任选另一个。量词覆盖很广，却没有取消两边共享同一对象的条件。
可以用一个简单思想例子看清区别：两台计算器都显示 f(x)，只要它们使用同一个 f，结果自然一致；若一台计算 x、另一台计算 x+1，同名接口就不足以建立关系。这个例子不描述论文实验，只解释证明命题的逻辑结构。
不透明抽象因此有双重意义：它避免借用未经证明的数值恒等式，也把一项关键判断留在模型与现实的对应关系上。评价证明时，除了问“推理是否严密”，还要读清楚同一个符号在两边分别指向什么。
三个开放性思考问题
1. 若两个 exp 实现只相差极小舍入误差，共同解释下的等价证明还保留多少信息？
参考思路
它仍揭示两边使用函数的结构关系，但不能自动给出最终误差界。微小差异经过后续运算，可能被放大，也可能改变分支。值得区分的是“结构相同”“实现逐点相同”和“结果足够接近”：三种主张需要的假设与证据并不一样。
2. 确定性翻译减少了随机性，为什么没有同时消除对翻译器的信任？
参考思路
同一输入总得到同一模型，使错误可重复、可定位；但稳定地产生错误模型仍然可能。证明系统检查模型中的命题，并不会仅因翻译可重复，就确认它忠实于源程序。这里的进步在于信任对象更明确、可审查，而语义保持仍是另一项需要论证的关系。
3. 一个模型在语义轴上达到 30/30、联合通过却只有 22/30，这究竟说明代码能力还是证明能力的边界？
参考思路
失败可能来自代码错误，也可能来自缺少注解、证明自动化不足或预算耗尽。附录 B.1 就有代码不变、补齐内存范围注解后通过的案例。因此分数同时受到生成、表达条件和完成证明的影响。若不区分这些原因，“未验证”很容易被误读成“错误”，通过率也容易被误读成纯粹的模型能力。