[LG]《VeriGuard:EnhancingLLMAgentSafe

爱生活爱珂珂 2025-10-09 07:02:31

[LG]《VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation》L Miculicich, M Parmar, H Palangi, K D Dvijotham... [Google Cloud AI Research] (2025)

VeriGuard:通过形式验证代码生成提升LLM代理安全性

随着大型语言模型(LLM)代理广泛应用于医疗等敏感领域,安全、隐私等风险日益凸显。传统基于静态规则的防护手段虽有必要,但无法提供形式化安全保证,易被绕过。为此,VeriGuard框架创新地引入“正确即构造”(correct-by-construction)理念,通过两阶段策略:

1️⃣ 离线阶段:基于用户自然语言安全需求,利用LLM自动生成行为策略代码与形式化约束,结合自动测试和形式验证(利用Nagini工具)迭代优化,确保策略满足安全规范,避免模糊和不一致。

2️⃣ 在线监控阶段:在代理执行每个动作前,实时调用已验证策略函数做安全检查,违规则根据不同策略(终止任务、阻断动作、暂停工具执行或协作重规划)干预,平衡安全与任务完成率。

实验证明,VeriGuard在Agent Security Bench、EICU-AC和Mind2Web-SC等多领域基准测试中,显著降低攻击成功率至近零,同时保持高任务成功率,优于现有防御机制。多种策略集成展现出最佳安全效用权衡,兼顾严防与灵活性。

此外,VeriGuard通过利用LLM生成代码及其验证辅助反馈,推动了安全策略从经验性防护向形式化、可证明安全转变,适配复杂多变环境。当前挑战包括LLM生成约束的非确定性和验证工具能力限制,未来研究可聚焦于自动化安全规范生成和验证效率提升。

总结而言,VeriGuard打造了一套面向LLM代理的安全保障新范式,为高风险场景中的可信部署奠定坚实基础。

全文链接:arxiv.org/abs/2510.05156

AI安全 形式验证 LLM代理 VeriGuard 可信AI

0 阅读:0