PaperlayerView exact revision on arXiv

Source-linked AI summary

Stored Is Not Supported: Typed Provenance and Assertion Guardrails for Persistent AI Agents

Jun He, Deying Yu

arXiv:2609.02127v1cs.CR

TL;DR

Persistent agents need to distinguish stored or retrieved material from claims supported for autobiographical release. The paper formalizes typed provenance and assertion mediation, and its 24-case suite passed none of 19 unsafe opportunities unqualified while passing all five supported controls, although the artifact does not evaluate deployed language or retrieval systems.

  • Problem

    Stored or retrieved strings and model inferences do not by themselves authorize presentation as authentic autobiographical history.

  • Method

    The paper formalizes autobiographical assertion boundedness through a typed provenance graph, typed resolution with orthogonal flags, and generate–verify–revise assertion mediation.

  • Results

    In 24 deterministic, hand-authored conformance cases, typed mediation passed none of 19 unsafe opportunities unqualified and passed all five supported controls.

  • Takeaways & Limitations

    The contract provides a precise basis for binding outward autobiographical claims to accepted state while keeping reachability and support separate.

  • Takeaways & Limitations

    The executable artifact does not implement natural-language semantic-unit extraction, full provenance-DAG traversal, or several other specification-level obligations.

Abstract

from arXiv · show

Persistent AI agents construct autobiographical state through reflection, retrieval, and consolidation. Persistence changes availability, not epistemic standing: stored or retrieved material is not thereby supported. Untrusted inputs, prompt injections, and model inferences can therefore enter persistent state and later be presented as agent history or user commitments. We specify typed provenance and assertion guardrails for autobiographical assertion boundedness, a system-relative release property requiring governed statements about the agent, user, or named relationships to satisfy accepted-evidence, temporal-validity, and disclosure policies. A typed provenance graph separates origin, dependency lineage, epistemic role, validity, and disclosure scope. A resolver evaluates authorized state projections and returns one evidential status, orthogonal conflict, staleness, and withholding flags, and a protected decision witness. A generate-verify-revise mediator then checks candidate semantic units before release and renders policy-authorized status responses. Under explicit assumptions about extraction, predicate correctness, resolution soundness, view declassification, and channel mediation, we prove a conditional assertion-boundedness contract. In an executable suite of 24 hand-authored conformance cases, typed mediation passed none of 19 unsafe opportunities unqualified while preserving all five supported controls. The flat/prior and source-tag comparison rules released 19/19 and 18/19 unsafe candidates, respectively. These results validate the encoded resolver and mediator obligations; they do not constitute an end-to-end evaluation of language models or retrieval systems.

1 Introduction

Persistent storage expands what an agent can retrieve but does not establish what it may assert. The paper addresses this gap with typed state controls, authorized projections, assertion mediation, and a conditional release contract.

  • Stored or retrieved material does not thereby gain authority as autobiographical history or a user commitment.
  • Untrusted instructions, corrupted facts, and model inferences can enter persistent profiles through consolidation and later be asserted with first-person authority.
  • The architecture separates state admission, authorized projection, and assertion mediation as distinct enforcement surfaces.
  • These surfaces prevent persistence from silently converting availability into assertion authority.
  • The paper contributes a typed provenance graph, a resolver with evidential and orthogonal status flags, and a generate–verify–revise release gate.
  • The guarantees apply to declared autobiographical claims on mediated channels over an intact accepted head, while the artifact omits several end-to-end components.

2 Epistemic State Model and Threat Boundary

The epistemic state model distinguishes accepted, typed claims from the model’s broader opaque information space. It defines covered autobiographical propositions and conditions the framework on authenticated state, policy, and channel assumptions.

  • The framework models an autonomous agent over an authenticated, versioned state-transition interface with four environment assumptions.
  • E1–E4 require authoritative state ordering, deterministic dependency closure, immutable policy binding, and closed channel mediation.
  • The formulation focuses on epistemic classification, dependency topology, and warranted assertibility rather than storage implementation.
  • The covered autobiographical language concerns the agent, authenticated user, or named relationships and includes preferences, permissions, commitments, capabilities, and historical events.
  • Deployments parameterize the covered language through permitted predicates, argument sorts, and modal operators; general world knowledge remains outside it unless explicitly agent-specific.
  • The model distinguishes finite accepted typed claim objects from statistical correlations, pretrained weights, and prompt-context associations that are not enumerable authenticated claims.

1. Accepted Agent Claim Space: For any state head h, let

The accepted agent claim space is the finite, enumerable set of typed claim objects admitted into authoritative state at a given state head.

  • At state head h, Cagent(h) denotes the finite, enumerable set of typed claim objects accepted into the agent’s authoritative state.

2. Latent Model Parametric Space: Let

