Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture

• URL: http://arxiv.org/abs/2605.16407v1
• Date: Wed, 13 May 2026 12:01:41 GMT
• Title: Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture
• Abstract summary: We present a framework for verifying the deterministic structured computations surrounding a large language model.<n>We extend a Lean 4 trust-boundary architecture to the generic interfaces of modern LLM pipelines.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present a framework for verifying the deterministic structured computations surrounding a large language model rather than the model itself, extending a Lean 4 trust-boundary architecture to the generic interfaces of modern LLM pipelines. Certificate validity is a Lean 4 kernel type-check plus a sorry-free transitive axiom audit against the trusted set {propext, Classical.choice, Quot.sound}; other assumptions are declared and partitioned by tier (mathematical placeholders, cryptographic assumptions, ML/human oracles). The technical contribution comprises three local certificate families and two operators. The families are conflict-aware bilattice grounding (with an emission-gate soundness lemma), embedding sensitivity and paraphrase stability, and Hoare-style agent action. The operators are a Maximal Certifiable Residue, which turns abstention into the maximum-weight certifiable residue with audit-logged dropped claims, and a Compositional Stability theorem, which yields a closed-form pipeline-wide perturbation budget from per-layer gains and margins. The three families plus a Universal Assurance Card consolidator form the per-call deliverable for high-stakes deployments: patent and legal retrieval, regulated finance, clinical decision support, and agentic systems with irreversible side effects. A compiled Lean 4 reference artifact (Lean v4.30.0-rc2, Mathlib) covers all 22 certificate types, with 17 of 46 kernel-audited declarations axiom-free, the rest depending only on the trusted set and declared assumptions, and zero uses of sorryAx or Lean.ofReduceBool. The three families are empirically tested through four registered pilots: bilattice grounding on adversarially perturbed HotpotQA, embedding sensitivity in short- and long-form settings, and Hoare-style agent action on a filesystem sandbox with adversarial prompt injection.

Related papers

• Runtime Observability for Heterogeneous Attention Memory [20.158719055939383]
  We give a runtime observability contract that covers all four memory classes with three operators.<n>We compose the per-stage stack into an executable request-level risk ledger.
  arXiv  Detail & Related papers  (2026-08-06T10:41:50Z)
• ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers [77.95933562142014]
  ITPEval is the first benchmark for evaluating automated formal proof translation across four major ITPs.<n>We release itpeval, a unified multi-ITP verification infrastructure with state-isolated warm backends.
  arXiv  Detail & Related papers  (2026-07-07T22:05:55Z)
• From Sparse Features to Trustworthy Proxies: Certifying SAE-Based Interpretability [53.681678236115836]
  We study when can an SAE-based explanation be treated as a faithful view of an underlying frozen LM.<n>Our framework derives an upper bound on the base model's expected risk using four measurable quantities.<n>We show that the bound becomes non-vacuous on GPT-2 Small, Gemma-2B, and Llama-3-8B at practical sample sizes.
  arXiv  Detail & Related papers  (2026-06-16T18:28:23Z)
• Methods for Formal Verification of Agent Skills: Three Layers Toward a Mechanically Checkable Capability-Containment Proof [0.0]
  We give a precise semantics for skill behaviour faithful to how a skill is consumed by an LLM-driven runtime.<n>We present three composable methods that together raise a skill from declared or tested to formal.<n>All three methods plus the bundle producer and re-checker ship as zero-dependency JavaScript modules in the open-source enclawed framework.
  arXiv  Detail & Related papers  (2026-05-09T19:27:38Z)
• Certified Purity for Cognitive Workflow Executors: From Static Analysis to Cryptographic Attestation [0.0]
  A prior three-layer governance architecture proves governance completeness, provenance completeness, and the impossibility of ungoverned effects.<n>This paper closes the gap through four mechanisms.<n>We prove four theorems: structural purity by construction, bypass elimination for all five BEAM bypass classes, certificate integrity, and gate completeness.
  arXiv  Detail & Related papers  (2026-05-01T19:04:37Z)
