PAGR: Proof-Carrying Algebraic-Geometric Retrieval: A Quiver-, Provenance-, and Sheaf-Theoretic Framework for Grounded LLM Retrieval

• URL: http://arxiv.org/abs/2609.06127v1
• Date: Sat, 05 Sep 2026 14:51:32 GMT
• Title: PAGR: Proof-Carrying Algebraic-Geometric Retrieval: A Quiver-, Provenance-, and Sheaf-Theoretic Framework for Grounded LLM Retrieval
• Abstract summary: 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.<n>We propose Proof-Carrying Algebraic-Geometric Retrieval (PAGR), a framework that separates these questions mathematically.
• Score: 7.3040623979718475
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Partial Identification under Causal Orders by Linear Programming [46.16293902963101]
  We show that any counterfactual inquiry induces a partial, topological ordering over relevant variables.<n>This allows bounding arbitrary counterfactual and nested counterfactual queries.
  arXiv  Detail & Related papers  (2026-08-25T11:42:38Z)
• TREAT: Evaluating Access to Formal Knowledge across Equivalent Mathematical Representations [0.0]
  Key challenge is recognizing when an unfamiliar formulation denotes a known formal object.<n>Treat is a benchmark for evaluating whether large language models can recover known theorem identities.<n>Treat provides a controlled testbed for evaluating representation-robust access to formal knowledge.
  arXiv  Detail & Related papers  (2026-07-29T23:02:46Z)
• A diagrammatic field theory of quantum error correction [0.0]
  We develop a framework for quantum error correction centred on fusionspace codes in unitary fusion categories.<n>We compute geometry-dependent Ising four-point weights for growing code families.<n>We also formulate conformal-block likelihood data and compute geometry-dependent Ising four-point weights.
  arXiv  Detail & Related papers  (2026-07-09T20:10:13Z)
• A homotopy-type-theoretic generalization of neurosymbolic inference [46.36639624013224]
  neurosymbolic (NeSy) systems compute one functional: a belief-weighted sum of a logical quantity over a space of $$-structures.<n>We develop the framework from scratch for NeSy systems, prove a conservativity theorem that recovers the classical functional when symmetries are trivial, and show that the symmetry our framework exposes is exactly the one behind reasoning shortcuts.
  arXiv  Detail & Related papers  (2026-06-16T12:22:12Z)
• What are the Right Symmetries for Formal Theorem Proving? [23.981613344642152]
  We show that semantically equivalent statements can exhibit drastically different proof success rates.<n>This raises a central question: what are the right symmetries for formal theorem proving?<n>We introduce rewriting categories, a category-theoretic framework capturing the compositional, generally non-invertible transformations induced by proof tactics.
  arXiv  Detail & Related papers  (2026-05-21T10:00:47Z)
• NOETHER: A Constructive Framework for Metamorphic Pattern Discovery from Operator Algebras [6.691613382732758]
  Metamorphic Testing is recognised in IEEE/ISO software-testing standards and increasingly recommended for AI systems.<n>Existing approaches share an inductive grounding that leaves three foundational questions open.<n>We propose a framework whose downstream step from operator algebra to MetaPattern set is mechanical and provable.
  arXiv  Detail & Related papers  (2026-05-17T11:18:35Z)
• Geometric Factual Recall in Transformers [57.48371649045765]
  A common view casts internal weight matrices as associative memories over pairs of embeddings, requiring memorization counts that scale linearly with the number of facts.<n>We develop a theoretical and empirical account of an alternative, emphgeometric form of memorization in which learned embeddings encode structure directly.<n>In a controlled setting where a single-layer transformer must memorize random vectors from subjects to a shared attribute set, we prove that a logarithmic embedding dimension suffices.<n>We extend these results to the multi-hop setting, providing constructions with and without chain-of-thought that exhibit a provable
  arXiv  Detail & Related papers  (2026-05-12T17:22:22Z)
• Fully Geometric Multi-Hop Reasoning on Knowledge Graphs with Transitive Relations [50.05281461410368]
  We introduce GeometrE, a geometric embedding method for multi-hop reasoning.<n>It does not require learning the logical operations and enables full geometric interpretability.<n>Our experiments show that GeometrE outperforms current state-of-the-art methods on standard benchmark datasets.
  arXiv  Detail & Related papers  (2025-05-18T11:17:50Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  We introduce a neuro-symbolic framework for autoformalizing Euclidean geometry. One challenge is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize. We provide automatic semantic evaluation for autoformalized theorem statements.
  arXiv  Detail & Related papers  (2024-05-27T14:35:10Z)
• Enriching Disentanglement: From Logical Definitions to Quantitative Metrics [59.12308034729482]
  Disentangling the explanatory factors in complex data is a promising approach for data-efficient representation learning. We establish relationships between logical definitions and quantitative metrics to derive theoretically grounded disentanglement metrics. We empirically demonstrate the effectiveness of the proposed metrics by isolating different aspects of disentangled representations.
  arXiv  Detail & Related papers  (2023-05-19T08:22:23Z)
• A Category-theoretical Meta-analysis of Definitions of Disentanglement [97.34033555407403]
  Disentangling the factors of variation in data is a fundamental concept in machine learning. This paper presents a meta-analysis of existing definitions of disentanglement.
  arXiv  Detail & Related papers  (2023-05-11T15:24:20Z)
• Finite-Function-Encoding Quantum States [52.77024349608834]
  We introduce finite-function-encoding (FFE) states which encode arbitrary $d$-valued logic functions. We investigate some of their structural properties.
  arXiv  Detail & Related papers  (2020-12-01T13:53:23Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.