论文标题
统计假设测试计划的声音和相对完整的信念Hoare逻辑
Sound and Relatively Complete Belief Hoare Logic for Statistical Hypothesis Testing Programs
论文作者
论文摘要
我们提出了一种新方法，以正式描述统计推断的要求，并检查程序是否适当使用统计方法。具体而言，我们定义了信仰Hoare逻辑（BHL），以形式化和推理通过假设检验获得的统计信念。对于假设检验的Kripke模型，此程序逻辑是合理的，并且相对完成。我们通过示例证明，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.
