Document Open Access Logo

Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL

Authors Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.18.pdf
  • Filesize: 0.81 MB
  • 18 pages

Document Identifiers

Author Details

Michikazu Hirata
  • School of Computing, Tokyo Institute of Technology, Japan
Yasuhiko Minamide
  • School of Computing, Tokyo Institute of Technology, Japan
Tetsuya Sato
  • School of Computing, Tokyo Institute of Technology, Japan

Funding

  • Hirata, Michikazu: supported by JSPS Research Fellowships for Young Scientists and JSPS KAKENHI Grant Number 23KJ0905
  • Minamide, Yasuhiko: supported by JSPS KAKENHI Grant Number 19K11899 and 20H04162
  • Sato, Tetsuya: supported by JSPS KAKENHI Grant Number 20K19775

Cite AsGet BibTex

Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato. Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.18

Abstract

Higher-order probabilistic programs are used to describe statistical models and machine-learning mechanisms. The programming languages for them are equipped with three features: higher-order functions, sampling, and conditioning. In this paper, we propose an Isabelle/HOL library for probabilistic programs supporting all of those three features. We extend our previous quasi-Borel theory library in Isabelle/HOL. As a basis of the theory, we formalize s-finite kernels, which is considered as a theoretical foundation of first-order probabilistic programs and a key to support conditioning of probabilistic programs. We also formalize the Borel isomorphism theorem which plays an important role in the quasi-Borel theory. Using them, we develop the s-finite measure monad on quasi-Borel spaces. Our extension enables us to describe higher-order probabilistic programs with conditioning directly as an Isabelle/HOL term whose type is that of morphisms between quasi-Borel spaces. We also implement the qbs prover for checking well-typedness of an Isabelle/HOL term as a morphism between quasi-Borel spaces. We demonstrate several verification examples of higher-order probabilistic programs with conditioning.

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Mathematics of computing → Probabilistic algorithms
Keywords
  • Higher-order probabilistic program
  • s-finite kernel
  • Quasi-Borel spaces
  • Isabelle/HOL

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Reynald Affeldt, Cyril Cohen, and Ayumu Saito. Semantics of probabilistic programs using s-finite kernels in Coq. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pages 3-16, New York, NY, USA, 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3573105.3575691.
  2. Robert J. Aumann. Borel structures for function spaces. Illinois Journal of Mathematics, 5(4):614-630, 1961. URL: https://doi.org/10.1215/ijm/1255631584.
  3. Jeremy Avigad, Johannes Hölzl, and Luke Serafin. A formally verified proof of the central limit theorem. Journal of Automated Reasoning, 59(4):389-423, 2017. URL: https://doi.org/10.1007/s10817-017-9404-x.
  4. Alexander Bagnall and Gordon Stewart. Certifying the true error: Machine learning in Coq with verified generalization guarantees. Proceedings of the AAAI Conference on Artificial Intelligence, 33:2662-2669, 2019. URL: https://doi.org/10.1609/aaai.v33i01.33012662.
  5. David A. Basin, Andreas Lochbihler, and S. Reza Sefidgar, Sefidgar. CryptHOL: Game-based proofs in higher-order logic. Journal of Cryptology, 33:494-566, 2020. Google Scholar
  6. Marek Biskup. Lecture note of math245b in UCLA. https://web.archive.org/web/20210506130459/https://www.math.ucla.edu/~biskup/245b.1.20w/, 2020. Accessed: January 17. 2023.
  7. Manuel Eberl, Johannes Hölzl, and Tobias Nipkow. A verified compiler for probability density functions. In European Symposium on Programming (ESOP 2015), volume 9032 of LNCS, pages 80-104. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46669-8_4.
  8. Michèle Giry. A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis, pages 68-85, Berlin, Heidelberg, 1982. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0092872.
  9. Noah D. Goodman et al. Church: a language for generative models. In UAI 2008, Proceedings of the 24th Conference in Uncertainty in Artificial Intelligence, pages 220-229. AUAI Press, 2008. Google Scholar
  10. Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. 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. URL: https://doi.org/10.1109/lics.2017.8005137.
  11. Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato. Program logic for higher-order probabilistic programs in Isabelle/HOL. In Michael Hanus and Atsushi Igarashi, editors, Functional and Logic Programming, pages 57-74, Cham, 2022. Springer International Publishing. Google Scholar
  12. Johannes Hölzl. Markov processes in Isabelle/HOL. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 100-111. Association for Computing Machinery, 2017. URL: https://doi.org/10.1145/3018610.3018628.
  13. Johannes Hölzl, Armin Heller, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk. Three chapters of measure theory in Isabelle/HOL. In Interactive Theorem Proving, ITP 2011, pages 135-151. Springer Berlin Heidelberg, 2011. Google Scholar
  14. Cezary Kaliszyk and Christian Urban. Quotients revisited for Isabelle/HOL. In Proceedings of the 2011 ACM Symposium on Applied Computing, SAC, pages 1639-1644, New York, NY, USA, 2011. Association for Computing Machinery. URL: https://doi.org/10.1145/1982185.1982529.
  15. Ondřej Kunčar and Andrei Popescu. From types to sets by local type definitions in higher-order logic. In Jasmin Christian Blanchette and Stephan Merz, editors, Interactive Theorem Proving, pages 200-218, Cham, 2016. Springer International Publishing. Google Scholar
  16. Andreas Lochbihler. Probabilistic functions and cryptographic oracles in higher order logic. In Programming Languages and Systems, pages 503-531, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-49498-1_20.
  17. Mihails Milehins. An extension of the framework types-to-sets for Isabelle/HOL. In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022, pages 180-196, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3497775.3503674.
  18. Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, Berlin, Heidelberg, 2002. Google Scholar
  19. Andrei Popescu and Dmitriy Traytel. Admissible types-to-pers relativization in higher-order logic. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571235.
  20. Adrian Sampson. Probabilistic programming. http://adriansampson.net/doc/ppl.html. Accessed: January 25. 2023.
  21. Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Justin Hsu. Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, bayesian inference, and optimization. Proceedings of the ACM on Programming Languages, 3(POPL):1-30, 2019. URL: https://doi.org/10.1145/3290351.
  22. Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani. Denotational validation of higher-order bayesian inference. Proc. ACM Program. Lang., 2(POPL), 2017. URL: https://doi.org/10.1145/3158148.
  23. Shashi Mohan Srivastava. A Course on Borel Sets. Springer, 1998. URL: https://doi.org/10.1007/b98956.
  24. Sam Staton. Commutative semantics for probabilistic programming. In Hongseok Yang, editor, Programming Languages and Systems, pages 855-879, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg. Google Scholar
  25. Sam Staton. Probabilistic Programs as Measures, pages 43-74. Cambridge University Press, 2020. URL: https://doi.org/10.1017/9781108770750.003.
  26. Jean-Baptiste Tristan, Joseph Tassarotti, Koundinya Vajjha, Michael L. Wick, and Anindya Banerjee. Verification of ML systems via reparameterization, 2020. URL: https://arxiv.org/abs/2007.06776.
  27. Matthijs Vákár, Ohad Kammar, and Sam Staton. A domain theory for statistical probabilistic programming. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290349.
  28. Matthijs Vákár and Luke Ong. On s-finite measures and kernels, 2018. URL: https://doi.org/10.48550/ARXIV.1810.01837.
  29. Frank Wood, Jan Willem van de Meent, and Vikash Mansinghka. A new approach to probabilistic programming inference. In Proceedings of the 17th International conference on Artificial Intelligence and Statistics, pages 1024-1032, 2014. Google Scholar
  30. Hongseok Yang. Semantics of higher-order probabilistic programs with continuous distributions. https://alfa.di.uminho.pt/~nevrenato/probprogschool_slides/Hongseok.pdf. Accessed: February 8. 2023.
  31. Yizhou Zhang and Nada Amin. Reasoning about “reasoning about reasoning”: Semantics and contextual equivalence for probabilistic programs with nested queries and recursion. Proc. ACM Program. Lang., 6(POPL), January 2022. URL: https://doi.org/10.1145/3498677.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact