Tatva: Formally Verifying AI-Generated GPU Kernels

While LLM-based kernel generators automate the synthesis of AI kernels for heterogeneous accelerators, standard numerical testing can miss critical structural errors, such as silently omitted intermediate operations. We introduce Tatva, a semantic equivalence checker that formally verifies tensor programs at the PyTorch/Triton boundary, where their high-level computational semantics remain explicit. Given an unoptimized PyTorch baseline and an optimized candidate, Tatva lowers both programs to a common Directed Acyclic Graph (DAG) representation, decomposes high-level operations into primitive mathematics, and scalarizes the computations into formulas for the Z3 SMT solver. Preliminary evaluations on KernelBench demonstrate that Tatva successfully proves equivalence for supported straight-line, loop-free kernels while identifying subtle mathematical divergences that evade standard random numerical testing.