Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Verifying Exact Conditions for Implementations of Density Functional Approximations

Sameerah Helal, Zhe Tao, Cindy Rubio-González, Francois Gygi, Aditya V. Thakur

TL;DR

This work introduces XCVerifier, a formal-verification framework for checking whether density functional approximations (DFAs) implemented in Libxc satisfy the known exact conditions of density functional theory (DFT). It encodes DFA implementations into delta-complete first-order logic via dReal, using symbolic differentiation and domain-splitting to verify local conditions over input domains defined by $r_s$ and $s$. Across five DFAs (PBE, SCAN, LYP, AM05, VWN RPA) and seven exact conditions, XCVerifier completes 13 verifications or counterexamples and partially verifies 7 more, with 11 timeouts, highlighting both feasibility and scalability challenges—especially for SCAN. The results align largely with a prior grid-search approach (PB), supporting the viability of formal methods for DFA verification while outlining concrete directions for improving solver scalability, expanding condition coverage, and addressing numerical issues intrinsic to DFAs.

Abstract

Density Functional Theory (DFT) is used extensively in the computation of electronic properties of matter, with various applications. Approximating the exchange-correlation (XC) functional is the key to the Kohn-Sham DFT approach, the basis of most DFT calculations. The choice of this density functional approximation (DFA) depends crucially on the particular system under study, which has resulted in the development of hundreds of DFAs. Though the exact density functional is not known, researchers have discovered analytical properties of this exact functional. Furthermore, these exact conditions are used when designing DFAs. We present XCVerifier, the first approach for verifying whether a DFA implementation satisfies the DFT exact conditions. XCVerifier was evaluated on five DFAs from the popular Libxc library and seven exact conditions from recent work. XCVerifier was able to verify or find violations for a majority of the DFA/condition pairs, demonstrating the feasibility of using formal methods to verify DFA implementations.

Towards Verifying Exact Conditions for Implementations of Density Functional Approximations

TL;DR

This work introduces XCVerifier, a formal-verification framework for checking whether density functional approximations (DFAs) implemented in Libxc satisfy the known exact conditions of density functional theory (DFT). It encodes DFA implementations into delta-complete first-order logic via dReal, using symbolic differentiation and domain-splitting to verify local conditions over input domains defined by and . Across five DFAs (PBE, SCAN, LYP, AM05, VWN RPA) and seven exact conditions, XCVerifier completes 13 verifications or counterexamples and partially verifies 7 more, with 11 timeouts, highlighting both feasibility and scalability challenges—especially for SCAN. The results align largely with a prior grid-search approach (PB), supporting the viability of formal methods for DFA verification while outlining concrete directions for improving solver scalability, expanding condition coverage, and addressing numerical issues intrinsic to DFAs.

Abstract

Density Functional Theory (DFT) is used extensively in the computation of electronic properties of matter, with various applications. Approximating the exchange-correlation (XC) functional is the key to the Kohn-Sham DFT approach, the basis of most DFT calculations. The choice of this density functional approximation (DFA) depends crucially on the particular system under study, which has resulted in the development of hundreds of DFAs. Though the exact density functional is not known, researchers have discovered analytical properties of this exact functional. Furthermore, these exact conditions are used when designing DFAs. We present XCVerifier, the first approach for verifying whether a DFA implementation satisfies the DFT exact conditions. XCVerifier was evaluated on five DFAs from the popular Libxc library and seven exact conditions from recent work. XCVerifier was able to verify or find violations for a majority of the DFA/condition pairs, demonstrating the feasibility of using formal methods to verify DFA implementations.
Paper Structure (18 sections, 13 equations, 3 figures, 2 tables, 1 algorithm)

This paper contains 18 sections, 13 equations, 3 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Exact Conditions in DFT
  3. XCVerifier
  4. XCEncoder
  5. Verifier
  6. Experimental Results
  7. Experimental Setup
  8. Verifying Local Conditions using XCVerifier
  9. Comparing XCVerifier to PB
  10. Related Work
  11. Analysis of Density Functional Theory Approximations
  12. Correctness in High Performance Computing
  13. Analysis of Floating-Point Programs
  14. Discussion
  15. Improving Scalability of the Solver
  16. ...and 3 more sections

Figures (3)

  • Figure 1: Regions where the PBE functional satisfies or violates conditions according to PB (top) and XCVerifier (bottom). For PB: (region hatched) is a counterexample to the condition, is a point that satisfies the condition. For XCVerifier: is a region that contains a counterexample marked with ×, is a region that is verified to satisfy the condition, indicates a timeout, and indicates an inconclusive result.
  • Figure 2: Regions where the LYP functional satisfies or violates conditions according to PB (top) and XCVerifier (bottom). For PB: (region hatched) is a counterexample to the condition, is a point that satisfies the condition. For XCVerifier: is a region that contains a counterexample marked with ×, is a region that is verified to satisfy the condition, indicates a timeout, and indicates an inconclusive result.
  • Figure : Verifier(input domain $D$, formula $\psi$)