Summary
Tensor contraction sequences are foundational computations in quantum chemistry, quantum physics, and materials science. As these workloads grow in scale and complexity, scientists increasingly rely on optimization techniques — mixed precision, reordering, and fusion — to reduce runtime and memory costs. While effective, these optimizations can introduce subtle numerical errors that are difficult to detect and that erode confidence in scientific results. The project's novelties are a scalable formal verification framework for optimized tensor contraction sequences and a principled method for c
