Search Results

Documents authored by Sato, Tetsuya

Document
DOI: 10.4230/LIPIcs.ITP.2023.18
Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL

Authors: Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

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.
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{hirata_et_al:LIPIcs.ITP.2023.18,
  author =	{Hirata, Michikazu and Minamide, Yasuhiko and Sato, Tetsuya},
  title =	{{Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{18:1--18:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.18},
  URN =		{urn:nbn:de:0030-drops-183933},
  doi =		{10.4230/LIPIcs.ITP.2023.18},
  annote =	{Keywords: Higher-order probabilistic program, s-finite kernel, Quasi-Borel spaces, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.102
*-Liftings for Differential Privacy

Authors: Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, and Pierre-Yves Strub

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
Recent developments in formal verification have identified approximate liftings (also known as approximate couplings) as a clean, compositional abstraction for proving differential privacy. There are two styles of definitions for this construction. Earlier definitions require the existence of one or more witness distributions, while a recent definition by Sato uses universal quantification over all sets of samples. These notions have different strengths and weaknesses: the universal version is more general than the existential ones, but the existential versions enjoy more precise composition principles. We propose a novel, existential version of approximate lifting, called *-lifting, and show that it is equivalent to Sato's construction for discrete probability measures. Our work unifies all known notions of approximate lifting, giving cleaner properties, more general constructions, and more precise composition theorems for both styles of lifting, enabling richer proofs of differential privacy. We also clarify the relation between existing definitions of approximate lifting, and generalize our constructions to approximate liftings based on f-divergences.
Cite as

Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, and Pierre-Yves Strub. *-Liftings for Differential Privacy. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 102:1-102:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{barthe_et_al:LIPIcs.ICALP.2017.102,
  author =	{Barthe, Gilles and Espitau, Thomas and Hsu, Justin and Sato, Tetsuya and Strub, Pierre-Yves},
  title =	{{*-Liftings for Differential Privacy}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{102:1--102:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.102},
  URN =		{urn:nbn:de:0030-drops-74358},
  doi =		{10.4230/LIPIcs.ICALP.2017.102},
  annote =	{Keywords: Differential Privacy, Probabilistic Couplings, Formal Verification}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.156
Codensity Liftings of Monads

Authors: Shin-ya Katsumata and Tetsuya Sato

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract
We introduce a method to lift monads on the base category of a fibration to its total category using codensity monads. This method, called codensity lifting, is applicable to various fibrations which were not supported by the categorical >>-lifting. After introducing the codensity lifting, we illustrate some examples of codensity liftings of monads along the fibrations from the category of preorders, topological spaces and extended psuedometric spaces to the category of sets, and also the fibration from the category of binary relations between measurable spaces. We next study the liftings of algebraic operations to the codensity-lifted monads. We also give a characterisation of the class of liftings (along posetal fibrations with fibred small limits) as a limit of a certain large diagram.
Cite as

Shin-ya Katsumata and Tetsuya Sato. Codensity Liftings of Monads. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 156-170, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{katsumata_et_al:LIPIcs.CALCO.2015.156,
  author =	{Katsumata, Shin-ya and Sato, Tetsuya},
  title =	{{Codensity Liftings of Monads}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{156--170},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.156},
  URN =		{urn:nbn:de:0030-drops-55329},
  doi =		{10.4230/LIPIcs.CALCO.2015.156},
  annote =	{Keywords: Monads, Lifting, Fibration, Giry Monad}
}
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