Proving LLM-Generated GPU Kernels Correct and Safe: Floating-Point Verification in Lean and VerCors

Archibald Browne, Eugene Lee, Cristopher Salvi

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…