RESOLVE：通过测试、归约与证明对GPU内核进行语言无关的验证
RESOLVE: Language-Agnostic Validation of GPU Kernels Through Testing, Reduction, and Proof
浏览论文内容
中文总结 AI 辅助
RESOLVE结合测试与形式化验证，通过扰动测试、降并发重写和F*/Pulse证明，实现GPU内核的语言无关验证，并成功验证融合GEMM及发现巨型内核中的新错误。
中文摘要 AI 辅助
AI系统现在能够编写和优化生产级GPU内核，但验证这些内核仍然是一个重要挑战。仅在少数随机输入上评估内核，并检查其输出在数值容差范围内与可信参考内核匹配，这并不足够：竞争条件可能导致非确定性行为，在测试中无法显现；数值容差可能隐藏错误，即使在广泛校准后也可能导致误报。为应对这一挑战，我们提出了RESOLVE，它结合了测试与形式化验证，构建了一个全面的内核验证流水线。该流水线分三步操作：首先，使用二进制插桩扰动执行时序以暴露竞争条件，从而测试非确定性。其次，一个智能体重写候选内核和参考内核，以获得“降并发”版本，这些版本更易于分析，但在所有测试中仍产生逐位相同的输出。第三，在F*/Pulse框架中对降内核进行形式化分析，并证明它们在实数上执行相同的计算。这绕过了对数值容差的需求。我们展示了RESOLVE能够使用KernelBench验证广泛选择的内核，并在三个最先进的框架和语言中证明融合GEMM的等价性：CUTLASS、Triton和Gluon。它还分析了以难以验证著称的巨型内核，并发现了四个先前未报告的问题，包括两个明确的错误。我们展示了智能体可以使用RESOLVE修复这些问题，且性能影响极小，这凸显了当智能体能够严格检查其结果时，它们可以积极地进行优化。
英文摘要
AI systems can now write and optimize production GPU kernels, but validating them remains an important challenge. Evaluating the kernel on a few random inputs and checking that its outputs match a trusted reference kernel within numeric tolerances is not sufficient: races can cause nondeterministic behavior that fails to manifest in tests, and numeric tolerances can hide bugs and cause false positives even after extensive calibration. To address this challenge, we present RESOLVE, which combines testing and formal verification to build a comprehensive kernel validation pipeline. It operates in three steps: First, it tests for nondeterminism using binary instrumentation that perturbs execution timing to expose races. Second, an agent rewrites the candidate and reference kernels to obtain "reduced-concurrency" versions that are simpler to analyze but still produce bitwise-identical outputs in all tests. Third, the reduced kernels are formally analyzed in the F*/Pulse framework and prove that they perform the same computation on real numbers. This sidesteps the need for numeric tolerances. We show that RESOLVE can validate a broad selection of kernels using KernelBench, and prove equivalence across fused GEMMs in three state-of-the-art frameworks and languages: CUTLASS, Triton, and Gluon. It also analyzes mega-kernels, notoriously difficult to validate, and finds four previously unreported issues, including two clear bugs. We show that agents can use RESOLVE to repair the issues, with minimal performance impact, highlighting that agents can optimize aggressively when they can rigorously check their results.
发表机构
- University of California, Riverside（加州大学河滨分校）
- Math, Inc.（Math公司）
- Microsoft Research（微软研究院）
机构由 AI 辅助整理，请以论文原文为准。
