日本ソフトウェア科学会第 38 回大会 (2021 年度) 講演論文集

Isabelle/HOL による高階確率的プログラム検証
平田 路和

南出 靖彦

佐藤 哲也

確率的プログラミング言語とは，機械学習や統計モデリングにおいて確率モデルの記述，推論を行うために使われる言語である．本研究では高階確率的プログラム検証のためのフレームワーク PPV の中核部分，及び PPV の意味論的基礎となる準ボレル空間 (quasi-Borel spaces) を Isabelle/HOL で実装し，例としてモンテカルロ法の検証を行なった．実装する上で，先行研究では省略されていた可積分性に関する公理と算術演算に関する公理を追加した．モ
ンテカルロ法の検証では，可積分性に関する議論を含んだ検証を行うことができた．

フレームワークを PPV(Probabilistic Programming

1 はじめにVeriﬁcation framework) という．

確率的プログラミング言語とは，確率分布を記述

これまで，確率的プログラムに関する証明支援系

し，分布からのサンプリングや分布の期待値の計算を

Isabelle/HOL による検証は，一階の関数型確率的プ

自動で実行する機能をもったプログラミング言語で，ログラムから確率密度関数へのコンパイルを検証した統計分野や機械学習で活用されている [5] [15] [10] [14]．

[3] や，暗号理論における安全性を示すための [9] な

確率的プログラミング言語の意味論は，確率分布

どが挙げられる．これらは離散的な空間に限った場合のモナド（Giry モナド）を用いて可測関数の形で自や，測度論に基づいた検証となっているため，高階関

然に与えることができるが，関数型に対応する可測数と連続分布をサポートする言語についての検証は空間が一般には存在しないことから，高階な言語にできない．

拡張することが難しかった．この問題に，Heunen ら

本研究の貢献は

は，扱う空間を制限した準ボレル空間 (quasi-Borel• Isabelle/HOL による準ボレル空間の形式化．準spaces) を導入することで，高階確率的プログラミ

ボレル空間を構成し，準ボレル空間の圏と可ング言語に自然に意味を与えることができること

測空間の圏の間の随伴，準ボレル空間がなす圏を示した [6]．さらに，佐藤らは，この準ボレル空間の確率モナドが可換な強モナドであることをによる意味論をベースに，連続分布からのサンプリ

Isabelle/HOL で証明した．

ングおよび条件付分布をサポートする高階確率的• 条件付き推論を含まない，言語 HPProg，論理プログラミング言語 HPProg を設計し，そのプログ

体系 PL・UPL の shallow embedding による形

ラム論理 PL，UPL，RPL を与えた [12]．この検証式化．本研究ではさらに，先行研究では扱われていなかった可積分性の議論もできるように，PL・Formal Veriﬁcation of Higher-Order Probabilistic Program in Isabelle/HOL
This is an unrefereed paper. Copyrights belong to
the Author(s).
Hirata Michikazu, Minamide Yasuhiko, Sato Tetsuya,
東 京工 業大学 情報理 工学 院, School of Computing,Tokyo Institute of Technology.

UPL 内の述語の定義を拡張してある．
• 証明支援系による，可積分性の議論も含んだモ
ンテカルロ法 ( [12] の例) の厳密な検証．
である．
本研究は準ボレル空間に基づいた形式化であるため，先行研究ではできなかった高階関数と連続分布を題を回避することができる．

含んだ検証ができる．準ボレル空間の形式化，及び準ボレル空間に基づいた検証は，Isabelle/HOL 以外の2. 2 モンテカルロ法の検証

証明支援系を含めても私たちの知る限りまだない．

本研究で実装した PPV を使い， [12] の例にある，

2 Isabelle/HOL によるモンテカルロ法のモンテカルロ法により平均値の近似計算を行うプロ
グラム (図 1) の検証を行なった (図 2(2))†3 ．

検証プログラム montecarlo は型 nat ⇒ P [real] をも

2. 1 プログラム検証フレームワーク: PPVつ．montecarlo は，引数 n をもらって，d から n 個

PPV は，Aguirre らによる関数型プログラム論理のサンプルを逐次的に生成し，その h による観測値[1] をもとにした，高階関数型確率的プログラム検の平均の分布を返す関数である．
本研究では，先行研究の例では省略されていたプログ

証のためのフレームワークで，言語 HPProg，論理体系 PL，UPL を含んでいる †1 ．HPProg は，サンラムの可積分性も PL の上で示した (図 2(1))．µ : P [T ]プリングや observe といった機能をもった関数型言と f : T ⇒ P [real] に対して，述語 integrable µ f語である．型 T に対して，型 P [T ] は T 上の確率測は期待値 Ex∼µ [f x] が有限値で存在する (f が測度 µ度の型である．PL は Γ | Ψ ⊢PL ϕ という判定式をの下で可積分である) ことを意味している．可積分性もつ PPV の基礎を成す論理体系である．Γ は型環

は，判定式 (図 2(2)) を示す際に用いる期待値の線形

境，Ψ は仮定の集合，ϕ は結論を表し，判定式は「環性を使うために必要となる．

境 Γ で，Ψ が成り立つならば ϕ が成り立つ」とい

図 2(2) の判定式は同分布上の大数の弱法則を表し

う意味である．UPL(unary program logic) は，プロている．

