اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدA Domain Theory for Statistical Probabilistic Programming
117
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance datatypes. Our semantics justifies important program equivalences including commutativity. Our new semantic model is based on `quasi-Borel predomains. These are a mixture of chain-complete partial orders (cpos) and quasi-Borel spaces. Quasi-Borel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with higher order functions. By contrast, quasi-Borel predomains do support both a commutative probabilistic powerdomain and higher-order functions. As we show, quasi-Borel predomains form both a model of Fiores axiomatic domain theory and a model of Kocks synthetic measure theory.
قيم البحث
اقرأ أيضاً
The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language with primitives for sampling from discrete distributions. However, co
ntinuous distributions have to be discretized because the corresponding measures cannot be defined on all subsets of their carriers. This paper proposes the use of synthetic topology to model continuous distributions for probabilistic computations in type theory. We study the initial $sigma$-frame and the corresponding induced topology on arbitrary sets. Based on these intrinsic topologies we define valuations and lower integrals on sets, and pro
Types in logic programming have focused on conservative approximations of program semantics by regular types, on one hand, and on type systems based on a prescriptive semantics defined for typed programs, on the other. In this paper, we define a new
semantics for logic programming, where programs evaluate to true, false, and to a new semantic value called wrong, corresponding to a run-time type error. We then have a type language with a separated semantics of types. Finally, we define a type system for logic programming and prove that it is semantically sound with respect to a semantic relation between programs and types where, if a program has a type, then its semantics is not wrong. Our work follows Milners approach for typed functional languages where the semantics of programs is independent from the semantic of types, and the type system is proved to be sound with respect to a relation between both semantics.
This paper investigates the usage of generating functions (GFs) encoding measures over the program variables for reasoning about discrete probabilistic programs. To that end, we define a denotational GF-transformer semantics for probabilistic while-p
rograms, and show that it instantiates Kozens seminal distribution transformer semantics. We then study the effective usage of GFs for program analysis. We show that finitely expressible GFs enable checking super-invariants by means of computer algebra tools, and that they can be used to determine termination probabilities. The paper concludes by characterizing a class of -- possibly infinite-state -- programs whose semantics is a rational GF encoding a discrete phase-type distribution.
Pyro is a probabilistic programming language built on Python as a platform for developing advanced probabilistic models in AI research. To scale to large datasets and high-dimensional models, Pyro uses stochastic variational inference algorithms and
probability distributions built on top of PyTorch, a modern GPU-accelerated deep learning framework. To accommodate complex or model-specific algorithmic behavior, Pyro leverages Poutine, a library of composable building blocks for modifying the behavior of probabilistic programs.
A major trend in academia and data science is the rapid adoption of Bayesian statistics for data analysis and modeling, leading to the development of probabilistic programming languages (PPL). A PPL provides a framework that allows users to easily sp
ecify a probabilistic model and perform inference automatically. PyAutoFit is a Python-based PPL which interfaces with all aspects of the modeling (e.g., the model, data, fitting procedure, visualization, results) and therefore provides complete management of every aspect of modeling. This includes composing high-dimensionality models from individual model components, customizing the fitting procedure and performing data augmentation before a model-fit. Advanced features include database tools for analysing large suites of modeling results and exploiting domain-specific knowledge of a problem via non-linear search chaining. Accompanying PyAutoFit is the autofit workspace (see https://github.com/Jammy2211/autofit_workspace), which includes example scripts and the HowToFit lecture series which introduces non-experts to model-fitting and provides a guide on how to begin a project using PyAutoFit. Readers can try PyAutoFit right now by going to the introduction Jupyter notebook on Binder (see https://mybinder.org/v2/gh/Jammy2211/autofit_workspace/HEAD) or checkout our readthedocs(see https://pyautofit.readthedocs.io/en/latest/) for a complete overview of PyAutoFits features.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
