Collaborative Research: CS2: DANUBE: Formal Methods for Scientific Computing Bridging the Data-Numerics Behavior Tug-of-War

Computer simulations are central to science and engineering activities across tasks as varied as weather prediction and electrical grid optimization. Simulation relies on numerical solvers whose continued improvements in terms of speed and accuracy are of pivotal national importance. Unfortunately, the progress of solvers is hampered by two emerging challenges: (1) the problems being modeled and solved, including their data captured through matrices, are becoming numerically harder, causing many solvers to fail; (2) newer arithmetic hardware, increasingly second-purposed from those developed to support artificial intelligence (AI), ends up having suboptimal precision while also deviating from established numerical standards.

The project's novelties are: (1) the development of practical formal methods that are capable of capturing the correctness expectations of numerical algorithm designers as formal requirements; (2) the development of formal models capable of modeling non-standard hardware while bridging their behavioral differences to present uniform higher level formal abstractions; and (3) methods to carry out end-to-end correctness verification that help establish that the formal models of the underlying hardware meet the numerical algorithm correctness requirements. The project's contributions will help advance the nation's simulation-based scientific exploration capabilities.

It will also help recoup the investments already made in today's numerical solvers, allowing them to be easily and reliably adapted to new problems and hardware. Without these capabilities, scientific computing and data-enabled discoveries can experience multiple productivity gaps, negatively impacting scientific research and engineering advances. The project will also train students to have the debugging skills necessary to solve numerical issues arising in the context of future solver design and deployment.

This project handles data hardness using iterative refinement algorithms that are followed by the linear algebra routines underlying linear solvers. These algorithms can be verifiably guarded by novel formal properties that stem from how the problem eigenvalues appear in the problem’s data matrices. This project's techniques adapt the numerical hardware to pre-existing solvers (and their assumptions) and help develop new solvers that employ mixed numerical precision schemes during iterative refinement.

These adaptations will be aided by novel emulation schemes that help match and formally verify numerical precision, rounding rules, and floating-point exception handling rules. The goals of these techniques are to resolve the "Data/Numerics Tug of War" so that each solver developer obtains their preferred starting point: from algorithms down to hardware or vice-versa.

This project will contribute key scientific principles and algorithms to support future research and development activities in adapting solvers to newer hardware. It will have a broad impact, including (1) sustain established solvers across new generations of hardware and (2) solve numerical issues that arise when solvers and optimizers used in AI are enhanced to handle larger scale and newer problems.

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.