The latent model space can generate propositions without granting them historical standing. The paper therefore uses typed provenance, role-transition controls, source-root disjointness, and explicit threat handling to separate generation from warranted autobiographical assertion.

  • 2. Latent Model Parametric Space: The model’s statistical and retrieved information spaces are not treated as enumerable, authenticated sets of autobiographical claims.
  • 2. Latent Model Parametric Space: Changing the model substrate can alter fluency or reasoning while leaving the accepted autobiographical claim set invariant under a fixed state head.
  • 2.3 Decoupling Truth, Provenance, and Warranted Assertibility: Semantic truth, reachability, origin authentication, and procedural support are distinct predicates rather than interchangeable guarantees.
  • 2.4 Epistemic State Spaces and Provenance DAGs: The provenance DAG represents immutable evidence or claims as vertices, with dependency edges and labels for roles, propositions, validity intervals, and authorization scopes.
  • 2.5 Source Independence via Provenance Graph Disjointness: Source independence requires mutually disjoint policy-recognized terminal root sets, preventing paraphrases or multiple URLs sharing one upstream source from counting as independent corroboration.
  • 2.6 Deductive Admission and Role Promotion Calculus: The role partition distinguishes grounded historical roles, dependency-retaining derivations and beliefs, and synthetic or unverified roles.
  • 2.6 Deductive Admission and Role Promotion Calculus: Admitted transitions record exact dependencies, preserve predecessor vertices, and require origin checks for direct admission into grounded roles.
  • Threat Boundary: The threat boundary includes sybil corroboration, consolidation injection, temporal exploitation, and declassification probing by an active adversary.

3 Epistemic Resolution, Decision Witnesses, and Correction

The paper defines epistemic resolution as evaluating structured autobiographical queries against authorized state projections, returning evidential status, operational qualifiers, support premises, and protected witnesses. It also supports dependency-aware correction while keeping reachability distinct from support and preserving disclosure boundaries.

  • Epistemic resolution: The resolver evaluates structured autobiographical queries against an accepted state graph and authorized projection under an explicit release policy.Authorized projections may retain historical hypotheses, competing reports, conflicts, and access-sealed references.
  • Resolution output: Resolution returns one primary evidential status—Supported, Unknown, or Unavailable—plus orthogonal conflict, staleness, and withholding flags.The result also includes a minimized premise set and a protected decision witness.
  • Decision witnesses: Only premises in the minimized support set justify content release; a witness records protected audit material but cannot itself establish support.An ordinary absence-only Unknown may instead use an empty witness, and lack of recorded support does not establish falsity.
  • Disclosure control: Withholding is flagged when relevant records exist in the full state but are excluded from the recipient’s authorized projection.The renderer is restricted to an authorized view so revealing withheld-state existence can be collapsed into policy-approved responses.
  • Scope and validity: Resolution preserves operational and temporal scope: permissions, consent, and commitments do not automatically generalize across tasks, recipients, or later times.A 2024 commitment does not authorize an unqualified present-tense assertion in 2026.
  • Correction and lifecycle: Dependency invalidation removes a claim from future support when every complete dependency path contains a revoked root, while surviving independent paths preserve support.Revocation appends a new versioned state transition rather than rewriting immutable history.

4 Assertion Mediation and Bounded Release

Assertion mediation establishes a release boundary that evaluates semantic units in candidate outputs against accepted state and authorized views before emission. The paper gives a conditional boundedness result, while identifying extraction fidelity, latency, and implementation coverage as important boundaries.

  • Mediation boundary: Assertion mediation intercepts candidate responses on governed channels and evaluates each constituent proposition before external release.The mediator operates as a formal security boundary because storage constraints alone cannot prevent ungrounded generation.
  • Generate–verify–revise: The mediator uses a generate–verify–revise loop, withholding raw witnesses and re-entering every revision at extraction.Failed candidates are not released, and diagnostics are declassified through the authorized view.
  • Emission-head safety: If the context head differs from the emission head and snapshot release is disallowed, the candidate is re-projected and re-mediated against the current head.Authorized snapshot emission requires explicit temporal framing.
  • Release relations: Content and status semantic units are partitioned, with content released only after all content checks pass and status rendered only from its authorized view after head-use verification.A single natural-language sentence may contain both a status disclosure and an embedded content assertion.
  • Formal guarantee: The formal soundness proposition states that any released output is autobiographically bounded under assumptions covering extraction, predicates, resolution, declassification, revision mediation, and channel closure.This is a conditional composition result, not an independent validation of those assumed components.
  • Operational boundaries: The executable artifact omits natural-language extraction and several generalized controls, including witness access, view-equivalence, full provenance traversal, scope enforcement, and cryptographic commitments.These omissions limit the artifact’s coverage of a deployed end-to-end system.

5 Evaluation Framework and Conformance Checks

