A cubical formalisation of topos causal models: intervention, sheaf gluing, and the intuitionistic do-calculus

探偵のジレンマ：なぜ因果関係には新しい地図が必要なのか

あなたは、ある謎を解こうとしている探偵だと想像してください。あなたの手元には、「雨が降った」「芝生が濡れている」「スプリンクラーが作動していた」という手がかりのリストがあります。かつて、科学者たちはこれらの手がかりを単なる事実のリストとして扱っていました。もし芝生が濡れていれば、彼らは雨が降ったのだと推測したかもしれません。しかし、現実の世界はもっと複雑です。もしあなたがスプリンクラーを回すことで、自ら芝生を濡らしたとしたらどうでしょう？ それによって「雨が降った」という事実は変わってしまうのでしょうか？ これこそが**因果推論（causal inference）**の核心です。単に何が一緒に起きているかだけでなく、私たちが介入し、ルールの書き換えを行ったときに、何が何を「引き起こす」のかを解き明かすことなのです。

何十年もの間、専門家たちは図や数学を用いて、これらの因果関係の連鎖を追跡してきました。しかし最近、新しいアイデアが登場しました。それは、因果関係の世界全体を、静止した絵としてではなく、どこを見ているかによって変化する「移り変わる風景」として捉えるという考え方です。これは、形や構造がいかに組み合わさっているかを研究する数学の一分野である**トポス理論（Topos Theory）**の領域です。これは、情報の断片を「接着」するための普遍的な言語だと考えてください。もし、手の中では完璧にフィットするパズルのピースが、テーブルの上に並べようとすると完全な絵にならないとしたら、それは問題です。この新しい数学が解決しようとしているのは、まさにそのような問題です。大きな問いはこうです。「この高度な数学を用いることで、私たちが実験を通じて世界を変えているときでも、因果関係を理解するための、落ち度のないシステムを構築できるだろうか？」

論文の歩み：因果関係のレゴセットを組み立てる

この論文は、コンピュータによって検証された大規模な建設プロジェクトです。カレン・サルガシアン（Karen Sargsyan）率いる著者たちは、「トポス因果モデル（Topos Causal Models）」という大胆な新理論を取り上げ、Cubical Agdaというコンピュータプログラムの中でゼロから再構築しました。このプログラムを、接続が数学的に完璧でない限り、二つのブロックを結合することを拒む、非常に厳格なレゴマスターだと考えてください。目標は、マハデバン（Mahadevan）という研究者が提案した理論、すなわち「トポス（数学的な宇宙）」の規則を用いて、因果関係の全宇宙を記述できるという理論を検証することでした。

著者たちは単に理論をコピーしたわけではありません。彼らはそれをテストし、修正し、元の著者が気づかなかった点を見つけ出しました。ここでは、彼らのデジタル建設現場という視点を通して、その発見を説明します。

1. 「Doボタン」と真理のフィルター

元の理論では、介入（例えば、変数 $X$ を特定の値 $x$ に強制すること、記法では $do(X = x)$ と書く）は、特別な「特性写像（characteristic map）」として記述されます。街の巨大な地図を想像してください。もし特定の通りを封鎖したい場合、単に通りを消去するのではなく、地図の上に特別な「真理のフィルター」を描きます。このフィルターは、その通りが封鎖されている場所だけを強調し、他の場所には干渉しません。

著者たちは、このフィルターをコンピュータコードの中に構築しました。彼らは、このフィルターが約束通りに機能することを証明しました。つまり、そのフィルターは「封鎖された通り」を正確に特定し、それ以外には干渉しません。これは単なる巧妙なトリックではなく、この数学的宇宙における根本的なルールであることを彼らは示しました。もし、地図の自然な流れに合わない値を強制しようとすれば、システムはそれを拒絶します。これにより、「Doボタン」がこの新しい枠組みにおいて、堅実で信頼できるツールであることが確認されました。

2. 時として失敗する「接着剤」

元の理論の最もエキサイティングな約束の一つは、**層の接着（Sheaf Gluing）**でした。想像してみてください。三人の探偵が、それぞれ異なる角度から犯罪現場を見ているとします。もし探偵Aが探偵Bと同意し、探偵Bが探偵Cと同意するなら、彼ら全員が全体像について同意していると仮定してもよいでしょう。この数学において「接着」とは、これらの局所的な視点を、一つの巨大なグローバルな真実へと繋ぎ合わせることを意味します。

