为大模型流水线构建可验证的信任边界，确保关键环节的确定性计算安全。
Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture
- 用形式化证明证书验证流水线外围计算，而非模型本身
- 三类证书覆盖对抗扰动、嵌入敏感性和代理行为可靠性，支持高风险应用
- 提供可审计的残差最大值和分层稳定性定理，适合金融、医疗等严苛场景
我们提出一个框架，用于验证大型语言模型流水线外围的确定性结构化计算，而非模型本身。该框架扩展了 Lean 4 的信任边界架构，适配现代 LLM 流水线的通用接口。证书有效性由 Lean 4 内核类型检查及无 sorry 的传递公理审计构成，仅依赖于受信集合 {propext, Classical.choice, Quot.sound}；其余假设按层级划分（数学占位符、密码学假设、机器/人类预言）。技术贡献包括三类本地证书与两个操作算子：冲突感知双格基底（附发射门保真引理）、嵌入敏感性与改写稳定性、霍尔风格代理行为。操作算子包括最大可验证残差（将放弃请求转为最高权重可证残差，并记录审计日志），以及组合稳定性定理（从每层增益与余量推导出全管道扰动预算的闭式解）。三类证书与通用保证卡合并器构成高风险部署的每次调用交付物，适用于专利与法律检索、受监管金融、临床决策支持及具有不可逆副作用的智能体系统。已编译的 Lean 4 参考实现（Lean v4.30.0-rc2，Mathlib）涵盖全部 22 种证书类型，其中 17/46 内核声明无公理依赖，其余仅依赖受信集与明示假设，且无使用 sorryAx 或 Lean.ofReduceBool。三类证书通过四项注册试点验证：在对抗扰动的 HotpotQA 上测试双格基底，在短/长文本设置中评估嵌入敏感性，在带对抗提示注入的文件系统沙箱中验证霍尔风格代理行为。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。