Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
This conference talk explores a novel approach to semantics lifting for scientific computing, focusing specifically on Fast Fourier Transform (FFT) implementations. Learn how researchers from Carnegie Mellon University and SpiralGen, Inc. address the challenges of verifying LLM-generated scientific code through a stepwise semantics lifting methodology. The presentation demonstrates how the extended SPIRAL framework, combined with symbolic execution and theorem proving, can statically derive high-level code semantics from machine-generated kernels. Discover the results of preliminary tests that successfully lifted GPT-generated FFT code to high-level specifications, establishing a structured verification path for complex scientific software where numerical stability and precise floating-point arithmetic are critical. This 17-minute talk was presented at the Theory and Practice of Static Analysis workshop on January 21, 2025, sponsored by ACM SIGPLAN.