著者たちは、二人の探偵であれば、これが常に機能することを証明しました。彼らの視点が重なり合い、一致する場合、それらは完璧に接着できます。しかし、三人以上の探偵が関わる場合に**不具合（グリッチ）**があることを見つけました。彼らは、すべてのペアにおいては完璧に一致するものの、三人をすべて組み合わせようとすると絵が崩れてしまうシナリオ（「スペッカーの三角形」）を構築しました。そこには、すべての局所的な手がかりに適合する単一のグローバルな物語が存在しないのです。これは「文脈依存性の障害（contextuality obstruction）」です。それは、二つずつのペアでは合うけれど、いざテーブルの上にすべて並べてみると、真ん中に穴が開いてしまうパズルピースのようなものです。著者たちは、これがコードのバグではなく、数学の「実在する特徴」であることを証明しました。つまり、複雑な因果システムにおいては、局所的な部分が一致しているからといって、必ずしもグローバルな解が存在するとは限らないということです。局所的なチェックだけでなく、グローバルなチェックが必要なのです。

3. 「魔法のモダリティ」の修正

この理論は、異なる状況下でどの因果的事実が「安定」しているか、あるいは「真」であるかを決定するために、ローヴェア・ティニー・トポロジー（Lawvere-Tierney topology）（ここでは「魔法のモダリティ」と呼びます）と呼ばれる特別なツールを使用しています。元の論文では、この魔法のツールに対して三つのルールが挙げられていました。著者たちが計算を実行したところ、問題が見つかりました。その三つのルールでは不十分だったのです。彼らは、そのツールが三つのルールに従っているにもかかわらず、論理が破綻してしまう（「増幅的（inflationary）」ではない、つまり常に物事を維持したり大きくしたりできない）という、奇妙な三段階の梯子を発見しました。

彼らは、第四のルールを追加することで、これを修正しました。この新しいルールによって、魔法のツールは正しく機能するようになりました。そして、このツールが「Do-calculus（因果計算の規則）」をいかに安定させるかを示しました。世界をどのように切り取ろうと、あるいは視点を変えようと、因果関係の核となるルールは揺るぎません。彼らはさらに、この「魔法」の具体的な動作例として、「二重否定（double-negation）」トポロジーを示しました。これは、曖昧で不確かな真実を、明確な古典的事実へと変換するフィルターとして機能します。

4. 世界間での真理の輸送

最後に、著者たちは**輸送可能性（Transportability）**に取り組みました。ある世界（例えば東京の病院）で学んだルールを、別の世界（ニューヨークのクリニック）でも信頼できるでしょうか？ 彼らの枠組みでは、ある因果的事実をある場所から別の場所へ移動させることは、それが「魔法のモダリティ」の下で「安定」しているかどうかを確認することと同じです。もし事実が安定していれば、それは安全に移動できます。もし安定していなければ、移動した際に壊れてしまう可能性があります。彼らは、特定のタイプ（介入を含むもの）の事実については、この安定性が保証されることを証明しました。しかし、事実の値が世界間で変化する可能性がある、より複雑で現実世界のシナリオにおいては、数学的な処理がより難しくなり、完全に解決するにはさらなる作業が必要であることも指摘しています。

結論

この論文は、**検証（verification）**の勝利です。著者たちは単に「この理論は面白そうだ」と言ったのではありません。理論をコンピュータの中に構築し、厳格な論理規則に従わせ、以下のことを明らかにしました。

1. 「Doボタン」は、真理のフィルターとして完璧に機能する。
2. 局所的な合意は、時としてグローバルな真実を作ることに失敗する（「三人の探偵」の問題）。
3. 「魔法のモダリティ」のための元のルールは不完全であり、機能させるためには第四のルールが必要であった。
4. 一度修正されれば、このシステムは因果ルールが安定しており、異なる環境間でも輸送可能であることを証明する。

著者たちは、これらの結果が**マシン・チェック（機械検証）**されたものであるため、非常に自信を持っています。あらゆるステップがコンピュータによって検証されており、「おそらく」や「たぶん」といった曖昧な瞬間はありません。彼らは単にシミュレーションを行ったのではなく、数学的に証明したのです。ただし、これはあくまで「1-topos（特定の、より単純な種類の数学的宇宙）」に関するものであるという点には注意が必要です。彼らは、向きを持つ矢印（AがBを引き起こすが、BはAを引き起こさないという非対称性）を含む、因果関係の全容を完全に解決したわけではありません。しかし、今回取り組んだ範囲においては、彼らは岩のように堅固な基礎を築き、因果モデルの背後にある数学が、単なる美しいアイデアではなく、検証された、実際に機能する現実であることを証明したのです。