arXiv cs.AI· Hans-Martin Will, Allen L. Brown Jr., Matthew Fuchs·· 11 小时前AI 评分31
Eigenius：带认知分层与制度中介推理的类型化知识图谱 DBMS
Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning
AI 导读
Eigenius 是一个开源类型化知识图谱 DBMS，将类型系统、存储引擎与集成协议耦合在同一内核中，使数据溯源成为结构性不变量。其内核基于 Lean 4 机械化元理论，包含分离转换与本体归摄的依值类型理论 EigenTT、作为强类型集成边界的证明演算制度，以及内容寻址的不可变存储层。
正文 · AI 翻译
摘要：随着“AI 科学家”通过模型上下文协议（MCP）推动研究，依赖临时脚本的系统将无法胜任。有状态、相互关联的证据规模庞大，需要一种基于专门构建的数据库架构、可供机器遍历的保证机制。Eigenius 是一个开源、类型化知识图谱 DBMS，其构建基于一个单一前提：回答审计问题（“你知道什么，你的保证是什么？”）需要一个统一内核。通过将类型系统、存储引擎和集成协议紧密耦合，Eigenius 将数据溯源转变为结构性不变量，而非跨子系统边界重建的属性。该内核建立在三大支柱之上，其元理论已在 Lean 4 中机械化：依赖类型论（EigenTT），将合流转换与本体包含分离，并保持证明无关性为公理，使不同的保证仍可检查；证明演算制度作为强类型集成边界；以及内容寻址的不可变存储层。认知状态（声明/观察/推导/验证）在提交时强制执行的辩护逻辑上构成有界格。跨系统共态射携带显式公理策略（采纳、解除、相对化），在提交时传输见证，并将输出物化到图中，而 EigenQL 提供跨所有托管逻辑的 Grothendieck 查询视图，共享链上 IR 将多系统翻译坍缩为恒等。将经验辩护逻辑与进程内 Lean 4 项检查器配对，从固定数据对一项已发表的 Nature 研究进行端到端重计算，解除了全部 52 个推导结论，并揭示了原研究中四处机器检查的差异。
| 评论： | 对上一版稿件的少量更正 |
| 主题： | 数据库（cs.DB）；人工智能（cs.AI）；计算机科学中的逻辑（cs.LO） |
| 引用方式： | arXiv:2608.04457 [cs.DB] |
| （或使用 arXiv:2608.04457v3 [cs.DB] 获取此版本） | |
| https://doi.org/10.48550/arXiv.2608.04457 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Hans-Martin Will [查看邮箱]
[v1]
2026年8月5日 星期三 05:28:22 UTC（17 KB）
[v2]
2026年8月18日 星期二 15:52:48 UTC（17 KB）
[v3]
2026年11月5日 星期四 16:02:06 UTC（19 KB）
来源：arXiv cs.AI · arxiv.org