2024/05/25 by Yusuke Kawamoto, K. Kobayashi, Kawamoto, Yusuke +3
Computer Science · Decision Sciences · #Advanced Database Systems and Queries #Artificial Intelligence (cs.AI) #Bayesian Modeling and Causal Inference #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Scientific Computing and Data Management #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.2405.17492
openalex publication_date 2024/05/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.