論文の概要: Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning
- arxiv url: http://arxiv.org/abs/2608.04457v1
- Date: Wed, 05 Aug 2026 05:28:22 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-06 14:48:43.728839
- Title: Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning
- Title(参考訳): Eigenius: 先天的階層化と機関媒介推論を備えた型知識グラフDBMS
- Authors: Hans-Martin Will, Allen L. Brown, Matthew Fuchs,
- Abstract要約: Eigeniusは、単一の前提に基づいて構築された知識グラフである。
これは、データ証明をサブシステムの境界を越えて再構成された特性ではなく、構造的不変量に変換する。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: As "AI Scientists" emerge to drive research via the Model Context Protocol (MCP), systems relying on ephemeral scripts will fail. The sheer scale of stateful, interconnected evidence requires a machine-walkable warranty grounded in a purpose-built database architecture. Eigenius is an open-source, typed knowledge-graph DBMS built on a single premise: answering the audit question ("what do you know, and what is your warranty?") requires a unified kernel. By tightly coupling the type system, storage engine, and integration protocol, Eigenius turns data provenance into a structural invariant rather than a property reconstructed across subsystem boundaries. The kernel rests on three pillars: a dependent type theory woven through the core, institutions acting as strongly typed integration boundaries, and a content-addressed immutable storage layer. On this foundation, epistemic status (declared/observed/derived/verified) is enforced as a strict commit-time invariant. Cross-system translations (comorphisms) are checked at commit and materialized directly into the graph as durable, first-class resources. To eliminate O(N^2) polystore bottlenecks, shared on-chain intermediate representations (IRs) collapse multi-system translations to identity. Crucially, this architecture unifies both domains of scientific epistemology: it relies on justification logic for empirical science, while embedding a fast, in-process term checker to safely evaluate formal mathematical proofs (via Lean 4) without IPC overhead. In an end-to-end recomputation of a published Nature study from fragile scripts to a materialized evidence graph, all 52 derived conclusions hold from pinned data, surfacing four machine-checked discrepancies in the original study.
- Abstract(参考訳): モデルコンテキストプロトコル(MCP)を通じて研究を進める"AIサイエンティスト"が出現するにつれ、短命なスクリプトに依存するシステムは失敗する。
ステートフルで相互接続された証拠の規模は、目的に構築されたデータベースアーキテクチャを基盤とした、マシンウォーカブルな保証を必要とする。
Eigeniusは、単一の前提に基づいて構築されたオープンソースの型付きナレッジグラフDBMSである。
型システム、ストレージエンジン、統合プロトコルを密結合することにより、Eigeniusは、サブシステムの境界を越えて再構成されたプロパティではなく、構造的不変性に変換する。
カーネルは、コアを通して織られた依存型理論、強く型付けされた統合境界として機能する機関、コンテンツ適応不変ストレージ層という3つの柱に依存している。
この基盤では、厳格なコミットタイム不変量として、てんかん状態(宣言/保存/派生/検証)が強制される。
システム間の変換(コモルフィズム)はコミット時にチェックされ、永続的でファーストクラスのリソースとして直接グラフに実体化される。
O(N^2)ポリストアのボトルネックを取り除くため、共有オンチェーン中間表現(IR)は同一性へのマルチシステム変換を崩壊させる。
重要なことに、このアーキテクチャは科学認識学の両領域を統一する: IPCオーバーヘッドを伴わずに(Lean 4 を通じて)形式的な数学的証明を安全に評価するために、高速なプロセス内チェッカーを組み込む一方で、経験科学の正当化ロジックに依存している。
脆弱なスクリプトから物質化されたエビデンスグラフへのNature Researchのエンドツーエンドの計算では、52の導出した結論はすべてピン付きデータから保持され、元の研究ではマシンチェックされた4つの不一致を克服した。
関連論文リスト
- Self-Revising Discovery Systems for Science: A Categorical Framework for Agentic Artificial Intelligence [1.1458853556386797]
我々は材料科学のためのエージェント発見のカテゴリー論的記述を開発する。
CategoryScienceClawでは、型付きスキル、アーティファクト、オープンニーズ、ワークフロー突然変異、ゲート、ストレステスト、そして公開談話が、証明付き知識計算グラフとなる。
論文 参考訳(メタデータ) (2026-05-31T20:29:43Z) - Grokers: Bottom-Up Inductive Comprehension and Write-Time Intelligence over Typed Knowledge Graphs [0.0]
Grokersは、型付き知識グラフの永続的で構造化された理解を構築するためのアーキテクチャである。
自律的なGrokerエージェントは、型付きストリームグラフのノードを分析し、制御された言語モデル呼び出しを通じて構造化属性を抽出する。
論文 参考訳(メタデータ) (2026-05-07T17:28:36Z) - ADEMA: A Knowledge-State Orchestration Architecture for Long-Horizon Knowledge Synthesis with LLMAgents [16.053669481561354]
ADEMAは長期の知識合成のための知識状態オーケストレーションアーキテクチャである。
本稿では長軸知識合成のための知識状態オーケストレーションアーキテクチャとしてADEMAを提案する。
論文 参考訳(メタデータ) (2026-04-28T16:54:48Z) - Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
我々は、ハイブリッドAI+Lean 4パイプラインとして、特許分析のための正式に検証されたフレームワークを提示します。
DAG被覆コア(Algorithm1b)は、有界マッチスコアが固定されると完全に機械検証される。
クレームは、Lean 4でDAGとしてエンコードされ、強みを検証された完全な格子の要素と一致させ、信頼スコアは、証明された正しいモノトーン関数を通じて依存関係を通じて伝播する。
論文 参考訳(メタデータ) (2026-04-20T22:02:57Z) - Dynamic analysis enhances issue resolution [53.50448142467294]
DAIRA(Dynamic Analysis-enhanced Issue Resolution Agent)は、エージェントの推論サイクルに動的解析を組み込む自動修復フレームワークである。
テストトレース駆動の方法論によって駆動されるDAIRAは、軽量モニタを使用して重要なランタイムデータを抽出する。
Gemini 3 Flash Previewを使用すると、DAIRAは新たな最先端(SOTA)パフォーマンスを確立し、SWE-bench Verifiedデータセットで79.4%の解像度を達成する。
論文 参考訳(メタデータ) (2026-03-23T14:48:54Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳(メタデータ) (2025-11-26T06:39:19Z) - On Immutable Memory Systems for Artificial Agents: A Blockchain-Indexed Automata-Theoretic Framework Using ECDH-Keyed Merkle Chains [0.0]
本稿では,暗号的に固定された決定論的計算フレームワークであるMerkle Automatonの概念を紹介する。
各エージェントのトランジション、メモリフラグメント、推論ステップは、オンチェーンでルートされたMerkle構造内で実行される。
このアーキテクチャはメモリをキャッシュではなく台帳として再設定する - 内容がプロトコルによって強制され、暗号によって拘束され、形式論理によって制約される。
論文 参考訳(メタデータ) (2025-06-16T08:43:56Z) - Chain-of-Knowledge: Grounding Large Language Models via Dynamic
Knowledge Adapting over Heterogeneous Sources [87.26486246513063]
Chain-of-knowledge (CoK)は、大規模な言語モデルを拡張するフレームワークである。
CoKは推論準備、動的知識適応、解答統合の3段階からなる。
論文 参考訳(メタデータ) (2023-05-22T17:34:23Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。