🤖 AI

Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning

Eigeniusは、依存型理論、制度的統合境界、および不変ストレージを統合することで、認識論的ステータスを構造的不変量として強制し、それによって脆弱で一時的なAI研究用スクリプトを、科学的結論を検証し不一致を検出可能な、マシンウォーク可能で監査対応の証拠グラフへと置き換える、オープンソースの型付き知識グラフDBMSである。

原著者： Hans-Martin Will, Allen L. Brown Jr., Matthew Fuchs

公開日 2026-08-06

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Hans-Martin Will, Allen L. Brown Jr., Matthew Fuchs

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

探偵のジレンマ：なぜ真実を追跡するためのより良い方法が必要なのか

あなたは、巨大なミステリーを解こうとしている探偵だと想像してください。昔であれば、付箋に手がかりを書き留めたり、コルクボードに写真をテープで貼り付けたり、ノートに結論を書き込んだりしていたことでしょう。もし誰かに「なぜ執事が犯人だと分かったのですか？」と聞かれたら、あなたはノートをパラパラとめくり、証拠の連鎖を示すことができました。しかし、もしあなたのノートが、いつでも消去したり書き換えたりできる、バラバラで一時的なメモの集まりだったとしたらどうでしょう？もしあなたの「証拠」が、一度実行されたら跡形もなく消えてしまうスクリプトであり、どのように結論に至ったのかという痕跡を一切残さないものだとしたら？

これが、現在の科学者、そして急速に増加している「AI科学者」たちの仕事の現状です。彼らは強力なツールを使って複雑な実験を実行し、コードを書いていますが、その仕事の「証明」は、しばしば脆弱で一時的なファイルの中に存在しています。AIがここから学ぼうとする時、それはまるで、透明なインクで書かれたボードを使って謎を解こうとしているようなものです。私たちがこれから探求する論文、Eigeniusは、新しい種類の「探偵の台帳」が必要であると主張しています。それは、あらゆる情報の断片、あらゆる計算、そしてあらゆる結論が、決して偽造したり失ったりすることのできない方法で、永久に刻印され、型付けされ、連結されるシステムを提案しています。これは、単に事実を保存するだけでなく、それらの事実に対する「保証」、つまりそれらが真実であるという証明を保存するデータベースを構築することなのです。

論文：科学のための「真実の機械」を構築する

この論文は、AI科学者の時代に向けて特別に設計された新しい種類のデータベース、Eigeniusを紹介しています。著者である Hans-Martin Will、A. L. Brown Jr.、Matthew Fuchs は、現在の科学データの保存方法は、機械が信頼するにはあまりにも乱雑すぎると主張しています。今日、科学的な議論は、スクリプトと物語の間の「一時的なウェブ（儚い網）」であることが多く、監査が困難です。もしAIエージェントがこれらを読もうとしても、数学的な計算が正しく行われたのか、あるいは途中でデータが変更されていないのかを確信することができません。

Eigeniusは、すべてのアイテムに永久に変わることのないIDカードを持たせることで、データを高セキュリティの金庫のように扱うことでこれを解決します。その仕組みを、いくつかの楽しい比喩を用いて説明します。

1. 「エピステミック（認識論的）」IDカード（自分が何を知っているかを知る）
Eigeniusでは、すべてのデータに特定の「エピステミック・ステータス（認識論的状態）」タグが付与されます。これは、探偵のファイルに付けられた色分けされたバッジのようなものです。

Declared（宣言済み）: 「権威ある者がそう言ったので、これは真実であると私は言う。」（まだ証明はない）。
Observed（観測済み）: 「機械によってこれが起こるのを見た。」（現実世界の証拠）。
Derived（派生済み）: 「他の事実からこれを計算した。」（コンピュータによる計算）。
Verified（検証済み）: 「これが100%真実であることを示す、形式的でマシンチェックされた証明を持っている。」（黄金律）。

このシステムは、データを保存する前に、すべてのデータに対して必ずバッジを選択することを強制します。単に数字を放り込むことはできず、それがどこから来たのかを証明しなければなりません。これにより、「監査の問い（どうやってそれを知ったのか？）」は、後で推測しなければならないものではなく、データベース自体の構造的な一部となります。

2. 「Institution（制度/機関）」の架け橋（ユニバーサル・トランスレーター）
科学には多くの異なる言語があります。ある研究室はPythonを使い、別の研究室はLeanと呼ばれる数学ツールを使い、第三の研究室は統計プログラムを使うかもしれません。通常、これらを接続することは、英語からフランス語へ、そして日本語へと翻訳し、また英語に戻すようなものであり、エラーが紛れ込み、元の意味が失われてしまいます。これは「ポリストア・ボトルネック」と呼ばれ、非常にコストがかかります（数学的に言えば、それは $O(N^2)$ の問題であり、非常に急速に混乱が生じることを意味します）。

