最近一直在用 AI 写代码，但是上线时也总会隐隐不安，刚好看到一篇文章，讲到 AI 写 GPU 内核的事情，本文简单探讨一下。

1、开场：AI 代码生成的"甜蜜陷阱"

注：本文有 AI 辅助创作，确实排版和阅读都比纯手工更好。

想象一下：你正在优化一个深度学习模型的性能，于是让 AI 智能体帮忙生成一段 GPU 内核代码。几秒钟后：

• ✅ 代码生成了
• ✅ 编译通过了
• ✅ 性能提升了 30%
• ✅ 你精心准备的 500 个测试用例全部通过了

这时候，你敢把它直接部署到处理百万用户的线上运行环境中吗？

如果你犹豫了，恭喜你，你的直觉可能是对的。

最近几年，AI 已经不满足于只写 Python 脚本了，它们开始进军底层——为 GPU 编写高性能内核代码。在最近的 GPU Mode 内核竞赛中，NVIDIA 的工程师 Bryce Adelstein Lelbach 甚至感叹：“AI 生成的代码，我现在看都不需要看就能跑！”

听起来很美好？但现实是：当 AI 生成代码的能力越来越强，“我们到底能不能信任这些代码"反而成了最大的瓶颈。

今天，我们就借 Gimlet Labs 在 2026 年 PLDI 会议上的最新研究，用大白话聊聊：

• 🔍 为什么传统测试对 AI 生成的代码"不够用”？
• 🎯 什么是"形式化验证"，它凭什么比测试牛？
• 📱 这技术能用在手机 App 上吗？
• ⚡ 它和自动化测试到底谁更厉害？

准备好了吗？让我们开始这场"照妖镜"之旅。

2、传统测试的阿喀琉斯之踵

2.1、数值测试的工作原理

传统的内核验证依赖于数值测试：工程师定义一组测试用例，覆盖内核需要支持的各种情况，然后检查输出是否正确。这种方法简单直观，但存在一个根本性问题：

测试本质上是抽样，无论测试集多大，都只能覆盖无限输入空间中的有限样本。

2.2、一个真实的 Bug 案例

让我们看一个来自实际运行的例子。原始的 PyTorch 实现计算缩放点积注意力（Scaled Dot-Product Attention）时，在 softmax 之前对注意力分数进行了中间裁剪（clamp），将值限制在 [-5, 5] 范围内：

1
2
3
4
5
6
7
8

def forward(self, Q, K, V):
    scale = 1.0 / math.sqrt(Q.size(-1))
    scores = torch.matmul(Q, K.transpose(-2, -1)) * scale
    scores = torch.clamp(scores, -5.0, 5.0)  # 中间裁剪
    weights = F.softmax(scores, dim=-1)
    out = torch.matmul(weights, V)
    out = torch.clamp(out, -5.0, 5.0)
    return out

AI 生成的优化版本将手动注意力融合为高效的 SDPA，但悄悄移除了中间裁剪操作：

1
2
3
4
5

def forward(self, Q, K, V):
    scale = 1.0 / math.sqrt(Q.size(-1))
    out = F.scaled_dot_product_attention(Q, K, V, scale=scale)  # 缺少中间 clamp！
    out = torch.clamp(out, -5.0, 5.0)
    return out

2.3、为什么测试没有发现这个 Bug？

在随机测试中，两个版本返回了相同的输出！原因在于：

1. 边界条件罕见：大多数随机生成的测试用例产生的注意力分数本来就在有效范围内
2. clamp 成为恒等函数：对于范围内的值，裁剪操作不产生任何效果
3. 测试误导了判断：表面上看，优化版本"通过"了所有测试

但是，原始实现保证了进入 softmax 的所有注意力分数都在有界范围内，而优化版本移除了这个保证。这在实际运行环境中可能导致数值不稳定或溢出问题。

图 1：人类写的代码结构——注意中间有个 Clamp（限制器）

图 2：AI 生成的代码结构——中间的限制器不见了！

2.4、扩展测试真的有用吗？

你可能会想：“那就加更多测试用例，覆盖更多的配置、形状和范围！” 但这种方法很快就会崩溃：

• 输入空间过大：很难预测内核在生产环境中可能遇到的所有输入
• 组合爆炸：即使扫描不同的配置，也无法穷尽所有组合
• 条件触发：如果内核有条件分支，可能需要特定的值组合才能触发 bug

