Speaker: Giuseppe Primiero
Date and Time: Thursday, November 4th 2021, 16:30-18:00, Amsterdam time.
Venue: online.
Title: A Typed Natural Deduction System to verify Trustworthiness of Probabilistic Computations (joint work with Fabio Aurelio D’Asaro)
Abstract.
We present TPTND, a typed natural deduction calculus to verify trustworthiness of probabilistic programs as a safety property. To set the stage, we provide a simple case-study in a machine-learning setting to illustrate the need for such a system and its foreseeable use. For the formal presentation, we start with constructing distributions of aleatoric variables through formation rules, provide typing rules for deterministic programs under such distributions, and generalize to sampling under multiple instances of such programs to evaluate output frequency. We then formulate introduction and elimination rules for an operator to verify the trustworthiness of a program as an evaluation of its possibly unknown or opaque distribution against its fair and transparent counterpart. To conclude, we illustrate how standard meta-theoretical results of output preservation and progress for this calculus are interpreted to formulate a safety property.