CS2: Provably Correct Implementations of Density Functional Approximations

Density Functional Theory (DFT) is a phenomenally successful approach to finding approximate solutions to the Schrodinger equation, the fundamental equation that describes the quantum behavior of atoms and molecules. The fundamental results of Kohn, Hohenberg, and Sham showed that the ground-state energy from the Schrodinger equation is a unique functional of the electron density and subsequently reduced solving a complicated many-body problem to finding a consistent solution to a set of single-particle equations. However, the exact density functional is not known and scientists have developed hundreds of density functional approximations (DFAs). Choosing a DFA is perhaps the most important decision when performing a DFT calculation. The project's novelties are in using formal methods to ensure that the implementation of a DFA is provably correct. DFT calculations are widely used in a number of scientific and engineering fields, including solid state physics, computational chemistry, and materials science. Consequently, the project's impacts are in improving the correctness of scientific software in these application domains. The key insight of the project is that each DFA is a mathematical function with a known, albeit complicated, analytical form, and, hence, can be analyzed using formal-methods techniques such as Satisfiability Modulo Theory (SMT) solvers. The project will automatically verify whether a DFA implementation satisfies DFT exact conditions (known analytical properties of the exact functional). The project will automatically verify numerical properties of a DFA implementation (generation of Not a Number (NaN) and infinities, and numerical instabilities slowing down convergence). The project will develop techniques to generate provably correct minimal edits to a DFA implementation that are guaranteed to be numerically stable and continue to satisfy the same exact conditions. By analyzing existing DFAs and developing new DFAs, the project will have tremendous impact in a number of scientific and engineering fields. 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.