責任情報はなぜ重いのか：AI監査ログが失う区別をLeanで形式化した

Posted at 2026-06-15

はじめに

AIシステムの監査ログは、たいてい「何が起きたか」を記録します。

たとえば、

2026-06-15 10:00
AI system approved request X
score = 0.87
label = approved

のようなログです。

これは重要です。
しかし、責任を後から検査するには、これだけでは足りない場合があります。

同じ approved でも、

必要条件をすべて確認して承認した

のか、

一部の条件が未確認のまま承認した

のかでは、責任状態が違います。

この記事では、今回公開した Lean リポジトリ

https://github.com/GhostDriftTheory/responsibility-info-capacity

をもとに、次の主張を説明します。

責任情報は、単なる履歴ではない。
後から責任状態を監査・検査・検証するために、消してはいけない区別を背負っている。
その意味で、責任情報は「重い情報」である。

ここでいう「重い」は、感情的・倫理的な意味ではありません。
区別可能な有限状態数、つまり finite capacity の意味です。

これは Shannon 情報量の話ではありません。
Fintype.card で数えられる、区別可能な責任情報状態の数の話です。

▼責任情報容量　リポジトリ
https://github.com/GhostDriftTheory/responsibility-info-capacity

普通のログは何を落とすのか

たとえば、次の2つのケースを考えます。

ケースA：十分に確認して承認した

Human -> AI -> Approve

Condition A: verified
Condition B: verified
Condition C: verified
Unverified conditions: none

ケースB：未確認条件があるまま承認した

Human -> AI -> Approve

Condition A: verified
Condition B: unverified
Condition C: unverified
Unverified conditions: exist

操作ログだけを見ると、どちらも

AI approved

に見えるかもしれません。

しかし責任状態としては別です。

後から必要になる問いは、単に「承認されたか」ではありません。

どの証拠を使ったのか
どの条件を確認したのか
何が未確認だったのか
どの時点のデータに基づいたのか
誰がどの段階で関与したのか
検証可能な証明書はあったのか

です。

この区別がログから落ちると、後から責任状態を検査できません。

責任情報は「履歴 + fiber」として見る

Lean 側では、責任情報を次のような形でモデル化しています。

abbrev ResponsibilityInfo
    (History : Type u)
    (EvidenceFor : History -> Type v) : Type (max u v) :=
  Sigma EvidenceFor

これは、責任情報を

履歴 h
+
その履歴 h にぶら下がる責任関連情報 EvidenceFor h

として見る、ということです。

EvidenceFor h には、たとえば次のような情報が入ります。

証拠
来歴 / Provenance
確認状態
未確認条件
制約
境界条件
監査用メタデータ
ADIC証明書

重要なのは、EvidenceFor が History -> Type になっていることです。

つまり、責任情報は単なる直積ではありません。

History × Evidence

ではなく、

Sigma EvidenceFor

です。

履歴ごとに、意味のある証拠・来歴・制約・証明書の空間が違ってよい、という形です。

履歴への射影はあるが、逆向きには戻れない

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

def historyProjection
    {History : Type u}
    {EvidenceFor : History -> Type v} :
    ResponsibilityInfo History EvidenceFor -> History :=
  Sigma.fst

つまり、

責任情報 -> 履歴

という射影はあります。

しかし、その逆は一般には存在しません。

同じ履歴の上に、複数の責任関連fiberがあり得るからです。

Leanでは、次のような定理として表現しています。

theorem history_projection_not_injective
    (History : Type u)
    (EvidenceFor : History -> Type v)
    (h_two :
      ∃ h, ∃ e1 e2 : EvidenceFor h, e1 ≠ e2) :
    ¬ Function.Injective
        (historyProjection :
          ResponsibilityInfo History EvidenceFor -> History)

意味はこうです。

ある履歴 h の上に異なる証拠状態 e1 と e2 があるなら、
責任情報から履歴への射影は単射ではない。
つまり、履歴だけでは元の責任情報を一意に復元できない。

これは、ログ設計上かなり重要です。

一度、責任情報を履歴だけに潰してしまうと、後から元の責任状態を復元できません。

history-only log は責任fiberを失う

多くのログは、実質的には次のような観測です。

ResponsibilityInfo -> History -> Log

つまり、責任情報全体を見るのではなく、いったん履歴に落としてからログ化しています。

この形のログは、同じ履歴の上にある責任fiberの違いを区別できません。

Leanでは、この性質を次の方向で形式化しています。

def FiberInjective
    {History : Type u}
    {Q : History -> Type v}
    {Log : Type w}
    (obs : Sigma Q -> Log) : Prop :=
  forall {h : History} {q1 q2 : Q h},
    obs ⟨h, q1⟩ = obs ⟨h, q2⟩ ->
    q1 = q2

fiber-injective であるとは、

同じ履歴の上にある責任状態を、ログが区別できる

という意味です。

逆に、history-only log はこれを満たしません。

theorem history_factored_log_not_fiber_injective
    {History : Type u}
    {Q : History -> Type v}
    {Log : Type w}
    (alpha : History -> Log)
    (h_two : exists h : History, exists q1 q2 : Q h, q1 ≠ q2) :
    Not (FiberInjective (fun r : Sigma Q => alpha r.1))

これは、かなり直接的に次を言っています。

履歴だけを見て作られるログは、非自明な責任fiberを区別できない。

責任情報は履歴より容量が大きい

有限型として見ると、責任情報の容量は次のように数えられます。

theorem responsibility_info_card
    (History : Type u)
    (EvidenceFor : History -> Type v)
    [Fintype History]
    [∀ h, Fintype (EvidenceFor h)] :
    Fintype.card (ResponsibilityInfo History EvidenceFor)
      =
    ∑ h : History, Fintype.card (EvidenceFor h)

