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

arXiv: https://arxiv.org/abs/2208.07074 · HTML: https://mlsanity.com/paper/2208.07074/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 60 references that are in the map.
- First posted on arXiv 15 Aug 2022.

## Builds on (most cited first, 5 of 5)

- [Statistical Epistemic Logic](https://mlsanity.com/paper/1907.05995/) (2019)
- [An Epistemic Approach to the Formal Specification of Statistical Machine Learning](https://mlsanity.com/paper/2004.12734/) (2020)
- [Fifty years of Hoare's Logic](https://mlsanity.com/paper/1904.03917/) (2019)
- [Programming and Reasoning with Partial Observability](https://mlsanity.com/paper/2101.04742/) (2021)
- [Architecture-Guided Test Resource Allocation Via Logic](https://mlsanity.com/paper/2107.10948/) (2021)

## Built on by (most cited first, 3 of 3)

- [Formalizing Statistical Causality via Modal Logic](https://mlsanity.com/paper/2210.16751/) (2022)
- [StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs](https://mlsanity.com/paper/2405.17492/) (2024)
- [Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python](https://mlsanity.com/paper/2607.03951/) (2026)

## Abstract (arXiv)

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.