Eigeniusは、Institutionsを導入しています。これらはデータベース内部の専門的な「大使館」や「翻訳ブース」のようなものです。データが一つのシステムから別のシステムへ移動する際、単にコピーされるのではなく、**comorphism（共形態）**と呼ばれる厳格な型付きプロトコルによって翻訳されます。システムは、保存される前にその翻訳をチェックします。もし数学的な整合性が完全に一致しなければ、その翻訳は拒否されます。これにより、データが異なる科学ツール間を移動する際、意味が失われることなく、出発した時と全く同じ状態で到着することが保証されます。

3. 「Lean」の証明（魔法のスペルチェック）
純粋数学において、EigeniusはLean 4と呼ばれる強力なツールを使用します。Lean 4は、単なるタイポ（打ち間違い）をチェックするだけでなく、文章全体が論理的に成立しているかをチェックする「スペルチェッカー」だと考えてください。Eigeniusにおいて、このチェッカーはデータベースの内部で動作します。科学者が数学の定理が真実であると主張するとき、データベースは単にその言葉を鵜呑みにするのではなく、独自の内部スペルチェッカーを通じて証明を実行し、検証します。証明が成立すれば、その主張には「Verified（検証済み）」のバッジが付与されます。失敗すれば、それは拒否されます。これは外部のコンピュータを呼び出すことなく即座に行われるため、高速かつ安全です。

4. 「Immutable（不変）」の連鎖（壊れない台帳）
Eigeniusにおけるすべてのものは、**コンテンツ・アドレス（内容に基づくアドレス指定）**方式で保存されます。想像してみてください、本のタイトルではなく、その言葉自体のユニークな指紋によって識別される図書館を。もし一冊の本の中でカンマを一つでも変えれば、その指紋は変わり、全く別の本になってしまいます。これは、データの履歴がこれらの指紋の連鎖（Merkle tree）であることを意味します。もし誰かが過去の実験をこっそり改ざんしようとしても、指紋が一致しなくなるため、システムは即座にそれを検知します。

大規模なテスト：有名な研究の書き換え

このシステムが機能することを証明するために、著者たちは単に構築しただけでなく、学術誌『Nature』に掲載された有名な科学的研究を再実行しました。この研究は、特定の酵素（WRNヘリカーゼ）とそれが癌に果たす役割に関するものです。オリジナルの研究は、脆弱なスクリプトと一時的なファイルを使用して書かれていました。

チームはオリジナルのデータを取得し、Eigenius内でその議論全体を再構築しました。彼らは「一時的なスクリプト」を、強固で永続的な「証拠グラフ」へと作り変えました。

結果: 研究の52の派生した結論すべてが、固定されたデータに対してチェックを行った際、整合性が保たれていることが確認されました。
驚きの発見: このプロセスにより、オリジナルの論文のテキストと実際のデータとの間に4つの不一致が見つかりました。例えば、オリジナルの論文ではサンプルサイズが54であるとされていましたが、データによれば、いくつかの行が欠落していたため、実際には51であったことが示されました。もう一つのエラーは、統計計算が**13桁（10の13乗）**もズレていたことに関するものでした（これは極めて大きな差です！）。

これらは単なる「うっかりミス」ではありませんでした。これらは、オリジナルの主張と並んで、マシンでチェック可能な事実として記録されました。システムは、すべてのステップを「型付きのリソース」にすることを強制することで、オリジナルの研究に隠されていたエラーを無視できないものにしたのです。

なぜこれが重要なのか

論文は、AIエージェントが自律的に科学を行うようになるにつれ、乱雑で一時的なファイルに頼ることはできないと示唆しています。私たちは、型システム、ストレージ、および翻訳ルールを同時に所有する「カーネル（核となるエンジン）」を必要としています。Eigeniusは、「監査証跡」をデータ構造の永続的な一部にすることで、機械が信頼できるほど堅牢な科学的基盤を構築できると提案しています。

著者たちは、これがプロトタイプであり、「型付きのマージ（結合）」が常に正しく機能することを完全に証明する方法など、まだ未解決の課題があることを認めています。しかし、彼らの『Nature』の研究を用いた実験は、このアプローチが実現可能であることを示唆しています。それは、科学的手法を「語られる物語」から、機械が各リンクを一つずつチェックしながら歩んでいける「証拠の連鎖」へと変えるものなのです。これは単にデータを保存することではありません。真実に対する「保証」を保存することなのです。