つまり、

責任情報の容量
=
各履歴の上にある責任fiber容量の総和

です。

さらに、各履歴に少なくとも1つの証拠状態があり、どこか1つの履歴で2つ以上の証拠状態があるなら、

theorem responsibility_info_strictly_larger_than_history

によって、

履歴の容量 < 責任情報の容量

が示されます。

これが「責任情報は重い」の最小の数学的意味です。

PROVとの関係

既存の情報学には、Provenance / 来歴という標準的な語があります。

W3C PROVでは、情報がどの entity、activity、agent を通じて生成・変換されたかを扱います。

今回の形式化では、PROV-style qualified provenance を、責任情報fiberの一部として扱っています。

直感的には、

unqualified provenance relation
= 履歴

qualified provenance node
= その履歴の上に乗る責任関連fiber

です。

たとえば、単に

wasAttributedTo(entity, agent)

と書くだけではなく、その attribution に

role
attributes
relation id
validity constraints

などが乗る。

この qualified な部分が、後から責任状態を検査するときに効いてきます。

リポジトリでは、PROV-style qualified influence families として、次のような kind を扱っています。

generation
usage
communication
start
end
invalidation
derivation
attribution
association
delegation
revision
quotation
primary source

Lean側では end は予約語衝突を避けるために qualifiedEnd としています。

注意点として、これは W3C PROV-O の完全な OWL 実装ではありません。
あくまで、PROV-style qualified structure を有限容量として数えるためのモデルです。

ADICはラベルではなく certificate fiber

ADICは、ログに OK / NG のラベルを貼る仕組みではありません。

責任情報の観点では、ADICは certificate fiber です。

つまり、ある責任recordに対して、

この記録は境界条件を満たしているか
証拠は検証されたか
制約は満たされたか
検証結果は後から確認可能か

を示す証明書の層です。

証明書がないなら、その責任recordはADIC的には検証不能です。

証明書があるなら、その証明書自体が責任情報になります。

この意味で、ADICは普通の監査ログや閾値判定の代替ではありません。

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

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

責任情報が重い、というだけではまだ半分です。

重要なのは、

責任が重い判断ほど、保存すべき区別が増える

という点です。

Lean側では、責任weightごとに必要な区別容量を与える形で、これを表現しています。

abbrev RequiredResponsibilityInfo
    (History : Type u)
    (requiredCapacity : Weight -> History -> Nat)
    (weight : Weight) : Type u :=
  Sigma fun h : History => Fin (requiredCapacity weight h)

ある responsibility weight において、履歴 h に必要な証拠区別数を

requiredCapacity weight h

として与えます。

すると、required responsibility information の容量は、

theorem required_responsibility_info_card

により、

Σ h, requiredCapacity weight h

になります。

さらに、weight が上がったときに各履歴で required capacity が減らないなら、必要な責任情報容量も減りません。

どこかで strictly に増えれば、全体容量も strictly に増えます。

つまり、形式的には次のことが言えます。

責任weightが、保存すべき区別容量を増やす設計では、責任が重いほど必要な責任情報容量も増える。

これは、責任OSの中心的な考え方です。

人命、安全、金融、医療、物流、インフラ、自治体判断のように、判断の責任が重い領域では、単なる approved や score = 0.87 では足りません。

どの証拠を使ったのか
どの条件を確認したのか
どの条件が未確認だったのか
どの境界を越えていなかったのか
どの証明書が存在したのか
誰がどの段階で関与したのか

を保存する必要があります。

Verification Load：物理エネルギーではない

この記事で「重い」と言っているのは、物理エネルギーの話ではありません。

Lean側には VerificationEnergy という名前も出てきますが、外向きには VerificationLoad と呼ぶ方が正確です。

意味は、

監査
保存
照合
検証
再検査

にかかる操作的な負荷です。

責任情報容量が増えれば、それを保持・検証するための負荷も増える。

これは、任意の単調な load model に対して、

capacity が増えるなら verification load も増える

という形で表現できます。

用語整理

この記事の用語は、次のように対応します。

用語	この記事での位置づけ
Provenance / 来歴	誰が・何を通じて情報が生成・変換されたか
Traceability / 追跡可能性	後から遡って確認できる性質
Audit Trail / 監査証跡	誰が、いつ、何をしたかの記録
Metadata / メタデータ	責任状態の検査に必要なものだけが責任情報になる
Auditability / 監査可能性	後から確認できること
Verifiability / 検証可能性	規則・証明書に照らして正しいと示せること
State Transition / 状態遷移	AI判断を、単なる出力ではなく状態変化として見る
Accountability-Relevant Information / 責任情報	後から責任状態を検査するために失ってはいけない情報
Accountability State / 責任状態	誰が、何を根拠に、何を確認し、何を未確認のまま判断したかの状態
Information Loss / 情報欠落	本来区別すべき責任状態が同じログに潰れること

まとめ

普通のログは、何が起きたかを記録します。

しかし、責任を後から検査するには、

何が起きたか

だけではなく、

どの証拠に基づいたのか
どの制約を満たしたのか
何が未確認だったのか
どの証明書で検証できるのか
どの責任状態を区別すべきだったのか

が必要になります。

責任情報は、履歴より重い。

その重さは、雰囲気や倫理の話ではありません。

履歴の上に乗る責任関連fiberの容量であり、後から監査・検査・検証するために保存しなければならない区別の数です。

そして、責任が重いほど、保存すべき区別も増えます。

Responsibility OS と ADIC が必要になるのは、AIに倫理を期待するためではありません。

history-only log が落としてしまう責任情報の区別を、後から検証可能な形で保存する必要があるからです。

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up