Program logic for higher-order probabilistic programs in Isabelle/HOL. (English) Zbl 07570114
Hanus, Michael (ed.) et al., Functional and logic programming. 16th international symposium, FLOPS 2022, Kyoto, Japan, May 10–12, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13215, 57-74 (2022).
Summary: The verification framework PPV (Probabilistic Program Verification) verifies functional probabilistic programs supporting higher-order functions, continuous distributions, and conditional inference. PPV is based on the theory of quasi-Borel spaces which is introduced to give a semantics of higher-order probabilistic programming languages with continuous distributions. In this paper, we formalize a theory of quasi-Borel spaces and a core part of PPV in Isabelle/HOL. We first construct a probability monad on quasi-Borel spaces based on the Giry monad in the Isabelle/HOL library. Our formalization of PPV is extended so that integrability of functions can be discussed formally. Finally, we prove integrability and convergence of the Monte Carlo approximation in our mechanized PPV.
For the entire collection see [Zbl 1492.68018].
For the entire collection see [Zbl 1492.68018].
Keywords:
higher-order probabilistic programming language; program logic; formal verification; Isabelle/HOLSoftware:
Density Compiler; Church; Quasi-Borel Spaces; mathlib; pGCL; ML; Lifting; Transfer; Archive Formal Proofs; PVS; Isabelle/HOL; Lean; HOL; CoqReferences:
| [1] | Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Strub, P.Y.: A relational logic for higher-order programs. Proc. ACM Program. Lang. 1(ICFP) (2017). doi:10.1145/3110265 |
| [2] | Audebaud, P.; Paulin-Mohring, C.; Uustalu, T., Proofs of randomized algorithms in Coq, Mathematics of Program Construction, 49-68 (2006), Heidelberg: Springer, Heidelberg · Zbl 1235.68325 · doi:10.1007/11783596_6 |
| [3] | Aumann, RJ, Borel structures for function spaces, Ill. J. Math., 5, 4, 614-630 (1961) · Zbl 0101.28401 · doi:10.1215/ijm/1255631584 |
| [4] | Avigad, J.; Hölzl, J.; Serafin, L., A formally verified proof of the central limit theorem, J. Autom. Reason., 59, 4, 389-423 (2017) · Zbl 1425.68369 · doi:10.1007/s10817-017-9404-x |
| [5] | Bagnall, A., Stewart, G.: Certifying the true error: machine learning in Coq with verified generalization guarantees. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 33, pp. 2662-2669 (2019). doi:10.1609/aaai.v33i01.33012662 |
| [6] | Bertot, Y.; Castéran, P., Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (2013), Heidelberg: Springer, Heidelberg · Zbl 1069.68095 |
| [7] | Boldo, S., Clément, F., Faissole, F., Martin, V., Mayero, M.: A Coq formalization of Lebesgue integration of nonnegative functions. Research Report RR-9401, Inria, France (2021). https://hal.inria.fr/hal-03194113 |
| [8] | Cock, D., Verifying probabilistic correctness in Isabelle with pGCL, Electron. Proc. Theor. Comput. Sci., 102, 167-178 (2012) · doi:10.4204/eptcs.102.15 |
| [9] | de Bruijn, N., Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem, Indagationes Mathematicae (Proceedings), 75, 5, 381-392 (1972) · Zbl 0253.68007 · doi:10.1016/1385-7258(72)90034-0 |
| [10] | Eberl, M.; Hölzl, J.; Nipkow, T.; Vitek, J., A verified compiler for probability density functions, Programming Languages and Systems, 80-104 (2015), Heidelberg: Springer, Heidelberg · Zbl 1335.68037 · doi:10.1007/978-3-662-46669-8_4 |
| [11] | Giry, M.; Banaschewski, B., A categorical approach to probability theory, Categorical Aspects of Topology and Analysis, 68-85 (1982), Heidelberg: Springer, Heidelberg · Zbl 0486.60034 · doi:10.1007/BFb0092872 |
| [12] | Goodman, N.D., et al.: Church: a language for generative models. In: Proceedings of the 24th Conference in Uncertainty in Artificial Intelligence, UAI 2008, pp. 220-229. AUAI Press (2008) |
| [13] | Gordon, M.J.C., Melham, T.F.: Introduction to HOL (A Theorem Proving Environment for Higher Order Logic). Cambridge University Press (1993) · Zbl 0779.68007 |
| [14] | Harrison, J., The HOL Light theory of Euclidean space, J. Autom. Reason., 50, 173-190 (2013) · Zbl 1260.68373 · doi:10.1007/s10817-012-9250-9 |
| [15] | Heunen, C., Kammar, O., Staton, S., Yang, H.: A convenient category for higher-order probability theory. In: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017. IEEE Press (2017). doi:10.1109/lics.2017.8005137 · Zbl 1458.60005 |
| [16] | Hirata, M., Minamide, Y., Sato, T.: Quasi-Borel spaces. Archive of Formal Proofs (2022). https://isa-afp.org/entries/Quasi_Borel_Spaces.html. Formal proof development |
| [17] | Hölzl, J.: Markov processes in Isabelle/HOL. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp. 100-111. Association for Computing Machinery (2017). doi:10.1145/3018610.3018628 · Zbl 1425.68375 |
| [18] | Hölzl, J.; Heller, A.; van Eekelen, M.; Geuvers, H.; Schmaltz, J.; Wiedijk, F., Three chapters of measure theory in Isabelle/HOL, Interactive Theorem Proving, 135-151 (2011), Heidelberg: Springer, Heidelberg · Zbl 1342.68287 · doi:10.1007/978-3-642-22863-6_12 |
| [19] | Huffman, B.; Kunčar, O.; Gonthier, G.; Norrish, M., Lifting and transfer: a modular design for quotients in Isabelle/HOL, Certified Programs and Proofs, 131-146 (2013), Cham: Springer, Cham · Zbl 1426.68284 · doi:10.1007/978-3-319-03545-1_9 |
| [20] | Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci. 346(1), 96-112 (2005). doi:10.1016/j.tcs.2005.08.005. Quantitative Aspects of Programming Languages (QAPL 2004) · Zbl 1080.68063 |
| [21] | Lester, D.R.: Topology in PVS: continuous mathematics with applications. In: Proceedings of the Second Workshop on Automated Formal Methods, pp. 11-20. AFM, Association for Computing Machinery (2007). doi:10.1145/1345169.1345171 |
| [22] | Lochbihler, A.; Thiemann, P., Probabilistic functions and cryptographic oracles in higher order logic, Programming Languages and Systems, 503-531 (2016), Heidelberg: Springer, Heidelberg · Zbl 1335.68033 · doi:10.1007/978-3-662-49498-1_20 |
| [23] | Mathematical Components. https://math-comp.github.io. Accessed 12 Dec 2021 |
| [24] | Mhamdi, T., Hasan, O., Tahar, S.: Formalization of measure theory and Lebesgue integration for probabilistic analysis in HOL. ACM Trans. Embed. Comput. Syst. 12(1) (2013). doi:10.1145/2406336.2406349 · Zbl 1291.68362 |
| [25] | Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55-92 (1991). doi:10.1016/0890-5401(91)90052-4. Selections from 1989 IEEE Symposium on Logic in Computer Science · Zbl 0723.68073 |
| [26] | de Moura, L.; Kong, S.; Avigad, J.; van Doorn, F.; von Raumer, J.; Felty, AP; Middeldorp, A., The lean theorem prover (system description), Automated Deduction - CADE-25, 378-388 (2015), Cham: Springer, Cham · Zbl 1465.68279 · doi:10.1007/978-3-319-21401-6_26 |
| [27] | Nipkow, T.; Wenzel, M.; Paulson, LC, Isabelle/HOL: A Proof Assistant for Higher-Order Logic (2002), Heidelberg: Springer, Heidelberg · Zbl 0994.68131 · doi:10.1007/3-540-45949-9 |
| [28] | Sato, T., Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Hsu, J.: Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization. Proc. ACM Program. Lang. 3(POPL), 1-30 (2019). doi:10.1145/3290351 |
| [29] | Ścibior, A., et al.: Denotational validation of higher-order Bayesian inference. Proc. ACM Program. Lang. 2(POPL) (2017). doi:10.1145/3158148 |
| [30] | The mathlib community: the lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 367-381. Association for Computing Machinery (2020). doi:10.1145/3372885.3373824 |
| [31] | Tristan, J.B., Tassarotti, J., Vajjha, K., Wick, M.L., Banerjee, A.: Verification of ML systems via reparameterization (2020). https://arxiv.org/abs/2007.06776 |
| [32] | Wood, F., van de Meent, J.W., Mansinghka, V.: A new approach to probabilistic programming inference. In: Proceedings of the 17th International Conference on Artificial Intelligence and Statistics, pp. 1024-1032 (2014) |
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.
