「順序」が消える瞬間——AIガバナンスを責任工学で検査する

AIガバナンス担当者なら見覚えのある光景

あるAIを使った業務フローを2つ想像してみてください。

1つ目では、AIがある取引を「不審」としてフラグを立て、その後で人間の担当者がその取引を承認します。

2つ目では、人間の担当者が先に取引を承認し、その後でAIが「不審」というフラグを立てます——もう取引は実行済みで、フラグは手遅れです。

ところが、この2つのフローの最終結果は同じだったとします。取引のステータスは「承認済み」、リスクスコアは「3」と記録され、監査ダッシュボードに表示されるサマリー行はどちらも全く同じものになります。

ダッシュボードから見れば、この2つの履歴は区別できません。しかし「説明責任」の観点からは、これは全く異なる2つの物語です。一方は「システムは設計通りに機能した」、もう一方は「安全装置はすり抜けられた」。インシデント調査がサマリーにしかアクセスできないなら、どちらが真実かを判定する手段がありません。

これは特殊なエッジケースではありません。実は、結果・スコア・ラベルだけを記録し、そこに至る履歴を捨てるシステムでは、これは構造的に起こり得る問題です。しかもそれは比喩ではなく、数学的に正確に証明できる事実です。

▼責任OSの情報学への接続（Lean4リポジトリ） responsibility-info-kernel ※この責任工学を実装・形式化する中核概念が、責任os(Responsibility OS)です。

すでにある語彙——そして、その限界

情報学にはこの問題を語るための語彙が既に存在します。プロベナンス(provenance)、監査証跡(audit trail)、トレーサビリティ(traceability)、メタデータ、監査可能性、検証可能性。W3C PROVのような標準も、データや意思決定がどのように生まれたかを記述するために存在しています。

しかし、この語彙が説明していないことがあります。なぜ、ある種の情報を保持しておかなければ、後から「説明責任を果たす」ことが構造的に不可能になるのか。そして、なぜ「スコア」「合否ラベル」「操作回数の集計」といった、極めて自然な要約の取り方が、調査の際にまさに必要となる情報を静かに消し去ってしまうのか。

この隙間を埋めようとしているのが、**「Responsibility OS」**という枠組みです。既存の語彙を置き換えるのではなく、その下に数理的な基盤を与えようとしています。

「順序が効く」を表す2つの言葉:非可換性とcommutativization

Responsibility OSは、数学から2つの概念を持ち込みます。これが驚くほど効きます。

**非可換性(noncommutativity)**とは、単純に言えば「順序が結果を変える」ということの形式的な言い方です。「Aの後にB」と「Bの後にA」が異なる結果に至るなら、そのプロセスは非可換です。承認、編集、モデルの更新、権限変更——現実の多くのプロセスはこちらです。

commutativization(可換化)とは、システムが順序を忘れる要約だけを記録するときに起きることです。合計件数、最終スコア、合否ラベル。本当は異なっていた2つの履歴(「Aの後にB」と「Bの後にA」)が、同じ要約値になり得ます。要約が履歴を「可換化」した瞬間、元の順序は失われます。その要約だけをどれだけ巧妙に分析しても、元の順序を復元することはできません。

これらを合わせると、説明責任の核心的な問題が一文で言えます。

数式なしで結論だけ

ある最近のプロジェクトは、この主張をLean 4という証明支援システム上で形式化しました。Leanは数学的な議論を1行ずつ、抜け漏れなく、「信じてください」抜きで検証するツールです。注目すべき結果は2つあります。

1. 履歴を記録し始めた瞬間、順序そのものが情報になる。 区別可能な行動が2つ以上あるどんなプロセスでも、行動の時系列をシステムの状態と一緒に記録すれば、異なる順序で実行した場合、最終的な状態・出力・スコアが同じに見えても、記録としては必ず異なるものになることが証明されています。これは「サマリーが忘れることを、トレースは覚えている」を形式化したものです。

