top of page
検索

AIガバナンスを「再実行可能な証拠」にする――ADIC Lean 4 アーティファクトの公開

AIガバナンスで本当に難しいのは、「説明すること」ではなく、「あとから動かせない証拠として検証できること」です。

今回、GhostDrift数理研究所は、ADIC replay verification の中核理論を Lean 4 で形式化し、GitHub 上で第三者が再実行できるアーティファクトとして公開しました。

これは、単に「Leanで証明を書いた」という話ではありません。

GitHub から取得し、同じ手順で lake build を実行することで、ADIC certificate の replay verifier acceptance から semantic validity が従う、という中核構造を機械的に検証できる形にしたものです。



何を公開したのか

本アーティファクトは、ADIC certificate の replay verification に関する Lean 4 形式化です。中心となるファイルは以下に集約されています。

ADIC_RSound_Replay.lean

このアーティファクトは、ADICにおける certificate rows、spec rows、replay verification、semantic validity（意味論的妥当性）、そして acceptance soundness（受理の健全性）の関係を厳密に形式化したものです。

証明の方向性は、高レベルにおいて以下のように定式化されます。

ADIC certificate が replay verifier に受理される（Acceptance） $\Longrightarrow$ 対応する意味論的妥当性条件（Semantic Validity）が従う

以前の版から何が拡張されたのか

以前のバージョンの Lean アーティファクトが各プリミティブの R-SOUND を中心としていたのに対し、今回の版では replay ledger と DAG certificate までを含み、ADIC replay verification の中核理論を end-to-end に近い形で形式化しています。

観点

以前の版

今回の版

中心対象

各プリミティブの R-SOUND

replay verification 全体

主な範囲

interval arithmetic / local soundness

program replay / spec replay / replay ledger

証明の粒度

演算ごとの局所的健全性

verifier acceptance から semantic validity への構造的健全性

到達点

primitive-level soundness

end-to-end soundness に近い verifier closure

これは、単に個別の演算ルールの妥当性を検証する段階から、「ADIC certificate が replay verifier に受理されたとき、対応する意味論的条件がシステム全体として従う」という、全体構造の閉包性（Verifier Closure）を Lean 4 上で扱う構成へと移行したことを意味します。


「Leanで証明した」こと以上の意味：再実行可能性

本公開において最も重要な観測結果は、単に「Leanで証明を記述した」という事実ではありません。

第三者が GitHub からリポジトリを取得し、同一の手順で Lean 検証を機械的に再実行（Machine-checked）できる構造を確立した点にあります。

git clone [https://github.com/GhostDriftTheory/adic-lean-proof-replay.git](https://github.com/GhostDriftTheory/adic-lean-proof-replay.git)
cd adic-lean-proof-replay
lake exe cache get
lake build

すなわち、これは「特定の環境で通った証明」ではなく、「第三者が再実行し検証可能な証明資産（証拠）」としての外部固定です。


ADICが目指す「証拠連鎖」の検証

ADIC が目的とするのは、単なる実行ログの保存ではありません。

  • どの条件を満たしたから通過したのか

  • どの証拠に基づいて判断されたのか

  • その判断を第三者が検証できるのか

これらを「証拠連鎖」として扱うことです。今回のアーティファクトは、その思想と数理的構造を Lean 4 上で再実行可能な形に還元したものです。

AIの判断根拠を、ブラックボックスや事後的な説明のまま放置するのではなく、数学的に検証された正当性へと移行させる。ADICはそのための基盤となるアーキテクチャです。


結論：責任工学への移行

今回の公開は、ADIC が「AI判断の責任を、自然言語の説明ではなく、第三者が再実行できる証拠構造として扱う」方向へ進んでいることを示す、具体的な形式証明アーティファクトです。

AIガバナンスを理念やチェックリストに閉じず、検証可能な責任構造として設計する。

GhostDrift数理研究所では、この方向を「責任工学」として進めています。

 
 
 

コメント

bottom of page