Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
This program is tentative and subject to change.
We present AURA, a novel abstract interpretation for obtaining sound, precise bounds on the posterior distributions computed by probabilistic programs. AURA allows programmers to specify interval bounds that capture uncertainty or perturbations of the observed data. AURA abstractly computes the infinite set of posteriors that would result from performing inference for any possible data value in the specified perturbation range. AURA then certifies precise bounds on probabilistic queries over that set of posteriors. AURA’s precision stems from a novel gradient-based optimization leveraging the structure of probabilistic programs. Our evaluation across 11 benchmarks with data perturbation shows that AURA improves precision by an order of magnitude (12.8x on average) over the interval-based abstract interpreter, within a run time of 3.1 seconds (geomean), using a GPU parallel implementation.
This program is tentative and subject to change.
Mon 13 OctDisplayed time zone: Perth change
16:00 - 17:40 | |||
16:00 20mTalk | Relating Distances and Abstractions: An Abstract Interpretation Perspective SAS Marco Campion INRIA & ENS Paris | Université PSL, Isabella Mastroeni University of Verona, Caterina Urban Inria & ENS | PSL | ||
16:20 20mTalk | Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty SAS Zixin Huang University of Illinois at Urbana-Champaign, USA, Jacob Laurel Georgia Institute of Technology, Saikat Dutta University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-Champaign | ||
16:40 20mTalk | Specifying and Verifying Future Conditions SAS Yahui Song Standard Chartered Bank, Darius Foo National University of Singapore, Wei-Ngan Chin National University of Singapore | ||
17:00 20mTalk | Contextual Equality Saturation SAS | ||
17:20 20mTalk | Abstracting Concolic Execution for Soft Contract Verification SAS Bram Vandenbogaerde , Quentin Stiévenart Université du Québec à Montréal, Coen De Roover Vrije Universiteit Brussel Pre-print |