Conditioning in Probabilistic Programming

Nils Jansen, Benjamin Lucien Kaminski, Joost Pieter Katoen, Federico Olmedo, Friedrich Gretz, Annabelle McIver

Research output: Contribution to journalConference paperResearchpeer-review

Abstract

In this paper, we investigate the semantic intricacies of conditioning in probabilistic programming, a major feature, e.g., in machine learning. We provide a quantitative weakest pre-condition semantics. In contrast to all other approaches, non-termination is taken into account by our semantics. We also present an operational semantics in terms of Markov models and show that expected rewards coincide with quantitative pre-conditions. A program transformation that entirely eliminates conditioning from programs is given; the correctness is shown using our semantics. Finally, we show that an inductive semantics for conditioning in non-deterministic probabilistic programs cannot exist.

Fingerprint

Probabilistic Programming
Computer programming
Conditioning
Semantics
Precondition
Program Transformation
Operational Semantics
Reward
Markov Model
Correctness
Machine Learning
Eliminate
Learning systems

Cite this

Jansen, Nils ; Kaminski, Benjamin Lucien ; Katoen, Joost Pieter ; Olmedo, Federico ; Gretz, Friedrich ; McIver, Annabelle. / Conditioning in Probabilistic Programming. In: Electronic Notes in Theoretical Computer Science. 2015 ; Vol. 319. pp. 199-216.
@article{67b6ae38f3f84b6985e3ca45b39673fe,
title = "Conditioning in Probabilistic Programming",
abstract = "In this paper, we investigate the semantic intricacies of conditioning in probabilistic programming, a major feature, e.g., in machine learning. We provide a quantitative weakest pre-condition semantics. In contrast to all other approaches, non-termination is taken into account by our semantics. We also present an operational semantics in terms of Markov models and show that expected rewards coincide with quantitative pre-conditions. A program transformation that entirely eliminates conditioning from programs is given; the correctness is shown using our semantics. Finally, we show that an inductive semantics for conditioning in non-deterministic probabilistic programs cannot exist.",
author = "Nils Jansen and Kaminski, {Benjamin Lucien} and Katoen, {Joost Pieter} and Federico Olmedo and Friedrich Gretz and Annabelle McIver",
year = "2015",
month = "12",
day = "21",
doi = "10.1016/j.entcs.2015.12.013",
language = "English",
volume = "319",
pages = "199--216",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

Conditioning in Probabilistic Programming. / Jansen, Nils; Kaminski, Benjamin Lucien; Katoen, Joost Pieter; Olmedo, Federico; Gretz, Friedrich; McIver, Annabelle.

In: Electronic Notes in Theoretical Computer Science, Vol. 319, 21.12.2015, p. 199-216.

Research output: Contribution to journalConference paperResearchpeer-review

TY - JOUR

T1 - Conditioning in Probabilistic Programming

AU - Jansen,Nils

AU - Kaminski,Benjamin Lucien

AU - Katoen,Joost Pieter

AU - Olmedo,Federico

AU - Gretz,Friedrich

AU - McIver,Annabelle

PY - 2015/12/21

Y1 - 2015/12/21

N2 - In this paper, we investigate the semantic intricacies of conditioning in probabilistic programming, a major feature, e.g., in machine learning. We provide a quantitative weakest pre-condition semantics. In contrast to all other approaches, non-termination is taken into account by our semantics. We also present an operational semantics in terms of Markov models and show that expected rewards coincide with quantitative pre-conditions. A program transformation that entirely eliminates conditioning from programs is given; the correctness is shown using our semantics. Finally, we show that an inductive semantics for conditioning in non-deterministic probabilistic programs cannot exist.

AB - In this paper, we investigate the semantic intricacies of conditioning in probabilistic programming, a major feature, e.g., in machine learning. We provide a quantitative weakest pre-condition semantics. In contrast to all other approaches, non-termination is taken into account by our semantics. We also present an operational semantics in terms of Markov models and show that expected rewards coincide with quantitative pre-conditions. A program transformation that entirely eliminates conditioning from programs is given; the correctness is shown using our semantics. Finally, we show that an inductive semantics for conditioning in non-deterministic probabilistic programs cannot exist.

UR - http://www.scopus.com/inward/record.url?scp=84951776671&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2015.12.013

DO - 10.1016/j.entcs.2015.12.013

M3 - Conference paper

VL - 319

SP - 199

EP - 216

JO - Electronic Notes in Theoretical Computer Science

T2 - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -