PerMIT: 基于机器验证定理的LLM Agent持久内存安全架构

该论文提出 PerMIT 架构，旨在解决持久内存作为未受保护的攻击面问题，防止数据注入和投毒风险阻碍智能体间的内存共享。其核心机制基于显式信任假设：仅信任用户输入的原始数据和经网关确认的值。系统通过有限内存接口中介所有不可信的环境衍生值，在保留智能体驱动的多轮规划与工具选择能力的前提下，确保环境数据仅在网关确认后才能影响敏感操作。 研究团队在 Lean 4 中形式化并机器检查了两个完整性定理，证明环境衍生的内存数据只有在网关处被确认后才会到达敏感动作，且对智能体行为的影响仅限于网关显示的内容。这种设计将威胁模型中的每种攻击简化为单个可审计决策，可由人类、LLM 验证器或两者共同执行。在 Trojan Hippo 基准测试中，结合自验证与轻量级验证器，PerMIT 实现了零攻击成功率。此外，系统支持社区信任积累机制：每次确认都是对具体内容的记录，随着用户增多，高置信度项目可成为社区确认项而无需重复验证。 模拟结果证实了协同扩展属性：随着社区规模扩大，推广恶意知识或错误驱逐良性知识的风险下降，而单用户的验证成本并未增加。在 tau^2-bench 上，多达 90 个自主智能体利用 PerMIT 构建共享知识库，期间未发生直接内存注入，且生成的知识显著提升了新智能体在未见过任务上的表现。事实部分基于论文声明的 Lean 4 证明与仿真数据；推断部分认为该架构可能推动测试时自我改进的智能体发展；猜测部分涉及大规模社区部署后的实际信任演化路径，原文未提供真实世界长期运行数据。