Lecture 116: GPU Kernel Formal Verification
The talk addresses the critical challenge of establishing trust in high-performance GPU kernels generated by AI systems. While AI-based generators (like KForge) can produce highly efficient kernels, their correctness cannot be guaranteed by traditional testing methods. The speaker introduces formal verification, using a tool called Tatwa, which reasons about the semantic equivalence between a reference program (e.g., PyTorch model) and an optimized candidate (e.g., Triton kernel). The process involves decomposing high-level operations into basic mathematical primitives and expanding tensor operations into scalar terms for analysis by solvers like Z3. The primary limitations discussed include scalability, handling low-level semantics (like hardware intrinsics), and reasoning about thread synchronization.
Key takeaways
-
Limitations of Testing vs. Verification
3:40
Testing is inherently sampling and can only confirm correctness for tested inputs. Formal verification, however, aims to prove that the two programs (baseline and candidate) cannot disagree for *any* possible input, addressing the fundamental question of semantic equivalence.
-
Identifying Semantic Bugs (The Missing Clamp)
9:00
A key example demonstrated a scenario where an optimized candidate failed to include an intermediate `clamp` operation required by the reference program. This bug was missed by testing/fuzzing but was successfully identified by the verifier because it reasoned about the mathematical semantics, not just the output for sampled inputs.
-
Formal Verification Workflow
12:00
The process involves taking the PyTorch/Triton programs, lowering them to mathematical primitives, and then expanding tensor operations (like matrix multiplication) into scalar terms to allow solvers (Z3) to reason about the computation at the element level.
-
Bounded Verification Approach
19:10
Due to scalability issues, the approach uses bounded verification, limiting the summation range (e.g., capping a summation over K to a small value) to make the problem solvable by current solvers, acknowledging this as a current limitation.