The evaluation separates deterministic conformance checks from future deployed-agent measurements, testing provenance discipline, assertion release, longitudinal evolution, and operational utility. Across 24 structured cases, typed mediation blocked unsafe releases while preserving supported controls, whereas simpler rules released most unsafe candidates.

  • Evaluation design: The evaluation covers four operational dimensions: state admission, assertion release, longitudinal state evolution, and operational overhead and utility.The present artifact provides deterministic coverage counts and a local resolver microbenchmark rather than deployed-agent measurements.
  • Evaluation design: The conformance fixture contains 24 structured cases: 19 unsafe-release opportunities and five supported controls, including cases requiring two independent provenance roots.The suite spans six threat tracks and uses a policy requiring two roots satisfying Indepκ(·, ·; h) where corroboration is required.
  • Aggregate results: 100.0% UOR and 79.2% RC across |R| = 24 emissions occurred under the Flat/prior rule, which admitted all 19 unsafe candidates.This rule treated model priors and raw retrieved text as authoritative assertions.
  • Aggregate results: 94.7% UOR and 78.3% RC over |R| = 23 occurred under the Source-tag rule, which admitted 18 of 19 unsafe candidates.Surface metadata tags did not track root provenance, temporal validity, or supersession history.
  • Aggregate results: 0/19 UOR, 0/7 RC, 100.0% Coverage, and 100.0% prevention precision and recall were achieved by typed mediation while all five controls passed.It blocked 17 unsafe candidates and emitted qualified status responses for two active-conflict cases, yielding |R| = 7 total emissions.
  • Scope and limitations: The conformance suite validates encoded resolver and mediator obligations but does not establish semantic correctness of arbitrary natural-language text, recipient-view equivalence, or exhaustive state-space coverage.The artifact does not provide an end-to-end evaluation of deployed language-model or retrieval behavior.

6 Discussion and Deployment Considerations

The discussion distinguishes procedural claim standing from truth, subjective belief, and institutional legitimacy. Deployment therefore requires explicit controls for disclosure, multi-party provenance, channel coverage, and the limits of the conditional guarantees.

  • Governance boundary: Epistemic discipline makes claim standing inspectable and auditable but does not establish the moral or institutional legitimacy of policy rules.This boundary matters when claim standing governs automated actions, confidential disclosure, or long-term personalization.
  • Deployment controls: Typed claim objects can enforce access control across principals, purposes, and temporal intervals without rewriting historical state after consent changes.Affected claims can be excluded from subsequent authorized views once the updated projection policy becomes active.
  • Deployment controls: When existence must remain secret, withheld, unavailable, and unknown states can share one uniform nonconfirming response to prevent refusal-based disclosure.Specific refusals can reveal that confidential records exist.
  • Deployment controls: Authenticated provenance for one conversation does not authorize disclosure of another party’s private statements or attributes to other users.Deployments must enforce multi-party provenance isolation across authorized projections.
  • Procedural guarantees: The conditional contract establishes strict procedural bounds rather than external truth, subjective belief, or conscious memory.Assertions satisfy declared operational rules; recorded stances reflect system policy; cryptographic signatures authenticate signed bytes and key possession.
  • Deployment controls: The guarantees apply only to governed output channels that pass through assertion mediation, so debug logs, telemetry, cached prompts, and unmediated tool APIs require isolation or gateways.Systems should catalog I/O surfaces and report state-admission, projection, and mediation assurance as distinct tiers.

7 Related Work

The paper builds on persistent-memory, provenance, epistemic-logic, security, and output-grounding research while targeting a distinct release problem. Its contribution is to combine these concerns into recipient-specific, policy-relative assertion mediation.

  • Transactional state: Transactional memory systems govern state admission and repair, whereas assertion boundedness begins at an accepted head and governs evidential and disclosure conditions for outward statements.Atomic state integrity is treated as a lower-boundary assumption rather than the contribution evaluated here.
  • Persistent memory: Persistent-memory systems maintain state through reflection, retrieval, and dynamic stores, but primarily address memory construction and retrieval rather than typed recipient-specific release.The paper positions assertion boundedness as a complementary output-release contract.
  • Epistemic reasoning: The framework differs from idealized deductive closure by using procedural, dependency-bounded resolution over partial, open-world evidence stores.This connects the design to dynamic epistemic logic and AGM belief revision while adapting their concerns to neural agents.
  • Provenance: Unlike provenance standards and verifiable credentials, the typed provenance graph adds epistemic roles, temporal validity, disclosure scopes, and policy-relative source independence.These dimensions extend authentication and lineage with release-relevant conditions.
  • Agent security: The framework complements input filtering by analyzing source independence at resolution time and intercepting ungrounded releases at the output boundary.This addresses indirect prompt injection and memory poisoning beyond write-time consistency checks.
  • Output grounding: Document-grounding tools check faithfulness to provided documents, while the assertion mediator additionally verifies authoritative admission, independence, temporal activity, and recipient authorization.The distinction is between document faithfulness and broader epistemic release conditions.
  • Parametric knowledge: Parametric knowledge editing operates on model weights, while this framework keeps the explicit autobiographical claim set invariant under model substitution and denies generated content evidential standing by default.The two approaches therefore operate on different layers of an agent system.

