技術的概要：離散プログラム論理を用いた連続分布に対する正確なサンプリング器の検証

問題提起

連続確率分布に対するサンプリングアルゴリズムの大半の実装は、浮動小数点演算に依存している。多くのアプリケーションにとっては許容可能であるが、浮動小数点演算は解析が困難な丸め誤差を導入し、特に厳密な算術を仮定して形式的に開発されることが多い差分プライバシーにおいて、重大なセキュリティ脆弱性につながる可能性がある。

代替案として、計算可能な実数に基づく正確なサンプリングアルゴリズムを用いることが考えられる。これらは、連続的なサンプルの桁を任意の精度まで遅延的に生成できる。しかし、これらのアルゴリズムは複雑である。確率的選択、高階関数、動的に割り当てられた可変状態といった、意味論的に困難な言語機能の組み合わせを必要とする。確率的検証のための既存のプログラム論理はこのタスクには不十分である。先行研究は、離散分布への推論を制限するか、あるいは連続分布からのサンプリングのためのプリミティブの存在を仮定する（多くの場合、非計算可能な実数演算に依存している）かのいずれかである。その結果、離散的で状態を持つプログラミングモデル内で動作する、計算可能な正確な連続分布サンプリング器の正しさを検証する形式的な手法が存在しない。

手法

著者らは、計算可能な分布に対する正確なサンプリングアルゴリズムの正しさを検証するために設計された高階分離論理Continuous-Erisを提示する。Continuous-Eris は、離散確率プログラムの近似正しさを検証するための論理であるErisを拡張し、Iris分離論理フレームワークに基づいて構築されている。

核心的な手法は、離散的な推論と連続的な推論の間のギャップを埋める、以下の 3 つの論理的要素に依存している。

1. エラー・クレジット (Error Credits): Eris から借用されたもので、仕様の失敗確率の上限を表す分離論理リソース $E(r)$ である。これらは、低確率のエラー事象を除外するためにクレジットを「消費」することで、確率的プログラムに関するモジュラーな推論を可能にする。
2. タイム・レシート (Time Receipts): Mével らから適応されたもので、論理の部分正しさを内部化するために用いられる。残りの実行ステップ数 ($StepsLeft(k)$) を追跡することで、論理は潜在的に無限の実行の有限な接頭辞について推論できる。これは、正確なサンプリング器が無限のビット列を完全に生成することなく遅延評価を含むことが多いため、極めて重要である。
3. 事前サンプリングテープ (Pre-sampling Tapes): Clutch から適応されたもので、証明が将来の確率的サンプリングコマンドの結果を事前に決定することを可能にする。標準的なテープは有限であるが、著者らはこれらをタイム・レシートと組み合わせて無限の事前サンプリングテープをシミュレートする。このメカニズムにより、論理はプログラムが任意の有限の実行中に有限個のビットしか生成しないにもかかわらず、特定の実数 $r$（無限ビット列として表現される）に基づいてエラー・クレジットを条件付けることができる。

理論的基盤

この論理は、Marionneau らの離散的な正しさの仕様を連続的な設定に一般化する。離散確率質量関数によってサンプリング器を特徴付ける代わりに、Continuous-Eris は確率密度関数上のリーマン積分によってサンプリング器を特徴付ける。

$[0, 1]$ 内の一様実数を生成するサンプリング器 $U$ に対する中心的な仕様パターンは以下の通りである。
$$\forall F \in PC([0, 1]), \quad \left\{ E\left(\int_0^1 F(x) dx\right) \right\} U() \{ v. \exists r. E(F(r)) * IsReal\ v\ r \}$$
ここで、$F$ は有界な区分的連続関数である。論理は、クレジットの期待値が保存される限り、サンプリングされた値 $r$ が一様に引き出されたかのように、その値に基づいてクレジットを条件付けることを可能にする。このアプローチの健全性は、有限の事前サンプリングから導かれるリーマン和が積分を任意に近づけて近似でき、離散化誤差が「空中から生じた」エラー・クレジットによって支払われるという事実に依存している。

