A Contract-Grade Verifier for LLM-Generated GPU Kernels, and a Native Blackwell Backward for the Gated-Linear-Recurrence Family
本文介绍了一种严谨的、无容差的契约级验证器，通过以十二个对抗性门控取代宽松的单形状测试，揭示了当前 LLM 生成的 GPU 内核的高失败率，同时验证了针对门控线性递归族的一种新型原生 Blackwell 反向实现。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正在建造一个能够每秒烹饪数百万份餐点的机器人厨师。为了提高速度，你请一位超级聪明的 AI 为机器人的高速大脑（GPU）编写特定的指令（称为“内核”）。目标是让机器人的烹饪速度比人类快得多。但问题在于，如果机器人把吐司烤焦了，或者端上来一盘石头而不是汤，那么它跑得再快也毫无意义。在人工智能的世界里，这些“食谱”是驱动从聊天机器人到医疗诊断等一切事物的引擎。多年来，科学家们一直在检查这些 AI 编写的食谱是否有效，方法是品尝几口随机的样本。如果味道与原版“足够接近”，他们就宣布这个食谱是成功的。但如果机器人其实是在偷偷给你喂毒药，只是恰好吃起来像汤呢？如果它在做一小碗时表现完美，但在你尝试供应一整场宴会时却爆炸了呢？这篇论文提出了一个可怕的问题：我们是否仅仅因为我们的品鉴测试过于简单，就无法察觉其中的问题，从而在为那些实际上已经损坏的“快速”食谱欢呼？
论文作者决定构建一个更加严格的、“合同级”的检查员来检查这些 AI 编写的食谱。这个检查员不再只是品尝几口，而是创建了一套包含十二种不同测试的组合——比如检查机器人是否烧焦了食物、是否提供了错误的尺寸，或者是否偷偷将健康的食材换成了有毒的成分。他们用这个严格的检查员对 2,638 个已被一个流行系统宣布为“完美”的食谱进行了测试。结果令人震惊：那些“完美”的食谱中，有 62.1% 至少存在一个重大缺陷，且有 39.5% 已经彻底损坏，以至于任何“足够接近”的数学逻辑都无法为其开脱。这些不仅仅是微小的调味误差；它们是无声的灾难，比如一个将警告信号（如“NaN”或无穷大）转化为正常数值的机器人，在崩溃发生前隐瞒了真相。
为了证明他们并非在刻意刁难或使用一把坏掉的尺子，作者采取了一个聪明的做法。他们从头开始为一种特定类型的 AI 模型（称为门控线性递归家族）编写了自己的超高级食谱。这是一个针对最新一代计算机芯片（Blackwell）的手写全新指令集。他们使用一个金标准、双精度计算器测试了自己的食谱，并证明其是正确的。随后，他们将自己的食谱放入严格的检查员中进行测试。它通过了所有测试。这就是他们的“正向对照”：如果这个检查员只是一个旨在让所有人失败的工具，它也会让自己的完美食谱失败。既然它通过了，说明这个检查员是值得信赖的。它在开发过程中抓住了他们的小错误（例如缺失的安全检查），这证明它是一个公正的裁判，而非带有偏见的裁判。
论文还解决了一个针对新 Blackwell 芯片的特定且棘手的问题。这些芯片拥有一种非常有限的、极速的小型内存空间（张量内存）。官方的“食谱”试图占用过多的此类空间，导致计算机冻结或崩溃。作者的新食谱找到了完美管理这一空间的方法，避免了崩溃。然而，他们也诚实地说明了权衡之处：虽然他们的新食谱是安全且正确的，但它比现有的“快速”库要慢。他们并没有假装这是最快的东西；他们只是证明了这是第一个既原生于新芯片又真正正确的程序。
最后，这篇论文揭示了一个“严谨性差距”。目前测试 AI 生成代码的方式，就像是通过让一辆车驶过一次来检查一座桥是否稳固。而这个新的检查员则像是派出一辆卡车、一辆坦克和一场风暴来测试这座桥是否真的能承受压力。研究结果表明，该领域报告的进展比数字看起来要弱得多。大约有 1,487 个被“接受”的内核实际上是损坏的，而标准测试仅抓住了新检查员拒绝的那些“好”内核中的 14 个。作者认为，我们需要停止接受“足够接近”，转而要求“合同级”的正确性——检查诸如“它是否正确处理了无穷大？”以及“它每次给出的答案是否一致？”等问题——以确保未来的 AI 系统是建立在坚实的地基之上，而非建立在速度的幻象之上。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。