AIアシュアランスに必要な「責任情報」をLean 4で形式化する——監査ログだけでは検証できないAI判断の構造
- kanna qed
- 9 時間前
- 読了時間: 8分
はじめに
AIシステムの判断を「後から検証できる」と言うとき、現場が直面するのは技術的な問いです。
監査ログは残っている。しかし、何が足りないのか
「人間が確認した」という記録は残っている。しかし、何を確認したのか
AIが「承認」と出力した。しかし、どの条件を満たしてその出力に至ったのか
この記事では、GhostDrift数理研究所が公開した責任OSのLean 4形式化を通じて、AIアシュアランスに必要な「責任情報」とは何か、そして通常の監査ログでは何が構造的に足りないのかを技術的に整理します。対象読者は、AIシステムの設計・監査・ガバナンスに関わるエンジニア、およびAIアシュアランスの技術基盤に関心のある方です。
1. 通常の監査ログでは何が足りないか
監査ログが記録できるもの
通常の監査ログは以下を記録します。
いつ（タイムスタンプ）
誰が（操作者、システムID）
何をしたか（操作内容、出力結果）
これは「何が起きたか」の記録です。
監査ログで答えられない問い
しかし、AI判断の責任を後から検証しようとすると、次の問いには答えられません。問い通常ログどの証拠に基づいて判断したか✗ 残らない判断の順序が変わっていたら、結果は変わっていたか✗ 残らないどの条件が未確認のまま判断に至ったか✗ 残らない人間の確認責任はどこから始まり、どこで終わったか✗ 残らない処理が合成・連鎖した後も根拠は追跡できるか✗ 保証されないこれらは判断過程の責任情報です。結果の記録ではなく、責任状態の記録です。
問題の構造
通常の監査ログが「結果」を記録するのに対し、AIアシュアランスが必要とするのは責任状態を後から再構成できる情報です。情報科学の用語で言えば：
来歴（Provenance）：情報がどのエンティティ・アクティビティ・エージェントを経て生成されたか（W3C PROV）
追跡可能性（Traceability）：ある結果から行為主体や条件に遡れる性質
監査証跡（Audit Trail）：時系列の行為記録
これらは既存の概念として存在します。しかし、これらがAI判断の責任状態と接続されているかどうか——これが、責任情報の有無を決めます。
2. 「責任情報」とは何か
定義
責任情報（Accountability-Relevant Information） とは、AI判断・作用・状態遷移について、後から責任状態を監査・検査・検証するために失ってはいけない情報の集合です。具体的には以下を含みます。
来歴（どの経路で判断が生成されたか）
監査証跡（いつ・誰が・何をしたか）
追跡可能性（結果から条件へ遡れるか）
判断根拠（何の証拠に基づいたか）
確認状態（何が確認済みで、何が未確認か）
未確認条件（Unverified Conditions）（判断時点で確認されていなかった前提）
判断の順序（誰が先に何を決めたか）
不可逆性・影響範囲
メタデータとの関係
責任情報はメタデータの部分集合です。すべてのメタデータが責任情報になるわけではありません。「責任状態の検査に必要か」という基準で絞られたものが責任情報です。
非可換性という性質
責任情報の重要な性質として、非可換性（Noncommutativity） があります。「AIが先に判断し人間が後から確認する」と「人間が先に条件を確認してからAIが判断する」は、同じ「承認」という出力であっても、責任状態が異なります。順序を入れ替えると意味・責任が変わる——これが非可換性です。この性質が保持されないと、後から責任の帰属を検証できません。
情報欠落の問題
責任OSが防ごうとしているのは、単なるデータ圧縮による情報量の減少ではありません。本来は区別すべき責任状態が、同じ出力・同じスコアに見えてしまうこと——これが責任OSにおける情報欠落（Information Loss）です。AIが「安全」と出力したとしても、その判断が何を根拠にしていたか、どの条件が未確認だったかが失われていれば、後から責任を検査できません。
3. Lean 4で固定した6つの構造
責任OSのLean形式化が固定するのは、責任情報に最低限必要な構造です。以下の6層で構成されています。
層1：人間レビューの構造的限界（ALS）
リポジトリ: als-finite-experiment-kernel
copy
何を固定したか： 確認すべき項目が多く人間の認知能力の限界を超える局面では、人間レビューに構造的なリスク床が生じることを、有限モデルとして形式化しています。なぜ重要か： 「最後は人間が確認する」という設計の前提を、数理的に問い直すためのモデルです。一定条件を満たすアルゴリズム検証が、そのリスクを下回れる場合があることを、機械検証可能な形で示しています。これはAIと人間のどちらが優れているかという主張ではありません。「どの判断を人間が確認し、どこをアルゴリズム検証に任せるか」を設計する必要があるという、構造的な問いの形式化です。
層2：判断の順序と履歴の不可分性
リポジトリ: responsibility-info-kernel
copy
何を固定したか： AI判断における操作の順序・履歴の違いが、責任上の区別として保持されなければならないことを形式化しています。Leanでの対応： ResponsibilityOS.standard_trace_is_faithful として形式化されています。faithful（忠実）であるとは、操作上は異なる遷移が、責任情報を伴って記録されたときにも区別され続けることを意味します。これが崩れると——すなわち非可換な責任情報が可換に扱われると——判断の来歴は検証不能になります。
層3：通常ログでは復元できない構造
リポジトリ: responsibility-info-capacity
copy
何を固定したか： 通常の監査ログでは復元できない責任情報の構造を形式化しています。来歴・監査証跡・追跡可能性を接続した形で保持するには、記録形式そのものに結果以上の情報が必要です。技術的な含意： 責任情報の保持は、既存のログ拡張では達成できない部分があります。記録の設計段階で責任情報の構造を組み込む必要があります。
層4：処理合成後も保持される責任記録（Responsibility OS Kernel）
リポジトリ: responsibility-os-kernel
copy
何を固定したか： AI判断の操作・証拠・監査証跡・責任記録・判断根拠が、処理の合成後も切り離されずに保持される構造を形式化した中核理論です。Leanでの対応：
ResponsibilityOS.PreservesPolicy：「観測すべき責任・証拠の区別」（ObservationPolicy）を可視化された操作的視点が保存しているかを定義します。
ResponsibilityOS.forgetting_responsibility_layer_can_collapse_distinctions：責任レイヤーを忘却する操作的視点が、異なる責任トレースを同一視してしまうことを示します。
CollapseCounterexample.tracePolicy：操作的に同じに見える2つのトレース（traceA・traceB）が、責任の観点では区別されるべきであることを示す具体的な反例です。
技術的な含意： 複数システムをまたぐAI判断チェーンにおいて、どこかの工程で責任情報が失われないことを保証する構造が必要です。これは実装設計の問題です。
層5：第三者が再実行・検証できる証拠（ADIC）
リポジトリ: adic-ai-assurance-lean
copy
何を固定したか： AI判断の過程を、第三者が後から再実行・検証できる証拠として残すための技術基盤（ADIC：Analytically Derived Interval Computation）を形式化しています。重要な区別： 「記録がある」ことと「再実行・検証できる」ことは別です。AIアシュアランスが必要とするのは後者です。証拠としての再現性が、検証可能性の実体です。
層6：判断を責任ある構造へ写すモデル
リポジトリ: hiroshima-responsibility-functor
copy
何を固定したか： 通常の組織的判断を、Beaconによる確認とVerificationによる検証を通る責任ある構造へ写す関手モデルを形式化しています。技術的な位置づけ： 前5層が責任情報の内部構造を固定するのに対し、この層は責任情報を持つ構造と持たない構造の間の写像を形式化します。
4. 各GitHubリポジトリの役割
リポジトリ形式化の対象主なLean定理
人間レビューの構造的限界とアルゴリズム検証の有限モデル形式化
判断の順序・履歴の責任上の区別の形式化
通常ログでは復元できない責任情報の構造
処理合成後も責任情報を保持する責任OSの中核理論
第三者が再実行・検証できる証拠としてのADIC形式化
広島発AIアシュアランスの理論的位置づけ
5. AIアシュアランス実装でなぜ不可欠か
「説明できる」と「検証できる」は別の要件
現在のAIアシュアランス実装の多くは、説明可能性（Explainability）を中心に設計されています。しかし、説明できることと検証できることは異なる要件です。
説明可能性：「なぜこの判断をしたか」を人間に伝えられる
検証可能性：「この判断が定められた条件を満たしているか」を第三者がアルゴリズム的に確かめられる
責任情報が必要なのは後者のためです。
実装で直面する3つのギャップ
ギャップ1：ログ設計の段階で責任情報が抜ける後から責任情報を追加することは、構造的に困難です。「何が起きたか」を記録するログと、「なぜその判断に至ったか・何が未確認だったか」を記録する責任情報では、設計要件が異なります。ギャップ2：処理合成で責任情報が失われるマイクロサービス・ワークフロー・マルチエージェント構成では、各コンポーネントが責任情報を保持していても、合成後の構造で失われる場合があります。responsibility-os-kernel が形式化しているのはこの問題です。ギャップ3：「人間が確認した」という記録では不十分確認のログは残っても、「何をどの範囲で確認したか」「何が未確認のままだったか」という未確認条件（Unverified Conditions）は通常残りません。監査時に問われるのはここです。
責任情報が実装されているとはどういう状態か
以下の条件を満たすとき、責任情報が実装されていると言えます。
AI判断の根拠・順序・停止条件が、処理合成後も失われずに保持されている
未確認条件が記録されており、後から検査できる
第三者がアルゴリズム的に再実行・検証できる形で証拠が残っている
判断の来歴が機械的に追跡できる
責任OSのLean形式化は、この4条件に対応する情報構造上の要件を、Lean 4上の定義・定理・反例構成として固定したものです。
まとめ
概念 | 通常ログ | 責任情報 |
何が起きたか | ✓ | ✓ |
どの根拠で判断したか | ✗ | ✓ |
判断の順序・来歴 | △ | ✓（非可換性を保持） |
未確認条件 | ✗ | ✓ |
合成後も追跡できるか | ✗ | ✓（PreservesPolicy） |
第三者が再検証できるか | ✗ | ✓（ADIC） |
AIアシュアランスが「検証可能な責任情報の産業」になるとき、それは設計段階から責任情報
コメント