Collaborative Research: CS2: Formally Verified and Performance-Optimized Tensor Contraction Sequences in Quantum Many-Body Computations

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 connecting correctness guarantees directly with performance optimization. The project's impacts are more reliable and reproducible scientific computing, open-source tooling for the broader high-performance computing (HPC) and formal methods communities, and interdisciplinary training opportunities that bridge formal verification, numerical analysis, and high-performance computing. This project develops a scalable, sound, and precision-aware formal verification framework for reasoning about optimized tensor contraction sequences under interacting optimization strategies. The project creates automated modeling and property-checking methods for mixed-precision tensor contraction sequences using domain-specific satisfiability modulo theories (SMT) encodings in quantifier-free floating point (QF_FP), automated formula generation, and counterexample-guided abstraction refinement. It extends verification to contraction-order optimization and fusion through incremental SMT solving with solver-state reuse, portfolio-based solving, and equality-saturation methods that preserve tight numerical bounds. The project further integrates verification into multi-objective design space exploration, using interaction-aware analysis and graph-based performance–error optimization to identify Pareto-optimal implementations across FLOP count, memory usage, and verified numerical error. The expected result is a practical methodology for discovering tensor contraction implementations that are both high-performance and provably correct for mission-critical scientific workloads. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria. NSF Award ID: 2546786 | Program: 01002627DB NSF RESEARCH & RELATED ACTIVIT | Principal Investigator: Cunxi Yu | Institution: University of Maryland, College Park, COLLEGE PARK, MD | Award Amount: $266,000 View on NSF Award Search: https://www.nsf.gov/awardsearch/show-award/?AWD_ID=2546786 View on Research.gov: https://www.research.gov/awardapi-service/v1/awards/2546786.html