StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915322673496064 |
|---|---|
| author | Kawamoto, Yusuke Kobayashi, Kentaro Suenaga, Kohei |
| author_facet | Kawamoto, Yusuke Kobayashi, Kentaro Suenaga, Kohei |
| contents | Statistical methods have been widely misused and misinterpreted in various scientific fields, raising significant concerns about the integrity of scientific research. To mitigate this problem, we propose a tool-assisted method for formally specifying and automatically verifying the correctness of statistical programs. In this method, programmers are required to annotate the source code of the statistical programs with the requirements for these methods. Through this annotation, they are reminded to check the requirements for statistical methods, including those that cannot be formally verified, such as the distribution of the unknown true population. Our software tool StatWhy automatically checks whether programmers have properly specified the requirements for the statistical methods, thereby identifying any missing requirements that need to be addressed. This tool is implemented using the Why3 platform to verify the correctness of OCaml programs that conduct statistical hypothesis testing. We demonstrate how StatWhy can be used to avoid common errors in various statistical hypothesis testing programs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_17492 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs Kawamoto, Yusuke Kobayashi, Kentaro Suenaga, Kohei Software Engineering Artificial Intelligence Logic in Computer Science Statistical methods have been widely misused and misinterpreted in various scientific fields, raising significant concerns about the integrity of scientific research. To mitigate this problem, we propose a tool-assisted method for formally specifying and automatically verifying the correctness of statistical programs. In this method, programmers are required to annotate the source code of the statistical programs with the requirements for these methods. Through this annotation, they are reminded to check the requirements for statistical methods, including those that cannot be formally verified, such as the distribution of the unknown true population. Our software tool StatWhy automatically checks whether programmers have properly specified the requirements for the statistical methods, thereby identifying any missing requirements that need to be addressed. This tool is implemented using the Why3 platform to verify the correctness of OCaml programs that conduct statistical hypothesis testing. We demonstrate how StatWhy can be used to avoid common errors in various statistical hypothesis testing programs. |
| title | StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs |
| topic | Software Engineering Artificial Intelligence Logic in Computer Science |
| url | https://arxiv.org/abs/2405.17492 |