CS Compiler Seminar: Naifeng Zhang, "Semantics Lifting for Legacy Code Modernization and AI-Generated Code Verification."

Abstract: Modern compilers and code generation systems excel at lowering high-level specifications into optimized implementations, while the reverse direction, recovering high-level semantics from low-level code, remains relatively unexplored. This talk presents semantics lifting, a stepwise approach for recovering mathematical structure and program intent from low-level numerical kernels. Our framework is based on the key insight that many mathematics-based code generation rules express equivalences between representations and can therefore be applied in reverse. Building on this insight, we combine program analysis techniques such as symbolic execution with the reversal of mathematics-based rewrite rules to progressively lift implementations toward high-level specifications. For this talk, we focus on fast Fourier transform kernels as a case study to demonstrate how semantics lifting can enable legacy code modernization by recovering the high-level specifications needed to retarget existing implementations to new architectures, while also providing a principled approach to verifying the semantic correctness of complex AI-generated code.

Speaker Bio.: Naifeng Zhang is a final-year Ph.D. candidate in Electrical and Computer Engineering at Carnegie Mellon University, advised by Professor Franz Franchetti. His research focuses on mathematics-based code generation and reasoning for high-performance computational kernels. His work has been recognized with awards at PLDI and CGO. He received USC Provost’s Research Fellowship for three consecutive years and was named a Carnegie Institute of Technology Dean’s Fellow. He interned twice at NVIDIA, where his work on high-performance GPU code generation led to further development and adoption within NVIDIA Research.