AIの監査、「信じてください」から「数学的に確認できます」へ--GhostDrift、ADICの形式証明を公開 - PR TIMES|RBB TODAY
※本サイトはアフィリエイト広告を利用しています

AIの監査、「信じてください」から「数学的に確認できます」へ--GhostDrift、ADICの形式証明を公開

数学の定理証明にも使われるLean 4により第三者が再実行可能な証明を実現、EU AI Act施行前に日本発技術がAIガバナンスの新たな実装モデルを提示




「AIが何をしたかの証拠」を、後から誰でも同じ手順で再現・確認できる形で保存する--EU AI Actが求める第三者検証可能なAIガバナンス基盤です。

GhostDrift数理研究所は、AI判断を第三者が再実行・検証できる証拠として残す技術「ADIC(Advanced Data Integrity by Ledger of Computation)」の中核であるリプレイ検証理論を、Lean 4で検証可能な形式証明として公開しました。ADICは、判断の結果だけでなく判断に至る過程そのものを証拠として残す点で、従来の監査ログと本質的に異なります。

物流・製薬・金融・公共領域など、AIの判断が事故や重大な損失、行政判断に直結する高責任領域では、事後に「なぜその判断を通したのか」を説明できなければ、誰も責任をとれない「責任の蒸発」が起きてしまいます。ADICは、このような「みんな正しかったはずなのに問題が起きた」という事態を防ぎ、企業や組織がAIに対して確実な責任を持てる状態を実現する基盤です。


ADICが防ぐ「責任の蒸発」の構造

欧州では、重大な違反に対して最大で前年度全世界年間売上高の7%相当の制裁金が科され得るEU AI Actの本格適用が、2026年8月2日に迫っています。AIガバナンスへの要求水準は、従来のように社内に厳格なルールを設けて運用する段階から、外部の独立した第三者が検証できる証拠を提示する段階へと、グローバルに移行しつつあります。

今回公開した形式証明は、ADICの中核である「リプレイ検証」の考え方を、第三者がLean 4上で再実行・確認できる形にしたものです。これは、ADICの検証器が証明書を受理した場合に、その証明書が示す内容について、対応する妥当性条件が成立することを示すものです。Lean 4は、数学証明をコンピュータで検査する定理証明支援の仕組みです。なお、本形式証明はADICのリプレイ検証コアの健全性を対象とするものであり、実運用システム全体、実データから形式モデルへの変換、または完全性を証明するものではありません。今回の公開により、ADICは単なる構想や運用ルールではなく、第三者が再実行できる技術的証拠を伴うAIガバナンス技術として、実運用に向けた中核検証基盤を示しました。

開発哲学「和算2.0」:AIガバナンスの国際標準を支える日本の思想

ADICの設計思想の根底には、「手順そのものが信頼の根拠である」という日本の数学文化が流れています。

江戸時代の和算では、解法を算額に公開し「誰でも再実行できる手順」を示すことが信頼の証でした。無限の理論を語るより、「確実に検証できる範囲」を定めて手順を残す姿勢です。 ADICはこの精神の現代的実装です。AIの判断手順を証拠台帳として固定し、第三者が機械的に再実行・検証できるこの仕組みを、GhostDriftは「和算2.0」と位置づけ、日本発のAIガバナンス技術として国際標準への接続を目指します。



和算2.0--手順公開の精神をAI判断の再検証へ

代表コメント

株式会社GhostDrift数理研究所 代表取締役 前木 秀光
「AIの信頼が、事後的な『説明』や『監視』だけではすでに成立しない段階にあることは、もはやグローバルな社会の前提です。重要なのは、判断の後に第三者が同じ手順をたどり直し、何が根拠で、どこで止めるべきだったかを確認できることです。私たちがADICで実装しているのは、AI判断の"再検証責任"です。今回公開したLean 4による形式証明は、ADICのリプレイ検証コアが第三者に再実行できる技術基盤であることを示します。"見ているだけ"のガバナンスから、"後から確かめられる"アシュアランスへ--GhostDriftはその移行を、日本発の技術として実装します」

今後の展開:国際議論の起点「広島」から始まるAIアシュアランスの実装

GhostDriftは、物流・製薬など高責任領域へのADIC実装展開を進めながら、第三者検証性と再現性を核とした「AIアシュアランス」の国際標準への接続を目指します。AIシステムの判断が信頼・安全であることを技術的に保証するAIアシュアランスは、現在、英国・EU・米国においてAIガバナンスの中核領域として急速に整備が進んでいます。

この国際基準に向けた第一歩として、2026年4月、AIガバナンスの国際的な議論の起点となった「広島AIプロセス」の地で、ハイテク製造業物流で長年にわたる実績を持つ株式会社オンザリンクスと戦略的パートナーシップを締結し、製薬物流コールドチェーンにおける荷主責任証明基盤のPoCを開始しました。

本提携に基づく第一弾のマイルストーンとして、今後2ヶ月間で初期PoCを実施します。具体的には、ADICによる数理的な証明基盤が、実際の物流現場で長年の経験を持つオンザリンクス社の厳格な実務監査を通過できるか、その有効性を現場の視点から検証します。

日本発の責任ある技術の実装が、国際議論の出発点と同じ地からすでに始まっています。この2ヶ月間の実証結果をもって、GhostDriftは高責任領域におけるAIアシュアランスインフラの社会実装を次のフェーズへと進めます。オンザリンクスとの提携に関する詳細はこちらのプレスリリースをご覧ください。

■ リンク

GitHubリポジトリ:https://github.com/GhostDriftTheory/adic-lean-proof-replay
Zenodoプレプリント:https://zenodo.org/records/19821808
和算2.0:https://www.ghostdriftresearch.com/wasan20

■ 用語解説


■会社概要

【株式会社GhostDrift数理研究所】
代表者 前木 秀光
所在地 東京都新宿区北新宿4-4-4
設立 2026年2月10日
事業内容 高責任領域(物流・製薬・金融・重要インフラ等)におけるAIガバナンス技術の設計・実装支援
URL https://www.ghostdriftresearch.com
動画ライブラリ(日英各36本・計72本) https://www.ghostdriftresearch.com/videos
代表略歴
 京都大学総合人間学部 国際文明学科卒業。株式会社パソナグループ、株式会社マクロミルを経て、GhostDrift数理研究所を設立

GhostDrift数理研究所は、AI判断を第三者が再検証できる証拠レイヤー 「ADIC(Advanced Data Integrity by Ledger of Computation)」を開発し、 AIガバナンスの主張を再現可能な証拠・独立検証・形式証明へ接続します。 AIガバナンス・AIアシュアランスに関する日英計72本の動画シリーズを 公開するなど、領域の体系的な知識普及にも継続的に取り組んでいます。

本件に関するお問い合わせ

株式会社GhostDrift数理研究所 広報担当:前木(まえき)
お問い合わせフォーム:https://www.ghostdriftresearch.com/contact

企業プレスリリース詳細へ
PRTIMESトップへ
page top