AQUA: Automated Quantized Inference for Probabilistic Programs

Zixin Huang; Saikat Dutta; Sasa Misailovic

doi:10.1007/978-3-030-88885-5_16

AQUA: Automated Quantized Inference for Probabilistic Programs

Zixin Huang, Saikat Dutta, Sasa Misailovic

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English (US)
Title of host publication	Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Proceedings
Editors	Zhe Hou, Vijay Ganesh
Publisher	Springer
Pages	229-246
Number of pages	18
ISBN (Print)	9783030888848
DOIs	https://doi.org/10.1007/978-3-030-88885-5_16
State	Published - 2021
Event	19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021 - Virtual, Online Duration: Oct 18 2021 → Oct 22 2021

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12971 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021
City	Virtual, Online
Period	10/18/21 → 10/22/21

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/978-3-030-88885-5_16

Library availability

Discover UIUC Full Text

Cite this

Huang, Z., Dutta, S., & Misailovic, S. (2021). AQUA: Automated Quantized Inference for Probabilistic Programs. In Z. Hou, & V. Ganesh (Eds.), Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Proceedings (pp. 229-246). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12971 LNCS). Springer. https://doi.org/10.1007/978-3-030-88885-5_16

AQUA: Automated Quantized Inference for Probabilistic Programs. / Huang, Zixin; Dutta, Saikat; Misailovic, Sasa.
Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Proceedings. ed. / Zhe Hou; Vijay Ganesh. Springer, 2021. p. 229-246 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12971 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Huang, Z, Dutta, S & Misailovic, S 2021, AQUA: Automated Quantized Inference for Probabilistic Programs. in Z Hou & V Ganesh (eds), Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12971 LNCS, Springer, pp. 229-246, 19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021, Virtual, Online, 10/18/21. https://doi.org/10.1007/978-3-030-88885-5_16

Huang Z, Dutta S, Misailovic S. AQUA: Automated Quantized Inference for Probabilistic Programs. In Hou Z, Ganesh V, editors, Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Proceedings. Springer. 2021. p. 229-246. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-88885-5_16

Huang, Zixin ; Dutta, Saikat ; Misailovic, Sasa. / AQUA : Automated Quantized Inference for Probabilistic Programs. Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Proceedings. editor / Zhe Hou ; Vijay Ganesh. Springer, 2021. pp. 229-246 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{3026f22f31c54e88b7d22d7215d120bd,

title = "AQUA: Automated Quantized Inference for Probabilistic Programs",

abstract = "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{\textquoteright}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{\textquoteright}s NUTS and ADVI) and supports programs that are out of reach of exact inference tools, such as PSI and SPPL.",

author = "Zixin Huang and Saikat Dutta and Sasa Misailovic",

note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; 19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021 ; Conference date: 18-10-2021 Through 22-10-2021",

year = "2021",

doi = "10.1007/978-3-030-88885-5_16",

language = "English (US)",

isbn = "9783030888848",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "229--246",

editor = "Zhe Hou and Vijay Ganesh",

booktitle = "Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Proceedings",

address = "Germany",

}

TY - GEN

T1 - AQUA

T2 - 19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021

AU - Huang, Zixin

AU - Dutta, Saikat

AU - Misailovic, Sasa

PY - 2021

Y1 - 2021

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85118194644&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85118194644&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-88885-5_16

DO - 10.1007/978-3-030-88885-5_16

M3 - Conference contribution

AN - SCOPUS:85118194644

SN - 9783030888848

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 229

EP - 246

BT - Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Proceedings

A2 - Hou, Zhe

A2 - Ganesh, Vijay

PB - Springer

Y2 - 18 October 2021 through 22 October 2021

ER -

AQUA: Automated Quantized Inference for Probabilistic Programs

Abstract

Publication series

Conference

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this