A Typed Lambda-Calculus for Establishing Trust in Probabilistic Programs
Francesco A. Genco, Giuseppe Primiero
TL;DR
This work addresses trustworthy computation for probabilistic programs by aligning observed output frequencies with a target distribution. It introduces a typed probabilistic lambda-calculus $\lambda^{\circlearrowright}_{\mathtt{Trust}?}$ featuring an experiment operator $\circlearrowright_n$ and a trust-check operator $\mathtt{Trust}?$, together with a static confidence notion derived from the strong law of large numbers. The authors develop a reduction semantics, prove progress and termination, and define a framework to reason about global behaviour via a confidence ordering that converges to trust under increasing sample size. The approach enables analysis of opaque probabilistic programs, supports conditional probabilities and conjunctions/disjunctions, and sets the stage for integrating blackbox processes and a deductive extension for formal trust reasoning.
Abstract
The extensive deployment of probabilistic algorithms has radically changed our perspective on several well-established computational notions. Correctness is probably the most basic one. While a typical probabilistic program cannot be said to compute the correct result, we often have quite strong expectations about the frequency with which it should return certain outputs. In these cases, trust as a generalisation of correctness fares better. One way to understand it is to say that a probabilistic computational process is trustworthy if the frequency of its outputs is compliant with a probability distribution which models its expected behaviour. We present a formal computational framework that formalises this idea. In order to do so, we define a typed lambda-calculus that features operators for conducting experiments at runtime on probabilistic programs and for evaluating whether they compute outputs as determined by a target probability distribution. After proving some fundamental computational properties of the calculus, such as progress and termination, we define a static notion of confidence that allows to prove that our notion of trust behaves correctly with respect to the basic tenets of probability theory.