LLM Agent 提示注入的相对安全性：机械化定义、防御与判定

Brijesh Dongol 的论文提出 PlanTERS 框架，以相对参考 Agent 的方式定义 LLM Agent 面对提示注入时的安全性：参考 Agent 在相同运行时监控下执行相同计划，但所用模型从不服从不可信内容；如果一个 Agent 的每次泄漏都是参考 Agent 已经存在的泄漏，那么就称该 Agent 相对安全。论文给出围栏定理，证明在首次读取不可信内容时撤销可注入工具且不再恢复，可以使有限运行中的所有计划在事件层面相对安全；这一结论的条件是每次注入为单次调用，且模型按预先固定的时间表服从，并可在公平性条件下扩展到可能无限的运行。作者在 Isabelle/HOL 中证明或反驳带围栏、预算、审批、循环和双 LLM 的 Agent 的相对安全性。