ECE Associate Professor Bo Yuan receives an NSF grant, titled “CS2: Formally Verified and Performance-Optimized Tensor Contraction Sequences in Quantum Many-Body Computations”. This project is a collaboration between Rutgers University, University of Maryland and North Carolina State University. PI Bo Yuan's share is $266K.

 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 encodings in quantifier-free floating point, 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.

More details of this project can be found https://www.nsf.gov/awardsearch/show-award?AWD_ID=2546787

Congratulations to Bo on this interesting project!