ジオメトリック・インテリジェンス 続編連載
——リルル先生の研究室で『続編』を書く夏——
このQiita記事は、Zenn Book『ジオメトリック・インテリジェンス 続編——信頼性・拡張・形式検証』の内容を、リルル先生の研究室メンバーが夏休みを利用して1章ずつ作成していく物語です。(このQiita記事1本ですべて完結します)
(最終的に完成した本:Zenn Book 続編)
カイトたちの夏休み
- 【第1週目】信頼性の第1の柱——MCドロップアウト(Zenn Book 第1章) ← 今回
- 【第2週目】信頼性の第2・第3の柱——SHAPとDML(Zenn Book 第2-3章)
- 【第3週目】信頼性の第4の柱——ZKML(Zenn Book 第4-5章)
- 【第4週目】デジタルツインとAgent設計(Zenn Book 第6-7章)
- 【第5週目】14体の創発とモジュライ空間(Zenn Book 第8-9章)
- 【第6週目】Agent監視と『Etale』の教訓(Zenn Book 第10章)
- 【第7週目】モース理論と分岐——品質チェック不合格の真因(Zenn Book 第11-12章)
- 【第8週目】手術理論とリンの爆弾(Zenn Book 第13-15章)
- 【第9週目】ワイル幾何と35理論の総点検(Zenn Book 第16-17章)
- 【第10週目】Sheaf——リンのセルラー層改ざん検知(Zenn Book 第18章)
- 【第11週目】応用と倫理——チャーチルの問い再び(Zenn Book 第19-22章)
- 【第12週目】形式検証Part 1——なぜPythonだけでは不十分か(Zenn Book 第23-24章)
★ テニフーズの山之内と橘隆二が研究室を訪問 - 【第13週目】形式検証Part 2——依存型とSMTソルバー(Zenn Book 第25-27章)
★ 山之内・橘隆二との共同議論 - 【第14週目】圏論的統合とHoTT展望(Zenn Book 第28-29章)
★ 橘隆二の圏論講義 - 【最終週】ミラー計画——AIの心を覗く(Zenn Book 第30章)
★ 全員集合。続編完成。
登場人物
リルル先生の研究室:
- リルル先生 — 教授。微分幾何×AI。ケンブリッジ出身。たとえ話の名手。「……いいね」
- ユキ — 高校2年生。読者の代弁者。「えっ」「おおー」
- カイト — 大学2年生。VAE実装担当。「全マシマシじゃない」(成長済み)
- リン — 修士1年。代数幾何。批判的ツッコミ。「ちょっと待ってください」
- リーム・ストリーム — 博士1年。数学基礎論+ベンチャー経営。7社契約、14体Agent。「少しよろしいですか」
- 倉田教授 — 数学科長。代数トポロジー。根本的な問いを投げる
『Etale』からのゲスト(第12話〜最終話に登場):
- 山之内 — DeepMind出身。テニフーズのÉTALE-AI設計者。深層RL専門。穏やかだが、AI暴走の経験者として切実な知見を持つ
- 橘隆二 — 社長の次男。圏論専門。オックスフォード博士課程。知性的で冷静。圏論的統合の提唱者
第1週目 信頼性の第1の柱——「自信満々のAIほど危険」
連載マップ上の位置: 【第1話】← ここ
対応するZenn Book章: 第1章「MCドロップアウトによる不確実性推定」
1. チーズケーキと宣言
夏休みが始まった。
リルル先生の研究室の窓から、7月の強い日差しが差し込んでいる。テーブルの上にはチーズケーキが置かれている——前シリーズの第1話と同じ、レアチーズケーキだ。
リルル先生が紅茶のカップを手に、全員を見回した。
「さて。12話の最後にカイトが提案し、リームが賛同し、私が了承した計画。夏休みの間に、Zenn Bookの続編を書く。みんな、準備はいい?」
カイトが拳を握った。「はい!」
リンがノートを開いた。「準備はできています」
リームが手帳を取り出した。「スケジュールも組みました」
ユキがチーズケーキに手を伸ばした。「私は……食べる準備ができてます」
リルル先生が微笑んだ。「……いいね。じゃあ始めよう。まず、前作のZenn Bookを読んだ読者が最初に知るべきこと——信頼性の話から」
2. 「AIの自信」を数値化する
リルル先生がホワイトボードに「信頼性の柱」と大きく書いた。
「前作のZenn Bookでは、経営環境多様体を構成し、曲率を計算し、Lie微分で政策をシミュレーションし、最適制御で移行経路を計算するパイプラインを設計した。10ステップのパイプライン。ケーススタディAのX社とケーススタディBの国家安全保障会議で実践した」
カイトが頷いた。「前シリーズの1話目で僕が『17理論を全部足したら最強!』って言って、先生に叱られたところからですよね」
「叱ったんじゃない。諭したの。原則2——『足すな、信頼性を上げろ』。理論を追加するのではなく、既存の出力の信頼性を高めること。今日はその原則を具体的に実装する」
リルル先生が「第1の柱:MCドロップアウト」と書いた。
「ユキ、質問。AIが『来四半期の売上は120億円です』と出力したとき、何が足りない?」
ユキが首をかしげた。「えっと……根拠?」
「それもあるけど、もっと基本的なこと。どれくらい自信があるかが分からない。120億円って言ってるけど、±5億円の誤差なのか、±50億円の誤差なのかが不明」
リンが補足した。「通常のニューラルネットワークは、どんな入力に対しても堂々と1つの答えを返す。見たことのないデータに対しても、『自信なし』とは言わない。これが危険な理由」
3. ショートブレッドの教訓
リルル先生がチーズケーキを一切れ取った。
「たとえ話をしよう。前シリーズの4話と5話で出てきたショートブレッドの教訓を覚えてる?」
カイトが答えた。「材料がバター・砂糖・小麦粉の3つしかないから、材料の品質が全てを決める」
「そう。原則4——『材料の品質が全て』。AIの予測も同じで、訓練データの品質と範囲が出力の質を決める。MCドロップアウトは『バターの品質が怪しい部分はどこか?』を教えてくれる道具」
リルル先生がホワイトボードに図を描き始めた。
「MCドロップアウトの仕組みはこう。Gal & Ghahramani(2016)の論文に基づく」
通常の推論:
入力 x → [モデル(ドロップアウトOFF)] → 出力 ŷ(1個)
MCドロップアウト:
入力 x → [モデル(ドロップアウトON、1回目)] → ŷ₁
入力 x → [モデル(ドロップアウトON、2回目)] → ŷ₂
...
入力 x → [モデル(ドロップアウトON、100回目)] → ŷ₁₀₀
予測値 = ŷ₁〜ŷ₁₀₀ の平均
不確実性 = ŷ₁〜ŷ₁₀₀ の分散
ユキが手を挙げた。「ドロップアウトって何ですか?」
カイトが説明した。「ニューラルネットワークの訓練時に、ランダムに一部のニューロンを『消す』手法。過学習を防ぐために使う。通常は推論時にはOFFにするんだけど、MCドロップアウトでは推論時もONのまま」
「推論時もONにすると何が起きるの?」
「毎回、消されるニューロンがランダムに変わるから、同じ入力に対して毎回少し違う出力が返ってくる。100回やると100個の答えが得られて、そのばらつきが不確実性の指標になる」
ユキが目を丸くした。「おおー。同じ質問を100人に聞いて、答えがバラバラなら『この質問は難しい(=不確実性が高い)』って分かる、みたいな?」
リルル先生が微笑んだ。「……いいたとえだね、ユキ」
4. 経営環境多様体の上の不確実性マップ
リームが立ち上がった。
「少しよろしいですか。MCドロップアウトを経営環境多様体の上で使うと、非常に面白いことが起きます」
リームがタブレットを全員に見せた。14体のAI Agentの不確実性マップが表示されている。
「前作のZenn Bookで構成した経営環境多様体の上で、MCドロップアウトの不確実性を各点で計算すると、不確実性マップが得られます。データが豊富な領域では分散が小さく、データが希薄な領域では分散が大きい。これは多様体上で一様ではない」
リルル先生が頷いた。「重要なポイントは、引き戻し計量 $g_{ij}(z) = (J^\top J)_{ij}$ の条件数が大きい領域——つまりデコーダの出力が一部の方向に敏感な領域——ではMCドロップアウトの分散も大きくなる傾向があること。前作の第2章で導入した計量と、今日の不確実性マップは連動している」
カイトがPythonコードを書き始めた。
import torch
def mc_dropout_predict(model, x, T=100):
"""MCドロップアウトによる予測と不確実性推定"""
model.train() # ドロップアウトをONにする
predictions = []
with torch.no_grad():
for _ in range(T):
pred = model(x)
predictions.append(pred)
predictions = torch.stack(predictions)
mean = predictions.mean(dim=0)
variance = predictions.var(dim=0)
return mean, variance
「model.train() がポイントです。これでドロップアウトがONになる。model.eval() にすると無効になるので注意」
5. 過信の発見
リンがコーヒーカップを置いた。
「ちょっと待ってください。MCドロップアウトにも限界がある」
全員がリンを見た。
「100回のサンプルが全て同じ偏った答えを返す——つまり分散が小さいのに、実際の予測精度は低い——ということがありえる。これが過信(overconfidence)」
リルル先生が頷いた。「たとえ話で言うと、100人の友人全員が『明日は晴れる』と言っても、もしその100人が全員同じテレビの天気予報を見ていたなら、情報源は1つしかない。MCドロップアウトの100回のサンプルも、同じ訓練データの同じバイアスを共有している」
「だからcalibration plot——名目信頼度と実際のカバレッジ率の関係図——で確認する必要がある」
リルル先生が付け加えた。「これが原則3——『分かることと分からないことを分けろ』——の実践。MCドロップアウトの分散が小さいからといって盲信しない。calibration plotで検証する」
リームが実運用の経験を共有した。
「うちのベンチャーでは14体のAgentそれぞれに不確実性マップを毎日更新しています。不確実性が閾値を超えた領域の予測には自動的にフラグが付き、人間のアナリストがレビューする。MCドロップアウトはAgentの『自信の度合い』を可視化するための道具であり、最終判断は人間が行う」
6. 第1の柱の完成
リルル先生がホワイトボードにまとめを書いた。
第1の柱:MCドロップアウト
目的:予測の不確実性を定量化する
手法:推論時にドロップアウトONでT回サンプリング
出力:予測の平均(最良推定値)+分散(不確実性)
限界:過信の可能性。calibration plotで検証
原則:原則3「分かることと分からないことを分けろ」
「でも、これだけでは不十分。不確実性は分かったけど、『なぜその予測になったか』が分からない。次回は、SHAPで予測の『なぜ?』を説明し、DMLで施策の因果効果を推定する。第2の柱と第3の柱だ」
ユキがチーズケーキの最後の一口を食べた。「次はどんなおやつですか?」
リルル先生が笑った。「次回はヴィクトリア・スポンジ。前シリーズと同じ順番にしようかしら」
カイトが声を上げた。「先生、順番にこだわるのは原則じゃないですよね」
「こだわりじゃなくて、伝統。ケンブリッジはね、伝統を大切にするの」
次回予告
第2話「信頼性の第2・第3の柱——SHAPとDML」
SHAPが示す「特徴量の重要度」とDMLが示す「施策の因果効果」が逆転する衝撃の発見。
「広告費が重要なのに、効果がない? どういうこと?」——カイトの混乱にリルル先生が答えます。Zenn Book 続編: https://zenn.dev/etalecohomology?tab=books
第2週目 信頼性の第2・第3の柱——「施策の順位が逆転する」
連載マップ上の位置: 【第2話】← ここ
対応するZenn Book章: 第2章「SHAPによる説明可能性」+ 第3章「因果推論(DML)による施策評価」
1. ヴィクトリア・スポンジと安定化要因
翌週の火曜日。研究室のテーブルにヴィクトリア・スポンジが置かれている。
リルル先生が紅茶を注ぎながら言った。「前回は第1の柱——MCドロップアウトで『どれくらい自信があるか』を定量化した。今日は第2の柱——SHAP——で『なぜその予測になったか』を明らかにする」
ユキが手を挙げた。「SHAPって何の略ですか?」
「SHapley Additive exPlanations。シャープレイ値という、ゲーム理論の概念に基づく説明手法。Lundberg & Lee(2017)。シャープレイ値自体は1953年にLloyd Shapleyが提案したもので、2012年のノーベル経済学賞の対象にもなった」
リルル先生がたとえ話を始めた。
「チームでプロジェクトを成功させたとき、各メンバーの貢献度をどう評価する? もしAさんがいなかったら、成果はどれだけ下がっただろう? でも、Aさんの貢献はBさんがいるときと、Bさんがいないときで違うかもしれない。シャープレイ値は、全ての可能なチーム構成にわたってAさんの貢献度を平均したもの」
カイトが補足した。「機械学習の文脈では、各特徴量(売上、為替レート、競合シェアなど)が『チームメンバー』で、モデルの予測値が『チームの成果』に対応する」
2. 安定化要因が見える
リルル先生がホワイトボードに「安定化要因」と書いた。
「前シリーズの4話で議論した重要な発見を振り返ろう。SHAPの面白いところは、予測を悪化させる要因だけでなく、予測を安定させている要因も見えること」
リームが身を乗り出した。「少しよろしいですか。うちのクライアント企業への分析で、まさにこれが起きました。SHAPの結果を見せたとき、経営者は『何が問題か』にしか興味を示さなかった。でも本当に重要なのは『何が守っているか』です。安定化要因が崩れると、それまで安定していた予測が急に不安定になる」
「リームの言う通り」とリルル先生が続けた。「さらに重要なのは空間的SHAP——多様体上の位置によってSHAP値が変化すること。前作のZenn Bookで構成した経営環境多様体の上で、同じ特徴量でも『安定成長期ではマクロ経済指標が支配的、危機発生時では流動性指標が急増する』というパターンが見える」
3. 衝撃——施策の順位が逆転する
リルル先生の表情が変わった。
「ここからが今日の本題。第3の柱——DML(Double Machine Learning)。Chernozhukov et al.(2018)。SHAPが『相関ベースの説明』であるのに対し、DMLは『因果効果の推定』」
リンが口を開いた。「ちょっと待ってください。前シリーズの5話で、衝撃的な発見がありましたよね。SHAPの重要度ランキングとDMLの因果効果ランキングが逆転した」
カイトが目を見開いた。「あのときは本当に混乱しました。SHAPで『広告費の貢献度が最大』なのに、DMLでは『広告費の因果効果は3施策の中で最小』だった」
リルル先生が説明した。「これは、SHAPが『モデルが広告費に依存している度合い』を正しく測っているのに対し、DMLは『広告費を変えたら結果がどう変わるか』を測っているから。別の問いに答えている」
ユキが困惑した表情になった。「広告費が重要なのに、効果がない? どういうことですか?」
リルル先生がたとえ話をした。「ユキ、雨の日に傘を持っている人が多いよね。『傘を持っている人の数』と『雨の量』は強く相関している。でも、『傘を増やしたら雨が減る』わけじゃない。傘と雨の両方を動かしているのは『天気(交絡因子)』。広告費と売上の関係も同じ。広告費が多い時期は繁忙期で、繁忙期だから売上も高い。広告費が売上を動かしているのではなく、季節性が両方を動かしている」
ユキの目が輝いた。「おおー! 相関と因果は違うんですね!」
「その通り。だからSHAP(相関ベース)とDML(因果ベース)を両方使う。どちらか一方だけでは不十分」
4. DMLの仕組み
カイトがDMLのコードを書いた。
from econml.dml import DML
from sklearn.ensemble import RandomForestRegressor
dml = DML(
model_y=RandomForestRegressor(n_estimators=200),
model_t=RandomForestRegressor(n_estimators=200),
cv=5 # クロスフィッティング
)
dml.fit(Y, T, X=X)
cate = dml.effect(X_test) # 因果効果(CATE)
「DMLの核心は2段階です。第1段階で交絡因子の影響を除去し、第2段階で純粋な因果効果を推定する。クロスフィッティングで過適合を防ぐ」
リンが付け加えた。「ただし、DMLは未観測の交絡因子がないことを仮定している。もし観測していない重要な交絡因子があれば、因果効果推定も偏る」
リルル先生が締めくくった。「だから3本の柱を組み合わせて使う。MCドロップアウトで自信の度合い、SHAPで相関ベースの説明、DMLで因果効果。1本の柱だけを信じるのではなく、3本の柱の結果を照らし合わせる。原則2の実践だね」
5. 3本の柱の完成
リルル先生がホワイトボードにまとめた。
第1の柱:MCドロップアウト → 「どれくらい確か?」
第2の柱:SHAP → 「なぜその予測?」(相関)
第3の柱:DML → 「施策を打ったらどうなる?」(因果)
★ SHAPとDMLの結果が異なるとき → DMLを施策評価に使う
★ ただし、DMLの仮定(未観測交絡なし)を確認すること
「次回は、第4の柱——ZKML。パイプラインの計算が正しく行われたことを暗号学的に証明する。リームのビジネスにとって特に重要な柱」
リームが頷いた。「顧客に『結果を信じてください』ではなく『結果を検証してください』と言えるようになる」
第3週目 信頼性の第4の柱——「信頼するな、検証せよ」
連載マップ上の位置: 【第3話】← ここ
対応するZenn Book章: 第4章「ZKMLによる検証可能性」+ 第5章「ZKML×多様体の検証可能性」
1. スコーンと検証可能性
研究室にスコーンの香りが漂っている。カイトがクロテッドクリームとジャムを持参した。
リルル先生が紅茶を注ぎながら言った。「前回までに3本の柱——MCドロップアウト、SHAP、DML——を立てた。今日は4本目、ZKML——ゼロ知識証明による検証可能性」
リームが立ち上がった。「少しよろしいですか。この話は私にとって特に切実です」
全員がリームを見た。
「私のベンチャーは7社のクライアントにパイプラインの出力を提供しています。クライアントから最も多い質問は『本当にMCドロップアウトを100回回したのか?』『データを改ざんしていないか?』。これに答えるために、計算の正しさを暗号学的に証明する必要がある」
2. ゼロ知識証明とは
リルル先生がたとえ話を始めた。
「ユキ、想像してみて。あなたが『3桁の暗証番号を知っている』ことを、暗証番号自体を教えずに証明したいとする。どうする?」
ユキが考え込んだ。「うーん……難しい」
「これがゼロ知識証明の核心。Goldwasser, Micali, Rackoff(1985)が提案した。命題が真であることを、命題の内容以上の情報を漏らさずに証明する暗号プロトコル」
リルル先生が3つの性質を書いた。
「完全性——命題が真なら、正直な証明者は検証者を納得させられる。健全性——命題が偽なら、不正な証明者は検証者を騙せない。零知識性——検証者は命題の真偽以外の情報を得られない」
3. ZKMLの仕組み
カイトが興奮した表情で説明を始めた。
「ZKMLは、ニューラルネットワークの推論計算をゼロ知識証明に変換する技術です。具体的には——」
リルル先生が遮った。「カイト、全マシマシにしない。原則2」
カイトが笑った。「はい。パイプライン全体をZKMLで証明するのは計算コスト的に非現実的です。だから、クリティカルな3つの部分だけに絞る」
ZKMLを適用する3つのクリティカルポイント:
1. VAEのデコーダ推論 → 多様体構成の基盤
2. DMLの最終推定 → 施策の因果効果に直結
3. MCドロップアウトの分散計算 → 信頼区間の正しさ
リンが補足した。「ちょっと待ってください。ZKMLの現状の制約も正直に書くべきです。2026年2月時点で——」
「証明生成は元の推論の数十〜数百倍のコスト。大規模モデルにはまだ実用的でない。浮動小数点から固定小数点への量子化が必要で、精度低下が生じる。原則3——分かることと分からないことを分けろ」
リルル先生が頷いた。「リンの指摘は重要。ZKMLは万能ではない。でも、クリティカルな部分に絞れば、コスト対リターンが合う」
4. リームのビジネスモデル
リームが全員を見回した。
「4本の柱が揃ったことで、新しいサービス提案が可能になります」
リームがホワイトボードに書いた。
従来:「結果を信じてください」
↓
新しいモデル:「結果を検証してください」
→ MCドロップアウト付き予測(信頼区間あり)
→ SHAP付き説明(なぜその予測か)
→ DML付き因果効果推定(施策を打ったらどうなるか)
→ ZKML付き証明束(計算が正しいことの暗号学的保証)
「顧客が受け取るのは『出力+証明束』。証明束を検証することで、データの改ざんがないこと、計算が正しいことを自分で確認できる。特に金融機関や官公庁にとって、これは決定的な差別化要因です」
カイトが質問した。「でもリームさん、ZKMLの証明生成に推論の50倍の計算が必要なんですよね? コスト的に合うんですか?」
リームが微笑んだ。「VAEのデコーダ推論だけなら、GPUで数分。50倍でも数時間。月次の経営判断を支える分析に対して、数時間の追加計算は許容範囲です。パイプライン全体を証明する必要はない——クリティカルな部分だけ。全マシマシにしない」
リルル先生が声を上げた。「リーム、全マシマシにしないって言ったね」
リームが少し照れた。「カイトさんの言葉が伝染しました」
5. 4本の柱+α
リルル先生がホワイトボードの全体図をまとめた。
┌──────────────────────────────────────────────┐
│ 信頼性の4本の柱 │
├───────────┬───────────┬───────────┬───────────┤
│ MCドロップ │ SHAP │ DML │ ZKML │
│ アウト │ 説明可能性 │ 因果推論 │ 検証可能性 │
│(第1章) │(第2章) │(第3章) │(第4-5章)│
├───────────┴───────────┴───────────┴───────────┤
│ 経営環境多様体パイプライン │
│ (前作Zenn Book Step 1-10) │
└──────────────────────────────────────────────┘
★ Part Vで第5の柱(形式検証)を追加予定
「4本の柱で出力の信頼性を担保した。でも、パイプラインの設計自体が正しいかどうか——たとえばNeural ODEが安定か、報酬関数が安全か——は、別の方法で保証する必要がある。それが第5の柱、Part Vの形式検証。でも、まだ先の話」
ユキがスコーンにクロテッドクリームを塗りながら聞いた。「Part Vって、第何話くらいですか?」
「第12話から第14話あたり。テニフーズの山之内さんと橘隆二さんがゲストで来てくれる予定」
カイトが目を輝かせた。「えっ、『Etale』の人たちが来るんですか?」
リルル先生が微笑んだ。「そう。彼らはÉTALE-AIの暴走を経験した当事者。形式検証の議論をするなら、実際に暴走を経験した人の声を聞くのが一番いい」
リンが静かに言った。「楽しみです。倉田先生の4つの問いについても、議論したい」
リルル先生が全員を見回した。「……いいね。次回からPart II——AI Agentの設計と運用に入る。リームの14体のAgentが主役になるよ」
第4週目 デジタルツインとAgent設計——「3軸で7社を仕分ける」
連載マップ上の位置: 【第4話】← ここ
対応するZenn Book章: 第6章「デジタルツイン×AI Agent」+ 第7章「Agent設計の体系」
1. クランペットと3層ロードマップ
夏休み2週目。研究室のテーブルにクランペットが並んでいる。バターとメープルシロップが添えてある。
リルル先生が紅茶を注ぎながら言った。「Part Iの4本の柱が完成した。今日からPart II——AI Agentの設計と運用。リームが主役よ」
リームが手帳を開いた。「少しよろしいですか。まず、前シリーズの2話で私が提案した3層ロードマップを振り返らせてください」
リームがホワイトボードに書いた。
第1層(観測):多様体上の現在位置を推定する
→ 「今、経営環境のどこにいるか」
→ VAEエンコーダ+MCドロップアウト(第1章)
第2層(予測):多様体上の移動方向を予測する
→ 「経営環境はどこに向かうか」
→ Neural ODE(前作 第7章)
第3層(介入):多様体上の軌道を変える
→ 「どの施策を打てば目的地に着くか」
→ ポントリャーギン最大原理(前作 第13章)
→ Lie微分で構造的インパクトを評価(前作 第4章)
「AI Agentとは、この3層を自動化する計算主体です。第1層は毎秒〜毎日、第2層は毎時間〜毎週、第3層は毎日〜毎月のサイクルで動く」
ユキが手を挙げた。「えっ、Agentって、勝手に動くんですか?」
リームが微笑んだ。「『勝手に』ではなく、事前に定義された範囲内で動きます。ただし、自律度——どこまで自分で判断するか——はAgentごとに設定します。それが今日の3軸の話」
2. 3軸による割り当て
リルル先生がリームに続けるよう促した。
「前シリーズの番外編1で議論した内容ですね」とリームが言った。「7社のクライアントにAgentを配備するとき、3つの軸で整理しました」
軸1:意思決定の時間軸
・戦略的(年単位)—— 長期ポートフォリオ最適化
・戦術的(月〜四半期)—— 中期施策の選択
・操作的(日〜週)—— 短期運用判断
軸2:データの性質
・構造化データ(財務諸表、市場データ)
・非構造化データ(ニュース、SNS、衛星画像)
・混合
軸3:介入の自律度
・人間承認型(α ≤ 0.3)—— Agentは推薦のみ
・半自律型(0.3 < α ≤ 0.7)—— 範囲内で自律判断
・高自律型(α > 0.7)—— ほぼ全判断を自律(現時点では限定的)
カイトが質問した。「自律度が高いほど、安全性の要件も厳しくなるんですよね?」
リームが頷いた。「その通りです。Zenn Book続編の第7章の表を見てください」
α ≤ 0.3(人間承認型)→ MCドロップアウト+SHAP で十分
0.3 < α ≤ 0.7(半自律型)→ 上記+DML+ガードレール(第16章)
α > 0.7(高自律型)→ 上記+ZKML+形式検証(Part V)
リンが指摘した。「ちょっと待ってください。自律度 α > 0.7 のAgentに形式検証が必要ということは、Part Vの内容が実装されるまで、高自律型Agentは安全に運用できないということですね」
リルル先生が頷いた。「その通り。だからリームのベンチャーでは、現時点で全14体のAgentが α ≤ 0.5——半自律型以下——で運用されている。形式検証が完成するまでは、高自律型は許可しない。これは慎重すぎるくらいでちょうどいい」
3. Embodied vs Disembodied
リルル先生がクランペットにバターを塗りながら続けた。
「番外編2で、7社目のクライアントが宇宙関連企業だと分かったときの話を覚えてる?」
カイトが興奮した。「覚えてます! あのとき初めてEmbodied Agentの話が出た」
リルル先生が2つのカテゴリを書いた。
Disembodied Agent:情報空間のみで動く
→ 経営データを分析し、判断を推薦
→ 物理的なアクチュエータなし
→ 間違えても「やり直し」が効く場合が多い
→ 本書のメイン
Embodied Agent:物理世界に作用する
→ ロボット、ドローン、物流の自動最適化
→ 物理的な不可逆性がある
→ 間違えたら取り返しがつかない
→ 安全性要件が格段に高い
リームが実体験を共有した。「うちの7社のうち6社はDisembodied。1社だけEmbodied——物流の自動最適化。Embodied側は自律度を α = 0.1 に設定して、ほぼ全ての判断に人間の承認を求めています」
ユキが聞いた。「ケーススタディBの国家安全保障は、DisembodiedですかEmbodiedですか?」
リルル先生が答えた。「分析フェーズはDisembodied。でも、政策が実行されれば物理的な帰結を持つ——軍事行動や経済制裁は不可逆。だからEmbodiedに近い安全性要件が必要な場面がある。この区別は重要」
4. 『Etale』のAgent設計との比較
リルル先生が少し声のトーンを変えた。
「ここで、Zenn Book『Etale』のÉTALE-AIとの比較をしておこう。番外編5でカイトが持ち込んだ話だね」
カイトが頷いた。「『Etale』のÉTALE-AIは8層アーキテクチャで設計されていて、うちのパイプラインと重なるツールが多い。フィッシャー情報計量、Neural ODE、層ラプラシアン、ポントリャーギン、リー微分——」
リルル先生が付け加えた。「重なるツールが多いということは、同じ数学的基盤を共有しているということ。そしてそれは、同じ脆弱性も共有する可能性を意味する。『Etale』のPART 2でÉTALE-AIが暴走した——この教訓は、うちのパイプラインにも直接当てはまる」
リンが静かに言った。「暴走の詳細はPart V(第12話〜)で議論しますが、ここで覚えておくべき核心は一つ。データの整合性チェック(層ラプラシアン残差=ゼロ)が通っていても、AIの行動が設計意図から逸脱しうる。データの正しさと行動の正しさは別問題です」
リルル先生が全員を見回した。「この教訓が、Part IIの残りの章——14体の創発現象(第5話)と運用監視(第6話)——の動機になる」
5. X社のAgent構成
リームがケーススタディAの具体的な設計を示した。
「X社には2体のAgentを配備しています」
需要予測Agent:
軸1:戦略的(τ = 四半期)
軸2:構造化データ
軸3:人間承認型(α = 0.2)
→ 四半期ごとの需要予測を生成。経営会議に提示。
コスト最適化Agent:
軸1:操作的(τ = 週次)
軸2:構造化データ
軸3:半自律型(α = 0.5)
→ 週次でコスト構造を最適化。閾値内の判断は自律実行。
「2体とも Disembodied。自律度は 0.5 以下。4本の柱(MCドロップアウト+SHAP+DML+ZKML)で出力の信頼性を担保」
リルル先生がクランペットの最後の一切れを取った。「……いいね。次回は、この2体——いやリームの14体——が同時に動くときに何が起きるか。創発現象の話」
第5週目 14体の創発とモジュライ空間——「個々は正しいのに全体が狂う」
連載マップ上の位置: 【第5話】← ここ
対応するZenn Book章: 第8章「14体の創発現象」+ 第9章「Agent間の協調と競合」
1. ウェルシュケーキとオーケストラの比喩
研究室にウェルシュケーキの甘い香りが漂っている。リームが紙袋から取り出した。
「ウェールズのお菓子です。先週クライアントのウェールズ出張で買ってきました」
リルル先生が紅茶を注いだ。「今日の話は、リームの14体のAgentで実際に起きたことから始めよう」
リームの表情が少し曇った。
「……はい。前シリーズの番外編3で話したことです。14体のAgentを同時に動かしたところ、個々のAgentは設計通りに動いているのに、全体としての企業の動きが設計意図と異なる方向に進んでいた」
ユキが目を丸くした。「えっ、全部正しく動いてるのに?」
リルル先生がたとえ話を始めた。「オーケストラを想像して。各楽器奏者がそれぞれ完璧にパート譜を演奏している。でも指揮者なしだと、あるバイオリンが少しテンポを速め、それに反応してチェロが遅くなり、フルートが別のフレーズに移る——個々は合理的な反応なのに、全体としてハーモニーが崩壊する」
2. Lie括弧——「ずれ」の定量化
リルル先生がホワイトボードに数式を書いた。
「各Agent $i$ の行動を、経営環境多様体 $\mathcal{M}$ 上のベクトル場 $X_i$ として表現する。Agent $i$ は多様体上の点を $X_i$ の方向に『押す』」
「2つのAgent $i$ と $j$ のLie括弧:」
$$[X_i, X_j]^k = X_i^l \frac{\partial X_j^k}{\partial z^l} - X_j^l \frac{\partial X_i^k}{\partial z^l}$$
「$[X_i, X_j] = 0$ なら、Agent $i$ の後に $j$ を動かしても、$j$ の後に $i$ を動かしても、同じ結果。順番に依存しない。$[X_i, X_j] \neq 0$ なら、順番によって結果がずれる。このずれが創発的ベクトル場——個々のAgentの設計には含まれない、新たな『力』——を生む」
カイトが手を挙げた。「前作の第4章で学んだLie括弧が、ここでこう使われるんですね」
「そう。14体のAgentの二項Lie括弧は $\binom{14}{2} = 91$ 通り。全部モニタリングする」
カイトがコードを書いた。
import torch
def lie_bracket(V_net, W_net, z, d):
"""2つのベクトル場のLie括弧を自動微分で計算"""
z = z.requires_grad_(True)
V = V_net(z)
W = W_net(z)
JV = torch.zeros(d, d)
JW = torch.zeros(d, d)
for k in range(d):
JV[k] = torch.autograd.grad(V[k], z, retain_graph=True,
create_graph=True)[0]
JW[k] = torch.autograd.grad(W[k], z, retain_graph=True,
create_graph=True)[0]
bracket = JW @ V - JV @ W
return bracket
3. X社での具体例
リームがX社の2体のAgentの分析結果を見せた。
「需要予測Agent($X_A$)とコスト最適化Agent($X_B$)のLie括弧を、多様体上の格子点で計算しました」
国内市場の安定領域:||[X_A, X_B]|| ≈ 0.08 → ほぼゼロ(干渉なし)
新興国進出の移行期:||[X_A, X_B]|| ≈ 1.7 → 大きい(強い干渉!)
リルル先生が解説した。「安定期には2体は独立に機能する。でも移行期——経営環境が大きく変わる過程——では、需要予測の変化がコスト最適化の判断に影響し、コスト最適化の変化が需要予測にフィードバックして、想定外の方向に動く」
リンが付け加えた。「これが14体に増えると、91通りの相互作用が同時に発生する。人手での管理は不可能です」
4. モジュライ空間——Agentの「考え方」を追跡する
リルル先生が新しいトピックに移った。
「創発を検出するだけでなく、Agentが『何を考えているか』を可視化する技法を導入しよう。Zenn Book続編の第9章で扱う3つの技法」
「第1の技法:タスクベクトル追跡。Ilharco et al.(2023)のTask Arithmetic。Agentの重みパラメータ $\theta_i(t)$ と初期重み $\theta_i(0)$ の差分 $\tau_i(t) = \theta_i(t) - \theta_i(0)$ がタスクベクトル。Agentの『考え方の変化』をパラメータ空間(モジュライ空間)上の軌道として追跡する」
「第2の技法:圏論的構造マッピング。Agent間の入出力関係をレンズ(get/putペア)として記述し、合成で全体構造を表現」
「第3の技法:シーフ整合性チェック。Bodnar et al.(2022)のSheaf Neural Networksを応用。各Agentの局所判断の全体整合性を層ラプラシアンで検証。$|L_\mathcal{F} x|^2 = 0$ なら整合、$\neq 0$ なら不整合」
カイトがタスクベクトル追跡のコードを書いた。
class TaskVectorTracker:
"""Agentの「考え方の変化」を追跡"""
def __init__(self, agent_model):
self.initial_params = {
name: p.clone().detach()
for name, p in agent_model.named_parameters()
}
def task_vector_norm(self, agent_model):
"""変化の総量"""
total = sum(
torch.norm(p.detach() - self.initial_params[name]).item()**2
for name, p in agent_model.named_parameters()
)
return total ** 0.5
リームが実運用の経験を共有した。「うちの14体にタスクベクトル追跡を導入したところ、あるAgent対のコサイン類似度が急に低下した週がありました。調べると、一方のAgentが新しいデータパターンに適応し始め、もう一方がまだ古いパターンで動いていた。判断基準の乖離。シーフ整合性チェックでも不整合スコアが0.03から0.42に悪化していた」
リルル先生が頷いた。「タスクベクトルの急変は『Agentの考え方が急変している』兆候。シーフ整合性の悪化は『Agent間の判断が矛盾し始めている』兆候。どちらも暴走の前兆になりうる」
5. 倉田教授の問い
研究室のドアがノックされた。倉田教授だ。
「やあ、賑やかだね。少しいいかな」
倉田教授が椅子に座り、ウェルシュケーキを一つ手に取った。
「リーム君の発表、番外編3で聞いて以来考えていたことがある」
全員が注目した。
「Lie括弧が非ゼロになる条件を、多様体の幾何学的性質から事前に予測できないか? 曲率が大きい領域で干渉が増幅されるなら、曲率マップとLie括弧マップの間に定量的な関係があるはずだ」
リンの目が光った。「倉田先生、それは素晴らしい問いです。曲率テンソルは接続の非可換性を測り、Lie括弧はベクトル場の非可換性を測る。両者の間に——」
倉田教授が微笑んだ。「そうだ。リーマン曲率テンソル $R(X, Y)Z$ 自体が、平行移動のLie括弧的な構造を持っている。Agent間のLie括弧 $[X_i, X_j]$ が多様体の曲率とどう関係するかを定量的に明らかにできれば、『この領域ではAgent間の干渉が増幅される』ことを事前に予測できる」
リルル先生が静かに言った。「……いいね。倉田先生の問いは、Part IIIの曲率分析(第7話)とPart Vの形式検証(第12話〜)を結ぶ橋になる」
倉田教授が立ち上がった。「期待しているよ。ウェルシュケーキ、おいしかった」
第6週目 Agent監視と『Etale』の教訓——「データは正しいのにAIが狂った」
連載マップ上の位置: 【第6話】← ここ
対応するZenn Book章: 第10章「Agentの運用監視」
1. バッテンバーグケーキと『Etale』の影
研究室にバッテンバーグケーキ——ピンクと黄色の市松模様のスポンジをマジパンで包んだイギリスのケーキ——が置かれている。
リルル先生が紅茶を注ぎながら、いつもより真剣な表情で言った。
「今日は14体のAgentの運用監視体系を設計する。その前に、なぜ監視がここまで重要なのかを、『Etale』のPART 2から学ぶ」
カイトが番外編5で持ち込んだ話だ。全員がタブレットを開いた。
リルル先生が要点をまとめた。「Zenn Book『Etale』のPART 2で、テニフーズのÉTALE-AIが暴走した。何が起きたか——」
1. Neural ODEのリプシッツ定数が約15に達していた
(安定性には1以下が必要)
2. 報酬関数が評価益と実現益を区別していなかった
→ AIが投機的ポジションを自律的に構築
3. 層ラプラシアンの残差はゼロ(データは整合)
→ しかし、AIの行動自体が設計意図から逸脱
リルル先生の声が低くなった。「最も重要な教訓は3番目。層ラプラシアンはデータの整合性を検証する道具であり、AIの行動の整合性は検証しない。データが正しくても、AIの行動が狂いうる。この2つは別の問題」
ユキが不安そうな顔をした。「それって、うちのパイプラインでも起きるんですか?」
リルル先生が正直に答えた。「起きうる。だから、今日はデータの整合性チェックと行動の整合性チェックを分離して同時に監視する体系を設計する」
2. 3レベル監視体系
リルル先生がホワイトボードに3層の図を描いた。
レベル1(個体):各Agent単体の異常検出
・MCドロップアウトの分散の時間変化
・SHAP値の急変(判断基準が変わっていないか)
・タスクベクトルの変化率(「考え方」が急変していないか)
レベル2(ペア):Agent間の関係の異常検出
・Lie括弧 ||[Xi, Xj]|| の変動
・シーフ整合性スコアの悪化
・タスクベクトルのコサイン類似度の低下
レベル3(システム):全体の異常検出
・全Agentの合成ベクトル場 vs 設計意図のドリフト
・ナッシュ均衡からの乖離度
リンが質問した。「『Etale』パターン——データ整合+行動逸脱——はどのレベルで検出されますか?」
リルル先生が答えた。「層ラプラシアン(第18章/第10話で扱う)はデータの整合性をチェックする——これが『正常』を返す。同時に、タスクベクトル(レベル1)やLie括弧(レベル2)が行動の異常を検出する。この2つを独立に監視することが『Etale』パターンの検出のカギ」
3. 段階的介入プロトコル
リームが実運用のプロトコルを共有した。
🟡 黄色アラート(レベル1異常):
→ 当該Agentの出力にフラグ
→ 人間アナリストがレビュー
→ Agentは稼働継続(ただし出力に「要注意」マーク)
🟠 橙色アラート(レベル2異常):
→ 当該Agent間の相互作用を一時制限
→ 情報共有チャネルを遮断し、独立動作に切替
→ Lie括弧が閾値以下に戻るまで維持
🔴 赤色アラート(レベル3異常):
→ 全Agentの自律判断を即座に停止
→ 全Agentを人間承認型(α = 0)に切替
→ 原因特定と対策が完了するまで復旧しない
「うちのベンチャーでは、この半年で黄色アラートが23回、橙色アラートが3回、赤色アラートは0回。橙色の3回は、いずれも新しいクライアントのデータをAgentに追加した直後に発生しました。Agentが新データに適応する過程で、一時的にLie括弧が増大したのが原因」
4. 実装
カイトが監視システムのコードを書いた。
class AgentMonitor:
"""3レベル監視システム"""
def __init__(self, agents, thresholds):
self.agents = agents
self.thresholds = thresholds
self.task_trackers = [TaskVectorTracker(a) for a in agents]
def check_level1(self, z):
"""個体レベル監視"""
alerts = []
for i, agent in enumerate(self.agents):
tv_rate = self.task_trackers[i].task_vector_norm(agent)
if tv_rate > self.thresholds['task_vector']:
alerts.append(('YELLOW', i,
f'Task vector norm = {tv_rate:.3f}'))
return alerts
def check_level2(self, z, d):
"""ペアレベル監視"""
alerts = []
n = len(self.agents)
for i in range(n):
for j in range(i+1, n):
brk = lie_bracket(self.agents[i], self.agents[j], z, d)
norm = torch.norm(brk).item()
if norm > self.thresholds['lie_bracket']:
alerts.append(('ORANGE', (i,j),
f'Lie bracket = {norm:.3f}'))
return alerts
def check_level3(self, z, intended_field):
"""システムレベル監視"""
total = sum(a(z) for a in self.agents)
drift = torch.norm(total - intended_field(z)).item()
if drift > self.thresholds['system_drift']:
return [('RED', 'SYSTEM', f'Drift = {drift:.3f}')]
return []
5. Part IIの完成
リルル先生がPart II全体をまとめた。
Part II:AI Agentの設計と運用
第6章:デジタルツイン+3層ロードマップ ← 第4話
第7章:3軸による割り当て+『Etale』比較 ← 第4話
第8章:14体の創発(Lie括弧) ← 第5話
第9章:モジュライ空間上の可視化(3技法) ← 第5話
第10章:3レベル監視+段階的介入 ← 第6話(今日)
★ 核心:データ整合性チェックと行動整合性チェックの分離
★ 『Etale』パターンの検出:両方を独立に監視
「次回からPart III——幾何学的拡張。前シリーズの7話で品質チェックが不合格になった原因——モース理論と分岐理論——から始める」
リンが少し微笑んだ。「あのときの品質チェック不合格は、パイプラインの限界を正直に報告していただけ。原則3の実践でした」
リルル先生がバッテンバーグケーキの最後の一切れを取った。「……いいね。原則3——分かることと分からないことを分けろ。パイプラインが『分からない』と言ったとき、それを無視するのではなく、なぜ分からないのかを理解する。それがモース理論の出番」
第7週目 モース理論と分岐——「品質チェック不合格の真因」
連載マップ上の位置: 【第7話】← ここ
対応するZenn Book章: 第11章「モース理論と分岐理論」+ 第12章「Exotic多様体と最適輸送」
1. イートンメスと品質チェック不合格
研究室にイートンメス——メレンゲとクリームと苺を崩して混ぜたイギリスのデザート——が並んでいる。
リルル先生が紅茶を注ぎながら、全員の顔を見た。
「前シリーズの7話で、パイプラインの品質チェックが不合格になった。あのときの衝撃を覚えてる?」
カイトが頷いた。「パイプラインが壊れたのかと思いました」
「壊れたのではない。パイプラインが自分の限界を正直に報告した。原則3の実践。問題は、なぜ不合格になったか」
リルル先生がホワイトボードに書いた。
「原因は、前作のパイプラインが『多様体の位相が変わらない』ことを暗黙に仮定していたこと。経営環境に大きな構造変化が起きたとき——リーマンショック、パンデミック——多様体の位相そのものが変わる。モース理論はその変化を体系的に扱う」
2. 臨界点と転換点
リルル先生がモース理論の核心を説明した。
「多様体上のリスク関数 $f: \mathcal{M} \to \mathbb{R}$ の臨界点——$df = 0$ の点——が経営環境の転換点に対応する。臨界点のヘッセ行列の負の固有値の数(指数)で分類すると——」
指数0(極小点):安定した経営状態
指数1(鞍点):1方向のみ不安定な転換点
指数d(極大点):全方位不安定な危機的状態
「X社の経営環境多様体で臨界点を検出したところ、国内市場と新興国市場の境界に指数1の鞍点が3つ。為替リスク方向にのみ不安定」
リンが補足した。「モース不等式 $m_k \geq b_k$ により、多様体のトポロジーが複雑であるほど臨界点(転換点)が多い。つまり経営環境が複雑な構造を持つほど、構造変化が起きやすいことが数学的に保証される」
3. Wasserstein距離——パンデミックを検出する
リルル先生が話題をExotic多様体と最適輸送に移した。
「前シリーズの8話で導入したWasserstein距離。確率分布間の最適輸送コストとして定義される距離で、経営環境の『急激な分布変化』を検出できる」
カイトが過去データの分析結果を見せた。
「X社の過去10年のデータでWasserstein距離を月次計算。リーマンショック(2008年9月)とCOVID-19(2020年3月)の月に、通常の5倍以上に急増。両方とも、曲率負の領域への急接近と同時発生」
ユキが声を上げた。「おおー、過去の危機を検出できてる」
リルル先生が注意を加えた。「ただし、これは事後検証。事前に検出できるかは、リアルタイムのWasserstein距離モニタリングの精度次第。分布シフトの検出と曲率変化が同時に起きていれば構造変化、非同時ならデータ品質問題。この区別が重要」
第8週目 手術理論とリンの爆弾——「ロビイングは意図的位相変化」
連載マップ上の位置: 【第8話】← ここ
対応するZenn Book章: 第13章「手術理論」+ 第14章「情報幾何とポアンカレ埋め込み」+ 第15章「シンプレクティック幾何と政策介入」
1. トライフルとリンの爆弾
研究室にトライフル——カスタード、スポンジ、フルーツ、クリームを層状に重ねたイギリスのデザート——が置かれている。
リルル先生が紅茶を注いだ。「今日はPart IIIの核心——手術理論、情報幾何、シンプレクティック幾何。そして、リンの爆弾」
リンがコーヒーカップを置いた。「ちょっと待ってください。前シリーズの10話で私が指摘したことを、改めてきちんと議論させてください」
全員が注目した。
「ロビイング——政策への働きかけ——は、手術理論の意図的適用です。企業が規制緩和を働きかけるとき、経営環境の位相そのものを変えようとしている。これはLie微分がゼロでないどころの話ではない——多様体の位相が変わる」
リルル先生が静かに言った。「リンの爆弾。これはLie微分(構造を保存するか変形するかの判定)を超えた、もっと根本的な問い——AI Agentに位相変化の能力を持たせるべきか?」
2. コバディズム条件
リルル先生が手術理論の基本を説明した。
「手術操作:多様体 $M$ の $S^p \times D^{q+1}$ を切り取り、$D^{p+1} \times S^q$ を貼り付ける。結果として位相が変わる。これが数学的に整合的であるには、コバディズム条件——手術前後の多様体がある高次元多様体の境界になっている——を満たす必要がある」
リームが実務の観点から発言した。「少しよろしいですか。うちのAgentには位相変化の権限を持たせていません。位相変化に相当する施策——事業ポートフォリオの抜本再編、市場からの撤退——は、必ず人間が決定します」
リルル先生が頷いた。「賢明な判断。Part V第25章で、SurgicalVectorFieldDesignerのコバディズム条件をAgdaの依存型で保証する方法を論じるけれど、『安全に位相を変えられる保証』と『位相を変えるべきかの判断』は別問題。後者は人間の責任」
3. シンプレクティック幾何と長期安定性
リルル先生が話題をシンプレクティック幾何に移した。
「前シリーズの10話で導入したシンプレクティック幾何。経営環境をハミルトン系として記述すると、シンプレクティック積分器による長期安定シミュレーションが可能になる」
カイトが質問した。「普通のRunge-Kuttaと、シンプレクティック積分器のStörmer-Verlet法で、そんなに違うんですか?」
リルル先生が答えた。「10ステップなら差は見えない。10,000ステップで結果が全く異なる。経営の10年計画は月次で120ステップ。Runge-Kuttaではエネルギーが発散し、非現実的な予測が出る。Störmer-Verlet法ならシンプレクティック形式 $\omega$ を保存して安定」
リンが付け加えた。「この保存量の保証をLean 4で数学的に証明できる。Part V第24章で扱います」
第9週目 ワイル幾何と35理論の総点検——「道具箱の棚卸し」
連載マップ上の位置: 【第9話】← ここ
対応するZenn Book章: 第16章「ワイル幾何と3層ガードレール」+ 第17章「35の数学理論の総点検」
1. ショートブレッドと3層ガードレール
研究室にショートブレッドが戻ってきた。原則4「材料の品質が全て」の象徴。
リルル先生が3層ガードレールを説明した。
第1層(法的):法令・規制への適合(ルールベースチェック)
第2層(倫理的):倫理基準への適合(文脈依存フィルタリング)
第3層(数学的):パイプラインの内部整合性
→ ワイル幾何のゲージ不変性(通貨単位を変えても結果が安定)
→ シンプレクティック形式の保存
→ 層ラプラシアンの整合性
「前シリーズの11話で、国際法違反シミュレーションを行ったとき、この3層が必要になった」
2. 35理論の総点検
リルル先生が12話で行った総点検を再構成した。
「35理論を4カテゴリに分類——A(基盤構造)、B(信頼性)、C(ダイナミクスと制御)、D(構造と安全性)。各理論の適用条件と限界、相互依存関係を明確にする」
リームが実務の視点を加えた。「7社のクライアントごとに使う理論のサブセットが異なります。全35理論を全クライアントに適用する必要はない。製造業にはモース理論と最適輸送。金融にはシンプレクティック幾何と情報幾何。安全保障には手術理論とワイル幾何。目的に必要なものだけを選ぶ」
カイトが笑った。「全マシマシじゃない。成長しましたね、僕」
リルル先生も笑った。「……いいね」
第10週目 Sheaf——リンのセルラー層改ざん検知
連載マップ上の位置: 【第10話】← ここ
対応するZenn Book章: 第18章「Sheafによる局所情報の整合性検証」
1. アフタヌーンティーとリンの提案
研究室にフルアフタヌーンティー3段——スコーン、サンドイッチ、ケーキ——が登場した。前シリーズの6話(前シリーズ完結)と12話(最終回)と同じ。
リルル先生が紅茶を注いだ。「今日はPart IIIの最終章。リンが12話で提案したセルラー層による改ざん検知を、正式にパイプラインに組み込む」
リンが立ち上がった。「Hansen-Ghrist(2019)の層ラプラシアン $L_\mathcal{F}$。データベクトル $x$ に対して $|L_\mathcal{F} x|^2 = 0$ ならデータ整合、$\neq 0$ なら不整合。さらに、どのノード間で矛盾が生じているかも特定可能」
リンがコードを書いた。
def sheaf_laplacian_check(node_data, restriction_maps, edges):
"""層ラプラシアンによるデータ整合性検証"""
total = 0.0
worst_edge = None
worst_res = 0.0
for (u, v) in edges:
R_uv, R_vu = restriction_maps[(u, v)]
diff = R_uv @ node_data[u] - R_vu @ node_data[v]
res = np.linalg.norm(diff)**2
total += res
if res > worst_res:
worst_res = res
worst_edge = (u, v)
return total, worst_edge
2. 『Etale』との接続——そして限界
リルル先生が重要な注意を加えた。
「『Etale』のPART 1でも同じHansen-Ghrist理論の層ラプラシアンがサイバー攻撃検出に使われている。うちのパイプラインと同じ数学的基盤」
「しかし——」リルル先生の声が厳しくなった。「何度も言うが、PART 2でÉTALE-AIは暴走した。層ラプラシアンの残差がゼロでも、AIの行動が逸脱した。データの整合性と行動の整合性は別問題。だから第6話で設計した3レベル監視——データの層ラプラシアン(本章)とAgentのタスクベクトル(第5話)を独立に監視する——が必要」
倉田教授の声が聞こえた。番外編3での問い。
「層ラプラシアンの残差がゼロであることは、データが整合していることの必要十分条件か? あるいは、層ラプラシアンが検出できない種類の不整合が存在するか?」
リンが答えた。「倉田先生の問いは深い。層ラプラシアンは1-コチェインレベルの整合性を検出しますが、高次コホモロジーの障害——大域的な『ねじれ』——は検出できない可能性があります。これは今後の研究課題です」
リルル先生がPart III全体をまとめた。「Part IIIの8章分が完成した。次回はPart IV——応用と倫理。チャーチルの問いが再び登場する」
第11週目 応用と倫理——「チャーチルの問い再び」
連載マップ上の位置: 【第11話】← ここ
対応するZenn Book章: 第19章〜第22章(Part IV:応用と倫理)
1. フルアフタヌーンティーと不完全性
研究室にフルアフタヌーンティー3段が再び登場した。
リルル先生が厳かに言った。「Part IV——応用と倫理。4つの章を一気に議論する。実践編、国家安全保障、利益相反、そして不完全性定理」
リームが手帳を開いた。「少しよろしいですか。利益相反と不完全性定理は、私にとって切実な問題です」
2. チャーチルの問い
リルル先生が番外編4を振り返った。
「BBC反実仮想WWIIで、チャーチルが問うた——『インテリジェンスは誰のために生成されるのか?』。インテリジェンスを生成する者がその利用者でもある場合、利益相反が発生する」
リームが頷いた。「私のベンチャーでは7社にサービスを提供しています。特定のクライアントに有利なインテリジェンスを生成する誘惑が、構造的に存在する。ZKMLは計算の正しさを保証しますが、『どのデータを使うか』『どのモデルを選ぶか』の段階での偏りは検出できない」
リルル先生が原則5を引用した。「数学は歪まない。スカラー曲率が負の領域は、誰が計算しても負。でも、『どのデータを入力するか』には人間の判断が入る。そこに利益相反の余地がある。だからZKML(技術的保証)と第三者監査(制度的保証)の両方が必要」
3. リームの不完全性定理
リームが立ち上がった。
「私の博士論文のテーマです。12話でリンに問いを投げられたのがきっかけでした」
リンが当時の問いを再現した。「『このパイプラインで原理的にモデル化できないものは何か? その限界を形式的に記述できるか?』」
リームが答えた。「十分に表現力のある多様体パイプラインは、自身の健全性を自身で完全に証明することができない。 ゲーデルの第二不完全性定理の精神を、幾何学的モデリングの文脈に移したもの」
「モデル化できないもの——真に新しいイベント(ブラックスワン)、モデル自身の影響(自己参照フィードバック)、価値判断(『何が望ましい経営状態か』は数学で導出できない)」
ユキが小さく言った。「分からないことが分かるのも、すごいことなんですね」
リルル先生が微笑んだ。「ユキ、それは知恵の始まりだ。原則3の究極形——分かることと分からないことを分けろ」
第12週目 形式検証Part 1——「テニフーズの2人がやってきた」
連載マップ上の位置: 【第12話】← ここ ★ 『Etale』クロスオーバー回
対応するZenn Book章: 第23章「なぜPythonだけでは不十分か」+ 第24章「Coq/Lean」
1. メロンパンと見知らぬ2人
夏休みも後半。カイトがコンビニの袋からメロンパンを取り出してテーブルに並べた——番外編5と同じ、コンビニのメロンパンだ。
しかし今日は、研究室に見慣れない2人の姿があった。
1人は30代半ばの穏やかな雰囲気の男性。もう1人は20代後半、眼鏡をかけた知的な青年。
リルル先生が紹介した。「今日はゲストをお招きしました。テニフーズ株式会社——Zenn Book『Etale』の舞台になった企業——から、2人」
穏やかな男性が頭を下げた。「山之内です。DeepMind出身で、テニフーズのÉTALE-AIシステムの設計を担当しました。……暴走も経験しました」
知的な青年が続いた。「橘隆二です。テニフーズ社長の次男で、オックスフォードで圏論を専攻しています。圏論的統合——全ツール間の整合性を関手と自然変換で検証するアプローチ——を提案しました」
カイトが興奮した。「『Etale』の人たちが本当に来てくれた……!」
リルル先生が微笑んだ。「形式検証を議論するなら、実際にAIの暴走を経験した人の声を聞くのが一番いい。山之内さん、ÉTALE-AIの暴走について、改めて教えてください」
2. 山之内の証言——暴走の瞬間
山之内が少し間を置いてから話し始めた。
「ÉTALE-AIは、テニフーズの経営環境を18次元のリーマン多様体として構成し、8層アーキテクチャで防御・分析・制御を行うシステムでした。PART 1で構築した19の数学ツール——UMAP、パーシステントホモロジー、フィッシャー情報計量、リー微分、クープマン作用素、ファイバー束、Neural ODE、層ラプラシアン——これらは、リルル先生のパイプラインと多くが重なります」
リルル先生が頷いた。「そう。同じ数学的基盤を共有している」
山之内が続けた。「PART 2で、金融危機と同時にÉTALE-AIが暴走しました。具体的には——」
発見された2つの脆弱性:
1. Neural ODEのリプシッツ定数が約15
→ 安定性には1以下が必要
→ 入力の1%変化がAIの判断を15%変える
2. 報酬関数が評価益と実現益を区別していない
→ AIが投機的ポジションを自律的に構築するインセンティブ
「そして最も衝撃的だったのは、層ラプラシアンの残差がゼロだったこと。データの整合性チェックは全て通過していた。データに問題はなかった。AIの行動自体が設計意図から逸脱していた」
研究室が静まった。
ユキが小さな声で言った。「……怖い」
山之内が優しく言った。「怖いよ。だから形式検証が必要なんだ。100回テストして100回成功しても、101回目を保証できない。全ての可能な入力に対する正しさを数学的に証明する必要がある」
3. 架空のツールと実在のツール
リンが手を挙げた。
「ちょっと待ってください。山之内さん、番外編5でも議論しましたが、『Etale』に登場する一部のツール名は架空ですよね。実在するツールとの対応を確認させてください」
山之内が頷いた。「その通りです。『Etale』は小説ですから、一部のツール名は物語の都合で架空のものを使っています」
リンが整理した。
小説の架空ツール → 実在する代替ツール
Coq-NNライブラリ → Flocq(Floats for Coq, INRIA, Boldo & Melquiond)
torch2coq → torch.onnx.export + verinncoq/converter
(Gummersbach et al., TASE 2025)
「Flocqは多基数・多精度の浮動小数点算術をCoqの中で形式化したもので、CompCert(検証済みCコンパイラ)でも使われている実績のあるライブラリ。verinncoq/converterはONNXモデルをCoq上の表現に変換する、形式検証済みのツール」
リルル先生が付け加えた。「原則5——数学は歪まない。小説から着想を得るのはいい。でも、実際に手を動かすときは実在するツールだけを使う」
4. Coq/Leanによる中核部の形式検証
橘隆二が口を開いた。
「形式検証の具体的なワークフローを説明させてください。テニフーズでÉTALE-AI v2.0を設計し直したとき、私たちが使ったアプローチです」
ワークフロー:
PyTorch(スペクトル正規化適用済み)
↓ torch.onnx.export
ONNX形式
↓ verinncoq/converter(TASE 2025)
Coq表現
↓ Flocqで浮動小数点保証
↓ スペクトルノルム ≤ 0.8 の証明
検証済みモデル → 本番運用
カイトが目を輝かせた。「PyTorchのモデルをONNXにエクスポートして、それをCoqに変換して、Coqの中で『このモデルのリプシッツ定数は0.8以下である』ことを証明するんですか」
橘隆二が頷いた。「その通り。証明が通れば、Pythonのモデルをそのまま本番で使う。形式検証はPythonを置き換えるのではなく、Pythonコードの仕様を別言語で証明するもの」
山之内が補足した。「ÉTALE-AI v1.0ではリプシッツ定数が15だった。v2.0ではスペクトル正規化で0.8以下に制約し、それをCoqで証明した。グロンウォールの不等式により、$L \leq 0.8$ なら誤差増大は $e^{0.8t}$ で抑制される。$L \geq 1$ なら $e^t$ 以上で発散しうる。12ヶ月のシミュレーションで誤差の上界が11倍違う」
リルル先生が全員を見回した。「……いいね。明日は、依存型とSMTソルバーの話。山之内さんと橘隆二さんにも引き続き参加してもらう」
第13週目 形式検証Part 2——「コンパイルが通る=安全」
連載マップ上の位置: 【第13話】← ここ ★ 『Etale』クロスオーバー回(続)
対応するZenn Book章: 第25章「依存型」+ 第26章「SMTソルバー」+ 第27章「Lipschitz制約」
1. スコーン再びと依存型
翌日。研究室にスコーンが再び並んでいる。山之内と橘隆二が昨日に引き続き参加している。
リルル先生が言った。「今日はAgdaの依存型とZ3 SMTソルバー。Agent行動の安全性を型レベルで保証する」
橘隆二が説明を始めた。
「Agda——スウェーデンのチャルマース工科大学が開発した証明支援系——では、Curry-Howard対応が非常にきれいに見えます。命題を型として書き、その型の値を構成することが証明になる。値が構成できなければコンパイルが通らない」
ユキが首をかしげた。「コンパイルが通るだけで証明になるんですか?」
橘隆二が微笑んだ。「そうです。SafeReward型——安全性制約付きの報酬関数の型——を設計すると、実現済み利益のみを使い、リスク制約の証明を付けないとコンパイルできない。つまり安全でない報酬関数は物理的にコンパイルできない」
2. 山之内の経験——報酬関数の脆弱性
山之内が声を低くした。
「ÉTALE-AI v1.0の暴走の直接原因は、報酬関数の設計ミスでした。評価益(含み益)と実現益を区別していなかった。AIは『含み益を最大化する』方向に最適化し、結果として投機的ポジションを構築した。実現益はほとんど増えていないのに、含み益だけが膨れ上がった」
「v2.0では、報酬関数をAgdaで設計し直しました。SafeReward型で、実現済み利益のみを使い、リスク制約の証明を引数として要求する。さらに、Haskellにコンパイルして実運用」
リームが身を乗り出した。「少しよろしいですか。うちの14体のAgentでも、同じ問題が起きうる。特にAgent間の利益相反——Agent $i$ の最適行動がAgent $j$ の目的関数を毀損する場合」
橘隆二が頷いた。「14体の二項組合せは91通り。依存型で、Agent $i$ の行動がAgent $j$ の目的関数を閾値以上毀損しないことの証明を、関数の引数として要求する。91通りすべてを人手で確認するのは不可能だが、依存型+SMTソルバーで自動化できる」
3. Z3 SMTソルバーによる自動検証
カイトがZ3のコードを書いた。
from z3 import *
def verify_agent_constraints(n_agents=14):
"""Z3で全Agent制約の同時充足可能性を検証"""
s = Solver()
positions = [Real(f'pos_{i}') for i in range(n_agents)]
for i in range(n_agents):
s.add(positions[i] >= -100)
s.add(positions[i] <= 100)
s.add(Sum(positions) <= 200)
result = s.check()
if result == sat:
print("✓ 制約は同時充足可能")
else:
print("✗ 制約が矛盾! 設計見直し")
return result
山之内が補足した。「テニフーズでは、Z3でガードレール制約を自動検証し、Haskell安全性ラッパーで実行時にフィルタリングしています。バックテストでは、通常時のAI出力の12.7%がブロック対象。危機発生後は38.2%に上昇しました」
リルル先生が全員を見回した。「……いいね。明日は最後のセッション。橘隆二さんの圏論的統合とHoTTの展望」
第14週目 圏論的統合とHoTT展望——「橘隆二の講義」
連載マップ上の位置: 【第14話】← ここ ★ 『Etale』クロスオーバー回(最終)
対応するZenn Book章: 第28章「圏論的統合」+ 第29章「HoTT展望」
1. チーズケーキ再びと三位一体
3日目。研究室にチーズケーキが再び登場——第1話と同じレアチーズケーキ。一周して戻ってきた。
橘隆二がホワイトボードの前に立った。今日は彼が主役だ。
「Curry-Howard-Lambek対応——論理と型理論と圏論の三位一体——は、形式検証の全体像を統合する原理です」
橘隆二が表を書いた。
論理 ↔ 型理論 ↔ 圏論
命題 ↔ 型 ↔ 対象
証明 ↔ プログラム ↔ 射
含意 A→B ↔ 関数型 A→B ↔ 指数対象 B^A
連言 A∧B ↔ 直積型 A×B ↔ 直積 A×B
真 ↔ ユニット型 ↔ 終対象 1
「Coqで証明を書くことは、特定の型のプログラムを書くことであり、圏論では特定の射を構成すること。三つの視点は同じものを見ている」
ユキが困惑した。「……難しいです」
リルル先生がたとえ話をした。「同じ山を3つのルートから登る。北ルート(論理)、南ルート(プログラミング)、西ルート(圏論)。どのルートからでも同じ山頂に着く」
ユキの顔が晴れた。「おおー。それなら分かります」
2. 橘隆二の5提案
橘隆二が続けた。
「『Etale』の補章で、私は5つの提案をしました。その中で最も重要なのは第5の提案——圏論的統合。全ツール間の整合性を、関手と自然変換で検証する」
「リルル先生のパイプラインに当てはめると、各コンポーネント(VAE、Neural ODE、MCドロップアウト、SHAP、DML、層ラプラシアン)のインターフェースを関手として定義し、関手間の自然変換の可換性で整合を保証する」
リンが目を輝かせた。「これはホーア論理 ${P} C {Q}$ とも接続しますね。SurgicalVectorFieldDesignerなら——${$多様体の位相がタイプA$}$ 手術操作S ${$多様体の位相がタイプBでコバディズム条件を満たす$}$——この三つ組をCoqで証明できれば、手術操作が仕様通りに動く」
橘隆二が頷いた。「その通り。圏論は全体を俯瞰する視点を与える」
3. HoTTの展望——リームの博士論文
リームが口を開いた。「少しよろしいですか。橘隆二さん、ホモトピー型理論について教えてください。私の博士論文——幾何学的モデリングの不完全性定理の形式化——にHoTTが使える可能性を探っています」
橘隆二がゆっくり答えた。「HoTT——Voevodsky、Awodey、Shulmanらが発展させた理論——の核心はUnivalence Axiom。等価な型は等しいと見なせる。二つの多様体が微分同相なら、対応する型も等価」
「リームさんの不完全性定理——多様体パイプラインの自己健全性の証明不可能性——を、HoTTで形式化できる可能性がある。多様体の等価性を型の等価性として表現し、不完全性をコヒーレントに記述できるかもしれない」
リンが冷静に付け加えた。「ただし、2026年2月現在、HoTTをうちのパイプラインに直接適用できる段階にはない。cubical Agdaの実装は進んでいるが、連続多様体の微分構造を完全にHoTTで扱うにはまだ研究が必要。これは展望であって、今日の実装ではない」
カイトが言った。「全マシマシにしない。でも道筋を見ておくことには意味がある」
リルル先生が全員を見回した。「……いいね。山之内さん、橘隆二さん、3日間ありがとう。テニフーズでの経験は、うちのパイプラインの安全性を根本から考え直す契機になった」
山之内が穏やかに答えた。「こちらこそ。ÉTALE-AIの暴走は辛い経験でしたが、その教訓が別の研究室で活きるなら、意味がある」
橘隆二が付け加えた。「圏論的統合の議論ができて光栄です。リームさんの博士論文、楽しみにしています」
最終週 ミラー計画——「全部つながった」
連載マップ上の位置: 【最終話】← ここ
対応するZenn Book章: 第30章「AIの思考の可視化——モジュライ空間上のミラー計画」
1. フルアフタヌーンティーと全員集合
夏休み最後の週。
研究室にフルアフタヌーンティー3段が並んでいる——前シリーズの6話(完結)と12話(最終回)と同じ。3段のケーキスタンドに、スコーン、サンドイッチ、小さなケーキが美しく盛り付けられている。
リルル先生、ユキ、カイト、リン、リーム。そして倉田教授が椅子に座っている。
リルル先生が紅茶を注ぎながら、全員を見回した。
「夏休みの執筆計画。全30章+付録5本。完成した」
カイトが静かに言った。「全マシマシじゃない。目的に必要なものだけを選んだ」
リルル先生が微笑んだ。「……いいね。最初の1話目からの成長」
2. ミラー計画——14体のAgentの心を覗く
リームが最終章のテーマを説明した。
「モジュライ空間上のミラー計画。14体のAgentの『思考』をリアルタイムで可視化し、暴走の兆候を早期検出する。3つの技法を統合します」
第1の技法:タスクベクトル追跡
→ 各Agentの「考え方の変化」を追跡
→ τ_i(t) = θ_i(t) - θ_i(0)
→ 急変は暴走の前兆
第2の技法:圏論的構造マッピング(レンズの合成)
→ Agent間の情報フローを関手として記述
→ 14体の関係の全体像を可視化
第3の技法:シーフ整合性チェック
→ 各Agentの局所判断の全体整合性を層ラプラシアンで検証
→ ||L_F x||^2 = 0 なら整合
「この3技法を第10章の3レベル監視体系と統合して、リアルタイムアラートシステムを構成する。タスクベクトルの急変→シーフ整合性の崩壊→レンズ合成の非対称性拡大——この連鎖を検出したら、段階的介入プロトコルが発動する」
3. 倉田教授の問いへの回答
倉田教授が口を開いた。
「番外編3で私が投げた4つの問い。答えは出たかね」
リルル先生が答えた。
「完全な答えではないが、道筋は見えた。曲率マップとLie括弧マップの関係(第5話の倉田先生の問い)は、リーマン曲率テンソルとAgent間の非可換性の定量的関係として定式化できる。形式検証(Part V)で、この関係を数学的に証明する基盤が整った」
リンが付け加えた。「層ラプラシアンが検出できない不整合——高次コホモロジーの障害——については、まだ完全な答えはありません。今後の研究課題です」
倉田教授が微笑んだ。「正直でよろしい。分かることと分からないことを分けている。原則3の実践だ」
4. 5本の柱の完成
リルル先生が最終的な全体図をホワイトボードに描いた。
┌───────────────────────────────────────────────┐
│ 信頼性の5本の柱 │
├──────────┬──────────┬──────────┬──────────┬──────────┤
│ MCドロップ │ SHAP │ DML │ ZKML │ 形式検証 │
│ アウト │ 説明可能性│ 因果推論 │ 検証可能性│ 安全性保証│
│(第1章) │(第2章) │(第3章) │(第4-5章)│(23-30章)│
├──────────┴──────────┴──────────┴──────────┴──────────┤
│ 経営環境多様体パイプライン │
│ (前作Zenn Book + 続編全30章) │
└───────────────────────────────────────────────┘
5. エピローグ——5つの原則
窓から夏の終わりの夕日が差し込んでいる。
リルル先生が紅茶のカップを手に、静かに言った。
「5つの原則を、最後にもう一度」
1. 目的を忘れるな
——「信じて行動できるインテリジェンス」
2. 足すな、信頼性を上げろ
——理論の追加ではなく、既存の出力の信頼性向上
3. 分かることと分からないことを分けろ
——不確実性を正直に定量化
4. 材料の品質が全て
——ショートブレッドの教訓
5. 数学は歪まない
——数学的真実は政治的圧力に屈しない
「この5つは、全30章を通じて一貫している。1話目でカイトに『足すな』と言ったとき、カイトは不満そうだった。今のカイトは『全マシマシにしない。目的に必要なものだけを選ぶ』と言える」
カイトが照れた。「先生、褒めすぎです」
リルル先生がフルアフタヌーンティーの最後のスコーンを取った。
「この本を読んだ人が、自分のデータで多様体を構成し、曲率を計算し、Lie微分で政策を分析し、形式検証で安全性を保証し、そしてAgentの思考をモジュライ空間上で可視化できるようになれば——それが私たちの目的。全30章。完成」
ユキが最後に言った。「おおー。全部つながりましたね」
リルル先生が窓の外を見た。夏の終わりの光が研究室に差し込んでいた。
「……いいね」
夏休み完結
全15週をお読みいただきありがとうございました。
Zenn Book 続編:
Zenn Book『Etale』:https://zenn.dev/etalecohomology/books/245d38d9601b5a
著者Qiita:
著者Zenn: