AI RESEARCH
Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture
arXiv CS.CL
•
ArXi:2605.16407v1 Announce Type: cross 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.