StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs

TL;DR

StatWhy is a formal verification tool designed to ensure correctness in statistical hypothesis testing programs by automatically checking programmer annotations and requirements, thereby reducing misuse and errors in scientific research.

Contribution

The paper introduces StatWhy, a novel tool that uses formal verification to validate statistical programs' correctness through annotations, addressing a critical gap in statistical software reliability.

Findings

StatWhy successfully verifies correctness of OCaml-based statistical programs.

The tool identifies missing or incorrect requirements in statistical code.

Application examples show reduction of common statistical errors.

Abstract

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.