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

FLOPS2022
May 10, 2022

Introduction

Probabilistic Programming Language

Probabilistic Programming Languages
Programmers write a probabilistic distribution as a program.
The languages support sampling and conditioning.
∗Ex.

∗The distribution when we roll two dice and at least one die is 4.

Adrian, S. Probabilistic programming.
https://www.cs.cornell.edu/courses/cs4110/2016fa/lectures/lecture33.html.

Introduction

Probabilistic Programming Language

Probabilistic Programming Languages
Monte Carlo method
For a sequence x1 , . . . , xn sampled from a distribution d,Ex∼d [h(x)] ≈ the average of h(x1 ), . . . , h(xn ).
(d is a probability distribution on X and h : X ⇒ real is a function.)montecarlo : nat ⇒ P [real]montecarlo n ≡ if (n = 0) then return 0else do {m ← montecarlo (n − 1);x ← d;
return ((1/n) ∗ (h(x) + m ∗ (n − 1))) }P [real] is the type of probability distributions on real.
Expected property: The grater n is, the closer montecarlo n is to Ex∼d [h(x)].

Introduction

Probabilistic Programming Language

Semantics of Probabilistic Programming Languages
Semantics based on measure theory
The probability monad (the Giry monad) G.
InterpretationΓ ⊢ e : P [X] −−−−−−−−−→ A measurable function JeK : JΓK → G(JXK).
Problem: Function spaces (with desired properties) do not exist in general.

Semantics based on quasi-Borel spaces[Heunen+, LICS2017]
A suitable model for higher-order languages.
Function spaces exist.
Every probability distribution on standard borel spaces (e.g. Rn , N) isrepresented as a probability distribusion on a quasi-Borel space.
The probability monad is commutative strong.

Introduction

Probabilistic Programming Language

The Verification Framework PPV[Sato+, POPL2019]
PPV(Probabilistic Programming Verification framework) is a verification
framework for higher-order probabilistic programming language.
PPV consists of the language and three kind of logics(Assertion logic, Unary logic, Relational logic).
The language supports sampling and conditioning.
Its semantics is based on quasi-Borel spaces.
PPV was applied to verify
Monte Carlo method,Importance sampling, andGaussian mean learning.

Introduction

Contributions

Contributions
Goal:
Verification of higher-order probabilistic programs with proof assistant.

Contributions:
Formalizing quasi-Borel spaces in Isabelle/HOL
Formalizing a core part of PPV(The language, Assertion logic, Unary logic)
Our PPV does not support conditioning.
We introduced integrability in the logic because it is necessary.

Verification of the Monte Carlo method on mechanized PPV (includingthe integrability)

Introduction

Contributions

Contributions
Goal:
Verification of higher-order probabilistic programs with proof assistant.

We choose Isabelle/HOL.
Rich probability theory library (including the Giry monad)

Quasi-Borel spaces
PPVIntegrability of Monte Carlo approximation
Verification of the Monte Carlo method
Total

8,950
3,100
150
300
12,500Verification of Monte Carlo Approximation

Outline1Introduction

2

Verification of Monte Carlo Approximation3

Formalization of PPV

4Conclusion

Verification of Monte Carlo Approximation

The Weak Law of Large Numbers

Verification of Monte Carlo Approximation
Monte Carlo method
For a sequence x1 , . . . , xn sampled from a distribution d,Ex∼d [h(x)] ≈ the average of h(x1 ), . . . , h(xn ).
(d is a probability distribution on X and h : X ⇒ real is a function.)montecarlo : nat ⇒ P [real]montecarlo n ≡ if (n = 0) then return 0else do {m ← montecarlo (n − 1);x ← d;
return ((1/n) ∗ (h(x) + m ∗ (n − 1))) }Theorem (The weak law of large numbers)
Let (Xn )n=1,2,··· be i.i.d. random variables with the mean µ and the varianceσ 2 < ∞. For ε > 0,X1 + · · · + Xnlim Pr− µ ≥ ε = 0.
n→∞nVerification of Monte Carlo Approximation

The Weak Law of Large Numbers

Verification of Monte Carlo ApproximationΓ ≡ ε : real, µ : real, σ : real, d : P [X], h : X ⇒ realΨ ≡ {σ 2 = Vx∼d [h x], µ = Ex∼d [h x], ε > 0, integrable d h, integrable d h2 }
Γ | Ψ ⊢UPL montecarlo : nat ⇒ P [real] | ∀n : nat.n > 0 → Pr [|y − µ| ≥ ε] ≤ σ 2 /nε2y∼r nintegrable µ f

The expected value Ex∼µ [f x] exists as a finite value(f is integrable w.r.t. µ).

Theorem (The weak law of large numbers)
Let (Xn )n=1,2,··· be i.i.d. random variables with the mean µ and the varianceσ 2 < ∞. For ε > 0,
X1 + · · · + Xnlim Pr− µ ≥ ε = 0.
n→∞nVerification of Monte Carlo Approximation

The Weak Law of Large Numbers

Verification of Monte Carlo ApproximationΓ ≡ ε : real, µ : real, σ : real, d : P [X], h : X ⇒ realΨ ≡ {σ 2 = Vx∼d [h x], µ = Ex∼d [h x], ε > 0, integrable d h, integrable d h2 }
Γ | Ψ ⊢UPL montecarlo : nat ⇒ P [real] | ∀n : nat.n > 0 → Pr [|y − µ| ≥ ε] ≤ σ 2 /nε2y∼r n
Γ | Ψ ⊢PL ∀n : nat.integrable (montecarlo n)(λx.x) ∧ integrable (montecarlo n)(λx.x2 )

