ADICとは何か？ Lean 4形式検証とRed-Team監査で検証するAI監査フレームワーク

Posted at 2026-03-12

AIや予測モデルを実運用に載せるとき、本当に必要なのは「当たるかどうか」だけではありません。

どの条件で実行されたのか
どの入力に対してその結論が出たのか
後から閾値や設定が都合よく変えられていないか
第三者が同じ結論を再現できるか

この問題に対して、GhostDrift数理研究所が公開しているのが ADIC です。

ADICは、単なる予測やスコア出力の仕組みではありません。計算の正当性・再現性・改変耐性を、証明書と台帳として固定するための検証可能計算フレームワークです。

本記事では、公開中の2つの実装資産をもとに、ADICの技術的な意味を整理します。

Red-Teamテストを含む監査実装
https://github.com/GhostDriftTheory/ghostdrift-adic-audit-JP
Lean 4 による形式検証アーティファクト
https://ghostdrifttheory.github.io/adic-lean-proof/

ADICは「あとから言い逃れできない計算」を作るための枠組み

多くのAIシステムは、モデル性能や推論精度の議論には強くても、運用時に何が固定され、何が後付けで変えられ得るかという点が曖昧なままです。

ADICが狙っているのはそこです。

ADICでは、計算結果だけでなく、以下をまとめて固定します。

split や threshold などの判定条件
入力データの同定情報
実行コード
実行環境
判定理由
再検証用エビデンス

つまりADICは、「計算した」ではなく「この条件で計算し、この理由でこの判定に至った」を第三者が追試できる形で残すための技術です。

公開リポジトリは「時系列予測のドリフト監査」を題材にしている

公開されている ghostdrift-adic-audit-JP は、運用中の時系列予測に対して、ドリフト（分布変化 / regime shift）を再現可能な監査プロトコルとして固定する実装です。

設計のポイントは明確です。

Calibration期だけで基準を決める
Test期は評価のみに使う
結果を見た後で閾値調整しない
証明書・台帳・時系列エビデンスをまとめて出力する

この構造により、後から都合よく基準を動かす行為を構造的に排除する方向に設計されています。

実装上は、監査実行後に少なくとも次のような成果物が出力されます。

certificate.json
ledger.csv
evidence_timeseries.csv

これにより、「判定が出た」だけで終わらず、その判定を第三者が追跡・検証できる形になります。

Red-Teamテストが入っている意味

このリポジトリの重要な点は、単に監査を実行するだけでなく、Red-Team観点の検証スクリプトが用意されていることです。

公開されている redteam_adic_integrity_suite_JP.py では、攻撃面が大きく2層に分けられています。

Layer-A: 指紋の改ざん

ここでは、ファイル・設定・コード・環境に対してハッシュ指紋を取り、改変の痕跡を残す方向で設計されています。

具体的には、次のような要素が固定対象です。

設定JSONのフィンガープリント
実行コードのSHA
実行環境の情報
依存関係のハッシュ
evidenceファイル自体のSHA

つまり、**「結果だけ同じに見せる」「証拠ごと差し替える」**といった操作に対して、痕跡が残る構造になっています。

Layer-B: 意味論的な攻撃

もう一段重要なのがこちらです。

単なるファイル改ざんだけでなく、意味的には危険なのに見かけ上は通してしまう攻撃を検知対象に入れています。

スクリプト内では、たとえば次のような観点が見えます。

必須列の欠落
欠損率の異常増加
行数の極端な削減
数値トークン差分の評価
円環シフトの検知
データ契約違反の検知

ここが重要です。

AIやデータシステムでは、壊れ方は「ファイルが書き換わった」だけではありません。列が欠けた、意味が変わった、前提が崩れた、比較基準がズレたという壊れ方のほうが現実には厄介です。

ADICのRed-Teamテストは、この意味論レベルの破綻まで検査対象に含めています。

ADICは「Integrity」と「Semantics」を分けている

Red-Teamスクリプトの説明には、Integrity & Semantics の2段階 Verify という発想が入っています。

これはかなり大事です。

多くの検証は、

ファイルが壊れていない
ハッシュが一致した
スキーマが合っている