2. ある要約が2つの異なる順序を1つに潰してしまったら、その要約からは絶対に元に戻せない。 これは単なる観察ではなく、「不可能性」の証明です。あるスコア・ラベル・ダッシュボードの数値が、2つの異なる履歴を同じ値に写してしまった瞬間、その値だけから「どちらの履歴だったか」を再構成する方法は、アルゴリズム的にも、監査手続き的にも、どんな工夫をしても存在しません。情報は「見つけにくい」のではなく、「もう無い」のです。

このような潰れに耐え、後から検査可能な状態を保つ情報を、このプロジェクトは**「責任情報(responsibility information)」**と呼んでいます。形式化された主張を平易に言うと、こうなります。

これは例外ではなく、デフォルトである

ここからが、ガバナンス担当者の「稀な失敗モード」という考え方を変えるかもしれない部分です。

別の結果は、こう問いかけます。2つの操作を、n個の状態を持つシステム上の任意の関数としてモデル化したとき、それらが「可換」になる(つまり順序が結果に影響しない)のはどれくらいの頻度か。形式的に証明された答えはこうです:状態数が101以上のシステムでは、操作のペアの少なくとも99%が非可換であり、状態数が増えるほど、この割合は100%に近づくことが証明されています。

つまり、ある程度複雑なシステムにおいて「順序はあまり関係ないだろう」という前提は、安全な既定値ではありません。数学的には、それは例外の方なのです。

なぜ「形式検証済み」が単なる飾り言葉ではないのか

ここまでの内容は、説得力のある読み物として書くだけでも成立します。しかし、それをCIが通っているLean 4の開発として示すことには意味があります。理由は、ここで述べた主張は「直感的にはありそうだが、過大に言い過ぎるか、微妙に間違えるのが簡単な」種類のものだからです。「要約は常に情報を失う」「ログは多ければ多いほど良い」「非可換性は稀である」——どれも、もう少し掘ると怪しくなる言い方です。

形式検証は精密さを強制します。このプロジェクトのドキュメント自身が、主張していないことを明示しています。すべての実世界システムが非可換だとは主張していない。完全なトレース保存が常に必須だとも主張していない。法的・制度的な責任理論を形式化したとも主張していない。証明されているのは、より大きな説明責任の議論を支える、狭いが土台となる数理的な核です。ガバナンス担当者にとって、その核こそが「確実であってほしい」部分です。

用語の対応表

情報学の用語 Responsibility OSの用語 ここでの意味 監査証跡・プロベナンス 責任情報 後から検査するために必要な区別を保存している情報 集計・スコアリング・ラベリング commutativization(可換化) 順序を消してしまう要約への圧縮 状態遷移の履歴 トレース・時系列履歴 「何が、どの順序で起きたか」の完全な記録 トレーサビリティの欠如 情報損失(責任の意味での) 「データ量が減る」だけでなく「検査可能な区別」が失われること 「XはYより先に行われたか」(監査上の問い) 順序に依存した検査可能な区別 履歴からしか答えられず、潰された要約からは絶対に答えられない問い

実務への落とし込み

AIガバナンスの実務における結論は、「とにかく全部ログを取れ」ではありません。もっと具体的です。

あるスコア・ラベル・指標を監査やインシデント調査の証拠として使う前に、「意味的に異なる複数の出来事の系列が、同じこの値を生み得るか」を問うべきです。もし答えが「はい」なら、その値は順序についての証拠には使えません。順序を保存した記録だけがその役割を果たせます。

特に複数ステップ・エージェント型のAIシステム——同じ最終アクション(例:「取引承認」)が、モデル呼び出し・ツール利用・人間の介入の、全く異なる系列を経て到達し得るシステム——では、順序を保存した記録は、そうした説明責任上の問いに答えるための原理的な前提になります。

「監査ログがある」ことと、「誰が何をどの順序で行ったかに答えられる」ことは、別の主張です。前者は後者を含意しません。そして今では、自分たちが持っているのがどちらなのかを、正確に確認する方法があります。

さらに詳しく

形式的な定義、不可能性定理、有限状態系に関する一般性の証明、そしてそれらをポリシー保存の枠組みに接続する圏論的な橋渡しまでを含む、Lean 4による開発全体は、responsibility-info-kernelリポジトリで公開されており、すべての証明にギャップがないことはCIによって継続的に検証されています。