技術要約：Eigenius：エピステミック層状化と制度媒介推論を備えた型付き知識グラフDBMS

1. 問題提起

Model Context Protocol (MCP) を用いて研究ループを駆動する自律的な「AI科学者」の台頭は、現在の科学データインフラストラクチャにおける決定的な限界を露呈させた。既存のシステムは一時的なスクリプトや叙述的な散文に依存しており、人間による手動監査は可能であっても、自律的なエージェントが要求する「暗号学的に安全で、完全に歩行可能な証明チェーン」には不十分な、脆弱なパイプラインを生み出している。

Pharosプロジェクト（2008年）のような、機械監査可能な科学の定式化への過去の試みは、連邦型アーキテクチャに依存していたためにスケールに失敗した。Pharosは、SQL Server、DataNet、HOL定理証明器といった異種サブシステムを、不透明なカスタムブリッジを介して繋ぎ合わせていた。このアプローチは統一されたカーネルを欠いていたため、以下の問題を引き起こした：

オントロジーの断片化： スキーマとインスタンスデータが異なるカテゴリに存在していた。
構造的不変量の欠如： システム間の変換は一時的なものであり、形式的にチェックされていなかった。
ポリストアのボトルネック： $N$ 個のシステムを統合するために $O(N^2)$ のペアワイズ・アダプターが必要であった。
推論の統合不能： 経験的な正当化論理と形式的な数学的証明が、共有の型システムを持たない別々のエンジンによって処理されていた。

核心となる課題は、「何を知っており、その保証（warranty）は何か？」という監査の問いを、サブシステム間の境界を越えて再構成される属性としてではなく、データモデル自体の構造的不変量として扱うデータベースアーキテクチャを構築することである。

2. 方法論およびアーキテクチャ

Eigeniusは、統一された数学的カーネル上に構築された、オープンソースの型付き知識グラフDBMSである。本システムは、連邦型スタックを、型システム、ストレージエンジン、および統合プロトコルを密結合させた単一のアーキテクチャへと置き換える。

中核となる柱

依存型理論 (EigenTT): カーネルは、中心部に織り込まれた依存型理論（CICファミリー）を使用する。スキーマとデータは統一されており、クラスを宣言することはリソースをコミットすることと同義である。コミットの単位は**レイヤー（layer）**であり、これは親ポインタを持つ不変のリソースセットである。レイヤーのアイデンティティは、標準的なCBORのSHA-256によるコンテンツアドレス指定が行われ、グラフ履歴へのMerkleコミットを形成する。
エピステミック層状化 (Epistemic Stratification): すべてのリソースは、コミット時に厳格な不変量として強制されるエピステミック・ステータス（認識論的状態）を保持する。システムは以下を区別する：
- Declared (宣言): 証拠を伴わない権威（適切性はチェックされる）。
- Observed (観測): 外部のプロベナンス（由来）と共に記録されたもの。
- Derived (派生): 型付き計算によって生成されたもの。
- Verified (検証): 形式的に再チェックされた証明項を伴うもの。
  この層状化は正当化論理（justification logic）に基づいており、科学的な主張は観測や慣習に依存し、それらは証明器によって解消できないことを認めた上で、すべての保証が事実的（factive）であるとは限らないことを前提としている。
制度媒介推論 (Institution-Mediated Reasoning): 外部の推論器（ODEソルバー、定理証明器など）を統合するために、Eigeniusは、格納されたストアドプロシージャの強力な型付き一般化として、**GoguenおよびBurstallの制度（institutions）**を適応させる。
- コモルフィズム (Comorphisms): システム間の相互変換は、エンジン内でネイティブに実行される強力に型付けされたETLパイプラインである「コモルフィズム」としてモデル化される。
- コミット時チェック: 変換 $m: S \to T$ がペイロードの型と一致しない場合、スキーマ違反と同様に拒絶される。
- 実体化 (Materialization): 従来の連邦型データベースでは変換は一時的なものであるが、Eigeniusはコモルフィズムの出力を、コンテンツアドレス指定された耐久的なリソースとしてグラフ内に直接実体化する。

形式検証の統合

純粋数学を扱うために、EigeniusはIPC（プロセス間通信）のオーバーヘッドを発生させることなく、不透明な証明ペイロードを検証する課題を解決する：