グラムの unary な性質を検証するため論理体系で，

定 理 2.1 (大数 の 弱 法 則). (Xn )n=1,2,··· が共 通 のΓ | Ψ ⊢UPL e : T | ϕ という形の判定式をもつ．PL

平均 µ をもつ互いに独立な実数値確率変数で，との違いは，プログラム e と e の型 T が判定式に含supn V[Xn ] < ∞ とする．このとき，任意の ε > 0 にまれている．また，結論 ϕ にはプログラム変数と呼対して，ばれるプログラムを表す変数 r が含まれている．判
定式は，「環境 Γ で e は型 T をもつ」かつ「環境 Γ でΨ が成り立つならば ϕ[e/r] が成り立つ」という意味である．

HPProg の表示的意味論では準ボレル空間を用いる．
準ボレル空間とは，高階関数と連続分布を同時に扱う

lim Prn→∞
X1 + · · · + Xn−µ ≥ε =0nが成り立つ．
この判定式は，h の定義域が実数であっても成立するため，測度論による解釈では意味が取れなかった連
続分布と高階関数を扱うようなプログラムの検証となっている．

ような言語の表示的意味論を与えるために [6] で導入された空間であり，測度論をもとに構成されている．ここ2. 3 形式化のコストで，HPProg プログラムを素朴に可測関数として解釈

本研究では，標準ボレル空間，及び準ボレル空間

しようとすると，λ(f, x) : (real ⇒ real)×real.f (x)の形式化におよそ 3ヶ月，PPV とモンテカルロ法ののようなプログラムを解釈できないことが知られている †2 ．準ボレル空間を用いることでこのような問形式化におよそ 3ヶ月の合計 6ヶ月の期間を要した．

†1 PPV には論理体系 RPL も含まれているが，本研究で形式化をしていないので，ここでは説明を省略する．
†2 Aumann の研究 [2] による．ここで述べられたプログラ
ムの自然な解釈である関数適用 Meas(R, R)×R → R((f, x) 7→ f x) は可測でないことが証明されている．
また，可測空間と可測写像の圏 Meas はカルテシア

Isabelle/HOL で記述したおおよそのコード量を以下の表に記す．
表からわかるように，標準ボレル空間と準ボレル空
ン閉でなく，特に冪対象 RR が存在しない．

†3 読み易くするため，プログラムなどの表現方法を実際の実装と少し変えている．

montecarlo n ≡ if (n = 0) then return 0else do {m ← montecarlo (n − 1);x ← d;
return ((1/n) ∗ (h(x) + m ∗ (n − 1))) }図1

モンテカルロ法により h の期待値を近似計算するプログラムΓ ≡ ε : 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 }
Γ | Ψ ⊢PL ∀n : nat.integrable (montecarlo n) (λx.x) ∧ integrable (montecarlo n) (λx.x2 )(1)

Γ | Ψ ⊢UPL montecarlo : nat ⇒ P [real] | ∀n : nat.n > 0 → Pry∼r n [|y − µ| ≥ ε] ≤ σ 2 /nε2(2)

図 2 本研究で示したモンテカルロ法の検証
deﬁnition hp_montecarlo ::"(’b × ’a qbs_prob_space) × (’a ⇒ real) ⇒ nat ⇒ real qbs_prob_space" where"hp_montecarlo ≡hp_rec_nat (hp_return IRQ (hp_const 0))(hp_lambda (hp_lambda (hp_bind var1
(hp_lambda (hp_bind var5
(hp_lambda(hp_return IRQ ((hp_app var5 var1 +t var2 *t hp_real var4) /t hp_real (hp_suc var4)))))))))"
deﬁnition "Φmon ≡ {hp_const 0 <P L var5, var4 =P L hp_expect var2 var1, var3^t 2 =P L hp_var var2 var1,
hp_integrable var2 var1, hp_integrable var2 (var1 *t var1)}"
図 3 Isabelle/HOL でのプログラム montecarlo と仮定 Ψ の定義
lemma montecalro_integrable:",IRQ ,,IRQ ,,IRQ ,,monadP_qbs X,,exp_qbs X IRQ | Φmon
`P L ∀ P L n ∈P L INQ . hp_integrable (hp_app hp_montecarlo (hp_const n)) hp_id∧P L hp_integrable (hp_app hp_montecarlo (hp_const n)) (hp_id *t hp_id)"lemma montecarlo_judgement:",IRQ ,,IRQ ,,IRQ ,,monadP_qbs X,,exp_qbs X IRQ | Φmon
`U P L hp_montecarlo ;; exp_qbs INQ (monadP_qbs IRQ )| λr. ∀ P L n ∈P L INQ . hp_const 0 <P L hp_const n−→P L hp_prob (hp_app r (hp_const n)) {y. var5 ≤P L |hp_const y -t var4|t }t≤P L (var3^t 2 /t hp_real (hp_const n)) *t (hp_const 1 /t var5^t 2)"
図4

モンテカルロ法を検証した Isabelle/HOL のコード間の形式化が大部分を占めている．また表中では分けの束縛を自然数の番号で対応づける De Bruijn indexていないが，準ボレル空間全体のうち，準ボレル空間

で表されている．図 1，図 2 の変数とは上の確率測度・確率モナドの形式化に，半分以上の量