• GSAR: Typed Grounding for Hallucination Detection and Recovery in Multi-Agent LLMs [0.0]
  We present a groundedness framework that partitions claims into a four-way typology (grounded, ungrounded, contradicted, complementary)<n>GSAR is the first published groundedness framework coupling evidence-typed scoring with tiered recovery under an explicit compute budget.
  arXiv  Detail & Related papers  (2026-04-25T16:20:28Z)
• Trust but Verify: Introducing DAVinCI -- A Framework for Dual Attribution and Verification in Claim Inference for Language Models [53.279391576560755]
  Large Language Models (LLMs) have demonstrated remarkable fluency and versatility across a wide range of NLP tasks, yet they remain prone to factual inaccuracies and limitation.<n>This poses significant risks in high-stakes domains such as healthcare, law, and scientific communication, where trust and verifiability are paramount.<n>We introduce DAVinCI - a Dual Attribution and Verification framework designed to enhance the factual reliability and interpretability of LLM outputs.
  arXiv  Detail & Related papers  (2026-04-23T01:37:50Z)
• Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
  We present a formally verified framework for patent analysis as a hybrid AI + Lean 4 pipeline.<n>The DAG-coverage core (Algorithm 1b) is fully machine-verified once bounded match scores are fixed.<n>Claims are encoded as DAGs in Lean 4, match strengths as elements of a verified complete lattice, and confidence scores propagate through dependencies via proven-correct monotone functions.
  arXiv  Detail & Related papers  (2026-04-20T22:02:57Z)
• Claw-Eval: Toward Trustworthy Evaluation of Autonomous Agents [66.97968363332465]
  We introduce Claw-Eval, an end-to-end evaluation suite addressing all three gaps in agent benchmarks.<n>Claw-Eval comprises 300 human-verified tasks spanning 9 categories across three groups.<n>Every agent action is recorded through three independent evidence channels.
  arXiv  Detail & Related papers  (2026-04-07T17:43:18Z)
• Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving [0.0]
  This paper presents the Lean-Agent Protocol, a formal-verification-based AI guardrail platform.<n>Every proposed agentic action is treated as a mathematical conjecture.<n>This architecture provides cryptographic-level compliance certainty at microsecond latency.
  arXiv  Detail & Related papers  (2026-04-01T23:39:43Z)
• Towards Comprehensive Stage-wise Benchmarking of Large Language Models in Fact-Checking [64.97768177044355]
  Large Language Models (LLMs) are increasingly deployed in real-world fact-checking systems.<n>We present FactArena, a fully automated arena-style evaluation framework.<n>Our analyses reveal significant discrepancies between static claim-verification accuracy and end-to-end fact-checking competence.
  arXiv  Detail & Related papers  (2026-01-06T02:51:56Z)
• Eigen-1: Adaptive Multi-Agent Refinement with Monitor-Based RAG for Scientific Reasoning [53.45095336430027]
  We develop a unified framework that combines implicit retrieval and structured collaboration.<n>On Humanity's Last Exam (HLE) Bio/Chem Gold, our framework achieves 48.3% accuracy.<n>Results on SuperGPQA and TRQA confirm robustness across domains.
  arXiv  Detail & Related papers  (2025-09-25T14:05:55Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  Large language models (LLMs) are increasingly integrated into real-world personalized applications.<n>The valuable and often proprietary nature of the knowledge bases used in RAG introduces the risk of unauthorized usage by adversaries.<n>Existing methods that can be generalized as watermarking techniques to protect these knowledge bases typically involve poisoning or backdoor attacks.<n>We propose name for harmless' copyright protection of knowledge bases.
  arXiv  Detail & Related papers  (2025-02-10T09:15:56Z)
• SORRY-Bench: Systematically Evaluating Large Language Model Safety Refusal [64.9938658716425]
  SORRY-Bench is a proposed benchmark for evaluating large language models' (LLMs) ability to recognize and reject unsafe user requests.<n>First, existing methods often use coarse-grained taxonomy of unsafe topics, and are over-representing some fine-grained topics.<n>Second, linguistic characteristics and formatting of prompts are often overlooked, like different languages, dialects, and more -- which are only implicitly considered in many evaluations.
  arXiv  Detail & Related papers  (2024-06-20T17:56:07Z)

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.