Bayesian Networks and Proof-Nets: the proof-theory of Bayesian Inference

技術要約：ベイズネットワークとプルーフネット：ベイズ推論の証明論

問題提起
ベイズネットワーク（BN）は、確率的推論のための標準的なツールであり、結合確率分布のコンパクトで因数分解された表現を提供し、効率的な推論アルゴリズムを可能にする。しかし、既存の圏論的な確率的推論のアプローチは、豊かな構成的かつグラフィカルな言語（例：ストリング図）を提供している一方で、推論の計算コスト（時間および空間）を考慮できていないことが多い。逆に、標準的なBNアルゴリズムは効率的であるが、グラフ的推論と論理の構造的特性を統一する深い証明論的な基礎を欠いている。著者らは、構成的・グラフィカルな推論と計算効率を同時に収容できるフレームワーク、特に、圏論的確率論において欠落しがちな「コストを意識した」視点に対処できるフレームワークの必要性を指摘している。

手法
本論文は、線形論理（LL）、具体的にはそのグラフ構文である**プルーフネット（proof-nets）**を用いた、ベイズ推論の証明論的な記述を提案する。その手法は以下の通りである：

1. 形式体系の拡張： 著者らは、**確率的ボックス（probabilistic boxes）**を用いてマルチプリカティブ線形論理（MLL）を拡張する。これらのボックスは、ベイズネットワークのノードに関連付けられた条件付き確率テーブル（CPT）をエンコードする。構文には、標準的なMLLノード（テンソル、パー、カット、公理）に加え、構造規則（弱化、縮約）およびこれら新しい確率的ボックスが含まれる。
2. 対応関係： 著者らは、ベイズネットワークと**ベイズ・プルーフネット（bpn）**との間の健全かつ完全な対応関係を確立する。bpnは、ボックスがCPTを保持し、正の結論が区別され、すべての結論が正であるプルーフネットとして定義される。
3. 因子による意味論： 先行研究（例：[8]）の因子ベースの意味論を採用し、bpnの意味論は、ボックスに関連付けられた因子の積に続き、結論に含まれない変数の周辺化（和をとること）として定義される。これにより、その意味論はBNの標準的な定義と直接的に一致する。
4. グラフの分解： 帰納的な構文に従って厳密に分解されるプルーフツリーとは異なり、プルーフネットは柔軟なグラフ分解を可能にする。著者らは、分割（splitting）（ax-expansionによる）を利用して、bpnをカットノードによって接続されたサブネットへと分解し、「カットネット（cut-net）」と呼ばれる構造を形成する。
5. グラフ書き換え： 著者らは、カット消去（およびその双対であるカット拡大）をグラフ書き換えプロセスとして用いる。これには、標準的な簡約ルールと、グラフを「刈り取る（prune）」ために使用される特定の**ボックス／弱化簡約（box/weakening reduction）**が含まれ、これにより、無関係な変数の除去による周辺化を効果的に実行する。

主な貢献

• 推論の証明論的記述： 本論文は、カット消去およびカット拡大がベイズ推論において中心的な役割を果たすという、基礎的な理解を提供する。これは、推論を単なる計算としてではなく、証明の構造的な変換として捉えるものである。
• より強力な構成性： 著者らは、グラフに特有の「コンポーネント」の概念を導入しており、これは従来の木ベースの定義よりも強力である。著者らは**定理5.2（グラフの構成性）**を証明し、プルーフネットの意味論は、カットによって接続されたサブネットへとグラフをどのように分解するかに関わらず、構成的に計算できることを示している。
  $$\llbracket Cut(R_1, R_2) \rrbracket = \sum_Z (\llbracket R_1 \rrbracket \odot \llbracket R_2 \rrbracket)$$
  ここで、$Z$は周辺化される変数名を表す。
• d-分離のグラフィカルな証明： セクション7において、著者らはd-分離（条件付き独立性の基準）の健全性の直接的な図式的証明を提供する。グラフ分解と意味論の構成性を用いることで、グラフ上で（条件付け集合によってラベル付けされたエッジを除去した後に）2つの変数の集合が断絶している場合、それらは条件付き独立であることを示す。
• カットネットによる効率的な推論： 本論文は、プルーフネットを用いて効率的なBN推論アルゴリズム（変数消去法など）を模倣する方法を示す。bpnを根付きカットネット（rooted cut-net）（サブネットの木のような構造）へと変換することにより、計算コストを大幅に削減できることを示す。コストは、全変数数ではなく、カットネットの幅（width）（任意のサブネットにおける変数の最大数）によって決定される。
• 型付けと逐次化： グラフ分解（カットネット）が必ずしもシーケント計算の証明ツリーと直接対応しないという課題に対処する。著者らは、任意のカットネットを$\otimes/\parr$-展開によって、サブネットが最大で一つのカットによって接続される等価な形式へと変換できることを証明し（定理8.3）、これにより分解を有効なシーケント計算の証明ツリーへと翻訳できることを示す。

結果

• 健全性と完全性： BNとbpnの対応関係が健全かつ完全であることが証明されている。すべてのBNは正のbpnに写像され、任意の正のbpnの標準形はBNへと写像される。
• 停止性と合流性： 簡約系（標準的なカット消去および新しいボックス／弱化簡則を含む）は、停止的かつ合流的であることが証明されている。
• 計算効率： 本論文は、プルーフネットをカットネットへと因子分解することで、意味論を計算するための空間および時間の複雑さが、$O(m \cdot 2^n)$（$n$は全変数数）から$O(n \cdot 2^w)$（$w$はカットネットの幅）へと低下することを示す。これは、BNにおける変数消去法の効率化の利点を反映している。
• 不変性： bpnの意味論は簡約および拡大に対して不変であり、これにより書き換えプロセス中に確率的な意味が保持されることが保証される。

意義
本論文は、ベイズネットワークに見られる因数分解された計算の効率性と、証明論のグラフィカルかつ構成的な推論の両方の「最良の部分を解き放つ」ことを主張している。ベイズ推論を線形論理の豊かなツールボックスに根付かせることで、著者らは本質的に「リソースを意識した」フレームワークを提供している。これにより、証明の構造的操作（グラフ書き換え）が、確率的推論のステップ（周辺化および条件付け）に直接対応するという、統一的な扱いが可能となる。本研究は、抽象的で構造的なエレガンスを持つ圏論的確率論と、実用的でコストを意識した確率的推論の要求との間の溝を埋めるものであり、「証明論の礎石」（カット消去）が効率的な推論のメカニズムとして機能するという新しい視点を提供している。