根据研究发现，KernelBench 在评估解决方案的正确性时高估了 31%。

关键洞察：无论测试套件多么庞大，测试只能检查有限子集，而内核的行为空间实际上是无限的。这就是形式化验证要解决的问题。

3、破局之道——“形式化验证"登场

3.1、从"抽样"到"证明”：思维方式的革命

既然测试只能抽样，永远有漏网之鱼，那怎么办？

这就要引入形式化验证（Formal Verification）了。让我们用一个生活化的比喻来理解它：

传统测试就像：

• 我造 1000 辆不同重量的汽车开过这座桥
• 桥没塌
• 所以我说这座桥"应该"是安全的

形式化验证就像：

• 我不用任何真实的汽车
• 我直接用物理学和数学公式
• 证明：这座桥的结构，在任何情况下都绝对不可能塌

看到区别了吗？一个是"试出来的"，一个是"证出来的"。

3.2、形式化验证问什么问题？

在验证 AI 生成的代码时，形式化验证不再使用随机数据去跑测试，而是把输入变成"符号"（Symbol）——就像数学课上的 x、y、z，代表所有可能的值。

然后，它向底层的"求解器"（比如微软开发的 Z3）抛出一个极其尖锐的数学问题：

“在整个宇宙中，是否存在哪怕一种输入情况，会让’人类原始代码’和’AI 优化代码’输出不一样的结果？"

求解器会有三种回答：

✅ SAT（找到了！）
“我找到了一个反例！就是这个输入，会让两段代码输出不一样！”
→ 这就是一个实打实的 bug，而且求解器会直接把能触发 bug 的输入告诉你

❌ UNSAT（找不到）
“我搜遍了整个数学空间，不存在任何这样的输入！”
→ 这就是一个数学证明，两段代码在所有情况下都等价

❓ UNKNOWN（超时了）
“问题太复杂，我算不出来…”
→ 这是现实限制，需要优化验证策略

3.3、 还记得那个消失的限制器吗？

对于前面那个 AI 偷偷删掉限制器的案例，形式化验证器是这样工作的：

1. 人类代码：Softmax(Clamp(scores, -5, 5))
2. AI 代码：Softmax(scores)（没有 Clamp）

验证器问 Z3：

“是否存在某个 scores 值，让这两个公式的结果不一样？”

Z3 回答（仅用 0.01 秒）：

“SAT！我找到了！
当 scores = [-6, -7] 时：

• 人类代码：先把 -6 和 -7 限制到 -5，再做 softmax
• AI 代码：直接用 -6 和 -7 做 softmax
• 结果不一样！

→ 证明不等价！ Rejected!”

这个 bug，传统测试可能永远发现不了，但形式化验证 0.01 秒就揪出来了。

3.4、编译器的血泪史：为什么需要形式化验证

其实，编译器优化领域早就在用形式化验证了(我之前的文章也有写过，可以翻翻)：

案例 1：LLVM 的 Alive2
LLVM 是世界上使用最广泛的编译器框架（编译 C++、Rust 等语言）。它的每一个优化转换，都用 Alive2 进行形式化验证。为什么？因为优化器的 bug 太隐蔽了，测试根本抓不住。

案例 2：CompCert
这是一个完全用形式化方法验证正确性的 C 编译器。它生成的代码，有数学证明保证和原始代码等价。航空航天、医疗设备等高安全领域都在用它。

关键洞察：编译器优化和 AI 内核优化，面临的是同一类问题——微妙、依赖特定输入、下游很难诊断的 bug。测试不够用，必须上数学证明。

3.5、AI 内核优化的"自由度"与"约束”

当 AI 智能体生成优化内核时，它有很大自由度：

• 🔄 重构循环（改变计算顺序）
• 🔗 融合操作（多个步骤合并）
• 💾 改变内存布局（数据怎么存）
• 🔀 重新排序（先算啥后算啥）
• ⚡ 向量化策略（并行计算方式）

但这种自由不是无限的！有一个铁律：

参考 PyTorch 模型是"数学契约"
它定义了必须计算什么（What），而不是如何计算（How）

优化内核可以用任何花式技巧，但最终算出来的结果，必须和参考模型一模一样（对于每个输入）。

形式化验证就是这个契约的执法者。

4、验证器的"魔法"——代码如何变成数学公式

好，理论讲完了。你可能会好奇：验证器到底是怎么把代码变成数学公式的？

这确实是个复杂的过程，但我们可以用通俗的方式理解。就像工厂的流水线，代码要经过三道"工序"：