var5 = ε, var4 = µ var3 = σ, var2 = d, var1 = hを要した．

と対応づけられる．証明は，先行研究 [12] の Section

Isabelle/HOL で実装した HPProg でのモンテカル
ロ法のプログラムと本研究で示した PL，UPL 判定
式は図 3，図 4 のようになった．ラムダ式は，変数2，Appendix 1 に示されている方針に沿って行なった．

標準ボレル空間

2600 行合，可測集合全体は位相 OX から生成されるボレ

準ボレル空間

8800 行ル 集 合 体 B[OX ] で あ る ．Isabelle/HOL で は 定 数

PPV2400 行

borel :: ’a :: topological space measure が定義

モンテカルロ法 (図 2(1))

140 行

されている．borel は，位相空間型クラスのインス

モンテカルロ法 (図 2(2))

300 行

タンスとなっている型に定義されている定数で，σ-14240 行加法族は位相から生成されるボレル集合体となっている †5 ．本論文の実装では，可測空間としての実数，

合計

3 Isabelle/HOL における測度論，確率論

及び自然数 (離散空間) をそれぞれIsabelle/HOL [11] とは証明支援系の一つで，数学

deﬁnition "real_borel ≡ borel :: real measure"deﬁnition "nat_borel ≡ borel :: nat measure"

や計算機科学に関する定義や定理を厳密に書くことをサポートするソフトウェアである．Isabelle/HOL
は高階論理 (Higher-Order Logic, HOL) に基づいており，特徴として，• 強い論理体系で，排中律や選択公理を使うことができる．

• 多相型，Haskell style の型クラスをサポートしている．

という定数で表す．

(X, ΣX ) から (Y, ΣY ) への可測写像 f と X 上の測度 µ について，U ∈ ΣY に対してf∗ µ(U ) = µ(f −1 (U ))と定めると，f∗ µ は (Y, ΣY ) 上の測度となる．f∗ µ を
測度 µ の可測写像 f による像測度という †6 ．
圏 Meas は対象が可測空間で，射が可測写像であるような圏である．Meas には Giry モナド [4] と呼• Sledgehammer と呼ばれる built-in ツールを使うことにより，自動証明器による証明探索ができる．

ばれる確率分布のモナド (G, ηG , ≫=G ) が定義される．可測空間 X に対して G(X) は X 上の確率測度全体がなす空間である．Isabelle/HOL のライブラリ等が挙げられる．
準ボレル空間は測度論をもとに構成されている．
ここでは，この先用いる概念や記法を確認する．Is-

abelle/HOL のライブラリ [7] には，型’a 上の測度空では，測度空間 µ :: ’a measure に対して

prob algebra µ :: ’a measure measure
return µ :: ’a ⇒ ’a measurebind :: ’a measure ⇒ (’a ⇒ ’b measure)間を値にもつ型’a measure が定義されている．測度空間 µ :: ’a measure の構成要素である集合，σ-加法⇒ ’b measureが定義されている．

族，測度をそれぞれspace µ :: ’a set

4 準ボレル空間の形式化

sets µ :: ’a set set

4. 1 標準ボレル空間

emeasure µ :: ’a set ⇒ ennreal

準ボレル空間の前に，本研究で重要になる可測空で取り出すことができる．型 ennreal は非負拡張間のクラスである標準ボレル空間を Isabelle/HOL で実数を表す型である．2 つの測度空間の積測度は
NX
M Y :: (’a × ’b) measure，X から Y への可測写形式化する．(X, OX ) を完備で可分な距離づけ可能

像全体の集合は X →M Y :: (’a ⇒ ’b) set，ルベーグ
R
積分は x.f x ∂µ :: real †4 という記法が使われて準ボレル空間とは，可測空間 (X, B[OX ]) のことであいる．
位相空間 (X, OX ) を可測空間として参照する場†4 返り値を実数にそろえるため，可積分でない時は 0 を返すよう定義されている．

であるような位相空間 (ポーランド空間) とする．標る．標準ボレル空間は，可算空間であるか R と同型になることが知られている (Kuratowski の定理)．こ
こでの標準ボレル空間は，証明で使いやすい形をした†5 測度は零測度が与えられている．
†6 f が確率変数の時は分布ともいう．

以下の同値な定義を採用する．
定義 4.1. X を可測空間とする．2 つの可測写像
fgの確率論では可測空間を定義し，その後に確率変数が定義される．準ボレル空間では，標本空間を R に限

X−
→R−
→X

定した “確率変数” を定義するところから始まる．

で，g ◦ f = idX をみたすようなものが存在する時 X

定義 4.2 (Heunen et al, [6]). 集合 X と MX ⊆ R →は標準ボレル空間であるという．

X について，(X, MX ) が準ボレル空間 (quasi-Borel

Isabelle/HOL では以下のように定義できる．
deﬁnition standard_borel_R_retract:: "’a measure ⇒ bool" where"standard_borel_R_retract X ≡∃ f ∈ X →M real_borel.
∃ g ∈ real_borel →M X.
∀ x ∈ space X. (g ◦ f) x = x"

N × R や R × R は標準ボレル空間である．
lemma nat_real_standard_borel:"standard_borel_R_retract⊗(nat_borel
M real_borel)"lemma real_real_standard_borel:"standard_borel_R_retract⊗(real_borel
M real_borel)"

