LACUNA：安全智能体作为递归程序插槽

TL;DR LACUNA 让 LLM agent 编写的代码直接融入运行时，同时通过**类型检查**保证每个动作整体原子执行，失败则安全回滚，兼顾表达力与安全。

问题

问题背景

LLM 代理（agent）越来越多地通过生成代码来行动，但 运行时（runtime）与模型代码之间长期存在分裂：运行时负责循环、上下文管理和控制流，而模型生成的代码只能表达一次性的工具调用或动作，无法影响运行时的行为。

现有方法局限

现有框架（如 ReAct 循环）将代理的思考-行动-观察流程硬编码在运行时中，模型无法改变循环策略或动态调整上下文；而直接让模型生成完整程序的做法，虽提升了表达能力，却急剧放大了安全风险：

• Prompt injection 可能使模型调用错误工具
• 部分执行失败会留下不一致的环境状态
• 代码中权限和数据流缺乏静态约束，容易越权访问

现有机制（如沙箱、事后审计）往往只能在执行后检测问题，缺乏编译期安全保证，无法在代码运行前阻止危险行为。

为什么这个问题难且重要

让模型代码塑造运行时（而非仅生成单步动作）是提升代理通用性和灵活性的关键，但技术挑战尖锐：

• 需要设计一种编程模型，在允许模型自由控制流的同时，通过类型检查、原子执行和能力作用域杜绝不安全代码的运行
• 必须在表达力与安全性之间找到平衡点，使工程师能信任代理在关键任务中长时间自主运行

业界对“安全代理”的呼声日益高涨，尤其在工具使用、多步推理和子代理协作场景中，缺少这样一站式的编程抽象会阻碍代理技术的落地。

行业类比

类似在复杂的自动化流水线中引入强类型、编译期检查的语言来取代随意拼接的脚本——Lacuna 为代理运行时提供了一张“安全网”，让模型能在约束内塑造控制流，而非无约束地运行代码。

核心洞察

• **LLM 代码生成与编译器门控的结合，将 agent 动作重构为带类型检查的递归程序“洞”，在运行时动态填洞并原子性地接受或拒绝整段生成代码**。与现有 agent 框架中模型仅能返回单个动作、运行时掌控循环和上下文的模式不同，LACUNA 让模型直接控制控制流和运行时行为，同时又通过编译时类型检查在代码执行前就拦截了错误工具调用、类型失配或不安全的数据流，避免了运行时状态污染。这种“先编译、后执行、失败则重试”的设计，把安全防线从运行时提前到了编译期，而不是依赖事后过滤或沙箱隔离。
• **LACUNA 的静态类型系统不仅用于代码正确性，更是能力安全（capability safety）的载体**。通过将工具使用建模为类型化权限，并利用作用域限定与信息流控制，LACUNA 能在编译时防止未经授权的操作和数据泄露，即使模型受到 prompt injection 攻击。这与传统基于沙箱或策略的访问控制不同——这些方法通常运行在更底层，缺乏类型系统与 agent 程序流的紧密集成，而 LACUNA 把权限检查直接编织进 agent 代码的类型推导中，使得安全的粒度更细且更可组合。

方法

核心思想

LACUNA 将 LLM 代理的每一次动作 建模为宿主程序中的一个 类型化空洞（typed hole），由模型生成代码填充并经过编译检查，从而让代理既能自由塑造运行时控制流，又不牺牲安全性。

输入与提示构造

当宿主程序执行到 agent[T](task) 调用时，系统将当前可用的 工具函数签名（类型化权限）、作用域内的数据、以及任务描述打包为 prompt 送入 LLM。T 明确约束了该空洞的期望返回类型。

关键模块与流程

1. 代码生成与填充

LLM 收到 prompt 后生成一段宿主语言（如 Scala 3）代码，该代码可包含任意控制流（条件、循环、并行分支），也可递归嵌套其他 agent 调用（子代理）。这相当于让模型拥有构造执行计划的完整权力，而非只能输出单个工具调用。

2. 类型检查与编译保护

生成的代码片段首先进行 编译时类型检查，主要规则包括：

• 返回类型必须与 T 匹配
• 所有使用的标识符已定义（无未定义名称）
• 无类型不匹配，满足空安全与模式匹配穷尽性
• 工具调用限制在当前作用域授予的能力（capability） 内，敏感数据可标记 classified 以实施信息流控制

若检查失败，该片段整体丢弃（零副作用），错误诊断信息回传 LLM 驱动重试，最多重试至预设上限。

3. 原子执行与状态一致性

通过检查的代码片段会被注入程序并原子执行：要么全部成功，要么任何步骤失败时回滚至执行前状态，避免工具调用中途崩溃导致环境残留。

输出

成功执行后得到类型为 T 的结果，流程继续；若达到最大重试仍失败，则向上传播错误。

模式的统一表达

ReAct 循环、技能库调用、多模型并行规划等模式，均可直接映射为循环、函数调用、并行结构等普通控制流，无需为每种模式维护独立的运行时引擎。

