責任OSの基礎理論群を Lean 4 で形式化し、関連する6つのリポジトリを公開しました。
本記事では、AIシステムにおいて「監査ログを残す」だけではなぜ足りないのか、また責任を後から検証可能にするには何を記録すべきかを、情報学の概念とLean形式化の構造から整理します。
▼プレスリリース
https://prtimes.jp/main/html/rd/p/000000004.000182721.html
問題の整理：監査ログが「ある」ことと「検証できる」ことは別
AIシステムを本番運用していると、こういう設計判断をしていると思います。
- 推論のinput/outputをDBに保存する
- 判断の結果にタイムスタンプと担当者IDを付ける
- 異常検知のアラートをログに流す
これは正しいプラクティスです。でも、いざ問題が起きたとき「なぜその判断だったか」を後から説明しようとすると、こういう壁にぶつかることがあります。
ログ: {timestamp: "2026-06-01T09:23:11", action: "approved", operator: "user_42", result: "route_C"}
route_Cが選ばれたことは分かる。でも——
- どのfeatureが支配的だったか
- その時点でどの制約が有効だったか
- operatorはどこまで確認したのか
- なぜ
route_Bではなかったのか
——これらは残っていない。
これが、私たちが「監査ログは責任情報の部分集合に過ぎない」と言う理由です。
情報学の語彙で整理する
この問題を情報学の標準概念で整理すると、以下の3つが関係します。
来歴（Provenance）
W3C PROVの定義では、来歴はentity・activity・agentの関係として記述されます。agentはactivityやentityに対して責任（responsibility）を負う存在として位置づけられています。通常のログはactivityの記録はありますが、agentとentityの関係が切れていることが多い。
追跡可能性（Traceability）
ある結果から、それを生み出した行為主体や条件に遡れる性質です。ログが「何が起きたか」を記録するのに対し、追跡可能性は「その経路を実際に遡れること」を保証します。
監査証跡（Audit Trail）
誰が・いつ・何をしたかの時系列記録です。責任OSが問題にするのは、この記録が判断の根拠や確認状態と接続されているかどうかです。記録があっても孤立していれば、責任情報としては不十分です。
責任情報とは、これら3つが「責任状態を後から検査できるか」という一点でつながっている状態を指します。
非可換性：順序が消えると何が失われるか
今回の形式化で中心的な主張の一つが、責任情報は非可換であるというものです。
具体的にはこういうことです。
シナリオA: AIが判断 → 人間が事後確認 → 承認
シナリオB: 人間が条件確認 → AIが判断 → 承認
outputは同じ「承認」でも、責任状態は異なります。シナリオAでは人間の確認がAIの判断根拠を見ていない可能性がある。シナリオBでは人間の確認がAIの入力条件に影響している。
通常のログはこの順序の違いを保存しないことがあります。タイムスタンプはあっても、「どちらの判断が先の確認に基づいていたか」という因果の向きが失われる。
Lean形式化ではResponsibilityOS.standard_trace_is_faithfulとして、この「操作上は異なる遷移が、責任情報を伴って記録したときにも区別され続けること」を検証しています。
可換化の問題：スコアに落とすと何が消えるか
もう一つの中心的な問題が**可換化（commutativization）**です。
MLシステムでよくある設計として、複雑な判断プロセスを最終的にスコアや分類ラベルに集約することがあります。これは計算上必要なプロセスで、それ自体は問題ではありません。
問題は、このフラット化によって責任を検査するために必要な情報まで落ちてしまうことです。
# よくある設計
result = model.predict(features) # → 0.87
decision = "approved" if result > 0.8 else "rejected"
log(decision) # 残るのはdecisionだけ
この設計では、0.87という数値がどのfeatureの組み合わせから来たか、どの制約が有効だったか、0.8というthresholdが誰によってどの根拠で設定されたかが消えます。
Lean形式化ではResponsibilityOS.forgetting_responsibility_layer_can_collapse_distinctionsとして、責任レイヤーを忘却する操作的視点が、異なる責任トレースを同一視してしまうことを示しています。
ALSが示すこと：人間確認の構造的限界
ALS（Algorithmic Legitimacy Shift）は、「人間が全部確認する」設計の限界を有限モデルで形式化したものです。
確認すべき項目数をN、人間の確認予算をBとしたとき、B < Nの条件では、人間レビューには構造的なリスク床が生じます。一方、一定の条件を満たすアルゴリズム検証はそのリスクを下回れる場合があります。
これは「AIが人間より優れている」という主張ではありません。「全件人間確認」を前提にしたガバナンス設計が、スケールすると責任の穴を生む構造になり得ることを、検査可能な形で示すものです。
高頻度・大量判断を行うAIシステムの設計において、「どの判断を人間が確認し、どの判断をアルゴリズム検証に委ね、どの条件で止めるか」を明示的に設計する必要があります。
実装上の含意：何を残すべきか
今回の形式化から実装上の示唆を引き出すとすると、こうなります。
最低限残すべき情報
- 判断に使ったfeatureとその値（inputの記録だけでなく、どのfeatureが有効だったか）
- 判断時に有効だった制約・閾値とその出所
- 人間確認のスコープ（何を確認し、何を確認していないか）
- 判断の順序（何が先で何が後か、因果の向き）
設計上の問いとして持つべきこと
- このログから、6ヶ月後に第三者が「なぜこの判断だったか」を再構成できるか
- 人間確認のUIは、確認できなかった項目を明示しているか
- スコアへの集約過程で、責任検査に必要な情報が消えていないか
公開したリポジトリ
今回公開した6つのリポジトリは、上記の主張を機械検証可能な形で固定したものです。
ALS Finite Experiment Kernel
人間レビューの構造的限界を有限モデルで形式化。
https://github.com/GhostDriftTheory/als-finite-experiment-kernel
Responsibility Information Kernel
判断の順序・履歴の違いが責任上の区別として残らなければならないことを形式化。
https://github.com/GhostDriftTheory/responsibility-info-kernel
Responsibility Information Capacity
通常のログでは復元できない責任情報の構造を、来歴・監査証跡・追跡可能性に接続して形式化。
https://github.com/GhostDriftTheory/responsibility-info-capacity
Responsibility OS Kernel
AI判断の根拠・証拠・責任記録が処理の合成後も保持される構造を形式化。
https://github.com/GhostDriftTheory/responsibility-os-kernel
ADIC AI Assurance Lean
AI判断過程を第三者があとから再実行・検証できる証拠として残す技術基盤の形式化。
https://github.com/GhostDriftTheory/adic-ai-assurance-lean
Hiroshima Responsibility Functor
通常の企業判断を、確認と検証を通る責任ある構造へ変換するモデルの形式化。
https://github.com/GhostDriftTheory/hiroshima-responsibility-functor
まとめ
- 監査ログは「何が起きたか」を記録するが、「なぜその判断だったか」を検証するには不十分
- 責任情報は来歴・追跡可能性・監査証跡が判断の責任状態と接続されている状態を指す
- 判断の順序（非可換性）とスコアへの集約（可換化）は、責任情報の損失リスクが高い設計ポイント
- ALSは「全件人間確認」設計がスケールすると構造的な限界を生むことを示す
- 今回のLean形式化は、これらの主張を機械検証可能な形で固定したもの
技術デモなどのお問い合わせは下記フォームからどうぞ。
https://www.ghostdriftresearch.com/contact