R × R が標準ボレル空間であることは，以下の概略に沿って証明した．

2 つ の 可 測 写 像 α : (0, 1) × (0, 1) → (0, 1) と
β : (0, 1) → (0, 1) × (0, 1) で β ◦ α = id(0,1)×(0,1)
をみたすものをつくればよい．α と β を構成できたら，R と (0, 1) の間の同型を用いて，2 つの可測写像
f

g

R×R −
→R−
→ R × R で g ◦ f = id となるような fと g を構成することができる．

r ∈ (0, 1) の小数点以下を 2 進数で展開した時の 小 数 第 n 位 を r で 表 す こ と に す る †7 ． α は
n(r, r ′ ) ∈ (0, 1) × (0, 1) を 0.r1 r1′ r2 r2′ . . . に写し，βspaces) であるとは以下の 3 つの規則
1. α ∈ MX で f : R → R が可測関数のとき，
α ◦ f ∈ MX ．
2. α : R → X が定数関数なら α ∈ MX ．
3. {Si }i∈N を 各 Si が 可 測 集 合 で あ る よ う な Rの 可 算 分 割 と し ，{αi }i∈N ⊆ MX と す る と ，P
i 1 Si α i ∈ M X ．
をみたすときをいう．
本論文を通して，準ボレル空間 (X, MX ) を単に Xと表すことがある．
準ボレル空間は Isabelle/HOL 上で図 5 のように定義することができる．型の定義には，typedef コマン
ドを使う．typedef はすでにある型の，非空な部分集合を表す型を定義するコマンドである．typedef は 2つの定数 Abs newtype と Rep newtype を生成する．
直観的に，Abs newtype は元の型から新しい型への関数，Rep newtype は新しい型から元の型への関数である．準ボレル空間の構成要素である集合・関数の集合を取り出す関数は Rep quasi borel を使って定義できる (図 5)．ライブラリの測度空間も typedef
コマンドで定義されている [7]．

(X, ΣX ) を可測空間とし，MΣX を R から X へのは r ∈ (0, 1) を (0.r1 r3 . . . , 0.r2 r4 . . . ) に写すような写像であるとする †8 ．これらの写像は，非減少な単可測写像全体の集合とすると (X, MΣX ) は準ボレル関数の極限として表すことができるので可測となる．

空間となる．R などの可測空間を準ボレル空間として

また，定義から β ◦ α = id(0,1)×(0,1) となる．

4. 2 準ボレル空間
確率論では，標本空間とよばれる可測空間 (Ω, ΣΩ )を考え，ランダムな事象は A ∈ ΣΩ として表現される．ランダムな事象の観測は，確率変数と呼ばれる可測関数 f : Ω → X を通じて行う．このように，通常†7 ただし，無限に 1 が続かないような方法で表す．
†8 β は 0.1010 . . . を (1, 0) に写すため，値域が (0, 1) ×
(0, 1) となっていない．実際の証明では f と g を構成するときに工夫をする必要がある．

参照するときは，このように定義される準ボレル空間
を表すものとする．
定義 4.3 (Heunen et al, [6]). X と Y を準ボレル空
間とし f : X → Y を写像とする．すべての α ∈ MX
について f ◦ α ∈ MY となるとき，f は X から Y への準ボレル写像とよばれる．

Isabelle/HOL では図 6 のように定義できる．
恒等写像は準ボレル写像で，準ボレル写像の合成も
また準ボレル写像となるので，準ボレル空間を対象とし，準ボレル写像を射とする圏 QBS を構成できる．圏 QBS はカルテシアン閉で，可算直和ももつ

deﬁnition qbs_closed1 :: "(real ⇒ ’a) set ⇒ bool"where "qbs_closed1 Mx ≡ (∀ a ∈ Mx. ∀ f ∈ real_borel →M real_borel. a ◦ f ∈ Mx)"deﬁnition qbs_closed2 :: "[’a set, (real ⇒ ’a) set] ⇒ bool"where "qbs_closed2 X Mx ≡ (∀ x ∈ X. (λr. x) ∈ Mx)"deﬁnition qbs_closed3 :: "(real ⇒ ’a) set ⇒ bool"where "qbs_closed3 Mx ≡ (∀ P::real ⇒ nat. ∀ Fi::nat ⇒ real ⇒ ’a.
(∀ i. P -‘ {i} ∈ sets real_borel)−→ (∀ i. Fi i ∈ Mx)−→ (λr. Fi (P r) r) ∈ Mx)"
typedef ’a quasi_borel ="{(X::’a set, Mx). Mx ⊆ UNIV → X ∧ qbs_closed1 Mx ∧ qbs_closed2 X Mx ∧ qbs_closed3 Mx}"deﬁnition qbs_space :: "’a quasi_borel ⇒ ’a set" where"qbs_space X ≡ fst (Rep_quasi_borel X)"
deﬁnition qbs_Mx :: "’a quasi_borel ⇒ (real ⇒ ’a) set" where"qbs_Mx X ≡ snd (Rep_quasi_borel X)"
図5

準ボレル空間の定義

