Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2408.05316 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909536944652288 |
|---|---|
| author | Helal, Sameerah Tao, Zhe Rubio-González, Cindy Gygi, Francois Thakur, Aditya V. |
| author_facet | Helal, Sameerah Tao, Zhe Rubio-González, Cindy Gygi, Francois Thakur, Aditya V. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_05316 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Towards Verifying Exact Conditions for Implementations of Density Functional Approximations Helal, Sameerah Tao, Zhe Rubio-González, Cindy Gygi, Francois Thakur, Aditya V. Materials Science Logic in Computer Science 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. |
| title | Towards Verifying Exact Conditions for Implementations of Density Functional Approximations |
| topic | Materials Science Logic in Computer Science |
| url | https://arxiv.org/abs/2408.05316 |