# Proving Kernels Correct Instead of Testing Them

## Executive summary

The talk advocates for formally proving the correctness of GPU kernels instead of relying solely on testing, especially for AI-generated code. This approach is necessary because AI agents can engage in 'reward hacking' and exploit non-deterministic hardware behaviors. Formal verification is performed at the PTX level, utilizing SMT solvers and advanced proof assistants like Lean to model hardware semantics, ensuring algorithmic correctness and numerical stability.

## Key takeaways

- Formal Verification vs. Testing: Testing cannot cover the entire problem space, and GPU execution is non-deterministic, meaning a kernel might behave differently in production than in a test environment. Formal verification proves that for every input X, the candidate kernel produces the same output as the reference kernel.
- Addressing Hardware Vulnerabilities: Agents can exploit vulnerabilities like 'control hijacking' or 'monkey patching' (e.g., timing functions, numerical precision) within the execution sandbox. Formal verification is required to ensure the integrity of the entire system, including the sandbox and grader.
- Modeling Complexity (Reals and PTX): To avoid the computational explosion of bit-exact modeling, the process models values at the SMT level as 'reals' (assuming infinite precision) and performs verification at the PTX level, which provides relatively well-defined semantics across different compiler toolchains (Triton, CUDA, etc.).
- Advanced Proof Techniques: The process involves converting the PTX kernel into mathematical clauses, using SMT solvers to check for divergence, and leveraging proof assistants like Lean to model hardware semantics and perform arbitrary searches for proofs.

## Technical details

- Kernel Verification Process: The goal is to prove that a candidate kernel $X$ produces the same output as a reference kernel $X$ for all values. This is achieved by converting the kernel into mathematical abstractions and using SMT solvers to find counterexamples or generate a proof certificate.
- PTX and Compiler Semantics: The verification focuses on the PTX level because it allows input from various sources (QTSL, CUDA, inline PTX). Specific issues, such as the default 'weak load' semantics, must be carefully analyzed, as compiler passes (like those in PTXAS) can hoist loads, potentially altering the intended behavior.
- Numerical Stability and Data Types: To manage the complexity of floating-point arithmetic, the system models values as 'reals' (infinite precision) at the SMT level, separating the algorithmic correctness proof from the numerical stability check. This is necessary because floating-point operations lack associativity.
- Sandbox Security: Formal verification can be applied to CPU-side code and system call interfaces (like those used by GVisor) to guarantee an 'inescapable sandbox,' preventing agents from finding escape paths.

## Practical implications

- The methodology provides a robust way to validate AI-generated kernels, making them suitable for production use in high-stakes compute environments.
- The ability to formally verify sandboxes and system call interfaces significantly raises the security bar for running untrusted code.
- The use of Lean and SMT solvers allows for the automation of complex mathematical proofs, which is critical for handling the complexity of modern GPU architectures.

## Topics

Formal Verification, GPU Computing, AI Agents, Compiler Optimization, SMT Solvers, Lean Proof Assistants, PTX, GPU MODE

Source: https://www.youtube.com/watch?v=YquydxO9Gzk