图 3：从代码到数学证明的三道工序

4.1、第一道工序：提取"计算意图"

想象你有两份菜谱：

• 📝 人类的菜谱：用 PyTorch 写的，很直白
• 🤖 AI 的菜谱：用 Triton 写的，优化过，看起来完全不一样

验证器第一步要做的，是把这两份菜谱都翻译成同一种"中间格式"，叫做 TensorAlgebra DAG。

PyTorch 代码怎么提取？

• 用 torch.compile 把代码变成一个"操作流程图"（FX Graph）
• 从图里读出每一步在干什么

Triton 代码怎么提取？

• Triton 更麻烦，因为它是编译好的"黑盒子"
• 验证器用 Inductor 后端重新编译一遍，生成 .ttir 文件（一种中间表示）
• 从 .ttir 里"倒推"：从最后的存储操作往回推，重建整个计算过程

关键点：两份完全不同的代码，现在变成了同一种格式，就可以比较了。

💡 类比：就像你要比较两本菜谱是否做的是同一道菜，先把它们都翻译成标准菜谱格式（材料、步骤、火候），才能对比。

4.2、第二道工序：拆解成"原子操作"

现在代码变成了统一格式，但还是太"高级"了。比如：

• Softmax(x) - Z3 不知道这是啥
• MatMul(A, B) - 矩阵乘法，Z3 也不认识
• Clamp(x, min, max) - 限制器，Z3 照样不懂

验证器要做的是**“拆解”**——把高级操作拆成数学基本操作：

1
2
3
4
5
6
7
8

Clamp(x, min, max) 
  → min(max(x, min), max)  // 拆成"取最小值"和"取最大值"

Softmax(x) 
  → exp(x) / sum(exp(x))  // 拆成指数、求和、除法

MatMul(A, B) 
  → ∑(A[i,k] * B[k,j])  // 拆成乘法和求和

图 4：人类代码拆解后——Clamp 变成了 min 和 max

图 5：AI 代码拆解后——注意 softmax 前没有 min/max

现在一眼就能看出区别了对吧？人类代码在 softmax 前有 min/max，AI 代码没有！

4.3、第三道工序：变成"符号公式"

现在代码已经拆成了基本数学操作，但还有一个问题：它们还在操作整个矩阵。

而 Z3 求解器只能处理单个数字（标量），不能直接处理矩阵。怎么办？

验证器使用一个巧妙的技巧：不验证整个矩阵，只验证矩阵中的任意一个元素。

举个例子：

1
2
3
4
5
6

# 矩阵乘法：C = A × B
# 整个矩阵：太大了，Z3 算不了

# 单个元素：C[i, j] = A[i,0]*B[0,j] + A[i,1]*B[1,j] + ...
# 用符号 i, j 表示"任意位置"
# Z3 只需要验证这一个元素的公式

关键洞察：如果对于任意位置 (i, j)，两个公式都相等，那整个矩阵就都相等。

有一个小技巧：有界验证

如果矩阵很大，比如 256×256，那一个元素的公式会展开成 256 项相加：

1

C[i,j] = A[i,0]*B[0,j] + A[i,1]*B[1,j] + ... + A[i,255]*B[255,j]  // 256 项！

这对 Z3 来说太大了，算不动。

验证器的解决办法：只展开一小部分，比如只展开 2 项：

1

C[i,j] ≈ A[i,0]*B[0,j] + A[i,1]*B[1,j]  // 只看 2 项

图 6：不需要展开全部 256 项，只看 2 项就能发现结构性差异

这样行吗？ 行！因为：

• 我们不是要算精确的输出值
• 我们只是要看两段代码的"结构"是否一样
• 如果连 2 项都不一样，那 256 项肯定也不一样
• 这就像验钞机，不需要看完整张钞票，看几个防伪点就够了

这个技巧叫 “有界翻译验证”（Bounded Translation Validation），LLVM 的 Alive2 也在用。

4.4、第四道工序：交给 Z3 求解

现在终于可以问 Z3 了！

验证器把两个公式交给 Z3：

• 📝 人类代码公式：min(max(softmax(...), ...), ...)
• 🤖 AI 代码公式：softmax(...)

然后问：

“Z3 大佬，是否存在某组输入，让这两个公式不相等？”

Z3 开始疯狂计算（其实只需要几毫秒到几秒）…

