責任情報はなぜ重いのか——AI監査ログが失う区別をLeanで証明した

1. はじめに：情報には「重さ」がある

「宇宙人がいた」という情報と、「本があった」という情報は、同じ一文でも重さが違うように感じられる。

ただし、ここで扱う「責任情報の重さ」は、驚きや珍しさの話ではない。

責任情報が重いとは、後から責任状態を監査・検査・検証するために、消してはいけない区別を多く背負っている、という意味である。

AIが「承認」と出力した。ログにも「承認」と残っている。しかし、その判断がどの証拠に基づき、どの条件が確認済みで、どの条件が未確認で、どの来歴と証明書に支えられていたかが消えていれば、後から責任状態を検証することはできない。

この差を、今回公開した Lean リポジトリ responsibility-info-capacity では、有限容量として形式化した。 ▼責任情報容量　リポジトリ https://github.com/GhostDriftTheory/responsibility-info-capacity

2. 普通のログは「何が起きたか」を残す

多くの監査ログは、誰が、いつ、何をしたかを残す。

これは重要である。監査証跡、来歴、追跡可能性は、AIシステムの検査に欠かせない。

しかし、それだけでは足りない場合がある。

たとえば、同じ「AIが承認した」という履歴でも、次の二つは責任状態が違う。

• 必要な条件を確認したうえで承認した

• 必要な条件が未確認のまま承認した

history-only log が両方を同じ履歴として扱うなら、そのログは責任情報を失っている。

3. 責任情報は「履歴」ではなく「履歴の上に乗る情報」である

責任情報は、単なる履歴ではない。

責任情報は、ある履歴に対して、その履歴を後から検査するために必要な情報が結びついたものである。

ここには、来歴、監査証跡、追跡可能性、メタデータ、未確認条件、証拠、制約、証明書、検証状態が含まれる。

数学的には、履歴だけを見るのではなく、履歴ごとに責任関連の fiber が乗っていると見る。

同じ履歴に見えても、その上に乗っている fiber が違えば、責任情報としては別の状態である。

4. 「履歴に戻す」ことはできても、「責任情報を復元する」ことはできない

責任情報から履歴を見ることはできる。

しかし、履歴から元の責任情報を一意に復元できるとは限らない。

これは重要である。

一度、責任情報を history-only log に落としてしまうと、後から「本当はどの証拠が確認済みだったのか」「どの条件が未確認だったのか」「どの証明書が存在したのか」を復元できない場合がある。

つまり、問題は説明不足ではない。

構造的に、消えた区別は戻せない。

5. だから責任情報は重い

責任情報が重いとは、倫理的に重い、気分として重い、という意味ではない。

責任情報は、後から責任状態を検査するために保存しなければならない区別を含む。

普通のログなら一つに潰してよい情報でも、責任の観点では潰してはいけない場合がある。

この「潰してはいけない区別」の数が増えるほど、責任情報の容量は増える。

これが、責任情報が重いという意味である。

6. 責任が重いほど、保存すべき区別も増える

責任が軽い場面では、最低限の記録で足りることがある。

しかし、人命、安全、金融、物流、医療、インフラ、自治体判断のように、判断の責任が重くなるほど、後から区別しなければならない状態は増える。

たとえば、単に「配送を許可した」だけでは足りない。

どの制約を確認したのか。誰が承認したのか。どのデータ時点に基づいたのか。未確認条件は何だったのか。停止すべき境界を越えていなかったのか。検証可能な証明書は存在したのか。

責任が重い判断ほど、保存すべき責任情報容量が増える。

7. PROVは「誰が・何を通じて」を支えるが、それだけでは終わらない

来歴、すなわち provenance は、情報がどこから来て、どの活動や関与者を通じて生成・変換されたかを記述する。

これは責任情報の重要な部分である。

しかし、責任OSが問題にするのは、来歴があるかどうかだけではない。

その来歴が、証拠、制約、確認状態、証明書、未確認条件と接続されているかである。

今回の Lean 形式化では、PROV-style qualified provenance を、履歴の上に乗る qualified fiber として扱う。

つまり、単なる履歴ではなく、責任状態を検査するための qualified な情報として数える。

8. ADICはラベルではなく証明書fiberである

ADICは、ログに「OK」や「NG」のラベルを貼る仕組みではない。

ADICが必要になるのは、ある責任記録が、定められた境界、証拠、制約、検証条件を満たしていることを、後から確かめられる形で残す必要があるからである。

その意味で、ADICは責任記録の上に乗る certificate fiber である。

証明書がなければ、その責任記録はADIC的には検証不能である。証明書があれば、その証明書自体が責任情報の一部になる。

だからADICは、普通のログや閾値判定の代替ではない。

責任情報を後から検証可能にするための層である。

9. 責任OSが必要になる理由

AIに倫理を期待するから責任OSが必要なのではない。

普通のログが、後から責任を検査するために必要な区別を落としてしまうから、責任OSが必要になる。

責任OSは、AI判断の結果だけを見るのではなく、その判断がどの責任情報を伴っていたかを保存・接続・検証するための情報基盤である。

履歴だけでは足りない。スコアだけでは足りない。ラベルだけでは足りない。

責任が重い判断では、責任情報も重くなる。

その重さを扱うために、Responsibility OS と ADIC が必要になる。

10. おわりに：これは責任の精神論ではなく、情報の容量の話である

責任情報は、気分として重い情報ではない。

後から責任状態を監査・検査・検証するために、保存しなければならない区別を背負っている情報である。

今回公開した responsibility-info-capacity は、その重さを Lean で形式化した。

これは、責任OSの実装そのものではない。しかし、責任OSがなぜ必要になるのかを支える、情報学的な土台である。

責任情報は、履歴より重い。そして責任が重いほど、保存すべき責任情報も重くなる。