Evaluating Wasserstein Distance between Outputs of Probabilistic Programs

確率的プログラムの入力の変動に応じた出力の変動を調べる方法の1つとして，出力の分布をワッサースタイン距離で測ることが考えられる．ワッサースタイン距離は，直観的には，点どうしの距離を確率分布の間の距離に拡張したもので，数学的には分布間のカップリング（与えられた分布を周辺分布に持つ確率分布）における点どうしの距離の期待値の下限である．近年ではWGANなどの機械学習手法にも用いられる．離散的な確率分布のみを持つ確率的プログラムについては，出力の分布間のワッサースタイン距離の上界を与える方法が提案されている[Aguirre+, 2021]．本発表では，連続的な確率分布を持つような確率的プログラムについてこの種の検証を行う下記の手法を提案し，正規分布からのサンプリングを含む確率的プログラムにおける提案手法の適用例を紹介する．先行研究[Aguirre+, 2021]では，出力の分布間のワッサースタイン距離の上界を与える関数を，プログラムの構造に関して帰納的に構成している．本研究では，このような関数を直接構成するのではなく，出力の分布間のカップリングを構成し，それに従う点の間の距離の期待値としてワッサースタイン距離の上界を与える．カップリングの構成は，可測空間と可測関数の圏上のスパンを介在して，カップリングを与える可測関数をプログラムの構造に関して帰納的に構成することによって行う．

A possible approach to measuring the sensitivity of a probabilistic program is measuring the Wasserstein metric between the distributions of outputs. Intuitively, it extends a metric between points to a metric between probability distributions. Mathematically, it is the greatest lower bound of expected metrics for couplings between given distributions, that is, a distribution whose marginals are the given distributions. Recently, in studies on machine learning such as WGAN, the Wasserstein metric appears. For probabilistic programs containing only discrete distributions, a previous study [Aguirre+, 2021] gives a method to over-approximate the Wasserstein metric between the distributions of outputs. In this presentation, we propose a new method to over-approximate the Wasserstein metric between the distributions of outputs of probabilistic programs that contain random samplings from continuous distributions. The previous study [Aguirre+, 2021] introduces a method of inductive construction of a function over-approximating the Wasserstein metric for the structure of programs. In our new method, instead of constructing directly a function over-approximating the Wasserstein metric, we construct a measurable function giving a coupling of the distributions of the outputs. Then, we calculate an upper bound of the Wasserstein metric of the distributions of outputs as the expected distance under the coupling. Here, the measurable function giving the coupling is constructed inductively on the structure of the program via spans over the category of measurable spaces and measurable functions.