GPU Kernel Formal Verification
This talk details the critical challenge of establishing trust in high-performance GPU kernels generated by AI. While AI tools like KForge can efficiently generate optimized kernels (e.g., replacing expensive divide operations with exponent/mantissa decomposition), the primary concern shifts from performance generation to correctness. The speaker introduces Tatwa, a tensor algebra equivalence checker, which uses formal verification (Z3 solvers) to reason about the semantic equivalence between a reference kernel (e.g., PyTorch model) and an AI-generated candidate kernel. The talk highlights that while testing is useful, only formal verification can detect subtle bugs, such as missing intermediate clamp operations or semantic discrepancies, by reasoning about the underlying mathematical primitives.
Key takeaways
-
Limitations of Testing vs. Verification
18:13
Testing is inherently sampling and can only prove the absence of bugs for tested inputs. Formal verification, however, reasons about the semantics and mathematical structure, allowing it to detect bugs (like missing clamps or incorrect scaling factors) that only manifest for specific, untested inputs.
-
The Need for Semantic Equivalence Checking
22:10
The core problem is ensuring that the optimized AI-generated kernel maintains the exact mathematical semantics of the original reference kernel. Tatwa achieves this by decomposing high-level operations (like `clamp` or `softmax`) into basic mathematical primitives for the Z3 solver to reason over.
-
Bounded Verification Approach
27:10
Due to computational complexity, the current approach uses bounded verification, limiting the summation or expansion of product terms (e.g., capping the reduction over k to a small value) to keep the problem solvable by solvers like Z3.