Seoul National University

We present a new Markov Chain Monte Carlo (MCMC) sampling algorithm for probabilistic programs. Our ap-proach and tool, called R2, has the unique feature of employing program analysis in order to improve the ef-ficiency of MCMC sampling. Given an input program P, R2 propagates observations in P backwards to ob-tain a semantically equivalent program P ′ in which ev-ery probabilistic assignment is immediately followed by an observe statement. Inference is performed by a suit-ably modified version of the Metropolis-Hastings algo-rithm that exploits the structure of the program P ′. This has the overall effect of preventing rejections due to pro-gram executions that fail to satisfy observations in P. We formalize the semantics of probabilistic programs and rigorously prove the correctness of R2. We also em-pirically demonstrate the effectiveness of R2—in par-ticular, we show that R2 is able to produce results of similar quality as the CHURCH and STAN probabilistic programming tools with much shorter execution time.