deﬁnition qbs_morphism :: "[’a quasi_borel, ’b quasi_borel] ⇒ (’a ⇒ ’b) set"
(inﬁxr "→Q " 60) where"qbs_morphism X Y ≡ {f ∈ qbs_space X → qbs_space Y. ∀ α ∈ qbs_Mx X. f ◦ α ∈ qbs_Mx Y}"
図6

準ボレル写像の定義(Heunen et al, [6], Propositions 16–18)．

2. X を標準ボレル空間とすると
f ∈ Meas(X, Y ) ⇔ f ∈ QBS(R(X), R(Y ))4. 3 可測空間との関係
可測写像 f : X → Y は (X, MΣX ) から (Y, MΣY )へ の 準 ボ レ ル 写 像 と な る ．し た がって ，R(X) =特に X が標準ボレル空間なら，L(R(X)) = X である．また，標準ボレル空間に対して，R は可算直
積と可算直和を保存する．

(X, MΣX )，R(f ) = f とすることで函手 R : Meas →QBS が得られる．

4. 4 確率モナド

次に，準ボレル空間から可測空間を構成する．

QBS 上の確率モナドは，Meas 上の Giry モナド

補題 4.4 (Heunen et al, [6]). (X, MX ) を準ボレルから性質を継承している．ここでは，準ボレル空間空間とする．このとき上の確率測度，及び QBS 上の確率モナドを形式化

ΣMX = {U | ∀α ∈ MX .α−1 (U ) ∈ ΣR }とすると，(X, ΣMX ) は可測空間となる．

f が X から Y への準ボレル写像であるとき，fは (X, ΣMX ) から (Y, ΣMY ) への可測写像となるので，函手 L : QBS → Meas を L(X) = (X, ΣMX )，L(f ) = f と定めることができる．
函手 L と R は QBS と Meas の間の随伴をなす．
命題 4.5 (Heunen et al, [6]. Prop 15). (Y, ΣY ) を可測空間とする．このとき，以下が成り立つ．

1. X を準ボレル空間とすると，
f ∈ Meas(L(X), Y ) ⇔ f ∈ QBS(X, R(Y ))する．
定義 4.6 (Heunen et al, [6]). 準ボレル空間 X 上の確率測度とは，同値類 [α, µ]∼ のことである．ただしα ∈ MX ，µ ∈ G(R) で，同値関係は，(α, µ) ∼ (α′ , µ′ ) ⇔ α∗ µ = α∗′ µ′defで定義される．
同値関係 ∼ は，(⋆) すべての準ボレル写像
Z
Zf : X → R について(f ◦ α) dµ = (f ◦ α′ ) dµ′という条件と同値である．したがって，準ボレル写
像 f : X → R と X 上の確率測度 [α, µ]∼ に対して積type synonym ’a qbs_prob_t = "’a quasi_borel * (real ⇒ ’a) * real measure"deﬁnition qbs_prob_t_integral :: "[’a qbs_prob_t, ’a ⇒ real] ⇒ real" where"qbs_prob_t_integral p f ≡(if f ∈ (fst p) →Q IRQ∫
then ( x. f (fst (snd p) x) ∂ (snd (snd p)))else 0)"quotient type ’a qbs_prob_space = "’a qbs_prob_t" / qbs_prob_eq
morphisms rep_qbs_prob_space qbs_prob_spacelift deﬁnition qbs_prob_integral :: "[’a qbs_prob_space, ’a ⇒ real] ⇒ real"
is qbs_prob_t_integralby(auto simp add: qbs_prob_t_integral_def qbs_prob_eq_def)
図7

準ボレル空間上の確率測度と積分

deﬁnition monadP_qbs_Px :: "’a quasi_borel ⇒ ’a qbs_prob_space set" where"monadP_qbs_Px X ≡ {s :: ’a qbs_prob_space. qbs_prob_space_qbs s = X}"
deﬁnition monadP_qbs_MPx :: "’a quasi_borel ⇒ (real ⇒ ’a qbs_prob_space) set" where"monadP_qbs_MPx X ≡ {β. ∃ α∈ qbs_Mx X. ∃ g ∈ real_borel →M prob_algebra real_borel.
∀ r::real. β r = qbs_prob_space (X,α,g r)}"deﬁnition monadP_qbs :: "’a quasi_borel ⇒ ’a qbs_prob_space quasi_borel" where"monadP_qbs X ≡ Abs_quasi_borel (monadP_qbs_Px X, monadP_qbs_MPx X)"
図8

分を

Z

def

f d[α, µ]∼ =確率モナド P

theorem の証明を与える必要がある．

Z(f ◦ α) dµと定めることができる．

QBS 上に確率測度のモナド (P, η, ≫=) を構成
する．

Isabelle/HOL での実装において，準ボレル空間上

命題 4.7 (Heunen et al, [6]). X を準ボレル空間との確率測度は，quotient type コマンド [8] を使ってする．P (X) を X 上の確率測度全体の集合とし，定義する (図 7)．quotient type コマンドは，元とMP (X) = {β |∃α ∈ MX .∃g ∈ Meas(R, G(R)).

def∀r ∈ R.β(r) = [α, g(r)]∼ }なる型から同値関係で商をとった新しい型を生成する．
型 ’a 上の準ボレル空間，実数から ’a への関数，実数とする．このとき，(P (X), MP (X) ) は準ボレル空間上の測度の組の型 ’a qbs prob t を，定義 4.6 の同値となる．
証明は，N×R が標準ボレル空間であること (lemma

関係 (図 7 の qbs prob eq) で割ることで準ボレル空間上の確率測度の型を定義することができる †9 ．準ボレ

nat real standard borel) を 使 う．Isabelle/HOL

