PSI: Exact symbolic inference for probabilistic programs

Timon Gehr, Sasa Misailovic, Martin Vechev

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Probabilistic inference is a key mechanism for reasoning about probabilistic programs. Since exact inference is theoretically expensive, most probabilistic inference systems today have adopted approximate inference techniques, which trade precision for better performance (but often without guarantees). As a result, while desirable for its ultimate precision, the practical effectiveness of exact inference for probabilistic programs is mostly unknown. This paper presents PSI (http://www.psisolver.org), a novel symbolic analysis system for exact inference in probabilistic programs with both continuous and discrete random variables. PSI computes succinct symbolic representations of the joint posterior distribution represented by a given probabilistic program. PSI can compute answers to various posterior distribution, expectation and assertion queries using its own backend for symbolic reasoning. Our evaluation shows that PSI is more effective than existing exact inference approaches: (i) it successfully computed a precise result for more programs, and (ii) simplified expressions that existing computer algebra systems (e.g., Mathematica, Maple) fail to andle.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 28th International Conference, CAV 2016, Proceedings
EditorsAzadeh Farzan, Swarat Chaudhuri
PublisherSpringer-Verlag
Pages62-83
Number of pages22
ISBN (Print)9783319415277
DOIs
StatePublished - Jan 1 2016
Event28th International Conference on Computer Aided Verification, CAV 2016 - Toronto, Canada
Duration: Jul 17 2016Jul 23 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9779
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other28th International Conference on Computer Aided Verification, CAV 2016
CountryCanada
CityToronto
Period7/17/167/23/16

Fingerprint

Exact Inference
Random variables
Algebra
Probabilistic Inference
Posterior distribution
Reasoning
Symbolic Analysis
Continuous random variable
Discrete random variable
Computer algebra system
Maple
Mathematica
Assertion
Joint Distribution
Query
Unknown
Evaluation

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Gehr, T., Misailovic, S., & Vechev, M. (2016). PSI: Exact symbolic inference for probabilistic programs. In A. Farzan, & S. Chaudhuri (Eds.), Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings (pp. 62-83). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9779). Springer-Verlag. https://doi.org/10.1007/978-3-319-41528-4_4

PSI : Exact symbolic inference for probabilistic programs. / Gehr, Timon; Misailovic, Sasa; Vechev, Martin.

Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. ed. / Azadeh Farzan; Swarat Chaudhuri. Springer-Verlag, 2016. p. 62-83 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9779).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Gehr, T, Misailovic, S & Vechev, M 2016, PSI: Exact symbolic inference for probabilistic programs. in A Farzan & S Chaudhuri (eds), Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9779, Springer-Verlag, pp. 62-83, 28th International Conference on Computer Aided Verification, CAV 2016, Toronto, Canada, 7/17/16. https://doi.org/10.1007/978-3-319-41528-4_4
Gehr T, Misailovic S, Vechev M. PSI: Exact symbolic inference for probabilistic programs. In Farzan A, Chaudhuri S, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. Springer-Verlag. 2016. p. 62-83. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-41528-4_4
Gehr, Timon ; Misailovic, Sasa ; Vechev, Martin. / PSI : Exact symbolic inference for probabilistic programs. Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. editor / Azadeh Farzan ; Swarat Chaudhuri. Springer-Verlag, 2016. pp. 62-83 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{18f06a212db04eed8680011efe6ef8b8,
title = "PSI: Exact symbolic inference for probabilistic programs",
abstract = "Probabilistic inference is a key mechanism for reasoning about probabilistic programs. Since exact inference is theoretically expensive, most probabilistic inference systems today have adopted approximate inference techniques, which trade precision for better performance (but often without guarantees). As a result, while desirable for its ultimate precision, the practical effectiveness of exact inference for probabilistic programs is mostly unknown. This paper presents PSI (http://www.psisolver.org), a novel symbolic analysis system for exact inference in probabilistic programs with both continuous and discrete random variables. PSI computes succinct symbolic representations of the joint posterior distribution represented by a given probabilistic program. PSI can compute answers to various posterior distribution, expectation and assertion queries using its own backend for symbolic reasoning. Our evaluation shows that PSI is more effective than existing exact inference approaches: (i) it successfully computed a precise result for more programs, and (ii) simplified expressions that existing computer algebra systems (e.g., Mathematica, Maple) fail to andle.",
author = "Timon Gehr and Sasa Misailovic and Martin Vechev",
year = "2016",
month = "1",
day = "1",
doi = "10.1007/978-3-319-41528-4_4",
language = "English (US)",
isbn = "9783319415277",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "62--83",
editor = "Azadeh Farzan and Swarat Chaudhuri",
booktitle = "Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings",

}

TY - GEN

T1 - PSI

T2 - Exact symbolic inference for probabilistic programs

AU - Gehr, Timon

AU - Misailovic, Sasa

AU - Vechev, Martin

PY - 2016/1/1

Y1 - 2016/1/1

N2 - Probabilistic inference is a key mechanism for reasoning about probabilistic programs. Since exact inference is theoretically expensive, most probabilistic inference systems today have adopted approximate inference techniques, which trade precision for better performance (but often without guarantees). As a result, while desirable for its ultimate precision, the practical effectiveness of exact inference for probabilistic programs is mostly unknown. This paper presents PSI (http://www.psisolver.org), a novel symbolic analysis system for exact inference in probabilistic programs with both continuous and discrete random variables. PSI computes succinct symbolic representations of the joint posterior distribution represented by a given probabilistic program. PSI can compute answers to various posterior distribution, expectation and assertion queries using its own backend for symbolic reasoning. Our evaluation shows that PSI is more effective than existing exact inference approaches: (i) it successfully computed a precise result for more programs, and (ii) simplified expressions that existing computer algebra systems (e.g., Mathematica, Maple) fail to andle.

AB - Probabilistic inference is a key mechanism for reasoning about probabilistic programs. Since exact inference is theoretically expensive, most probabilistic inference systems today have adopted approximate inference techniques, which trade precision for better performance (but often without guarantees). As a result, while desirable for its ultimate precision, the practical effectiveness of exact inference for probabilistic programs is mostly unknown. This paper presents PSI (http://www.psisolver.org), a novel symbolic analysis system for exact inference in probabilistic programs with both continuous and discrete random variables. PSI computes succinct symbolic representations of the joint posterior distribution represented by a given probabilistic program. PSI can compute answers to various posterior distribution, expectation and assertion queries using its own backend for symbolic reasoning. Our evaluation shows that PSI is more effective than existing exact inference approaches: (i) it successfully computed a precise result for more programs, and (ii) simplified expressions that existing computer algebra systems (e.g., Mathematica, Maple) fail to andle.

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

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

U2 - 10.1007/978-3-319-41528-4_4

DO - 10.1007/978-3-319-41528-4_4

M3 - Conference contribution

AN - SCOPUS:84978879599

SN - 9783319415277

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 62

EP - 83

BT - Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings

A2 - Farzan, Azadeh

A2 - Chaudhuri, Swarat

PB - Springer-Verlag

ER -