Hiroshima Responsibility Functor-広島の場所性を、AIアシュアランスの責任構造として数理化する(Lean4)
- kanna qed
- 5 日前
- 読了時間: 6分
問題の核心
AIが社会に実装されるとき、問われるのは性能だけではない。その判断が、どの条件を通り、何を証跡として残し、後から誰が検証できるのか。「信じてください」ではなく「確かめられます」と言えるか。これがAIアシュアランスの本質だ。しかしもっと深い問いがある。AIは、人間を「データ・スコア・閾値・最適化対象」へと変換しうる技術だ。「便利だから使う」「精度が高いから通す」という目的関数が成立した瞬間、その外にある尊厳・例外者・説明不能な痛み・未来世代が、判断構造の外へ落ちていく。核兵器とAIは同じ技術ではない。しかし両者は同じ層にある――人類が初めて、自分の存続条件を自分の技術で壊しうると自覚した層として。強い技術が人間を目的関数の中の対象へ変換し、その外にある尊厳・例外者・未来世代を判断構造の外へ落としうる、という構造的な接続がそこにある。核は都市と人間を「威力・半径・戦略効果」へ変換した。AIが人間を計算対象へ変換するとき、同じ構造が別の文脈で現れる可能性がある。
▼リーン証明

なぜ広島なのか
ここで重要なのは、「広島は平和の象徴だから」という理由でAIアシュアランスを語るのではない、という点だ。広島は、次の三条件を高い密度で満たす、AIアシュアランスにとってきわめて強い参照点である。
第一に、責任条件を破った判断が文明規模の結果を生んだ歴史的証人であること。
核を投下した側は、自らが持っていたはずの非交渉条件――非戦闘員を戦略目的の計算に組み込まない――を目的関数の前に破った。これは特定の国民や現在の国家を非難するためではなく、当時の意思決定がどのように責任条件を破ったかを記述するためである。その結果は広島・長崎だ。そしてその被害は一方向には向かわなかった。破った側自身の道義的基盤も、回収しきれない問いとして残り続けた。世界にとっては、最も強大な行為者が自らの制約を超えられるという前例が刻まれた。責任条件を破ることの被害は三方向に及ぶ――対象・当事者・世界秩序へ。
第二に、その記憶が制度として保存されていること。
記録ではなく制度として。記憶が過去を固定するのではなく、未来への責任の根拠として機能し続けている。
第三に、既存のAIガバナンスの制度的アンカーであること。
2023年G7広島サミットを起点としたHiroshima AI Processは、生成AIの安全・信頼・責任に関する国際原則形成の場として広島を選んだ。「広島発」はすでに国際的なAIガバナンス言語に接続された制度的事実だ。
広島でAIアシュアランスを掲げる責任
広島がAIアシュアランスの拠点となるなら、広島で事業を行う企業や研究者の責任は、むしろ重くなる。広島の場所性を使うということは、単に「信頼できそうな地域ブランド」を借りることではない。AI判断が人間を計算対象へ変換し、責任条件を飛ばし、証跡も再検証可能性も残さないまま社会へ流れることを、より強く拒む立場に立つということだ。したがって、広島でAIアシュアランスを掲げる者は、自らのAI・システム・事業判断について、少なくとも次の責任を引き受ける必要がある。
判断がどの条件を通ったのかを示すこと
その判断の証跡を残すこと
第三者が後から再検証できる形にすること
目的関数の外に落ちる人間の尊厳・例外者・未来世代を、判断構造の外へ放置しないこと
広島をAIアシュアランスの拠点と呼ぶなら、広島で行われるAI事業は、通常のAI事業よりも強い説明責任を引き受けなければならない。それは制約ではなく、広島でAIアシュアランスを掲げることの正当性そのものである。
数理的な定式化
このリポジトリは、広島拠点化を圏論の言語で記述する。通常の企業判断を次の圏 CC で表す。C:D→P→OC:D→P→O(判断 →→ 利益・効率評価 →→ 実行結果)広島責任圏 RR は、これを責任経路へ写す。R:DH→PH→B→E→V→A→O′R:DH→PH→B→E→V→A→O′(広島文脈の判断 →→ Beacon審査 →→ 証跡 →→ 検証 →→ 説明責任 →→ 実行結果)この写しを、広島責任関手(Hiroshima Responsibility Functor)として定義する。FH:C→RFH:C→RBB は Beacon admissibility。判断が通ってよい条件を満たしているかの境界だ。VV は Verification。判断が後から再検証できる証跡として残っているかを示す。AdmBVAdmBV は、射が BB と VV の両方を経由することとして定義される。BeaconまたはVerificationを飛ばす経路は、AdmBVAdmBV の意味で責任ある許容射ではない。
Leanで確認していること
Lean 4ファイルでは、次の点を機械的に検証している。
関手 FHFH が恒等射と合成を保つこと
FH(q∘p)FH(q∘p) が責任合成になること
BB または VV を通らない任意の経路が AdmBVAdmBV に属さないこと(普遍的排除)
AdmBV_iff_factorizes:実装と因数分解定義の同値性が公理ではなく定理として証明されていること
GitHub Actionsで自動検証が走っており、main へのpushのたびに全定理の通過が確認される。明示しておく。歴史的事実――広島が責任条件を破った判断の文明規模の証人であること、その記憶が制度として保存されていること、Hiroshima AI Processがあること――は圏論では証明できない。これらはLeanファイルの中で外部公理として明示的に宣言されている。圏論が証明するのは責任経路の構造だ。
何を主張し、何を主張しないか
主張すること
広島の場所性は、AI判断を責任・証跡・再検証へ写す構造として記述できる。BeaconとVerificationを経由しない判断は AdmBVAdmBV の意味で許容されない。この構造を支える歴史的前提について、広島は三条件を高い密度で満たす強い参照点だ。
主張しないこと
広島に拠点を置けば企業が自動的に倫理的になる、とは言わない。圏論が歴史的事実を証明する、とは言わない。これは政治的・国家的主張ではない。
最後に
AIの判断が人間を計算対象へ変換する前に、目的関数の外に落ちるものを責任として戻せ。その判断を、後から誰でも辿れる証拠として残せ。これは単なる技術提案ではない。歴史的な重みを持った数理的提案だ。この構造をLeanと圏論で検証可能な形にしたコードおよび検証環境は、以下のリポジトリにて公開・管理されている。👉 https://github.com/GhostDriftTheory/hiroshima-responsibility-functor ## 補足
GhostDriftにおける「責任経路」とは
責任経路とは、ADIC(Advanced Data Integrity by Ledger of Computation)のうち、AI判断・審査・証跡・検証・説明主体を、後から追跡可能な形で接続するための応用層である。
ADICそのものは、責任経路に限定される技術ではない。
ADICは、入力条件、計算過程、判断根拠、証跡、再検証可能性、事後改変不能性を、計算台帳として保存するための基盤技術である。
そのため、責任経路はADICの全体ではなく、AIアシュアランス領域においてADICが実現する重要な構造の一つである。
この文脈でいう責任経路とは、AI判断について、入力条件、判断主体、事前・事後の審査、保存証跡、第三者検証、説明主体が、後から追跡可能な形で接続された経路を指す。
これは法的責任の所在を自動的に決定するものではない。
また、倫理判断や組織設計を代替するものでもない。
責任経路が担うのは、「誰が、どの条件で、何を根拠に、どこまで検証可能な形で判断したか」を失わせないことである。
※既存の「責任経路」的概念との差分
GhostDriftの責任経路は、設計の問題ではなく実装の問題として扱う。証拠がなければ物理的に経路を通過できない構造をADICが担保し、Lean 4による形式証明によって第三者が検証可能な形で確認できる。
差分の核心は「設計されているかどうか」ではなく「数理的に通らないようになっているかどうか」である。
※由来
なお、この責任経路という考え方は、ADICを「数理モデルを責任ある道具に変換する装置」として説明した初期構想に由来します。
当時の記事では、予測精度そのものではなく、入力条件、残差構造、Beacon、動かせない閾値、監査可能性を重視し、AI判断を人間が後から検証できる枠内に置くことをADICの役割として説明していました。
現在の「責任経路」は、この考え方をAIアシュアランス領域に拡張し、AI判断・審査・証跡・第三者検証・説明主体を追跡可能に接続する構造として整理したものです。
参考:AI安全性の新指標|ADICが数理モデルを「責任ある道具」に変換する理由



「責任経路」という語は、一般的な定着語というより、近年特定の文脈で使われ始めている造語的な語彙に見えます。
公式広報記事で使用される場合、読者が貴社独自の定義として受け取る可能性もあるため、意味や用法の説明を添えた方がよいと思います。