Semantic Foundations of Higher-Order
Probabilistic Programs in Isabelle/HOL
Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato
Tokyo Institute of Technology

ITP2023
August 3, 2023

Probabilistic Programs
Programmers write probabilistic distributions as programs.
The languages infer posterior distributions after observing some events.
(conditional distributions)
Anglican, Church, Hakaru, WebPPL, …

Higher-order probabilistic programs= Higher-order functions + probabilistic programs
higher-order functions, sampling, conditioning2

Probabilistic Programs
Example (by Staton*)
1. We came to watch a road bicycle racing.
We want to know what time it is.

2. We know the rate of bikes per hour at each time.

Fig 2.4 in *3. We observed a 1 minute gap between two bikes.

4. What time is it?

1 minuite* Probabilistic Programs as Measures, Sam Staton, Foundations of Probabilistic Programming, 2020?

3

Probabilistic Programs
Posterior ∝ Likelihood × Prior
The rate
Prior
Likelihood
1. We want to know what time it is.
2. We know the rate of bikes per hour.
3. We observed a 1 minute gap between two bikes.
4. What time is it ?

4

Semantics of Probabilistic Programs
Semantics based on measure theory
The probability monad (the Giry monad) or s-finite kernels

Γ ⊢ e : P(T)Interpretation

A measurable function [[e]] : [[Γ]] → G([[T]])Problem: Function spaces do not exist in general

Semantics based on quasi-Borel spaces [Heunen+, LICS 2017]
A suitable denotational model for higher-order probabilistic programs
Function spaces always exist
The s-finite measure monad on quasi-Borel spaces[Scibior+, POPL 2018](Probability measures ⊆ σ-finite measures ⊆ s-finite measures)

5

Previous WorksMany proof assistants have measure theory library (Isabelle/HOL, Lean, Coq, …)

Formalization of semantics of probabilistic programs
1. [Hirata+, FLOPS2022] Quasi-Borel spaces and the probability monad in Isabelle/HOL
2. [Affeldt+, CPP2023] S-finite kernels in Coq• 1 does not support conditioning• 2 does not support higher-order functions• Both of 1 and 2 use de-Bruijn index to denote probabilistic programs
Hard to read, write, and reason about programs

6This Work(1)Formalizing semantics for higher-order probabilistic programs with conditioning
Isabelle/HOL terms as probabilistic programsHigher-order
Command for conditional distributions(based on the s-finite measure monad)

7

This Work(2)Automated type checking⊢ whattime : (real ⇒ real) ⇒ M[real]⊢t:TInterpretation(M[real]⋯ Distribution on ℝ)[[t]] ∈ Quasi-Borel space [[T]]In Isabelle/HOL⋯ A quasi-Borel space

8

Example: What time is it?

Example: What time is it?
Example (by Staton*)
1. We came to watch a road bicycle racing.
We want to know what time it is.

2. We know the rate of bikes per hour at each time.

Fig 2.4 in *3. We observed a 1 minute gap between two bikes.

4. What time is it?

1 minuite* Probabilistic Programs as Measures, Sam Staton, Foundations of Probabilistic Programming, 2020?

10

Example: What time is it?
Example (by Staton*)
1. We came to watch a road bicycle racing.
We want to know what time it is.

2. We know the rate of bikes per hour at each time.

Prior
Fig 2.4 in *3. We observed a 1 minute gap between two bikes.

4. What time is it?

Likelihood Posterior ∝ Likelihood × Prior1 minuite* Probabilistic Programs as Measures, Sam Staton, Foundations of Probabilistic Programming, 2020?

11

