SpringerLink
Log in

Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL

  • Conference paper
  • First Online:
Functional and Logic Programming (FLOPS 2022)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13215))

Included in the following conference series:

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now
Chapter
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 53.49
Price includes VAT (Germany)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 69.54
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    https://github.com/HirataMichi/PPV.

  2. 2.

    The original PPV also includes the relational program logic RPL. Since we have not formalized RPL, we omit the explanation of RPL.

  3. 3.

    \(\delta _x(U)\) is 1 if \(x \in U\) and 0 otherwise.

  4. 4.

    The standard Isabelle/HOL theory library includes a proof of this result: Isabelle2021-1.app/src/HOL/Probability/ex/Measure_Not_CCC.thy.

  5. 5.

    We choose the sequence that does not include infinite sequence of 1 at the tail. That is, we choose \(0.100\dots \) rather than \(0.011\dots \) for 1/2.

  6. 6.

    Actually, the domain of \(\beta \) is not \((0,1) \times (0,1)\)since \(\beta \) maps \(0.1010\dots \) to (1, 0). In the actual proof, some modification is neededwhen constructing f and g.

  7. 7.

    Strictly speaking, is the Lebesgue measure.

  8. 8.

    It should be noted that the original proof does not include the discussion on integrability.

References

  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). https://doi.org/10.1145/3110265

  2. Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 49–68. Springer, Heidelberg (2006). https://doi.org/10.1007/11783596_6

    Chapter  MATH  Google Scholar 

  3. Aumann, R.J.: Borel structures for function spaces. Ill. J. Math. 5(4), 614–630 (1961). https://doi.org/10.1215/ijm/1255631584

    Article  MathSciNet  MATH  Google Scholar 

  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). https://doi.org/10.1007/s10817-017-9404-x

    Article  MathSciNet  MATH  Google Scholar 

  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). https://doi.org/10.1609/aaai.v33i01.33012662

  6. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2013)

    MATH  Google Scholar 

  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). https://doi.org/10.4204/eptcs.102.15

    Article  Google Scholar 

  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). https://doi.org/10.1016/1385-7258(72)90034-0

    Article  MathSciNet  MATH  Google Scholar 

  10. Eberl, M., Hölzl, J., Nipkow, T.: A verified compiler for probability density functions. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 80–104. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46669-8_4

    Chapter  Google Scholar 

  11. Giry, M.: A categorical approach to probability theory. In: Banaschewski, B. (ed.) Categorical Aspects of Topology and Analysis. LNM, vol. 915, pp. 68–85. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0092872

    Chapter  Google Scholar 

  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)

    Google Scholar 

  13. Gordon, M.J.C., Melham, T.F.: Introduction to HOL (A Theorem Proving Environment for Higher Order Logic). Cambridge University Press (1993)

    Google Scholar 

  14. Harrison, J.: The HOL Light theory of Euclidean space. J. Autom. Reason. 50, 173–190 (2013). https://doi.org/10.1007/s10817-012-9250-9

    Article  MathSciNet  MATH  Google Scholar 

  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). https://doi.org/10.1109/lics.2017.8005137

  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). https://doi.org/10.1145/3018610.3018628

  18. Hölzl, J., Heller, A.: Three chapters of measure theory in Isabelle/HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 135–151. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22863-6_12

    Chapter  Google Scholar 

  19. Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131–146. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03545-1_9

    Chapter  MATH  Google Scholar 

  20. Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci. 346(1), 96–112 (2005). https://doi.org/10.1016/j.tcs.2005.08.005. Quantitative Aspects of Programming Languages (QAPL 2004)

  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). https://doi.org/10.1145/1345169.1345171

  22. Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher order logic. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 503–531. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49498-1_20

    Chapter  MATH  Google Scholar 

  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). https://doi.org/10.1145/2406336.2406349

  25. Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991). https://doi.org/10.1016/0890-5401(91)90052-4. Selections from 1989 IEEE Symposium on Logic in Computer Science

  26. de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378–388. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_26

    Chapter  Google Scholar 

  27. Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)

    Book  Google Scholar 

  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). https://doi.org/10.1145/3290351

  29. Ścibior, A., et al.: Denotational validation of higher-order Bayesian inference. Proc. ACM Program. Lang. 2(POPL) (2017). https://doi.org/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). https://doi.org/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)

    Google Scholar 

Download references

Acknowledgments

Minamide was supported by JSPS KAKENHI Grant Number 19K11899, and Sato was supported by JSPS KAKENHI Grant Number 20K19775.

Author information

Authors and Affiliations

  1. School of Computing, Tokyo Institute of Technology, Tokyo, Japan

    Michikazu Hirata, Yasuhiko Minamide & Tetsuya Sato

Authors
  1. Michikazu Hirata
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yasuhiko Minamide
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tetsuya Sato
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Michikazu Hirata .

Editor information

Editors and Affiliations

  1. Kiel University, Kiel, Germany

    Michael Hanus

  2. Kyoto University, Kyoto, Japan

    Atsushi Igarashi

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Hirata, M., Minamide, Y., Sato, T. (2022). Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL. In: Hanus, M., Igarashi, A. (eds) Functional and Logic Programming. FLOPS 2022. Lecture Notes in Computer Science, vol 13215. Springer, Cham. https://doi.org/10.1007/978-3-030-99461-7_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-99461-7_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-99460-0

  • Online ISBN: 978-3-030-99461-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation