AI物流の実装地を、Lean 4で形式的に選んだ話——恣意性を排除してなお広島が残った理由
- kanna qed
- 2 日前
- 読了時間: 6分
はじめに
先日、株式会社オンザリンクスとGhostDrift数理研究所の共同特許出願に関するプレスリリースを出しました。
https://prtimes.jp/main/html/rd/p/000000011.000169775.html プレスリリースの主役は共同特許——AI物流の現場における判断を「会社として責任を持って採用できる状態」で記録・検証するシステムです。
しかしGhostDrift側が今回大きく関わったもう一つの仕事があります。
「なぜ広島か」を形式的に示すこと。
実装地の選定にあたり、GhostDriftはLean 4（定理証明支援系）を使った形式化をGitHubに公開しています。
この記事は、その中身の解説です。なぜ形式化したのか、何を証明したのか、そして恣意性を極力排除してなお広島が残った理由を、できるだけ平易に説明します。
なぜ形式化したのか
AI物流の実装地を選ぶとき、通常は「縁があった」「拠点がある」「話が進みやすかった」で決まります。それ自体は悪いことではありませんが、外から見ると恣意的に見えます。
私たちが避けたかったのはまさにそこでした。
広島発でAI物流アシュアランスを実装するという構想は当初からありました。しかしその構想を「広島ありき」ではなく、「条件ありきで調べた結果として広島が残った」という形で示したかった。
そのために取った手順がこれです。
国際規格から評価条件を先に固定する
国内主要10都市圏を同じ基準で調べる
結果を形式化してGitHubに公開する
Lean 4を使ったのは、「誰でも検証できる形で公開する」ためです。特定企業の主張ではなく、コードとして公開されていて、GitHub Actions上でLean型チェッカーが通っている。反論したければコードに対して反論できます。
評価条件をどう設計したか
条件は2層で設計しました。
第1層：スクリーニング条件（物理・インフラ）
AI物流の実験場として最低限必要な条件です。ASAM OpenODD・EU AI Act・NIST AI RMF・ISO 42001の4規格から導出しました。
港湾・物流基盤があること
製造サプライチェーンのアンカーが港に連続していること
都市人流との交差があること（人間監視の設計検証のため）
ODD（運行設計領域）を切り出せること
ログ取得点が存在すること
人間監視経路を設計できること
責任回廊が追加設計なしで現時点で閉じていること
都市規模が過大でないこと
最後から2番目の「責任回廊が閉じている」がポイントです。これはLeanではClosedODDCorridorとしてdefで定義しました。opaqueにしなかったのは、「閉じている」の根拠を以下の4条件に還元して監査可能にするためです。
HasBoundaryDefinition：回廊の境界を記述できる
HasLoggingPoints：ログ取得点が存在する
HasInterventionPath：人間介入経路を設計できる
HasResponsibleActorsEnumerated：責任主体を列挙できる
また「閉じている」は「追加設計があれば閉じられる（DesignWork）」ではなく「現時点で閉じている」を要件としました。これは初期実装比較として事前登録した判断です。都市を見た後に変更していません。
第2層：制度統合条件（ガバナンス）
物理条件をクリアした都市が、AI物流アシュアランスの実証を制度として支えられるかを見ます。LeanではFullInstitutionalSandboxMatchとして定義しました。
AI物流アシュアランス実証に特化した制度焦点があること
AI開発者と地域課題のマッチング機能があること
課題が公開リストになっていること
地域内実証が制度的に要件化されていること
公的な実装支援があること
行政横断の調整層があること
10都市を比べた結果
国内主要10都市圏を同一の調査テンプレートで調べました。
スクリーニング条件の結果
東京・大阪・横浜川崎：都市規模が大きく、最初の実装エリアを絞り込むことが難しい（TooLargeForODDClosure）
名古屋：主要コンテナターミナルが飛島村側にあり、複数自治体にまたがる構造（OverComplexForInitialODD）
福岡北九州：博多港・北九州港の二港湾・二管理者体制で責任回廊の構成が複雑（OverComplexForInitialODD）
神戸・仙台・新潟：責任回廊を閉じるための追加設計が必要な状態（CorridorRequiresDesignWork）
広島・岡山：通過
制度統合条件の結果
岡山：GovTech Challenge OKAYAMAなど実証制度はあるが、AI物流アシュアランスに特化した制度焦点は一次資料上で確認できず
他8都市：同様に第1要件が未確認
広島のみ：通過
ひろしまAIサンドボックスが6要件すべてを満たしていました。
Leanで何を証明したか
上記の調査結果を、Lean 4で3つの定理として形式化しました。
定理1：screening_narrows_to_two
theorem screening_narrows_to_two :
∀ c : SurveyCity, PassesScreen c →
c = SurveyCity.Hiroshima ∨ c = SurveyCity.Okayama
スクリーニング条件を満たすのは広島・岡山の2都市のみ。10都市を全列挙してcase分析しています。
定理2：hiroshima_unique_full_institutional_sandbox
theorem hiroshima_unique_full_institutional_sandbox :
∀ c : SurveyCity, FullInstitutionalSandboxMatch c →
c = SurveyCity.Hiroshima
制度統合条件を満たすのは広島のみ。
ここで一点正直に書いておきます。FullInstitutionalSandboxMatchは6要件の連言ですが、この定理の証明では第1要件（HasAISpecificFocus）の否定だけで各都市を排除しています。残り5要件が各都市で満たされているかどうかは、形式的には証明していません。
これは設計上の意図的な選択です。連言の一つが偽なら全体が偽になるため、論理的には正しい。残り5要件の確認はEvidenceReportに委ねており、コード上のコメントにもその旨を明記しています。
定理3：hiroshima_uniquely_satisfies_all_conditions
theorem hiroshima_uniquely_satisfies_all_conditions :
∀ c : SurveyCity,
PassesScreen c →
FullInstitutionalSandboxMatch c →
c = SurveyCity.Hiroshima
両条件を同時に満たすのは広島のみ。定理1と定理2を実際に呼び出して証明しています。定理1で岡山を候補に残し、定理2で岡山を制度条件で排除する、という2段構えの構造です。
これらはGitHub Actions上でLean型チェッカーが検証しており、現時点でCIが通っています。
形式化の意味と限界
この形式化が証明しているのは「これらの公理を認めれば、定理が成立する」ということです。公理そのものが正しいかどうかは、Leanでは証明できません。
たとえばhiroshima_ai_specific（広島がAI特化制度を持つ）という公理は、ひろしまAIサンドボックスの一次資料に基づいています。その根拠はEvidenceReportに全部書いてあります。公理と根拠が対応しているかは、人間が確認するしかない。
形式化の価値は「証明した」ことではなく、「何を仮定しているかを全部見せた」 ことにあります。仮定に異議があればコードに対して反論できる。それが透明性です。
恣意性を排除してなお広島が残った
調査を始める前から広島発でやるという構想はありました。それでも条件を先に固定して10都市を同じ基準で調べた理由は、「広島ありきだった」という批判を避けるためだけではなく、自分たちの判断を自分たちで検証するためです。
結果として広島が残りました。それは構想の正しさを証明するものではありませんが、「条件を変えずに調べてもそうなった」という根拠になります。
この根拠があるからこそ、広島発でAI物流アシュアランスを実装することに確信を持って進めることができます。
おわりに
今回の形式化はあくまで出発点です。
HasClosedResponsibilityCorridor（現場の責任回廊設計）やSupportsAssuranceLoggingExperiment（実証ログ基盤）はまだ未実装で、OpenODD形式ファイルの作成も残っています。
次のステップは実装です。物流判断パケットシステムをYUKAIに載せ、広島の港湾・製造・人流の回廊で動かす。広島AIアシュアランス協議会の立ち上げとも連動させながら進めていきます。
コメント