如果返回 SAT： “找到了！输入 x = […] 时，两个公式结果不同！” → Bug 确认，拒绝部署

如果返回 UNSAT： “我搜遍了整个数学空间，它们永远相等！” → 获得数学级别的正确性证明，放心部署

如果返回 UNKNOWN： “问题太难了，我算不出来…” → 需要优化验证策略，或者退回到传统测试

4.5、真实战果：0.01 秒抓住消失的限制器

还记得那个被 AI 删掉的限制器吗？验证器是这样抓住它的：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13

人类代码：Softmax(Clamp(scores, -5, 5))
AI 代码：Softmax(scores)

Z3：正在搜索反例...
Z3：找到了！

反例输入：scores = [-6, -7]
人类代码输出：先限制到 -5，然后 softmax([−5, −5])
AI 代码输出：直接 softmax([−6, −7])
结果：不相等！

结论：SAT（不等价）
用时：0.01 秒

传统测试可能跑 10000 个用例都发现不了，形式化验证 0.01 秒搞定。

5、实战成绩单——验证器的"照妖镜"效果

Gimlet Labs 在 PLDI 2026 的演讲中公布了验证器的实测数据。他们拿 KernelBench Level 1 的 26 个 Triton 内核来测试，结果如下：

重点：那 2 个 SAT 的案例，都是通过了传统数值测试的，但形式化验证发现了它们的 bug！

5.1、案例 1：硬编码的缩放因子

人类代码支持任意的 scaling_factor 参数：

1
2
3
4
5
6
7
8

def forward(self, x):
    x = self.conv_transpose(x)
    x = x + self.bias
    x = torch.clamp(x, min=0.0, max=1.0)
    x = x * self.scaling_factor  # 👈 可配置
    x = torch.clamp(x, min=0.0, max=1.0)
    x = x / self.scaling_factor  # 👈 可配置
    return x

AI 生成的 Triton 内核把 scaling_factor 硬编码成了 2.0：

1
2
3
4
5

@triton.jit
def optimized_kernel(...):
    # 把 clamp/scale/clamp/unscale 折叠成一个 clamp
    # upper_bound 是针对 scaling_factor=2.0 预计算的
    x = tl.minimum(tl.maximum(x, 0.0), upper_bound)  # 👈 硬编码了！

传统测试为什么没发现？
因为测试用例只用了 scaling_factor=2.0，刚好和 AI 硬编码的值一样！

形式化验证怎么发现的？
验证器保持 scaling_factor 符号化（不给具体值），Z3 立即发现：当 scaling_factor ≠ 2.0 时，两段代码不等价！

→ SAT，找到反例，拒绝部署

5.2、案例 2：浮点精度的幽灵

这是个 HardSigmoid 函数的案例。人类代码：

1
2
3

def forward(self, x):
    return torch.nn.functional.hardsigmoid(x)  
    # 实际是：clamp((x + 3) / 6, 0, 1)

AI 优化后，把除以 6 改成了乘以倒数：

1
2
3
4
5

@triton.jit
def optimized(...):
    # 用乘法代替除法（更快）
    result = (x + 3.0) * 0.16666666666666666  # 👈 这是 fp64 字面量
    result = tl.minimum(tl.maximum(result, 0.0), 1.0)

看起来没问题？但是！ Triton 把这个 fp64 字面量编译成了 fp32，产生了精度损失：

1
2

参考：clamp(x/6 + 1/2, 0, 1)
AI 代码：clamp((x + 3) * 0.166666672, 0, 1)  # ← 注意最后一位不同

Z3 的发现：
在 x ≈ 2.9999987 附近，两个实现产生了不同的输出：

• 参考：0.9999999
• AI 代码：1.0
• 差异：2.6e-8（非常微小，但是结构性的数学差异）

传统测试为什么没发现？
测试可能设置了宽松的容差（如 atol=1e-5），这点差异被忽略了。

是否可接受？
这取决于具体需求。但重点是：在部署前就知道有这个差异，总比生产环境出问题强。

5.3、关键洞察：避免"误报"同样重要

一个"过度敏感"的验证器，看到什么都说"不等价"，也没用。

研究团队特别测试了：结构不同，但数学相同的代码，验证器能否识别？

例如：

• PyTorch 的融合 flex_attention
• vs 手动实现的等价版本

结果：验证器成功证明了它们等价（UNSAT），而不是误报。

→ 说明验证器不是乱叫的，它真的理解数学语义

