AIアシュアランス層がAIガバナンスに構造的に必要な理由を、Lean 4で機械検証した――ADICの数理骨格
- kanna qed
- 6 日前
- 読了時間: 3分
一番シンプルに言うと
冷蔵薬を運ぶAIが「この道で運べ」と決めた。でも薬がダメになった。
このとき、「温度を見て決めたのか、渋滞を見て決めたのか、誰が確認したのか」が残っていなければ、原因も責任者もわからない。
だから命や安全に関わる場所では、AIの「答え」だけでなく「理由・証拠・確認者」まで一緒に残す仕組みが必要になる。
このLeanは、その仕組みが数学的に意味のある骨格を持つことを、機械検証したものです。
何を前提にしたか
前提の大枠は一つですが、その中にいくつかの構造を置いています。
「AIの動きだけを見るのではなく、その判断理由・証拠・責任記録も一緒に追える世界を考える」
具体的には次の構造を置いています。
O：AIが実際にやる操作の世界（「この道で運べ」「この薬を優先」といった判断）
F：その操作に紐づく証跡のまとまり（温度センサーの値、血液検査の結果、確認した担当者など）
E = ∫_O F：操作と証跡を合わせた全体の世界（Grothendieck構成）
push / pull：操作が進むとき証跡も前向きに更新され（push）、監査のとき後ろ向きに追跡できる（pull）
push ⊣ pull（随伴）：前向き更新と後向き追跡が同じ構造の両側になっていること
standard section：各操作状態に「標準的な証跡」が対応していること
beck_chevalley：組織をまたいで視点を変えても、証跡の更新と監査の追跡が整合すること（この条件だけは構造的仮定として置いており、一般的な導出ではありません）
これらの前提はREADMEとLeanファイルに全て明記されており、隠れた仮定はありません。
何を証明したか
前提の上で、次の2つを機械検証しました。
1. 証跡層がある場合：操作と証拠が合成後も一緒に追える
操作Aのあとに操作Bをつないだとき、証跡も同じようにつながって追えることを証明しています（opcart_factor、cart_factor）。「判断の通り道」が合成後に壊れないことの数学的確認です。
2. 証跡層がない場合：違う理由が同じに見えてしまう
これが核心です。
具体的な小さな例を構成して、次のことを機械検証しました。
traceA ≠ traceB （判断根拠Aと判断根拠Bは違う）
U(traceA) = U(traceB) （でも証跡なしで見ると同じ操作に見える）
定理名：forgetting_trace_layer_can_collapse_distinctions
これは「雰囲気でそうかも」ではなく、Leanが受理した反例です。Leanを読める人なら誰でも独立に確認できます。
誰でもわかる言葉にすると
医療AIが「この薬を優先」と出したとき、結果だけ残っていても、「血液検査の値で判断したのか、既往歴で判断したのか、医師がどこで確認したのか」が消えると、後から安全確認できません。
このLeanが言っているのは、その「消える」という問題は雰囲気の話ではなく、証跡層が弱いと数学的に区別が潰れる反例を具体的に構成できるということです。
逆に言えば、「消えないようにする構造」を正しく作れば、合成後も追跡可能であることを数学的に保証できるということです。
このLeanがADICにとって重要な理由
ADICが言う「AIが何を根拠に判断したかを、後から第三者が検証できる形で残す」という考え方は、これまで「そうすべきだ」という主張でした。
このLeanによって、それは**「証跡層が弱いと、判断根拠の区別が構造的に潰れうる」ことが機械検証された論拠**を持つことになります。
営業文句ではなく、Leanが受理した数学的骨格として存在しています。
正確に言うべき限界
このLeanが証明していないことも明記します。
現実のAIシステムが安全であること
EU AI Act適合
ADICの実装が正しいこと
「beck_chevalley（組織をまたぐ視点変換の整合）」は構造的仮定として置いており、一般的な導出ではありません
証明したのは数学的骨格の部分です。現実への適用は別の話です。
技術的な確認方法
GitHubで公開しています。Lean 4とMathlibがあれば誰でも独立に型チェックできます。
lake update
lake exe cache get
lake env lean AIAssurance.lean
エラーなしで終了すれば、全定理が型チェックを通過しています。
コメント