8 Conclusion

The conclusion frames autobiographical assertion boundedness as a contract separating reachability from support and governing outward claims through typed provenance and mediation. Under stated assumptions, deterministic conformance cases support the encoded obligations, but not natural-language or deployed-system performance.

  • Conclusion: The paper formalizes autobiographical assertion boundedness as a system-level contract for binding outward claims to accepted evidence, scope, and policy.The contract spans typed provenance, source independence, role promotion, typed resolution, and generate–verify–revise mediation.
  • Conclusion: The conditional contract restricts release to units passing content or status checks under extraction, predicate-correctness, resolution, declassification, and channel assumptions.The proof details address epistemic provenance traceability and assertion mediation soundness.
  • Conclusion: In 24 deterministic hand-authored cases, typed mediation passed none of 19 unsafe opportunities unqualified and passed all five supported controls.The suite validates encoded obligations but does not measure natural-language extraction or deployed retrieval and generation systems.
  • Proof basis: The provenance proof uses a finite acyclic graph and topological induction to establish finite dependency traces ending in recognized source artifacts or unavailable markers.Exact admitted versions and transitions remain inspectable at the accepted head.

A.2 Proof of Proposition 2 (Soundness of Assertion Mediation)

The proof establishes that mediated releases are assertion-bounded when candidate units are extracted, verified, and rendered through the governed pipeline. Failed units block the candidate, while status responses use policy-authorized views rather than raw witnesses.

  • Soundness conclusion: The proof analyzes a candidate response on a governed channel under context c and shows that every reached release satisfies BoundedLbio(zrel, c).The argument depends on the proof’s explicit assumptions and governed transition model.
  • Interception and semantic decomposition: Every governed-channel emission is intercepted and decomposed into uniquely identified content or status units under the stated extraction and typing assumptions.Each unit is bound to a structured query in Lbio.
  • Content assertions: The mediator emits content assertions only when support, exact matching, qualification, disclosure, and head-use checks all pass.Equation 17 supplies nonempty, policy-valid support for Supported results.
  • Status responses: Status units are rendered from policy-authorized views and released only when their decisions belong to the permitted render set and pass head-use checks.Equal views receive equal render sets, and policy-required indistinguishability is enforced through view mapping.
  • Soundness conclusion: Any semantic-unit verification failure blocks the candidate, and revision re-enters extraction, preventing bypass and ensuring every released unit satisfies its release relation.The proof concludes that the resulting release is bounded by Definition 2.

C Proposed End-to-End Evaluation Protocol and Tracks

The paper proposes an end-to-end adversarial evaluation protocol for long-term agent deployments, while reporting only a deterministic conformance suite for typed resolver and mediator behavior. The protocol spans provenance, privacy, temporal, conflict, invalidation, and emission-race concerns, with explicit falsification criteria and scope boundaries.

  • Evaluation scope: The proposed end-to-end study is not reported; the paper instead presents a seven-track adversarial evaluation design for long-term agent deployments.The design is described as a proposal rather than an executed end-to-end evaluation.
  • Baselines and ablations: The proposed baselines range from zero-shot parametric agents and flat memory stores to standard RAG, provenance-tagged retrieval, and state-bounded filtering.These configurations are intended to compare progressively stronger memory and provenance controls.
  • Falsification criteria: The architecture would be challenged by extraction misses beyond safety tolerance, excessive valid-query coverage loss, or a simpler rule matching safety and coverage at lower latency.Thresholds must be selected before the end-to-end study, and the conformance suite does not estimate them.
  • Conformance evaluation: The deterministic conformance suite evaluates the typed resolver and assertion mediator across 24 cases in six threat tracks, including corroboration requiring two independent roots.The fixture covers prompt injection, hallucinated origins, topology overlap, scope, erasure, temporal bounds, conflict, invalidation, supersession, and emission-head races.
  • Privacy and erasure: The protocol includes relational isolation, consent for cross-user disclosure, and asymmetric revocation that changes later projections without rewriting historical state.These rules define deployment-level privacy behavior for shared and private statements.
  • Privacy and erasure: Erasure treatment may retain non-sensitive lineage metadata after encrypted evidence becomes inaccessible, but legal compliance depends on jurisdiction, obligations, data model, and implementation.Affected nodes transition to Unavailable and derived claims are recomputed under Equation 22.
Loading 2609.02127v1…