TY - GEN
T1 - PSI
T2 - 28th International Conference on Computer Aided Verification, CAV 2016
AU - Gehr, Timon
AU - Misailovic, Sasa
AU - Vechev, Martin
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2016.
PY - 2016
Y1 - 2016
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
Y2 - 17 July 2016 through 23 July 2016
ER -