AQUA: Automated Quantized Inference for Probabilistic Programs

被引:14
作者
Huang, Zixin [1 ]
Dutta, Saikat [1 ]
Misailovic, Sasa [1 ]
机构
[1] Univ Illinois, Urbana, IL 61801 USA
来源
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2021 | 2021年 / 12971卷
关键词
D O I
10.1007/978-3-030-88885-5_16
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
We present AQUA, a new probabilistic inference algorithm that operates on probabilistic programs with continuous posterior distributions. AQUA approximates programs via an efficient quantization of the continuous distributions. It represents the distributions of random variables using quantized value intervals (Interval Cube) and corresponding probability densities (Density Cube). AQUA's analysis transforms Interval and Density Cubes to compute the posterior distribution with bounded error. We also present an adaptive algorithm for selecting the size and the granularity of the Interval and Density Cubes. We evaluate AQUA on 24 programs from the literature. AQUA solved all of 24 benchmarks in less than 43 s (median 1.35 s) with a high-level of accuracy. We show that AQUA is more accurate than state-of-the-art approximate algorithms (Stan's NUTS and ADVI) and supports programs that are out of reach of exact inference tools, such as PSI and SPPL.
引用
收藏
页码:229 / 246
页数:18
相关论文
共 23 条
[1]   A Pre-expectation Calculus for Probabilistic Sensitivity [J].
Aguirre, Alejandro ;
Barthe, Gilles ;
Hsu, Justin ;
Kaminski, Benjamin Lucien ;
Katoen, Joost-Pieter ;
Matheja, Christoph .
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2021, 5
[2]   FairSquare: Probabilistic verification of program fairness [J].
Albarghouthi A. ;
D’Antoni L. ;
Drews S. ;
Nori A.V. .
Proceedings of the ACM on Programming Languages, 2017, 1 (OOPSLA)
[3]   A general framework for updating belief distributions [J].
Bissiri, P. G. ;
Holmes, C. C. ;
Walker, S. G. .
JOURNAL OF THE ROYAL STATISTICAL SOCIETY SERIES B-STATISTICAL METHODOLOGY, 2016, 78 (05) :1103-1130
[4]  
Borges M, 2014, ACM SIGPLAN NOTICES, V49, P123, DOI [10.1145/2594291.2594329, 10.1145/2666356.2594329]
[5]   Stan: A Probabilistic Programming Language [J].
Carpenter, Bob ;
Gelman, Andrew ;
Hoffman, Matthew D. ;
Lee, Daniel ;
Goodrich, Ben ;
Betancourt, Michael ;
Brubaker, Marcus A. ;
Guo, Jiqiang ;
Li, Peter ;
Riddell, Allen .
JOURNAL OF STATISTICAL SOFTWARE, 2017, 76 (01) :1-29
[6]   Storm: Program Reduction for Testing and Debugging Probabilistic Programming Systems [J].
Dutta, Saikat ;
Zhang, Wenxian ;
Huang, Zixin ;
Misailovic, Sasa .
ESEC/FSE'2019: PROCEEDINGS OF THE 2019 27TH ACM JOINT MEETING ON EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING, 2019, :729-739
[7]   Testing Probabilistic Programming Systems [J].
Dutta, Saikat ;
Legunsen, Owolabi ;
Huang, Zixin ;
Misailovic, Sasa .
ESEC/FSE'18: PROCEEDINGS OF THE 2018 26TH ACM JOINT MEETING ON EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING, 2018, :574-586
[8]   PSI: Exact Symbolic Inference for Probabilistic Programs [J].
Gehr, Timon ;
Misailovic, Sasa ;
Vechev, Martin .
COMPUTER AIDED VERIFICATION, (CAV 2016), PT I, 2016, 9779 :62-83
[9]  
Gelman A., 2013, Bayesian data analysis
[10]  
Goodman N. D., 2016, Probabilistic Models of Cognition