构建可审计的科学知识图谱数据库，让机器能自动验证研究结论真伪。
Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning
- 用类型系统与机构化边界统一数据结构与推理流程
- 52个推论全部通过验证，发现原论文4处机器可查错误
- 适合需可复现、可审计科研成果的研究者使用
随着'人工智能科学家'借助模型上下文协议（MCP）推动研究，依赖临时脚本的系统将失效。大规模状态化、互联证据需要一种机器可读的保证，基于专用数据库架构实现。Eigenius是一个开源的类型化知识图谱数据库管理系统，核心理念是：回答审计问题（你了解什么，你的依据是什么）需统一内核。通过紧密耦合类型系统、存储引擎与集成协议，将数据溯源转化为结构性不变量，而非跨子系统重建的属性。内核建立在三大支柱之上：贯穿核心的依赖类型理论、作为强类型集成边界的机构，以及内容寻址的不可变存储层。在此基础上，知识状态（声明/观测/推导/验证）被严格作为提交时不变量强制执行。跨系统转换（同构态）在提交时检查，并直接以持久化、一等资源形式存入图中。为消除多存储系统的O(N^2)瓶颈，共享链上中间表示（IR）将多系统转换简化为恒等映射。关键在于，该架构统一了科学认识论的两个领域：使用论证逻辑支持实证科学，同时嵌入快速的进程内项检查器，无需进程间通信开销即可安全求值形式数学证明（基于Lean 4）。在一次从脆弱脚本到可物化证据图的端到端重计算中，所有52个推论均基于固定数据成立，并揭示原《自然》论文中的4处机器可验证差异。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。