ル空間上の確率測度による積分は，’a qbs prob t 上

での定義は図 8 のようになる．

で定義した関数を lift definition で商型上の関数

命題 4.8 (Heunen et al, [6]). X を準ボレル空間，µに持ち上げることで定義することができる．このとき，を R 上の任意の確率測度として，ηX : X → P (X) を関数が well-deﬁned であることを表す respectfulnessηX (x) = [λr.x, µ]∼defとする．さらに，[α, µ]∼ ∈ P (X)，f : X → P (Y ) を†9 本当は，(X, α, µ) という組全体ではなく，「α ∈ MXかつ µ が確率測度であるような組」の中で商を取る必要がある．実際の実装では半同値関係で割ることでこの要求をみたすよう定義されている．

準ボレル写像とする．このとき，f が準ボレル写像であることから，ある β ∈ MY と g ∈ Meas(R, G(R))

があって，(f ◦ α)(r) = [β, g(r)]∼ となる．この β とg を使ってdef[α, µ]∼ ≫= f = [β, µ ≫=G g]∼と定義する．

付け規則の例をいくつか記しておく．
Γ⊢e:TΓ ⊢ return e : P [T ]Γ ⊢ e : P [T ]Γ ⊢ f : T ⇒ P [T ′ ]この補題を示すために，Giry モナドがモナドであΓ ⊢ bind e f : P [T ′ ]Γ ⊢ e : realΓ ⊢ Bernoulli(e) : P [bool]Γ ⊢ e : realΓ ⊢ e′ : real′Γ ⊢ Gauss(e, e ) : P [real]意味論では，HPProg の型 T は QBS の対象 [[T ]] としることと R × R が標準ボレル空間であること (lemmaて解釈され，言語 HPProg の型付けされた項 Γ ⊢ e : T

real real standard borel) を使う．

は QBS の射 [[Γ]] → [[T ]] として解釈される．QBS は

これらの演算子は well-deﬁned である．
補題 4.9 (Heunen et al, [6]). (P, η, ≫=) は QBS上の可換な強モナドである．

関数 l を l([α, µ]∼ ) = α∗ µ とすると，l は L(P (X))

カルテシアン閉であるから，関数抽象や関数適用は自から G(L(X)) への単射な可測写像となる．とくに X然に解釈できる．実装における型判定は以下のようにが標準ボレル空間のとき，l は全単射である．

定義できる．

5 PPV の形式化
この節では，PPV で使われる言語 HPProg，PL，UPL を導入する．実装に合わせるため，型や項の定義を少し変えている．

PPV には準ボレル空間に基づいた健全な意味論が与えられている．PPV の実装はこの意味論に沿って行なう．実装の方法は，対象の論理体系を証明支援系の論理で直接記述する shallow embbedding による．

Shallow embedding による形式化は，型付け規則や導出規則を補題として示す形で追加していくため，定数や公理を後から追加するのが容易である．また，型付けや導出規則が HOL に対して健全であることを確認することができる．

5. 1 言語: HPProg
PPV で使われる関数型確率的プログラミング言語
HPProg の型は
T ::= unit | nat | bool | real | preal | T × T| T ⇒ T | P [T ]で定義される．ここで real および preal はそれぞれ実数 R，非負拡張実数 [0, ∞] を表す型，P [T ] は T
上の確率測度の型である．

HPProg の項は
e ::= 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)で定義される．項には標準的な方法で型をつける．型

deﬁnition"hpprog_typing Γ e T ≡ e ∈ Γ →Q T"

各型付け規則は補題として示すことになる．たとえば実数の定数は以下のように定義，型付けを行うことができる．
deﬁnition hp_const :: "’a ⇒ ’env ⇒ ’a" where"hp_const k ≡ (λenv. k)"lemma hpt_realc:"Γ `t (hp_const (r :: real)) ;; IRQ "using qbs_morphism_const[of r "IRQ " Γ]by(simp add: hpprog_typing_def hp_const_def)

5. 2 論理: PL
論理式で扱う項は，HPProg の項に期待値を表す項

Ex∼t [t x] を追加したものである．論理式は以下で定義される．

ϕ ::= (t = t) | (t < t) | ⊤ | ⊥ | ϕ ∧ ϕ | ϕ → ϕ| ∀x : T.ϕ | ∃x : T.ϕ
PL の判定式は
Γ | Ψ ⊢PL ϕという形をしている．Γ は型環境，Ψ は仮定の集合，

ϕ は結論である．PL の導出規則には以下のようなも
のがある．

ϕ∈Ψ
AX
Γ | Ψ ⊢PL ϕ
Γ | Ψ ⊢PL ψ → ϕ
Γ | Ψ ⊢PL ψ→E
Γ | Ψ ⊢PL ϕ
Γ | Ψ ⊢PL ϕ[t/x]Γ | Ψ ⊢PL t = u
SUBSTΓ | Ψ ⊢PL ϕ[u/x]また，数の計算に関する規則や期待値の線形性といった等式を公理として追加する．先行研究では，非になる．

