PAGR：证明承载的代数几何检索——面向接地LLM检索的箭图、溯源与层论框架
PAGR: Proof-Carrying Algebraic-Geometric Retrieval: A Quiver-, Provenance-, and Sheaf-Theoretic Framework for Grounded LLM Retrieval
浏览论文内容
中文总结 AI 辅助
PAGR通过箭图、层论和半环溯源分离知识认证、表示学习与多跳组合，确保学习组件不提升为ground truth，提供不变性、完备性等数学保证。
中文摘要 AI 辅助
检索增强生成通常被表述为一个统计信息检索问题。基于图的变体增加了关系结构，但该结构的数学地位往往未被充分说明。三个不同的问题往往被混淆：哪些陈述被认证为知识，哪些潜在表示对检索有用，以及哪些多跳组合在语义上是可接受的。我们提出了证明承载的代数几何检索（PAGR），一个在数学上分离这些问题的框架。其符号层是一个由类型化箭图、路径方程和正Horn包含生成的多类关系理论。箭图表示为实体类型分配内积空间，为关系分配线性算子。细胞层测量局部到全局的一致性。半环溯源记录推导过程并支持机器可检查的证书。核心原则是认识论分离：学习到的几何可以排序和组织证据，但不能将假设提升为认证的ground truth。我们证明认证标准在学习组件任意替换下是不变的。进一步的结果包括条件完备性界限、将等距群识别为基于残差检索的相关对称性、上同调一致性诊断，以及用于可接受路径扩展的有界互模拟索引。PAGR是一个数学架构，用于分离系统应该在哪里查找与它被允许将什么视为知识。
英文摘要
Retrieval-augmented generation is usually formulated as a statistical information-retrieval problem. Graph-based variants add relational structure, but the mathematical status of that structure is often left underspecified. Three distinct questions tend to be conflated: which statements are certified as knowledge, which latent representations are useful for retrieval, and which multi-hop compositions are semantically admissible. We propose Proof-Carrying Algebraic-Geometric Retrieval (PAGR), a framework that separates these questions mathematically. Its symbolic layer is a many-sorted relational theory generated by a typed quiver, path equations, and positive Horn inclusions. A quiver representation assigns inner-product spaces to entity types and linear operators to relations. A cellular sheaf measures local-to-global consistency. Semiring provenance records derivations and supports machine-checkable certificates. The central principle is epistemic separation: learned geometry may rank and organize evidence, but cannot promote a hypothesis to certified ground truth. We show the certification criterion is invariant under arbitrary replacement of learned components. Further results include a conditional completeness bound, identification of the isometry group as the relevant symmetry for residual-based retrieval, a cohomological consistency diagnostic, and a bounded-bisimulation index for admissible-path expansion. PAGR is a mathematical architecture for separating where a system should look from what it is allowed to treat as knowledge.
发表机构
- Louisiana State University（路易斯安那州立大学）
机构由 AI 辅助整理，请以论文原文为准。
