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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'PSI: Exact symbolic inference for probabilistic programs'. Together they form a unique fingerprint.

  • 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