Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL-猫眼课题宝

DOI：

10.4230/lipics.itp.2023.18

发表时间：

2023

期刊：

影响因子：

通讯作者：

中科院分区：

其他

文献类型：

作者：

Michikazu Hirata;Yasuhiko Minamide;Tetsuya Sato

高阶概率程序用于描述统计模型和机器学习机制。它们的编程语言有三个特点：高阶函数、采样和条件。在本文中，我们提出了一个Isabelle/HOL库支持所有这三个功能的概率程序。我们扩展了我们以前的准Borel理论库Isabelle/HOL。作为该理论的基础，我们形式化了s-有限核，它被认为是一阶概率规划的理论基础，也是支持概率规划条件化的关键。我们还形式化了在拟Borel理论中起着重要作用的Borel同构定理。利用它们，我们发展了拟Borel空间上的s-有限测度单子。我们的扩展使我们能够描述高阶概率程序的条件直接作为一个Isabelle/HOL长期的类型是准Borel空间之间的态射。我们还实现了qbs证明器检查良好的Isabelle/HOL长期准Borel空间之间的态射的类型。我们展示了几个验证的例子高阶概率程序与条件

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

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

文献摘要

相似文献