💻 computer science

noDice: Inference for Discrete Probabilistic Programs with Nondeterminism and Conditioning

この論文は、マルコフ決定過程（MDP）の構築と決定図の活用を通じて、非決定性や条件付き推論をサポートする離散確率プログラミング言語「noDice」を提案し、従来の Dice エンジンの限界を克服する手法を提示しています。

原著者： Tobias Gürtler, Benjamin Lucien Kaminski

公開日 2026-02-24

📖 1 分で読めます☕ さくっと読める

原著者： Tobias Gürtler, Benjamin Lucien Kaminski

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

noDice：不確実性と「運命」を計算する新しい魔法の箱

この論文は、**「noDice（ノーダイス）」**という新しいコンピュータープログラムの仕組みについて説明しています。名前には「サイコロ（Dice）」という言葉が入っていますが、実は「サイコロを振らない」ことで、より賢く複雑な問題を解くことを目指しています。

わかりやすくするために、この技術を**「未来のシミュレーター」と「運命の分かれ道」**という物語で説明してみましょう。

1. 背景：なぜ「サイコロ」だけでは足りないのか？

現代のコンピューターは、確率（サイコロを振って出る目）を使って、天気予報や株価、人工知能の学習などをシミュレーションできます。これを「確率的プログラミング」と呼びます。

しかし、現実の世界には「確率」だけでは説明できない**「不確実性（ nondeterminism ）」**があります。

例：自動運転車が歩行者にぶつかるかどうか。
- 確率的な要素： 歩行者が急に飛び出す確率は 10%。
- 不確実な要素： 歩行者が「意図的に」飛び出すか、それとも「転んで」飛び出すか、あるいは「信号を無視する」か。これは確率で決まるのではなく、「最悪のシナリオ」を想定して考える必要があるのです。

これまでのツールは、「サイコロ（確率）」は得意でしたが、「意志や未知の選択（不確実性）」を同時に扱うのが苦手でした。そこで登場するのがnoDiceです。

2. noDice の魔法：3 つのステップで問題を解決

noDice は、複雑なプログラムを 3 つのステップで処理し、**「最も悪い場合でも、どれくらい安全か（または成功するか）」**を計算します。

ステップ 1：物語を「論理パズル」に翻訳する（コンパイル）

まず、noDice はプログラムを**「真（T）」か「偽（F）」**でしか書けない、シンプルな論理パズル（ブーリアン式）に変換します。

アナロジー： 複雑な小説を、すべて「はい」か「いいえ」で答えるアンケート形式に変えるようなものです。これにより、コンピューターが処理しやすい形になります。

ステップ 2：巨大な地図を「縮小」する（決定図）

次に、そのパズルを**「決定図（ADD）」**という特殊な地図に変えます。

アナロジー： 東京の全道路をすべて描いた巨大な地図（状態空間）があるとします。しかし、noDice は「ここは必ず通る道」「ここは誰も通らない道」を自動的に消去し、必要な道だけを残したコンパクトな地図にします。
これにより、計算量が爆発的に減り、巨大な問題でも扱えるようになります。

ステップ 3：迷路を「最悪のシナリオ」で解く（MDP）

最後に、その縮小された地図を**「マルコフ決定過程（MDP）」**という迷路に変えます。

アナロジー： この迷路には、**「運命の分かれ道」**があります。
- サイコロの分かれ道： 「70% の確率で左、30% で右」のように、確率で決まる道。
- 意志の分かれ道： 「敵が最悪の選択をするなら、どちらの道を選ぶか？」という、**「最悪の敵（または最悪の状況）」**が選ぶ道。
noDice は、**「敵がどんなに悪意を持って道を選んでも、私たちが目的（ゴール）にたどり着ける確率は最大でどれくらいか？」**を計算します。

3. 具体的な例：飛行機と車両の衝突回避

論文にある例を使って説明しましょう。

