GPU内核写得飞快，但谁来保证它是对的？

我最近刷到一个叫VeriTile的项目，专门给Triton写的GPU内核做形式化验证。这名字一听就硬核——Triton本身已经让内核开发比CUDA轻便得多，但bug照样会藏在算子边界、内存竞争这些隐蔽角落里。更关键的是，GPU上跑的计算往往没有传统单元测试能兜底，一次静默错误就能让整个训练结果作废。形式化验证的思路是：不靠跑用例猜对错，而是用数学证明告诉你这段内核逻辑成立。代价是证明过程可能需要人工辅助，而且能覆盖的范围有限。但方向对。当GPU算子越来越像基础设施、被上层框架默认信任时，"编译通过"和"逻辑正确"之间那道裂缝，迟早需要有人用比编译器和测试更硬的刀去补。VeriTile算是一个起点。

原文：VeriTile: Formal Verification for Triton Kernels · 来源：Hacker News