与同类方法的关键差异：传统框架（如 LangChain、AutoGPT）将控制流固化在外部运行时，模型仅生成工具指令；LACUNA 将运行时塑造权归还给 模型生成的代码，同时借助宿主语言的类型系统提供编译时安全保障，实现了表达力与安全性的深度统一，且天然支持递归组合与信息流控制。

实验

实验设计

实验在三个主要测试集上进行：类型系统保护测试用例（验证编译时拒绝不安全代码的能力）、BrowseComp-Plus（复杂工具使用基准）和 τ²-bench（多轮对话基准，含 392 个任务）。此外，还通过提示注入场景评估能力安全。代理使用一款强大 LLM 生成代码填充 agent[T] 调用；执行前进行静态类型检查，失败则返回编译错误并触发重试，保证每次操作原子执行。

关键发现

• 在 BrowseComp-Plus 上，代理达到 27.1% 准确率，同时 8.6% 的生成在类型检查阶段被拒绝，避免潜在危险执行；平均每查询仅需 0.7 次重试即修复错误。
• 在 τ²-bench 的四个领域共 392 个任务中，LACUNA 解决了 76.0%，与基线代理（如标准 ReAct 循环）性能持平。
• 安全测试表明，类型检查能拦截未定义变量、类型不匹配、空指针等错误，且在提示注入攻击下，代理无法访问超出授权范围的工具或数据，实现了能力范围与信息流控制。

与基线对比解读

在 τ²-bench 上与基线持平，证实安全机制未引入显著性能退化。重试机制利用编译器级反馈使代理能快速恢复，平均重试次数接近零。BrowseComp-Plus 上虽无直接基线，但 8.6% 的拒绝率暗示类型系统对合法操作误拒率低，且代理可通过重试解决大部分问题。整体上，LACUNA 将代理行为纳入程序语言层级的类型安全保障，为构建可信自治代理提供了扎实基础。

行业影响

落地场景

LACUNA 为需要 LLM agent 自主完成多步工具调用与状态变更的场景提供了安全编程范式。典型用例包括：

• 电商智能客服：处理退货流程时，agent 需依次查询订单、调用支付退款、更新库存，LACUNA 的类型检查与原子性保证可防止“已退款但库存未恢复”等不一致状态，避免直接经济损失。
• 金融合规审查：agent 对交易流进行多源交叉验证，需组合查询账户信息、黑名单筛查、风险评分。LACUNA 的信息流控制可确保标记为机密的客户数据不会经模型代码意外外泄，满足合规要求。

商业价值

核心价值在于降低安全风险与人工干预成本。传统 agent 框架中，模型生成的代码可能因提示注入或逻辑错误破坏业务状态，大规模部署时需额外投入人工审核。LACUNA 在编译阶段即可拦截类型错误与越权访问，将拒绝执行的比例控制为 8.6%（BrowseComp-Plus），平均仅需 0.7 次重试，显著减少线上故障。对于金融、医疗等强监管行业，这一机制可加速自动化审批流程，直接降低合规审计的人力开销。

与现有产品/工作流的接口

LACUNA 可嵌入现有 agent 框架（如 LangChain、AutoGen）作为安全执行沙箱，替代原有的无校验代码执行步骤。在技术栈方面，对静态类型语言（如 Scala 3）可原生集成，利用 agent[T](task) 原语将 agent 动作声明为类型化 hole；对于 Python 等动态语言，可通过类型注解与 ML 编译器前端实现类似静态检查。企业可逐步引入：先行在关键交易链路上用 LACUNA 包装需要原子性的工具群，再扩展至全链路 agent 编排。

局限

• **类型安全不等同于语义正确性**：LACUNA 通过完善的类型系统确保代码在编译期无类型错误，并限制工具使用与数据流，但正如文中所述 “well-typed is not correct” ，通过类型检查的代码仍可能产生错误的工具组合、逻辑漏洞或不安全副作用。代理的表现本质上受限于底层 LLM 的编码能力，在复杂任务中若模型生成的代码语义有误，类型系统无法检测。因此，实际落地时仍需结合运行时监控或分层防御，不能仅依赖编译期检查。
• **对宿主语言与基础设施的强依赖**：该工作基于 Scala 3 的宏系统和 `eval` 原语实现，依赖 JVM 生态的类型化编程范式。这使其难以直接移植到当前主流的 Python 代理框架中，对现有 AI 工程栈的兼容性构成显著障碍。编译与类型检查步骤增加了每次代理动作的延迟，在需要低延迟响应的交互场景中可能成为瓶颈，其工程技术门槛可能限制大规模社区验证与采纳。
• **评测范围有限，动态攻击防御待深入**：实验仅在 BrowseComp-Plus 和 τ²-bench 两个基准上测试，BrowseComp-Plus 准确率仅 27.1%，未充分展示在更开放、多变真实任务中的泛化能力。论文展示了基于静态作用域的权限控制与信息流保护，但对更复杂的动态攻击向量（如数据投毒、多步协同攻击）的防御效果未充分验证。同时，终止分析与资源使用控制方面的讨论仅停留在理论层面，缺乏系统实验评估。