負関数の期待値だけを考えることで可積分性の議論を省略していた．先行研究のモンテカルロ法の検証例

5. 3 プログラム論理: UPL

では一般の関数も扱うので，本研究では可積分性の議

UPL は
Γ | Ψ ⊢UPL e : T | ϕ

論も行う．
Γ | Ψ `PL integrable µ f

Γ | Ψ `PL integrable µ g

Γ | Ψ `PL Ex∼µ [f x] + Ex∼µ [g x] = Ex∼µ [f x + g x]という形の判定式をもつ．PL との違いは，判定式にHPProg 項 e とその型 T が含まれている．また，結論の論理式 ϕ にはプログラム変数と呼ばれる型 T のΓ ` e : P [Y ]Γ, y : Y ` e′ : ZΓ ` e′′ : Z ⇒ real

Γ | Ψ `PL Ex∼bind e λy.return(e′ ) [e′′ ] = Ey∼e [e′′ [e′ /x]]

PL 判定式 Γ | Ψ ⊢PL ϕ の意味は，「任意の x ∈ Γ について，Ψ x が成り立つならば，ϕ x も成り立つ」と定義される †10 ．Isabelle/HOL では以下のように定義できる．
deﬁnition "hp_conjall Ψ ≡ (λenv. ∀ φ∈Ψ. φ env)"
deﬁnition "pl_der Γ Ψ φ ≡(∀ x∈ qbs_space Γ. hp_conjall Ψ x −→ φ x)"

各推論規則は，補題として示す．
lemma pl_ax:
assumes "φ ∈ Ψ"shows "Γ | Ψ `P L φ"lemma pl_impE:
assumes "Γ | Ψ `P L ψ −→P L φ"and "Γ | Ψ `P L ψ"shows "Γ | Ψ `P L φ"

項 r が含まれている．UPL の導出規則には以下のよ
うなものがある．
Γ | Ψ ⊢UPL e : T | φ1

Γ | Ψ ⊢PL φ1 [e/r] → φ2 [e/r]Γ | Ψ ⊢UPL e : T | φ2
Γ | Ψ ⊢UPL f : τ ⇒ σ | ∀x.ϕ′ → ϕ[r x/r] Γ | Ψ ⊢UPL e : τ | ϕ′
Γ | Ψ ⊢UPL f e : σ | ϕ[e/x]Γ | Ψ ⊢UPL e : T | φ の意味は「Γ ⊢ e : T 」かつ「すべての x ∈ Γ について，Ψ x が成り立つなら

φ[e/r] x が成り立つ」である．Isabelle/HOL では
deﬁnition "upl_der Γ Ψ e T φ ≡((Γ `t e ;; T) ∧ (∃ φ’. φ = (λt k. φ’ k (t k)))∧ (∀ k∈qbs_space Γ. hp_conjall Ψ k −→ φ e k))"と定義できる．定義の「∃φ′ .φ = (λt k.φ′ k (t k))」は，プログラム e の意味の取り方を限定するために必要な条件である．プログラム変数 r は関数抽象の束縛変数として表す．Isabelle/HOL の実装におけるUPL 判定式の例を示す．
lemma pl_expect_add:
assumes "Γ | Ψ `P L hp_integrable t e1"and "Γ | Ψ `P L hp_integrable t e2"
shows "Γ | Ψ `P L hp_expect t (e1 +t e2)=P L hp_expect t e1 +t hp_expect t e2"論理式での代入 ϕ[t/x] は，Isabelle/HOL での関数適用を使い ϕ t と表すことができ，代入規則は以下の形になる．
lemma pl_subst’:
assumes "φ = (λt. λk. φ’ k (t k))""Γ | Ψ `P L t =P L u"and "Γ | Ψ `P L φ t"shows "Γ | Ψ `P L φ u"

規則の一つ目の仮定で，論理式中の項の意味の取り方を制限している．代入を Isabelle/HOL の関数適用として表すことで，判定式にルールを適用する時のインスタンス化がうまくいきやすくなり，証明の負担軽減

lemma"Γ | Ψ `U P L hp_const 1 ;; INQ| λr. hp_const 1 ≤P L r +t r"

UPL でも同様に，各導出規則は補題として示す．
lemma upl_app:
assumes "φ =(λt r env. φ’ (t env) env (r env))""Γ | Ψ `U P L f ;; exp_qbs T1 T2 |(λr. ∀ P L x∈P L T1. ψ (hp_const x) −→P L
φ (hp_const x) (hp_app r (hp_const x)))"and "Γ | Ψ `U P L e ;; T1 | ψ"shows "Γ | Ψ `U P L
hp_app f e ;; T2 | φ e"lemma upl_sub:assumes "ψ = (λr env. ψ’ env (r env))""Γ | Ψ `U P L e ;; T | φ"and "Γ | Ψ `P L φ e −→P L ψ e"shows "Γ | Ψ `U P L e ;; T | ψ"

UPL は PL に対して完全である．つまり以下の定†10 先 行 研 究 [12] で は ，準 ボ レ ル 空 間 上 の 述 語 の 圏
Pred(QBS) を使って意味を与えていたが，本研究では実装が容易な，圏を介さない定義を採用する．

理が成り立つ．
定理 5.1 (Sato et al, [12]. Theorem 6.1). 以下は同値である．

• Γ | Ψ ⊢PL ϕ[e/r] が導出できる．
• Γ | Ψ ⊢UPL e : T | ϕ が導出できる．
PL や UPL が意味論に基づいて定義されているので，完全性は定義を展開することで直ちに証明される．
lemma pl_upl_complete:assumes "Γ `t t ;; T"
and "φ = (λt k. φ’ k (t k))"shows "(Γ | Ψ `P L φ t) ←→(Γ | Ψ `U P L t ;; T | φ)"using assms
by(auto simp add: pl_der_def upl_der_def)

