AQUA: Automated Quantized Inference for Probabilistic Programs

Zixin Huang, Saikat Dutta, Sasa Misailovic

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 languageEnglish (US)
Title of host publicationAutomated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Proceedings
EditorsZhe Hou, Vijay Ganesh
Number of pages18
ISBN (Print)9783030888848
StatePublished - 2021
Event19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021 - Virtual, Online
Duration: Oct 18 2021Oct 22 2021

Publication series

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


Conference19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021
CityVirtual, Online

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'AQUA: Automated Quantized Inference for Probabilistic Programs'. Together they form a unique fingerprint.

Cite this