Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs. (English) Zbl 1532.68105
Summary: 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.
MSC:
| 68T27 | Logic in artificial intelligence |
| 03B42 | Logics of knowledge and belief (including belief change) |
| 03B70 | Logic in computer science |
| 62A01 | Foundations and philosophical topics in statistics |
Keywords:
knowledge representation; epistemic logic; program logic; Kripke model; statistical hypothesis testingReferences:
| [1] | Lang, T. A.; Altman, D. G., Statistical Analyses and Methods in the Published Literature: The SAMPL Guidelines, 264-274 (2014), John Wiley & Sons, Ltd, Ch. 25 |
| [2] | Wasserstein, R. L.; Lazar, N. A., The ASA statement on p-values: context, process, and purpose. Am. Stat., 2, 129-133 (2016) · Zbl 07665862 |
| [3] | Kawamoto, Y.; Sato, T.; Suenaga, K., Formalizing statistical beliefs in hypothesis testing using program logic, 411-421 |
| [4] | Hoare, C. A.R., An axiomatic basis for computer programming. Commun. ACM, 10, 576-580 (1969) · Zbl 0179.23105 |
| [5] | Winskel, G., The Formal Semantics of Programming Languages—An Introduction (1993), The MIT Press · Zbl 0919.68082 |
| [6] | Apt, K. R.; Olderog, E., Fifty years of hoare’s logic. Form. Asp. Comput., 6, 751-807 (2019) · Zbl 1427.68008 |
| [7] | Reynolds, J. C., Separation logic: a logic for shared mutable data structures, 55-74 |
| [8] | Suenaga, K.; Hasuo, I., Programming with infinitesimals: a while-language for hybrid system modeling, 392-403 · Zbl 1333.68181 |
| [9] | den Hartog, J.; de Vink, E. P., Verifying probabilistic programs using a Hoare like logic. Int. J. Found. Comput. Sci., 3, 315-340 (2002) · Zbl 1066.68081 |
| [10] | Atkinson, E.; Carbin, M., Programming and reasoning with partial observability. Proc. ACM Program. Lang., OOPSLA, 200:1-200:28 (2020) |
| [11] | von Wright, G. H., An Essay in Modal Logic (1951), North-Holland Pub. Co.: North-Holland Pub. Co. Amsterdam · Zbl 0043.00701 |
| [12] | Hintikka, J., Knowledge and Belief: An Introduction to the Logic of the Two Notions (1962), Cornell University Press |
| [13] | Fagin, R.; Halpern, J.; Moses, Y.; Vardi, M., Reasoning About Knowledge (1995), The MIT Press · Zbl 0839.68095 |
| [14] | Burrows, M.; Abadi, M.; Needham, R. M., A logic of authentication. ACM Trans. Comput. Syst., 1, 18-36 (1990) |
| [15] | Syverson, P. F.; Stubblebine, S. G., Group principals and the formalization of anonymity, 814-833 · Zbl 0948.94013 |
| [16] | Garcia, F. D.; Hasuo, I.; Pieters, W.; van Rossum, P., Provable anonymity, 63-72 |
| [17] | Halpern, J. Y., Reasoning About Uncertainty (2003), The MIT Press · Zbl 1090.68105 |
| [18] | Huber, F.; Schmidt-Petri, C., Degrees of Belief, vol. 342 (2008), Springer Science & Business Media |
| [19] | Bacchus, F.; Halpern, J. Y.; Levesque, H. J., Reasoning about noisy sensors and effectors in the situation calculus. Artif. Intell., 1-2, 171-208 (1999) · Zbl 0996.68192 |
| [20] | Kawamoto, Y., Statistical epistemic logic, 344-362 |
| [21] | Kawamoto, Y., Towards logical specification of statistical machine learning, 293-311 · Zbl 1535.68265 |
| [22] | Kawamoto, Y., An epistemic approach to the formal specification of statistical machine learning. Softw. Syst. Model., 2, 293-310 (2020) |
| [23] | Van Ditmarsch, H.; van Der Hoek, W.; Kooi, B., Dynamic Epistemic Logic, vol. 337 (2007), Springer Science & Business Media · Zbl 1156.03320 |
| [24] | Zadeh, L., Fuzzy sets. Inf. Control, 3, 338-353 (1965) · Zbl 0139.24606 |
| [25] | Nguyen, H. T.; Walker, C. L.; Walker, E. A., A First Course in Fuzzy Logic (2018), Chapman & Hall/CRC · Zbl 1405.03001 |
| [26] | Eberhart, C.; Yamada, A.; Klikovits, S.; Katsumata, S.; Kobayashi, T.; Hasuo, I.; Ishikawa, F., Architecture-guided test resource allocation via logic, 22-38 · Zbl 1489.68043 |
| [27] | Reiter, R., A logic for default reasoning. Artif. Intell., 1-2, 81-132 (1980) · Zbl 0435.68069 |
| [28] | Jr., H. E.K.; Teng, C., Evaluating defaults, 257-264 |
| [29] | Jr., H. E.K.; Teng, C., Nonmonotonic logic and statistical inference. Comput. Intell., 1, 26-51 (2006) |
| [30] | Jr., H. E.K.; Teng, C., Statistical inference as default reasoning. Int. J. Pattern Recognit. Artif. Intell., 2, 267-283 (1999) |
| [31] | Fagin, R.; Halpern, J. Y.; Moses, Y.; Vardi, M. Y., Knowledge-based programs, 153-163 · Zbl 1374.68102 |
| [32] | Laverny, N.; Lang, J., From knowledge-based programs to graded belief-based programs, part I: on-line reasoning*. Synth., 2, 277-321 (2005) · Zbl 1085.68163 |
| [33] | Sardiña, S.; Lespérance, Y., Golog speaks the BDI language, 82-99 · Zbl 1341.68025 |
| [34] | Levesque, H. J.; Reiter, R.; Lespérance, Y.; Lin, F.; Scherl, R. B., GOLOG: a logic programming language for dynamic domains. J. Log. Program., 1-3, 59-83 (1997) · Zbl 0880.68008 |
| [35] | Bratman, M., Intention, Plans, and Practical Reason (1987) |
| [36] | Belle, V.; Levesque, H. J., ALLEGRO: belief-based programming in stochastic dynamical domains, 2762-2769 |
| [37] | Hogg, R. V.; McKean, J. W.; Craig, A. T., Introduction to Mathematical Statistics (2004), Prentice Hall |
| [38] | Kanji, G. K., 100 Statistical Tests (2006), Sage |
| [39] | Bretz, F.; Hothorn, T.; Westfall, P., Multiple Comparisons Using R (2010), Chapman and Hall/CRC |
| [40] | Nielson, H. R.; Nielson, F. |
| [41] | Cook, S. A., Soundness and completeness of an axiom system for program verification. SIAM J. Comput., 1, 70-90 (1978) · Zbl 0374.68009 |
| [42] | Platzer, A., Logical Foundations of Cyber-Physical Systems (2018), Springer · Zbl 1400.93003 |
| [43] | Hähnle, R.; Huisman, M., Deductive software verification: from pen-and-paper proofs to industrial tools, 345-373 · Zbl 1482.68139 |
| [44] | Kripke, S. A., The undecidability of monadic modal quantification theory. Math. Log. Q., 2, 113-116 (1962) · Zbl 0111.01101 |
| [45] | Hughes, G. E.; Cresswell, M. J., A New Introduction to Modal Logic (1996), Psychology Press · Zbl 0855.03002 |
| [46] | Sober, E., Evidence and Evolution: The Logic Behind the Science (2008), Cambridge University Press |
| [47] | Kawamoto, Y.; Sato, T.; Suenaga, K., Formalizing statistical causality via modal logic, 681-696 · Zbl 07855153 |
| [48] | Neyman, J.; Pearson, E. S., On the problem of the most efficient tests of statistical hypotheses. Philos. Trans. R. Soc. Lond., Ser. A, Contain. Pap. Math. Phys. Character, 289-337 (1933) · Zbl 0006.26804 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
