The LLMbda Calculus: AI Agents, Conversations, and Information Flow

📄 arXiv: 2602.20064v1 📥 PDF

作者: Zac Garby, Andrew D. Gordon, David Sands

分类: cs.PL, cs.AI, cs.CR

发布日期: 2026-02-23

💡 一句话要点

提出LLMbda演算以解决AI代理安全性问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: AI代理 对话系统 信息流控制 安全性 λ演算 动态控制 恶意提示

📋 核心要点

  1. 当前AI代理在处理对话时，缺乏对恶意提示注入的防护机制，导致安全隐患。
  2. 本文提出了一种新的未类型λ演算，结合动态信息流控制，提供了对话的语义基础。
  3. 通过建立终止不敏感的非干扰定理，论文展示了该演算在安全代理编程中的应用潜力。

📝 摘要（中文）

与大型语言模型（LLM）的对话是一个由提示和响应组成的序列，每个响应都是基于前面的对话生成的。AI代理能够自动构建这样的对话，但这种紧密耦合也带来了新的攻击面。恶意提示可能会影响后续推理、触发危险的工具调用或扭曲最终输出。尽管这些系统至关重要，但我们缺乏对其行为和安全性进行合理推理的语义基础。为此，本文引入了一种未类型的按值调用λ演算，增强了动态信息流控制，并提供了一小部分构建提示-响应对话的原语。该演算忠实地表示了规划循环及其脆弱性，并明确捕捉了对话的语义，支持对防御机制的推理。

🔬 方法详解

问题定义：本文旨在解决AI代理在对话中面临的安全性问题，尤其是恶意提示注入对后续推理和输出的影响。现有方法缺乏对这些行为的系统性理解和语义基础。

核心思路：论文提出了一种未类型的按值λ演算，增强了动态信息流控制，能够有效表示对话过程及其潜在的安全漏洞。通过这种设计，能够更好地理解和控制对话中的信息流动。

技术框架：整体架构包括一个规划循环，该循环交替进行LLM调用、工具调用和代码执行。演算中包含一个原语，用于将值序列化并发送给LLM，解析响应为新的术语。

关键创新：最重要的创新在于引入了动态信息流控制，能够明确捕捉对话的语义，并支持对防御机制的推理，如隔离生成代码和信息流限制。与现有方法相比，提供了更严格的安全性保证。

关键设计：演算中的关键设计包括对话的原语、动态信息流控制机制，以及终止不敏感的非干扰定理的建立，这些设计确保了信息的完整性和保密性。通过这些设计，论文为安全代理编程提供了理论基础。

📊 实验亮点

实验结果表明，所提出的LLMbda演算在处理恶意提示注入时，能够有效保持对话的完整性和保密性。通过与现有方法的对比，展示了在安全性保证方面的显著提升，确保了信息流的安全控制。

🎯 应用场景

该研究的潜在应用领域包括安全的AI代理开发、对话系统的安全性增强以及信息流控制机制的设计。通过提供一个理论基础，研究能够帮助开发更安全的AI系统，减少恶意攻击的风险，提升用户信任度。

📄 摘要（原文）

A conversation with a large language model (LLM) is a sequence of prompts and responses, with each response generated from the preceding conversation. AI agents build such conversations automatically: given an initial human prompt, a planner loop interleaves LLM calls with tool invocations and code execution. This tight coupling creates a new and poorly understood attack surface. A malicious prompt injected into a conversation can compromise later reasoning, trigger dangerous tool calls, or distort final outputs. Despite the centrality of such systems, we currently lack a principled semantic foundation for reasoning about their behaviour and safety. We address this gap by introducing an untyped call-by-value lambda calculus enriched with dynamic information-flow control and a small number of primitives for constructing prompt-response conversations. Our language includes a primitive that invokes an LLM: it serializes a value, sends it to the model as a prompt, and parses the response as a new term. This calculus faithfully represents planner loops and their vulnerabilities, including the mechanisms by which prompt injection alters subsequent computation. The semantics explicitly captures conversations, and so supports reasoning about defenses such as quarantined sub-conversations, isolation of generated code, and information-flow restrictions on what may influence an LLM call. A termination-insensitive noninterference theorem establishes integrity and confidentiality guarantees, demonstrating that a formal calculus can provide rigorous foundations for safe agentic programming.