主要な貢献

1. Continuous-Eris 論理: エラー・クレジット、タイム・レシート、事前サンプリングテープを組み合わせ、計算可能な連続サンプリングアルゴリズムを検証する新しいプログラム論理。高階関数、可変状態、動的割り当てをサポートする。
2. 正確なサンプリング器の形式的検証: 著者らは、以下の正確なサンプリング器の形式的に検証された実装を提供する。
   • $[0, 1]$ 上の一様分布。
   • ガウス（正規）分布。
   • ラプラス分布。
     これらの実装は Karney によるアルゴリズムに基づき、遅延ビットリスト表現を利用している。
3. 検証された構成実数演算ライブラリ: Continuous-Eris 内で検証された、正確な実数演算（CReal の適応版）のライブラリ。このライブラリは、遅延実数に対する演算（加算、否定、スケーリング、比較）をサポートし、より単純な分布から複雑な分布を構築することを可能にする。
4. 差分プライバシーのための精度境界: 検証されたラプラス・サンプリング器が、差分プライバシーの文献で用いられる特定の精度境界を満たすという形式的証明。これは、サンプリング器の出力が浮動小数点近似に依存することなく、プライバシー保護メカニズムに必要な理論的保証に準拠していることを示している。
5. 機械化: すべての結果は、Iris フレームワークと Coquelicot 実解析ライブラリに基づき、Rocq 証明支援システム（旧 Coq）で機械化されている。

結果

本論文は、2 つの一様サンプルの最大値を計算するMaxU2プログラムの検証と、完全なKarney ガウス・サンプリング器の検証を通じて、Continuous-Eris の有用性を示している。

• MaxU2: 著者らは、このプログラムが確率密度 $\mu_{max}(x) = 2x$ で分布する値を返すことを証明する。証明には、再帰的なビット比較を処理するための反復積分と Löb 帰納法が含まれる。
• ガウス・サンプリング器: 検証はモジュラーな構造に従い、ベルヌーイ試行、整数部、棄却サンプリングループのサブルーチンを検証する。証明は、サンプリング器が正しいガウス密度を持つ値を生成することを確立する。
• ラプラス・サンプリング器: 著者らはラプラス分布のサンプリング器を検証し、追加の公理として付加することなく、論理から直接 $P[|L_{\epsilon, \mu} - \mu| > \frac{\log(1/\beta)}{\epsilon}] \leq \beta$ という尾部境界を導出する。

意義と主張

本論文は、可変状態と高階関数を利用する連続分布に対する正確な計算可能なサンプリング器を検証できる最初の手法を提供することにより、形式的検証における重要なギャップを埋めると主張している。

• 近似なしの正しさ: 連続プリミティブを仮定するか、浮動小数点演算を使用する先行研究とは異なり、Continuous-Eris は離散プリミティブ（ベルヌーイ試行）のみを使用して（任意の精度で）正確なサンプルを生成するアルゴリズムを検証する。
• 複雑性の処理: この論理は、通常、意味論的に推論することが困難である、確率性、可変状態、高階関数を組み合わせる際の意味論的課題を成功裡に管理する。
• 実用性: ラプラス・サンプリング器とその精度境界を検証することで、浮動小数点誤差に対する厳密な保証を持つ差分プライバシーシステムの構築基盤を提供する。
• 謙虚さ: 著者らは限界を認めている。現在の手法はリーマン積分に依存しており、クレジット分布関数が区分的連続である必要がある。これにより、非可算な不連続点（例えば、すべての有理点を避けるなど）を持つ分布に関する推論は妨げられる。さらに、本論文は部分正しさに焦点を当てており、これらのサンプリング器のほぼ確実な終了性の証明は、将来の作業や Total Eris などの他の論理に委ねられている。

要約すると、Continuous-Eris は、複雑で状態を持つプログラムが連続分布からの正確なサンプリングを正しく実装していることを検証するための厳密で機械化されたフレームワークを提供し、理論的な計算可能解析と実用的なプログラム検証の間のギャップを埋めるものである。