6、能用在移动端客户端开发吗？现实点说

很多人看到这里会问：我做手机 App 开发，这个形式化验证能用吗？

这是个好问题，但答案可能会让你失望：对于大部分移动端客户端开发，用处不大。

6.1、形式化验证不是"万能钥匙"

让我们实话实说：形式化验证主要针对的是计算密集型的数学运算代码，特点是：

• 输入输出都是数值（矩阵、张量、向量）
• 计算逻辑可以表达为数学公式
• 没有复杂的业务逻辑、用户交互、网络请求等

它擅长验证的东西：

• ✅ GPU 内核（矩阵乘法、卷积运算）
• ✅ AI 模型推理（Transformer、CNN 计算）
• ✅ 图像/信号处理算法
• ✅ 加密算法的数学部分

它不擅长验证的东西：

• ❌ 业务逻辑（用户点击按钮后该干啥）
• ❌ UI 交互（界面渲染、动画效果）
• ❌ 网络请求（API 调用、数据同步）
• ❌ 数据库操作（增删改查）
• ❌ 第三方 SDK 集成
• ❌ 复杂的状态管理

6.2、移动端客户端的现实场景

让我们看看典型的移动 App 代码：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20

// Android 典型代码
class LoginViewModel : ViewModel() {
    fun login(username: String, password: String) {
        viewModelScope.launch {
            _loginState.value = LoginState.Loading
            
            try {
                val response = authRepository.login(username, password)
                if (response.isSuccessful) {
                    userPrefs.saveToken(response.token)
                    _loginState.value = LoginState.Success
                } else {
                    _loginState.value = LoginState.Error(response.message)
                }
            } catch (e: Exception) {
                _loginState.value = LoginState.Error(e.message)
            }
        }
    }
}

这种代码：

• 涉及异步操作、网络请求、状态管理
• 没有复杂的数学计算
• 形式化验证帮不上忙，只能用传统的单元测试、集成测试

6.3、移动端能用形式化验证的特殊场景

不过，有几种特殊情况，形式化验证可能有用：

6.3.1、场景 1：移动端 AI 推理

如果你的 App 在手机上跑 AI 模型（离线推理），可能会用到：

1
2
3
4
5
6
7

// iOS 使用 Core ML 或自定义内核
class ImageProcessor {
    func optimizedConvolution(input: MLMultiArray) -> MLMultiArray {
        // AI 生成的优化卷积内核
        // 这部分可以用形式化验证
    }
}

6.3.2、场景 2：关键数值计算

金融 App 的利息计算、医疗 App 的健康指标算法：

1
2
3
4
5
6
7

// 精确的医疗计算
public class HealthMetrics {
    // AI 优化后的心率变异性计算
    public double calculateHRV(double[] rrIntervals) {
        // 这种数学密集型算法，可以考虑形式化验证
    }
}

6.3.3、场景 3：跨平台算法一致性

如果你需要保证 iOS 和 Android 的同一个算法计算结果完全一致：

1

iOS (Swift) 实现    ←→ 形式化验证 ←→    Android (Kotlin) 实现

但注意：这只对纯数学算法有用，业务逻辑还是用不上。

6.4、现实建议：移动端就用传统测试

对于 99% 的移动端开发者，以下方案更实用：

日常开发流程：

1
2
3
4
5
6
7
8
9

1. 单元测试（JUnit、XCTest）
   ↓
2. UI 测试（Espresso、XCUITest）
   ↓
3. 集成测试
   ↓
4. 真机测试 + Beta 测试
   ↓
5. 线上监控（Crashlytics、Sentry）

为什么传统测试更适合移动端？

• ✅ 快速反馈：改一行代码，跑一下测试，几秒搞定
• ✅ 覆盖真实场景：网络异常、权限拒绝、低内存等实际问题
• ✅ 容易上手：团队成员都会写
• ✅ 生态成熟：各种测试框架、工具链完善
• ✅ 成本低：不需要专门学 SMT 求解器

形式化验证的问题：

• ❌ 学习曲线陡：需要懂数学、懂 SMT 求解器
• ❌ 适用范围窄：只对数学密集型代码有用
• ❌ 工具链不成熟：移动端支持很少
• ❌ 性价比低：投入大量时间，能验证的代码很少

6.5、一句话总结

形式化验证是"手术刀"，不是"瑞士军刀"。

• 对于 GPU 内核、AI 模型推理等计算密集型代码：形式化验证是利器
• 对于移动端客户端的业务逻辑、UI 交互：还是老老实实写单元测试和 UI 测试吧

