Sound and Relatively Complete Belief Hoare Logic for Statistical Hypothesis Testing Programs

要約

統計的推論の要件を形式的に記述し、プログラムが統計的手法を適切に使用しているかどうかをチェックするための新しいアプローチを提案します。
具体的には、仮説検定を通じて取得した統計的信念を形式化し推論するための信念ホア ロジック (BHL) を定義します。
このプログラム ロジックは健全であり、仮説検定用のクリプキ モデルに関しては比較的完全です。
BHL が仮説検証における実際的な問題について推論するのに役立つことを例によって示します。
この枠組みでは、仮説検定を通じて統計的信念を獲得する際の事前信念の重要性を明らかにし、プログラムロジックの内外での統計的推論の正当性の全体像を議論します。

要約(オリジナル)

We propose a new approach to formally describing the requirement for statistical inference and checking whether a program uses the statistical method appropriately. Specifically, we define belief Hoare logic (BHL) for formalizing and reasoning about the statistical beliefs acquired via hypothesis testing. This program logic is sound and relatively complete with respect to a Kripke model for hypothesis tests. We demonstrate by examples that BHL is useful for reasoning about practical issues in hypothesis testing. In our framework, we clarify the importance of prior beliefs in acquiring statistical beliefs through hypothesis testing, and discuss the whole picture of the justification of statistical inference inside and outside the program logic.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google