Example: What time is it?
1. We came to watch a road bicycle racing.
We want to know what time it is.
Prior: Uniform(0,24)
pdf: p(t) =1
24{00 < t < 24o.w.

12

Example: What time is it?
2. We know the rate of bikes per hour at each time.

Fig 2.4 in *Given as an argument ff(t)⋯ The rate of bikes per hour at time t* Probabilistic Programs as Measures, Sam Staton, Foundations of Probabilistic Programming, 202013

Example: What time is it?
3. We observed a 1 minute gap between two bikes

1 minuite⟨The gap between two bikes at time t⟩ ∼ Exponential( f(t))
exp_density(x | f(t)) = f(t)e−xf(t)1− 60 f(t)Likelihood function: l(t) = exp_density(1/60 | f(t)) = f(t)e(1 minute = 1/60 hour)14

Example: What time is it?
4. What time is it?
Posterior ∝ Likelihood × Prior?

Prior: Uniform(0,24)
Likelihood function: l(t) = f(t)e

1− 60 f(t)The ratePriorLikelihood

15

Example: What time is it?
Posterior ∝ Likelihood × Prior
posterior_pdf(t) ∝ f(t)eposterior_pdf(t) =1×24
1

1− 60 f(t)f(t)e

− 60 f(t)1× 24=

1t=24
1−f(t)∫t=0 f(t)e 60 × 24 dt
1− 60f(t)∫t∈(0,24)∩U f(t)edt

PT∼Posterior [T ∈ U] =Around 100 lines for prooff(t)e

1− 60 f(t)1t=24−f(t)∫t=0 f(t)e 60 dt=NN16

Theory of Quasi-Borel Spaces andImplementing Probabilistic Programs

Quasi-Borel Spaces
A new denotational model for higher-order probabilistic programs[Heunen+, LICS2017]• Function spaces always exist (For measurable spaces, do not in general)⟹ Higher-order programs• Measures on standard Borel spaces (e.g. ℕ, ℝ, and Πi∈ℕℝ )⟹ Probability distributions• The s-finite measure monad[Scibior+, POPL 2018]⟹ Semantics for probabilistic programs18

Quasi-Borel Spaces in Isabelle/HOL
Our previous work[Hirata+, FLOPS2022]
Quasi-Borel Spaces
consist of underlying set and “random variables”

Morphisms (structure preserving functions)

Product SpaceFunction Space
List Space19

The S-Finite Measure MonadMeasures
Space of Measures, Return and Bind

The triple forms a commutative strong monad on QBS
Ex: Associativity

20

Probabilistic Programming Language
Language
HPProg⋯ A functional probabilistic programming language[Sato+, POPL2019]

T ::= nat ∣ bool ∣ real ∣ preal ∣ list[T] ∣ T × T ∣ T ⇒ T ∣ M[T]e ::= x ∣ c ∣ e e ∣ λx . ec ::= + ∣ − ∣ … ∣ Pair ∣ fst ∣ snd ∣ rec_nat ∣ rec_list ∣return ∣ bind ∣ query ∣ Uniform ∣ Gauss ∣ …

The type of distributions on T⊢ return : X ⇒ M[X]⊢ bind : M[X] ⇒ (X ⇒ M[Y]) ⇒ M[Y]⊢ Uniform : real ⇒ real ⇒ M[real]⊢ Gauss : real ⇒ real ⇒ M[real]21

Isabelle/HOL Terms as Programs
Semantics
Type T ⟹ Quasi-Borel space T

Typed term ⊢ t : T ⟹We regard Isabelle/HOL terms as probabilistic programs
Examples (deterministic terms):⊢ + : real ⇒ real ⇒ real

⊢ λx . [x, x + 1,x + 2] : real ⇒ List[real]⊢ λ( f, x) . f x : (real ⇒ real) × real ⇒ real
22

Isabelle/HOL Terms as Programs
Probabilistic Computations[[M[X]]] =Example:1. Pick a sample x from Uniform(0,5)
2. Return x + 1
Equal toConditioning

PriorLikelihoodPosterior

23

Automated Type Checking
Type check ⊢ t : T ⟺ Prove

Automate proofs for type checking

by tactic qbs• implemented in ML• similar to measurability prover in HOL-Analysis• The algorithm is based on type inference in functional programming languages

24

Measurability Prover VS QBS Prover
Measurability Prover (in HOL-Analysis)
Try to solve measurability
Measurable functions

Measurable sets

QBS prover
Try to solve membership•⟹ use•⟹ use

25

Conclusion• Formalizing the s-finite measure monad on quasi-Borel spaces⟹ Higher-order probabilistic programs with conditioning• Isabelle/HOL terms as programs + Developing proof automation for type checking⟹ Easier to write, read, and reason about probabilistic programs• Implementing several examples of probabilistic programs and proving their properties• What time is it?
• Convergence and stability of the Gaussian mean learning
etc.

26

Appendix

The Adjunction
Conversions
LQBS⊥
RMeas•Morphism

Measurable• If M is a standard Borel space, then L (R M) = M
Morphism iff measurable, when we use only standard Borel spaces
28Measures on Quasi-Borel Spaces
Measures on quasi-Borel spaces• S-finite measures on standard Borel spaces
Ex: the Lebesgue measure, probability measures on ℝ

• Integration
Quasi-Borel theory

Measure theory

The Lebesgue measure on quasi-Borel spaces

29