7、形式化验证 vs 自动化测试：谁更适合移动端？

刚才说了形式化验证不太适合一般的移动端开发，现在让我们具体对比一下，为什么在移动端场景下，自动化测试完胜。

7.1、快速对比表（移动端视角）

7.2、移动端开发的真实需求

让我们看看移动端开发实际需要测试什么：

需求清单：

1. ✅ 功能测试：点击按钮跳转到正确页面
2. ✅ 网络测试：断网、超时、服务器错误怎么处理
3. ✅ UI 测试：界面显示正确、适配不同屏幕
4. ✅ 权限测试：用户拒绝相机/定位权限怎么办
5. ✅ 异常测试：内存不足、磁盘满了会崩溃吗
6. ✅ 兼容性测试：iOS 14-17 都能跑吗
7. ✅ 性能测试：启动速度、内存占用、卡顿率

形式化验证能帮上忙的？ 几乎没有！

这些都是真实世界的复杂场景，不是纯数学计算，Z3 求解器帮不了你。

8、终章：AI 时代的信任危机与解决之道

8.1、问题的本质

Jason Wei 的“验证者定律”一针见血：

“AI 擅长解决的任务，取决于这个任务有多容易被验证。"

换句话说：

• 验证方法越强 → AI 越敢放飞自我
• 验证方法越弱 → AI 生成的代码你敢用吗？

当前困境：

• AI 写代码的能力：⭐⭐⭐⭐⭐（越来越强）
• 我们验证代码的能力：⭐⭐⭐（传统测试不够用了）

→ 对于 GPU 内核、AI 模型推理等计算密集型代码，信任成为瓶颈！

8.2、形式化验证的定位

形式化验证不是"炫技”，也不是"万能药"，而是针对特定领域的利器：

✅ 它能解决的：

• GPU 内核、AI 推理、科学计算等数学密集型代码的验证
• 编译器优化的正确性保证
• 跨平台算法一致性证明

❌ 它解决不了的：

• 移动端 App 的业务逻辑
• Web 应用的前后端交互
• 微服务的复杂调用链
• 用户体验问题

一句话总结：

形式化验证是"手术刀"，只在需要"数学级别确定性"的地方才用得上。

8.3、给不同开发者的建议

如果你是移动端/Web 开发者：

• ✅ 做好单元测试、集成测试、UI 测试
• ✅ 关注线上监控和 Bug 追踪
• ❌ 暂时不用关注形式化验证
• 💡 除非你在处理 AI 推理、加密算法等特殊场景

如果你是 AI/GPU 开发者：

• ✅ 关注形式化验证的发展
• ✅ 对于 AI 生成的内核代码，考虑使用验证工具
• ✅ 增强测试覆盖（边界条件、配置参数）
• 💡 Gimlet Labs 的工具值得关注

如果你是团队 Leader：

• 🎯 识别项目中哪些部分是"计算密集型"
• 🎯 这些部分如果用 AI 生成，考虑引入形式化验证
• 🎯 其他部分，传统测试方法已经足够好

8.4、实际影响

已经在用的地方：

• LLVM 编译器（Alive2）
• CompCert（航空航天级 C 编译器）
• GPU 内核优化（Gimlet Labs 等）

适用领域：

• 🖥️ 高性能计算
• 🤖 AI 模型推理优化
• ✈️ 安全关键系统（航空、医疗）
• 🔐 密码学实现

8.5、一句话总结

当 AI 能写代码的时候，对于计算密集型场景，我们需要的不是更多测试，而是数学证明。对于其他场景，传统测试依然是王道。

形式化验证是让 AI 生成的高性能代码真正走向生产的关键技术之一，但它不是万能的——选对场景，用对工具。

参考资源

• 原文：Formally Verifying AI-Generated GPU Kernels
• ARRAY 2026 演讲：完整视频
• 工具与论文：
  • Z3 SMT Solver（微软）
  • Alive2（LLVM 验证）
  • VOLTA（PTX 验证）
  • KernelBench 研究
  • Bounded Translation Validation (PLDI 2021)

作者声明：本文基于 Gimlet Labs 的技术博客创作，旨在用通俗语言向读者介绍形式化验证技术。文章澄清了形式化验证的适用范围：主要用于 GPU 内核等计算密集型代码，不适合一般的移动端客户端开发。技术细节请参考原文。