Verifying safety and correctness of GPU code generated by AI models
Proving LLM-Generated GPU Kernels Correct and Safe: Floating-Point Verification in Lean and VerCors
Programming Languages
Summary
Turning high-level math descriptions into fast GPU programs can cause errors and unsafe code, especially with tricky floating-point math and parallel threads. The authors study if advanced AI language models can generate these GPU programs correctly. They created a system where AI-generated GPU code is checked in detail using mathematical proof tools to ensure it matches the original description and runs safely without data conflicts. This method helps confirm that AI can write GPU code that is both correct and safe.
What this means in practice
- •For gpu software engineers: Automatically generate GPU kernels from high-level specs and verify their correctness and safety without relying on compiled tests.
- •For parallel computing developers: Ensure concurrency safety of GPU code produced by AI models by applying formal thread safety and data race verification methods.
Authors
Archibald Browne, Eugene Lee, Cristopher Salvi
Abstract
Modern statistical model development begins with a high-level specification in an automatic differentiation framework such as PyTorch, JAX, or TensorFlow, which is then lowered to a target backend by a compiler or implemented manually by a research engineer. In this paper, we study whether frontier language models can correctly perform the latter task by generating GPU kernels from high-level benchmark specifications. We introduce a framework in which a language-model agent uses Velvet, a program verifier for imperative programs embedded in Lean, to prove semantic equivalence between a high-level specification and a generated CUDA kernel under an explicit set of assumptions. It also asks the LLM to prove thread safety and data race freedom of the generated kernel in VerCors, a deductive verifier for parallel code. Our main contribution to the formal verification of LLM- generated GPU kernels is showing that a combination of Lean automation and language-model-guided proof construction can verify a broad set of basic neural- network building blocks over floating-point values, allowing LLMs to implement semantically correct and safe kernels. In our framework, floating-point verifications never rely on compiled code and are always checked via the Lean kernel.