integrable µ f

The expected value Ex∼µ [f x] exists as a finite value(f is integrable w.r.t. µ).

The integrability of the program is required to prove the UPL-judgment.

Verification of Monte Carlo Approximation

The Proof of Monte Carlo Method

The Proof of Monte Carlo Method
We proved according to the proof outline shown in [Sato+, POPL2019].
We additionally need to prove the integrability of the program.
Our proof requires a large number of steps of equational reasoning
because we have not implemented automation.
Pen and paper proof: 7 lines
Ey∼(tn ≫=(λm.d≫=(λx.return ((h x+m∗n)/(S n))))) [y]= Ey∼(tn ⊗d≫=(λ(m,x).return ((h x+m∗n)/(S n)))) [y]hx+m∗n= E(m,x)∼tn ⊗dSn1n=∗ E(m,x)∼tn ⊗d [h x] +∗ E(m,x)∼tn ⊗d [m]SnSn1n=∗ Ex∼d [h x] +∗ Em∼tn [m]
SnSn
1n=
∗µ+
∗ Em∼tn [m]SnSn=µ

In Isabelle: around 100 linesFormalization of PPVOutline

1Introduction

2

Verification of Monte Carlo Approximation3

Formalization of PPV

4Conclusion

Formalization of PPV

PPV: Syntax and Typing System

PPV: Syntax and Typing System
The programming language: HPProg
Te::=::=

unit | nat | bool | real | preal | T × T | T ⇒ T | P [T ],x | c | f | e e | λx.e | ⟨e, e⟩ | πi (e) | rec nat e e| return e | bind e e | Bernoulli(e) | Gauss(e, e).

P [T ] is the type of probability distributions on T .
Typing rules are standard.
Γ⊢e:TΓ ⊢ return e : P [T ]Γ ⊢ e : realΓ ⊢ Bernoulli(e) : P [bool]Γ ⊢ e : P [T ]Γ ⊢ f : T ⇒ P [T ′ ]Γ ⊢ bind e f : P [T ′ ]Γ ⊢ e : realΓ ⊢ e′ : real′Γ ⊢ Gauss(e, e ) : P [real]Formalization of PPVFormalization of PPVFormalization of PPV
We shallowly embed PPV.
Interpretation

Type T−−−−−−−−−→

Typed term Γ ⊢ e : TInterpretation−−−−−−−−−→

An object JT K of QBS

A morphism JeK : JΓK → JT K

In Isabelle/HOLdefinition "hpprog_typing Γ e T ≡ e ∈ Γ →Q T"

QBSObjects · · · Quasi-Borel spaces.
Morphisms · · · Structure-preserving functions.
Γ →Q T = the set of all morphisms from Γ to T.

Similarly, logics of PPV are defined according to its semantics.

Formalization of PPV

De Bruijn Index

Formalization of PPV
De Bruijn index
definition "var1 ≡ snd"
lemma hpt_var1:"Γ,,Z ⊢t var1 ;; Z"

definition "var2 ≡ snd ◦ fst"
lemma hpt_var2:"Γ,,Z,,Y ⊢t var2 ;; Z"NN
*Γ,,Z,,Y = (ΓQ Z)
Q Y

definition "λt ≡ curry"lemma hpt_abs:
assumes "Γ,,X ⊢t t ;; T"shows "Γ ⊢t λt t ;; X ⇒Q T"

Ex. Γ, y : Y ⊢ (λx.x) y : Ylemma "Γ,,Y ⊢t (λt var1) $t var1 ;; Y"

De Bruijn index makes reasoning cumbersome.

Formalization of PPVThe Original PPV vs Our Mechanized PPVThe Original PPV vs Our Mechanized PPVConditioning
Our mechanized PPV does not support the conditioning.
We use the probability monad[Heunen+, LICS2017] on QBS.
The original PPV uses the σ-finite measure monad[Scibior+, POPL2018]
on QBS.

The probability monad is constructed from the Giry monad which is includedin the standard library HOL-Probability.

Formalization of PPVThe Original PPV vs Our Mechanized PPVThe Original PPV vs Our Mechanized PPVIntegrability
We use the following Eqs. in the proof of the Monte Carlo approximation.
Ex∼d [f x + g x] = Ex∼d [f x] + Ex∼d [g x].
V(x,y)∼d1 ⊗d2 [f x + g y] = Vx∼d1 [f x] + Vy∼d2 [g y].
(1) holds if
f and g are non-negative, orf and g are integrable w.r.t. d.
In the proof of (2), we use (1) with functions which might be negative.

Integrability is necessary!

(1)
(2)

Conclusion

Conclusion

Conclusion
Formalizing quasi-Borel spaces in Isabelle/HOL
Formalizing a core part of PPV.
(The language, Assertion logic, Unary logic)
Our PPV does not support conditioning.
We added integrability in the logic because it is necessary.

Verification of the Monte Carlo method on mechanized PPV (includingthe integrability).
The formalization of quasi-Borel spaces is available at AFP*.
The entire formalization is available at author’s repository**.

* Quasi-Borel Spaces, Archive of formal proofs, 2022.
** https://github.com/HirataMichi/PPVConclusion

Future Works

Future Works

Conditioning
We need to formalize the σ-finite measure monad to support conditioning.
Proof automation
It may reduce cost of verification to prove simple Eqs. semantically,rather than apply rules manually.
Relational program logicWe expect no major difficulties.
Applications
Sample size required in importance sampling
Differential privacy