状況： 飛行機が着陸しようとしています。滑走路に車が通る可能性があります。
問題： 車の動きは「確率的」ですが、ドライバーが「いつ、どの速度で走るか」は**「不確実」**です。もしかしたら、ドライバーは飛行機が着陸する瞬間に故意に滑走路に飛び出すかもしれません（最悪のシナリオ）。
noDice の役割：
- 従来のツールは「車の動きを確率で平均化」してしまい、最悪のケースを見逃す可能性があります。
- noDiceは、「車がどんな戦略をとっても（遅く走ろうが、速く走ろうが、故意に止まろうが）、飛行機が安全に着陸できる確率は最大で 3.6% しかない」という**「最悪の場合の限界値」**を正確に突き止めました。

4. なぜこれがすごいのか？

従来の方法： 全ての可能性を一つ一つ試そうとすると、計算量が天文学的に増え、現実的な時間で答えが出ません（「状態空間の爆発」と呼ばれる問題）。
noDice の方法： 「決定図」という技術を使って、同じような道や無駄な道を自動的に消去します。これにより、巨大な迷路を、小さなノートに収まるサイズに圧縮して計算できます。
結果： 既存の最強のツール（Storm など）よりも、はるかに速く、かつ正確に「最悪のシナリオ」を計算できることが実験で証明されました。

まとめ

noDiceは、「確率（サイコロ）」と「意志（不確実性）」が混ざり合った複雑な世界を、「最悪のシナリオ」を見逃さないように、かつ**「無駄な計算を省いて」素早く**解き明かすための新しい魔法の箱です。

これにより、自動運転、ネットワークのセキュリティ、医療診断など、**「もしも最悪のことが起きたらどうなるか？」**を事前にシミュレーションし、安全なシステムを作るための強力なツールが生まれました。

noDice: 非決定性と条件付き推論を備えた離散確率プログラムへの推論

本論文は、Saarland University と University College London の研究者たちによって執筆された「noDice: Inference for Discrete Probabilistic Programs with Nondeterminism and Conditioning」に関する技術的サマリーです。

1. 問題設定 (Problem)

確率プログラミング言語（PPL）は、複雑な確率分布を直感的に表現するための強力な手段ですが、既存の推論エンジンには以下の重要な課題がありました。

非決定性（Nondeterminism）の欠如: 現代の PPL の多くは、マルコフ決定過程（MDP）に見られるような非決定的な選択（例：強化学習におけるエージェントの意思決定、未知の環境要因）をサポートしていません。
条件付き推論との組み合わせの難しさ: 非決定性と条件付き推論（観測データに基づくベイズ推論）を同時に扱うことは非常に困難です。非決定性が存在すると、プログラムは単一の確率分布ではなく、分布の集合をモデル化することになり、推論が非構成的（non-compositional）になります。つまり、部分プログラムの最大条件付き確率から全体の最大確率を導出できなくなります。
既存手法の限界: 現在、両者を組み合わせる唯一の方法は、プログラムの操作意味論を直接 MDP としてモデルチェックすることですが、これにより状態空間が爆発的に増大し、推論が非現実的になる傾向があります。

2. 手法 (Methodology)

著者らは、離散確率推論エンジン「Dice」を拡張した新しい推論フレームワーク**「noDice」**を提案しました。noDice はループのないプログラムを対象とし、非決定的選択と条件付き推論を効率的に処理するための以下の 3 段階の推論アルゴリズムを採用しています。

2.1 ブール式へのコンパイル (Boolean Compilation)

まず、Dice のコンパイルエンジンを用いて、確率プログラムをブール論理式に変換します。

プログラムの動作を反映するブール式（ $\phi$ ）と、観測（observe）の成功を反映するブール式（ $\gamma$ ）のペアを生成します。
非決定的な選択（nflip）と確率的な選択（flip）を区別するため、変数のアノテーション（確率値または非決定的フラグ）を保持した「トレース」を生成します。

2.2 決定図への構築 (Decision Diagrams)

生成されたブール式を内部表現として、**代数決定図（Algebraic Decision Diagram: ADD）**に変換します。