といった Integrity に偏りがちです。

しかし現実には、それだけでは足りません。

データの意味が変質していないか
本来の比較条件が崩れていないか
安全判断の前提が失われていないか

という Semantics の検証が必要です。

ADICは、ここを切り分けて扱おうとしている点が強いです。

つまり、「壊れていない」ではなく「誠実に同じ意味を保っているか」まで問う設計になっています。

Lean 4形式検証が入っている意味

さらにADICでは、中核補題について Lean 4 による形式検証アーティファクト が公開されています。

公開ページでは、ADICの中核補題が Lean 4 で形式検証されていること、そして ADIC_RSound.lean がその証明ファイルであることが示されています。

これは何を意味するのか。

端的に言えば、**「理論の核が人間の説明だけでなく、機械検証可能な形で外部化されている」**ということです。

普通、AI安全や監査の話は、概念説明で終わりがちです。

こういう思想です
こういう原則です
こういう監査が必要です

しかしそれだけでは、理論の核心が本当に成立しているのかは外から見えません。

Lean 4 の形式検証を置くことで、少なくとも中核補題の一部については、人間の文章ではなく proof assistant がチェック可能な形になっています。

これは「監査を語る側が、自分たちの理論核も外部検証にさらしている」という意味で重いです。

実装と形式検証が両方あることの価値

ADICの面白いところは、

片方で Lean 4 による理論核の機械検証があり
片方で Red-Team付き監査エンジンの実装が公開されている

という 理論と運用の両輪になっている点です。

形式検証だけでは、現実の運用攻撃には弱いことがあります。

逆に、実装テストだけでは、理論核が曖昧なままになることがあります。

ADICはこの中間を狙っています。

理論側では、機械検証可能な補題を置く
実装側では、証明書・台帳・エビデンスを出す
攻撃側では、Red-Teamで改変や意味論攻撃を試す

この三層構造によって、「安全そうに見える」ではなく「検証可能で、攻撃可能性も見に行っている」技術として出せるわけです。

ADICが向いている領域

この設計は、特に次のような領域と相性が良いです。

AI監査
モデル運用監視
ドリフト検知
品質保証
異常検知
監査証跡が必要な予測運用
後付け調整を嫌う規制産業

たとえば医療、製造、物流、エネルギー、品質管理のように、「あとから説明できる」だけでは足りず、「あとから変えていない」ことまで重要な領域では特に意味があります。

ADICは「精度向上ツール」ではなく「責任固定のための技術」

ここは誤解されやすい点です。

ADICは、予測精度を直接上げること自体を主目的とするツールではありません。

むしろ焦点は、

どういう条件で判定したか
何が破綻したときにNGとするか
その根拠をどう残すか
第三者が再検証できるか

にあります。

つまりADICは、最適化技術というより、責任境界を固定するための検証技術です。

この意味で、近年のAIガバナンス、AI安全性、AI説明責任の議論と非常に相性が良いです。

まとめ

ADICは、単なる監査ログ生成ツールではありません。

証明書を出す
台帳を残す
エビデンスを固定する
改変を検知する
意味論レベルの破綻も見る
中核補題を Lean 4 で形式検証する

という構造を通じて、「AIや計算の責任をあとから蒸発させない」ための基盤を作ろうとしています。

実際に公開されている資産を見ると、ADICは

理論を語るだけで終わらない
実装を置くだけで終わらない
攻撃を想定した検証まで入れている

という点で、かなり珍しい位置にあります。

AIシステムに必要なのが、単なる高性能ではなく、再現可能性・改変耐性・責任固定であるなら、ADICはそのための一つの具体的な技術回答になっています。

English Title

What Is ADIC? An AI Audit Framework Verified with Lean 4 Formalization and Red-Team Testing

English Summery

ADIC is a verifiable computation and audit framework designed to prevent post-hoc responsibility evaporation in AI and data-driven systems. It combines certificate and ledger generation, reproducible evidence, Lean 4 formalization of core lemmas, and Red-Team testing against integrity and semantic failure modes. Rather than optimizing only for performance, ADIC fixes the conditions, evidence, and verification path of a decision so that third parties can inspect, reproduce, and challenge it.

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up