要約
統計的手法は、様々な科学分野において広く誤用され、誤った解釈をされており、科学研究の完全性に重大な懸念を引き起こしている。この問題を軽減するために、我々は統計プログラムの正しさを正式に規定し、自動的に検証する新しい方法を提案する。この手法では、プログラマは統計プログラムのソースコードに、これらの手法に対する要求事項を注釈することが求められる。このアノテーションを通じて、未知の真の母集団の分布のような形式的に検証できないものも含め、統計手法の要件をチェックするよう注意を喚起する。我々のソフトウェアツールStatWhyは、プログラマーが統計手法の要件を適切に指定しているかどうかを自動的にチェックし、それによって対処すべき要件の欠落を特定する。このツールは、統計的仮説検定を行うOCamlプログラムの正しさを検証するために、Why3プラットフォームを使用して実装されている。StatWhyを使用することで、様々な一般的な統計的仮説検定プログラムにおける一般的なエラーを回避できることを実証する。
要約(オリジナル)
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 new 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 popular statistical hypothesis testing programs.
arxiv情報
| 著者 | Yusuke Kawamoto,Kentaro Kobayashi,Kohei Suenaga |
| 発行日 | 2024-11-01 16:16:45+00:00 |
| arxivサイト | arxiv_id(pdf) |