従来の Dice は二値決定図（BDD）を使用しますが、noDice はより一般的な出力値を持つ ADD を使用し、 $\phi$ と $\gamma$ を単一の決定図に統合します。
ADD はプログラムの構造的な冗長性（条件付き独立性など）を自動的に検出・削減し、状態空間を劇的に圧縮します。

2.3 MDP へのリフトと推論 (Lifting to MDPs)

構築された ADD を**マルコフ決定過程（MDP）**の骨格として利用します。

ADD の各ノードを MDP の状態に対応させ、ブール変数の選択（確率的または非決定的）を遷移確率または非決定的なアクションとして再導入します。
プログラムの観測がすべて成功したという条件下での出力値の最大確率は、この構築された MDP における**条件付き到達可能性（Conditional Reachability）**の問題として定式化されます。
推論には、Storm Model Checker で実装された二分探索ベースのアルゴリズム（Ceska et al. [2026]）を使用し、効率的に最大確率を計算します。

3. 主要な貢献 (Key Contributions)

noDice 言語の提案: 確率的選択、非決定的選択、第一級観測（first-class observations）を備えた、非再帰的な関数型言語の定義。
理論的基盤の確立: 決定図を用いてコンパクトな MDP を構築し、その MDP 上の条件付き到達可能性を通じて、noDice プログラムの出力値の最大確率を推論するアルゴリズムの理論的正当性を証明しました。
実装と評価: 原型実装を行い、ベンチマークセット（ランウェイ、クーポンコレクター、ネットワーク到達可能性、ベイズネットワークなど）を用いて既存の手法（Dice、Storm）と比較評価しました。

4. 結果 (Results)

実験結果は以下の通りです（Table 1 および Section 6.1 参照）。

状態空間の削減: noDice は、直接 MDP をエンコードした場合と比較して、構築される MDP の状態数を劇的に削減しました。特に、変数が多いベンチマーク（例：Coupon Collector, Bayesian Networks）において、ADD による構造的圧縮が有効に働きました。
推論効率:
- 多くのベンチマーク（Runway, Coupon, 3SAT, 大部分のベイズネットワーク）において、noDice は最先端のモデルチェッカー（Storm）よりも高速に推論を実行しました。
- 状態空間の次元が高い問題（多くの変数を持つ問題）において、noDice は Storm の状態列挙アプローチよりも優位性を示しました。
- 一方、状態空間が単純で変数が少ない問題（例：Network Reachability, Rabin）では、noDice のコンパイルオーバーヘッドが Storm の直接解析よりもコストがかかる場合がありました。
非決定性の影響: 非決定的な操作の割合が増加しても、ADD の構築時間はほぼ影響を受けず、モデルチェックの時間のみがわずかに増加しました。全体の実行時間はコンパイル時間が支配的であり、非決定性の量による大きな遅延は発生しませんでした。
最適化の効果: 状態圧縮（Probabilistic State Compression）は MDP のサイズをさらに削減しましたが、推論時間の大幅な短縮には直結しませんでした（コンパイル時間がボトルネックのため）。

5. 意義と結論 (Significance and Conclusion)

非決定性と条件付き推論の統合: noDice は、PPL において非決定性と条件付き推論を同時に扱い、その最大確率を効率的に推論する最初の体系的なアプローチの一つです。
スケーラビリティ: 決定図（ADD）を活用することで、状態空間の爆発を回避し、大規模な離散確率プログラムに対する推論を可能にしました。
実用性: 強化学習、ネットワーク検証、人工知能など、不確実性と非決定性が共存する分野におけるモデリングと推論の新たな基盤を提供します。

今後の課題として、無限ループのサポートや、最適なプログラム自体の合成（Program Synthesis）への拡張が挙げられています。

要約すると、noDice は「プログラム構造を決定図で圧縮し、それを MDP に変換して条件付き到達性を解く」というアプローチにより、従来のモデルチェック手法では扱えなかった大規模で複雑な確率的・非決定的プログラムの推論を可能にする画期的なツールです。