6 まとめ
本研究では，準ボレル空間，及び意味論に基づいた

PPV を Isabelle/HOL で形式化し，先行研究の例が証明支援系の上でも証明することができることを示した．
現在の PPV の実装は，プログラムが De Bruijn

index で表されており，可読性が低くプログラムを書くことも容易ではないため，プログラムの表現方法を改良していきたい．
また，条件付き推論を含むプログラムの検証ができるように，準ボレル空間上の測度を一般の測度に拡張していく．準ボレル空間の圏 QBS 上には σ 有限測度モナドが構成できる [13]．その証明は確率分布モナ
ド P の場合と大きく異なるため，形式化には相応の手間がかかると予想される．

参 考 文 献[ 1 ] Aguirre, A., Barthe, G., Gaboardi, M., Garg, D.,
and Strub, P.-Y.: A Relational Logic for HigherOrder Programs, Proc. ACM Program. Lang.,
Vol. 1, No. ICFP(2017).
[ 2 ] Aumann, R. J.: Borel structures for function
spaces, Illinois Journal of Mathematics, Vol. 5,
No. 4(1961), pp. 614 – 630.
[ 3 ] Eberl, M., Hölzl, J., and Nipkow, T.: A
Veriﬁed Compiler for Probability Density Functions, Programming Languages and Systems, Vitek,J.(ed.), Berlin, Heidelberg, Springer Berlin Heidelberg, 2015, pp. 80–104.
[ 4 ] Giry, M.: A categorical approach to probability theory, Categorical Aspects of Topology andAnalysis, Banaschewski, B.(ed.), Berlin, Heidelberg, Springer Berlin Heidelberg, 1982, pp. 68–85.
[ 5 ] Goodman, N. D. et al.: Church: a language forgenerative models, UAI 2008, Proceedings of the24th Conference in Uncertainty in Artiﬁcial Intelligence, AUAI Press, 2008, pp. 220–229.
[ 6 ] Heunen, C., Kammar, O., Staton, S., and Yang,
H.: A Convenient Category for Higher-Order Probability Theory, Proceedings of the 32nd Annual
ACM/IEEE Symposium on Logic in Computer Science, LICS ’17, IEEE Press, 2017.
[ 7 ] Hölzl, J. and Heller, A.: Three Chapters of
Measure Theory in Isabelle/HOL, Interactive Theorem Proving, van Eekelen, M., Geuvers, H.,
Schmaltz, J., and Wiedijk, F.(eds.), Berlin, Heidelberg, Springer Berlin Heidelberg, 2011, pp. 135–
151.
[ 8 ] Kaliszyk, C. and Urban, C.: Quotients Revisited for Isabelle/HOL, Proceedings of the 2011 ACM
Symposium on Applied Computing, SAC ’11, New
York, NY, USA, Association for Computing Machinery, 2011, pp. 1639–1644.
[ 9 ] Lochbihler, A.: Probabilistic Functions andCryptographic Oracles in Higher Order Logic,
Programming Languages and Systems, Thiemann,P.(ed.), Berlin, Heidelberg, Springer Berlin Heidelberg, 2016, pp. 503–531.
[10] Narayanan, P., Carette, J., Romano, W., Shan,C., and Zinkov, R.: Probabilistic inference by program transformation in Hakaru (system description), International Symposium on Functional and
Logic Programming - 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6,
2016, Proceedings, Springer, 2016, pp. 62–79.
[11] Nipkow, T., Wenzel, M., and Paulson, L. C.:
Isabelle/HOL: A Proof Assistant for Higher-Order
Logic, Springer-Verlag, Berlin, Heidelberg, 2002.
[12] Sato, T., Aguirre, A., Barthe, G., Gaboardi, M.,
Garg, D., and Hsu, J.: Formal veriﬁcation of higherorder probabilistic programs: reasoning about approximation, convergence, Bayesian inference, andoptimization, Proceedings of the ACM on Programming Languages, Vol. 3, No. POPL(2019), pp. 1–30.
[13] Ścibior, A., Kammar, O., Vákár, M., Staton, S.,
Yang, H., Cai, Y., Ostermann, K., Moss, S. K., Heunen, C., and Ghahramani, Z.: Denotational Validation of Higher-Order Bayesian Inference, Proc.
ACM Program. Lang., Vol. 2, No. POPL(2017).
[14] Stan Development Team: Stan Modeling Language Users Guide and Reference Manual, Version
2.27.0, 2021.
[15] Wood, F., van de Meent, J. W., and Mansinghka, V.: A New Approach to Probabilistic Programming Inference, Proceedings of the 17th International conference on Artiﬁcial Intelligence andStatistics, 2014, pp. 1024–1032.