インプロセス・チェッキング: カーネルは、最小限のRustタームチェッカー（nanoda_lib）をバイナリに直接リンクする。
依存ペア (Dependent Pairs): 検証された主張は、依存ペア $(P, t)$ として格納される（ $P$ は命題でありEigenTTにネイティブ、 $t$ は不透明なLean 4バイトである）。
バインディング問題: コミット時、カーネルは3部構成のチェックを行う：(1) インプロセスチェッカーによる証明の妥当性、(2) ミラー対応（Leanの定数とチェーンクラスIRIのマッピング）、(3) アンカーの一貫性（ソースアーカイブのハッシュ化）。

クエリ言語 (EigenQL)

EigenQLは、集計機能と、制度的設定のための2つの特定の節を備えた、型付きの層状Datalogである：

FIBER: クエリの実行中に外部の制度へディスパッチする。
INTO: 外部エンジンのレスポンスを、名前付きIRIとしてチェーン内に固定し、コミットパイプラインをトリガーする。

3. 主な貢献

本論文は、主に4つの貢献を述べている：

C1: 統一データモデル: 経験的な正当化論理と形式的な数学的証明を統一する、自己記述的な型付きグラフモデル。エピステミック・ステータスは、コミット時に強制される構造的なベースクラスである。形式検証は、中間表現（IR）に不透明な証明ペイロードをバインドする、組み込みのインプロセス・タームチェッカーを介して行われる。
C2: 制度統合プロトコル: ストアドプロシージャの強力に型付けされた一般化として、データベースの世界に「制度」を導入した。システム間の相互変換（コモルフィズム）は、コミット時に静的にチェックされ、耐久的なリソースとして実体化される。
C3: ポリストア・ボトルネックの排除: 共有の強力に型付けされた中間表現（IR）をグラフのスキーマにネイティブに引き上げることで、そのIRを共有するシステム間のコモルフィズム変換は純粋な恒等写像へと収束し、 $O(N^2)$ のアダプターコストを排除する。
C4: エンドツーエンドの再現: 脆弱なスクリプトから実体化されたエビデンスグラフへと移行することで、高名な研究（ChanらによるWRNヘリカーゼに関する研究）の完全な再計算と再エンコーディングを実施した。

4. 結果および評価

Rustで記述され、RocksDBストレージとgRPC APIを備えたプロトタイプを用い、マイクロベンチマークおよびマクロ評価を行った。

マイクロベンチマーク (インジェスチョン): システムはWordNetおよびUMLSの語彙（919万個のチェーンリソース）を取り込んだ。シングルコアで、秒間約5,200個の検証済みリソースのインジェスチョンを維持した。コミットゲートが主要なコストであり、構造的クラスレイヤーのロードは約28k/s、厳密に型チェックされた語彙エントリは約4k/sであった。
マクロ評価 (Nature研究の再現): ゲノムワイドな依存性スクリーニング、ウェットラボでの検証、およびin vivoモデルを含む、高名な研究を再実行した。
- 一貫性: 派生した52の結論すべてが、固定されたデータから保持されていた。
- 不一致の検出: 再計算により、論文の記述とデータとの間の、機械的にチェックされた4つの不一致が浮上した。これには、サンプルサイズの修正（ $n=54 \to 51$ ）や、正直な $p$ 値が13桁異なった擬似複製エラーが含まれる。
- 監査可能性: 論文内のすべての解析クラスはライブで実行可能であり、仮定は記述的な注釈ではなく、検査可能なリソースとなっている。

5. 意義および主張

本論文は、Eigeniusが次世代のAI主導型科学研究をサポートするために必要なデータベースカーネルを提供すると主張している。その意義は以下の点にある：

構造的不変量: データプロベナンスとエピステミック・ステータスを、事後的な再構成から、データモデルの構造的不変量へと変える。
エージェント対応インフラ: 自律的なエージェントが、科学的推論のためのタイトなループ（「コンパイラ」と「テストスイート」）を必要とする「エージェントの反転」に対処する。これは、一時的なスクリプトでは不可能である。
統一された認識論: 経験科学のための正当化論理と、数学のための形式検証という2つの科学的認識論の領域を、単一のエンジン内で成功裏に統合した。
検証可能な監査チェーン: オーディター（監査人）が、中間ミドルウェアに接触することなく、グラフのみを使用して、判決から生のデータおよび証明項に至る全証明パスを再歩行できる「クローズドな監査チェーン」を可能にする。

著者らは、重いネイティブライブラリをサポートするためにコンテナ化された基質としてのWasmを放棄した決定や、バリデータおよびコモルフィズム・タイプチェッカーの機械化に関する継続的な課題を含め、限界についても認めている。最終的な目標は、AI科学者が科学的グラフを横断し、変異させ、検証することを可能にすることである。