LLMlambda 计算：人工智能代理、对话与信息流
The LLMbda Calculus: AI Agents, Conversations, and Information Flow
AI总结：
本文提出了一种无类型的lambda计算模型，用于形式化描述和验证人工智能代理中对话和信息流的安全性。
摘要：
与大型语言模型（LLM）的对话是一系列提示和响应的序列，每个响应都是从先前对话中生成的。人工智能代理自动构建此类对话：给定一个初始人类提示，规划循环会交错调用LLM和工具调用以及代码执行。这种紧密耦合创建了一个新且不为人知的攻击面。恶意提示注入到对话中可能会破坏后续推理，触发危险的工具调用，或扭曲最终输出。尽管这些系统至关重要，但我们目前缺乏一个原则性的语义基础来推理其行为和安全性。我们通过引入一种无类型的按值lambda计算，其包含动态信息流控制和少量用于构建提示-响应对话的基本原理来解决这一差距。我们的语言包含一个基本原理用于调用LLM：它将值序列化，将其发送给模型作为提示，并将响应解析为新的术语。该语言忠实表示规划循环及其漏洞，包括提示注入如何改变后续计算的机制。语义明确捕捉对话，因此支持推理关于防御措施，如隔离的子对话、生成代码的隔离以及信息流限制对LLM调用的影响。一个不关心终止的非干扰定理确立了完整性和保密性保证，证明了一个形式化计算可以为安全代理编程提供严谨的基础。
英文摘要：
Large language models are increasingly deployed as agents: they plan, call tools, read untrusted data, and act on the results. This exposes them to prompt injection: data meant only to be read is obeyed as an instruction. The most principled defences replace content inspection with provenance: classifying data by source and keeping trusted and untrusted apart through a separation of duty (the dual-LLM pattern) and information-flow control. Yet the leading systems are hard to fully trust: flow tracking is easy to get wrong, deliberate relaxations are hard to audit, and the dual-LLM pattern is hard-wired into the architecture. We present LLMbda, an untyped call-by-value lambda calculus that makes provenance-based defence both expressible and provably sound, without committing to an architecture. It adds the operational core of agentic systems as first-class constructs: prompt-response conversations that can be forked and cleared, code generation, and dynamic information-flow control in which every value carries a label that every reduction propagates. Isolation becomes a policy a program expresses, and reclassification an explicit, auditable construct. Our central result is a termination-insensitive probabilistic noninterference theorem over the whole calculus, including code-generating agents, with an insulated variant that holds even when the attacker chooses all untrusted inputs. The verified interpreter is itself the harness that calls the model, to our knowledge the first LLM agent harness whose executable is the subject of machine-checked security theorems, so every agent inherits the guarantee. On the AgentDojo banking benchmark, an agent built within LLMbda, enforcement always on, matches the utility of CaMeL, a leading dual-LLM defence, run without its policy checks (which halve its utility), and resists all but two of 1296 attacked runs. Our harness and all proofs are in Lean.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
