R2: An Efficient MCMC Sampler for Probabilistic Programs
By Aditya V. Nori, Chung-Kil Hur, Sriram K. Rajamani, Selva Samuel. 2014
120 citations recorded by the source corpus.
We present a new Markov Chain Monte Carlo (MCMC) sampling algorithm for probabilistic programs. Our approach and tool, called R2, has the unique feature of employing program analysis in order to improve the efficiencyof MCMC sampling. Given an input program P, R2 propagates observations in P backwards to obtaina semantically equivalent program P' in which every probabilistic assignment is immediately followed by an observe statement. Inference is performed by a suitably modified version of the Metropolis-Hastings algorithm that exploits the structure of the program P'. This has the overall effect of preventing rejections due to program executions that fail to satisfy observations in P. We formalize the semantics of probabilistic programs and rigorously prove the correctness of R2. We also empirically demonstrate the effectiveness of R2—in particular, 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.
Subfields: Artificial Intelligence, Probabilistic & Bayesian Methods
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- Timon Gehr
- Martin T. Vechev
- A. Gordon
- Sasa Misailovic
- Aditya V. Nori
- Sriram K. Rajamani
- Shayak Sen
- Johannes Borgström
In Probabilistic & Bayesian Methods
- A. Gordon
- Sasa Misailovic
- Martin T. Vechev
- Timon Gehr
- Sriram K. Rajamani
- Shayak Sen
- Johannes Borgström
- Marcin Szymczak
Citations in the corpus
- An Introduction to Probabilistic Programming (2018, neutral): “, 2014), R2 (Nori et al., 2014), Figaro (Pfeffer, 2009), IBAL (Pfeffer, 2001)), PSI (Gehr et al.”
- PSI: Exact Symbolic Inference for Probabilistic Programs (2016, methodology): “NET [34] and R2 [39], and show the benefits of exact inference.”
- Debugging Machine Learning Tasks (2016, methodology): “We can thus implement computing PS using recent advances in inference techniques for probabilistic programs [12, 13].”
- A lambda-calculus foundation for universal probabilistic programming (2015, background): “To the best of our knowledge, the only previous theoretical justi-fication for trace MCMC is the recent work by Hur et al. (2015), who show correctness of trace MCMC for the imperative probabilistic language R2 (Nori et al. 2014).”