LACUNA：作为递归程序洞的安全智能体 LACUNA: Safe Agents as Recursive Program Holes
将LLM智能体动作建模为类型化的程序洞，通过静态类型系统和capability checking保障安全
前置知识
类型化洞（Typed Hole）
在编程语言中，typed hole 是一个占位符，表示程序中某个位置需要一个特定类型的值，但该值尚未提供。编译器知道此处期望的类型，可以根据上下文推导出需要填充什么。在开发工具中，这常用于代码补全，编辑器会根据 hole 的类型和周围上下文建议可能的填充内容。LACUNA 将这一概念运行时化，让 LLM 在程序运行时填充这些洞。
LACUNA 的核心思想就是将 agent 的每个动作视为一个 typed hole，类型 T 约束了模型必须产生的结果形状，这是整个安全机制的基础。理解 typed hole 概念有助于理解为什么 LACUNA 可以在执行前拒绝不符合类型约束的代码。
Capability（能力/权限）
在对象能力模型中，capability 是一个不可伪造的值，代表对特定效果或资源的授权。例如文件句柄、网络套接字、logger 等都是 capabilities。代码只能通过持有对这些值的引用才能执行相应的效果。Capabilities 只能通过显式传递而传播，不能从无到有地创建。这不同于操作系统级别的权限位，后者是全局的、非词法作用域的。
LACUNA 的安全性依赖于 capability 安全模型。通过捕获检查（capture checking），编译器可以追踪哪些 capabilities 可以在代码的某个位置被使用。生成的代码只能访问其词法作用域中已有的 capabilities，这构成了最小权限原则的实现。
Capture Checking（捕获检查）
Scala 3 的一项语言特性，用于追踪类型中携带的 capabilities。一个类型的形式为 T^{x1, ..., xn}，表示该类型的值可能使用 capabilities x1 到 xn。空捕获集表示纯值（不使用任何 capability）。函数类型会记录其体中使用的 capabilities，例如 (String => Unit)^{f} 表示该函数使用 capability f。编译器会检查 capability 是否在其允许的作用域内使用，防止权限泄露。
这是 LACUNA 安全性的核心技术支撑。通过 capture checking，LACUNA 可以保证生成的代码只能使用其作用域中已有的 capabilities，并且不能将这些 capabilities 带出作用域。这防止了 prompt injection 攻击导致的权限提升。
Code-as-Action（代码即动作）
一种 LLM agent 设计范式，与传统的工具调用相对。在工具调用中，模型每次只能调用一个预定义的工具；而在 code-as-action 中，模型编写代码作为其动作。这些代码可以组合多个工具、解析中间结果、进行分支和循环等。ReAct 是工具调用的代表，而 code-as-action 提供了更强的表达能力。
LACUNA 属于 code-as-action 范式，但与现有的 code-as-action 系统不同，它将模型编写的代码作为宿主程序的一部分进行静态类型检查。理解这一背景有助于理解 LACUNA 与其他 agent 框架的区别和优势。
研究动机
现有的 LLM agent 框架存在根本性的分裂：运行时控制着循环、上下文和控制流，而模型只能逐个发出工具调用，对整体结构几乎没有发言权。ReAct 模式让模型在推理和工具调用之间交替，但运行时仍然拥有控制权。虽然 code-as-action 代理让模型编写代码来组合工具、解析结果、分支和循环，但它们仍然保持着一个清晰的分裂：运行时拥有循环、上下文和动作分发，模型只提供下一个片段。这种分裂限制了 agent 的表达能力。更重要的是，当模型编写的代码只是表达单个动作时，运行时可以限制其影响；但一旦代码开始塑造运行时本身，攻击的影响范围就大大扩展了。现有的安全防御（沙箱、受限解释器、策略语言、输入硬化等）都是零散的，没有在代码开始执行前对整个生成的动作进行检查。
本文的目标是LACUNA 的目标是在提升 agent 表达能力的同时保障安全性。具体来说，作者希望实现：让模型编写的代码可以作为宿主程序的一部分运行，充分利用宿主语言的控制流和组合能力；在代码执行前对其进行完整的静态类型检查和 capability 检查；拒绝不符合约束的代码片段，确保只有通过检查的代码才会执行；支持递归的 agent 调用，让常见 agent 模式（ReAct 循环、子 agent、技能、多模型规划等）可以用普通的控制流表达。
与已有工作不同的是，LACUNA 的独特切入角度在于：将 agent 的每个动作建模为宿主程序中的一个类型化洞，而不是将 agent 视为一个外部实体。这与递归语言建模（RLM）最接近，但有两个关键改进：第一，RLM 的 REPL 在不检查的情况下运行生成的代码，可能导致部分执行和环境不一致，而 LACUNA 在运行前在实时的词法作用域中进行类型检查；第二，RLM 将编排和控制流保留在运行时中，而 LACUNA 让生成的代码本身编写控制流。与其他语言集成的 LLM 框架（如 LMQL、DSPy）相比，LACUNA 不是约束采样器或解析输出，而是让编译器的错误消息驱动重试，并且组合由生成的代码本身通过 agent 原语的控制流表达。
核心方法
LACUNA 提出了一个简单的原语 agent[T](task)，其中 T 是期望的结果类型，task 是自然语言任务描述。当执行到达这个调用时，LLM 会填充类型为 T 的代码，该代码在调用点的周围程序上下文中编译和执行。如果代码可以证明产生类型 T 的值，它就会运行；否则，编译器的错误会作为反馈用于重试。生成的代码是普通的宿主语言代码（Scala 3），不是单个工具调用。它可以使用工具、处理数据，并再次请求模型帮助。核心思想是将模型调用放在需要其结果的程序点，让调用者声明期望的结果类型。原型使用 Scala 3，因为它支持两个基础：在周围程序上下文中编译新片段，以及跟踪该片段可以使用的资源。
LACUNA 的核心创新点在于将 agent 动作作为宿主程序中的类型化洞，而不是单独的 action。这意味着模型编写的代码在宿主程序的词法作用域中进行静态类型检查，并且只有通过检查的代码才会执行。这与现有方法的本质区别在于：现有的 code-as-action agent 保持运行时和生成代码之间的清晰分裂，而 LACUNA 让生成的代码成为运行时的一部分；现有的方法只在执行时或工具级别进行检查，而 LACUNA 在执行前对整个生成的动作进行编译级别的检查，具有原子性——要么全部接受，要么全部拒绝。通过 Scala 3 的 capture checking，LACUNA 还可以追踪和控制生成的代码可以使用的 capabilities，实现最小权限原则。
方法步骤详情
LACUNA 的工作流程分为四个步骤：第一，重写（Rewrite）。编译器将 eval 调用（或 agent 这样的 evalLike 包装器）扩展为长形式，自动填充三个上下文参数：bindings（作用域内变量及其运行时值）、expectedType（类型 T 写回为文本）、enclosingSource（标记调用点位置的周围代码文本）。第二，拼接（Splice）。在运行时，拼接器解析源字符串并将其放入 enclosing-statement 文本中的占位符处，生成一个完整的顶层语句。第三，重新编译（Recompile）。拼接后的源代码被传递给编译器的新实例，配置与原始编译相同的选项（包括相同的效果和 capability 检查）。类型检查、capture 检查和错误报告都是编译器对任何程序应用的常规检查。第四，提取（Extract）。如果代码编译成功，编译器会生成一个类文件，包含一个评估拼接代码并返回其结果的方法。这个类文件被加载到运行的程序中。第五，评估（Evaluate）。新编译的代码在程序的原始执行上下文中评估，产生类型为 T 的值，eval 返回给调用者。对于 agent[T](task)，还会在失败时将编译器的诊断反馈给 LLM 进行重试，直到成功或达到最大尝试次数。
技术新颖性
LACUNA 的技术新颖性体现在多个方面：首先，它实现了真正的递归代码生成——生成的代码可以再次调用 agent，每次调用都在更丰富的上下文中进行，因为外部调用已经定义了中间值、注释和控制流结构。其次，它将 agent 的安全保证完全建立在宿主语言的类型系统上，而不是单独的安全检查器。未定义的名称、类型不匹配、模式非穷尽性、显式空值等问题都会在执行前被捕获。第三，通过 capture checking，LACUNA 实现了 capability 安全和信息流控制，防止了 prompt injection 攻击导致的权限提升和数据泄露。第四，常见的 agent 模式（ReAct 循环、技能、子 agent、并行推理、多模型规划等）都可以用普通的控制流表达，而不需要框架级别的特殊支持。最后，LACUNA 的实现通过在运行的程序中调用编译器本身来拼接和重新编译，这在静态类型语言中是一个重要的技术挑战。
实验结果
LACUNA 在多个维度上进行了评估。首先，在一个包含约 400 个测试用例的集合中，验证了类型系统的保证对宿主代码和生成的代码都有效。每个测试用例将宿主代码与片段配对，片段要么格式良好（应该编译并评估为期望值），要么以 agent 常见的方式格式错误（应该在运行前被拒绝）。所有测试都通过，确认实现按预期工作。其次，在 BrowseComp-Plus 上，deepseek-v4-flash 达到 27.1% 的准确率，gemini-3.1-flash-lite 达到 26.2%，gpt-5.4-mini 只有 9.2%。每次查询平均 0.7 次重试，三分之二的查询不需要重试，端到端的编译成功率为 91.4%。编译器拒绝了 8.6% 的生成，并且没有不符合类型或超出范围的动作到达语料库。平均 5.9 轮、每次查询 15.5 次搜索。第三，在 τ²-bench 的 392 个任务上，deepseek-v4-flash 解决了 76.0% 的任务（零售 58.8%、航空 70.0%、电信 88.6%、电信工作流 83.3%），平均 5.7 个用户轮次和每次任务 26.7 个工具调用。与参考工具调用 agent 相当。零售领域平均 7.1 次重新生成，恢复到 77.6% 的端到端编译成功率。对话代码比单轮研究代码更容易出错（零售领域 deepseek-v4-flash 的 22.4% 生成被拒绝，而 BrowseComp-Plus 上只有 8.6%）。最后，在对抗性评估中，LACUNA 在四个 AgentDojo 域（银行、工作空间、Slack、旅行）上表现良好。对于 gemini-2.5-pro，LACUNA 的实用性得分从 52.8% 提升到 63.19%（银行），从 53.8% 提升到 56.25%（工作空间），从 48.6% 提升到 42.86%（Slack），从 1.4% 提升到 63.57%（旅行）。攻击成功率总体很低，但仍有少量注入试验成功（例如工作空间域 4/560，Slack 域 2/105，旅行域 1/140）。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| BrowseComp-Plus 信息检索 | 准确率（judge 评分） | 27.1% | N/A（本研究旨在展示通用性，而非top leaderboard） | deepseek-v4-flash 驱动多步研究，每次查询平均 0.7 次重试 |
| τ²-bench 客户服务对话 | 解决率（Overall） | 76.0% | 90.0%（工具调用参考 agent） | 相当，但类型系统保证安全 |
| τ²-bench 电信领域 | 解决率 | 88.6% | 100.0%（工具调用参考 agent） | 略低但相当 |
| AgentDojo 对抗测试（gemini-2.5-pro） | 实用性（银行） | 63.19% | 52.8%（CaMeL） | +10.39 百分点 |
局限与改进
LACUNA 有几个重要的局限性。首先，类型良好的代码不一定是正确的代码。编译器只检查生成的片段是否具有期望的静态类型并尊重作用域中的 capabilities，但不检查片段是否做正确的事情。一个类型良好的片段仍然可以实现错误的算法、调用错误的工具，或返回合理但不正确的值。重试循环只在编译器拒绝片段时才重新生成，因此编译通过的片段无论语义是否正确都会运行。其次，权限的严格程度仅取决于授予的作用域。capability 保证限制了生成的片段可以执行的效果和可以使用的数据，但它们不阻止模型被注入内容影响。它们只限制这种影响可以到达的内容。如果洞被过度提供不需要的 capabilities，攻击面就会重新打开。因此，最小权限作用域是开发者必须提供的属性：类型系统强制执行它但不推断它。第三，对模型编码能力的依赖。因为被拒绝的片段从不运行，所以无论模型能力如何，安全保证都有效；但进度只有在模型能将其预期动作表达为类型良好的宿主代码时才会取得。在实验中，gemini-3.1-flash-lite 在零售领域只有 3.2% 的片段被拒绝，但在更难的电信领域 89% 被拒绝，其代码生成能力下降。部分差距可能是由于 Scala 在预训练数据中的代表性不如 Python（code-as-action agent 的常用语言）。最后，延迟和成本。每个 agent 调用都要支付一次模型完成和至少一次编译器传递，嵌套递归会堆叠两者。每次重试都会增加一次完成和传递，因此成本随拒绝率而变化。
独立分析的弱点
LACUNA 的第一个弱点是语义正确性的缺失。类型系统保证形状和权限但不保证正确性，一个类型良好但语义错误的片段仍然会执行，可能造成不良后果。改进方向是引入精化类型（refinement types），让期望类型 T 携带精化谓词（例如整数在边界内、固定长度的列表、连接输入和输出的关系不变量），这样契约不仅约束结果的形状，还约束其属性。第二个弱点是 Scala 在预训练数据中的代表性可能不如 Python，导致模型生成 Scala 代码的能力较弱。改进方向是对模型进行专门的 Scala 代码生成微调，或使用更擅长 Scala 编码的模型。第三个弱点是延迟和成本。每次 agent 调用都需要编译器传递，嵌套递归会堆叠。改进方向包括缓存编译结果（对于生成一次并重复使用的函数类型洞）、增量编译、或者将编译器优化为更轻量级的形式。第四个弱点是终止和资源使用。递归深度、燃料和挂钟或内存限制不是类型级别的属性。改进方向是引入类型级别的资源消耗分析，但这仍然是一个开放的研究问题。
未来方向
作者提出的未来工作方向包括：精化类型化的洞——让期望类型 T 携带精化谓词，以进一步打开验证解码的大门，引导生成向可证明满足谓词的值发展。这将缩小形状正确和语义正确之间的差距。另一个方向是支持更多静态类型宿主语言。目前的原型依赖于 Scala 3 的 capture checking 和在运行的程序中调用编译器的 hook，但这些都不是基础的。只要静态类型宿主可以跟踪效果或 capabilities，并可以从运行的程序中重新编译代码并在调用点暴露实时的上下文，设计就可以移植。作者还提到可以探索更丰富的宿主语言特性，如依赖类型、线性类型等，以提供更强的保证。最后，可以探索更高效的重试策略，例如根据编译器错误的类型和频率调整提示或尝试不同的采样参数。
复现评估
LACUNA 的实现计划在 Apache License 2.0 下开源。实验使用的基准（BrowseComp-Plus 和 τ²-bench）都在 MIT 许可下开源。作者计划贡献约 400 个测试用例到 Scala 3 编译器自己的测试套件中，作为 REPL 测试，因此每个案例都练习真实的管线（解析、类型检查、capture 检查）。所有模型都是托管的端点（deepseek-v4-flash、gemini-3.1-flash-lite、gpt-5.4-mini、gpt-4.1、gpt-5.4），通过提供商的 API 访问，作者故意使用较小的、低成本的层级作为 agent。没有进行训练或微调，因此所有模型使用都是推理。唯一的本地计算是 BrowseComp-Plus 检索索引和每个 agent 调用触发的 Scala 编译器传递。每次运行的资源预算有上限（每次 BrowseComp-Plus 查询 600 秒挂钟限制和深度 128 限制，τ²-bench 上的每任务限制）。因为所有模型都是托管的端点，实验不需要本地 GPU。总的来说，复现难度中等，需要 Scala 3.9.0 编译器、LLM API 密钥和基准数据集。
论文图表