arXiv:2512.23738cs.PLcs.AI2025-12被引 27

让大模型代理按时间顺序安全执行,防止违规操作。

Enforcing Temporal Constraints for LLM Agents

  • 用形式化语言定义动作时序规则,通过逻辑求解实时检查
  • 在真实场景中实现100%合规、0%危害,且任务效率更高
  • 适合高安全要求的客服与预订系统,如金融、航空领域

基于大模型的智能体被部署于安全敏感场景,但现有防护机制无法有效防止时序安全策略违规——例如在用户认证前访问敏感数据或向未授权支付方式退款。这些违规依赖对动作序列的推理,而非单一动作判断。当前防护系统依赖模糊的自然语言指令或事后监控,缺乏形式化保障。本文提出Agent-C框架,提供运行时保证,确保智能体满足正式时序安全属性。该框架引入领域专用语言描述时序约束(如“认证后才能访问数据”),将其转换为一阶逻辑,并利用SMT求解器在生成每个动作令牌时检测不合规行为。当大模型试图生成违规调用时,Agent-C采用受限生成技术,强制所有动作符合规范,并生成合规替代方案。我们在零售客服与航空公司票务系统两个真实应用中评估了Agent-C,涵盖多种开源与闭源语言模型。结果表明,Agent-C实现完全安全(100%合规,0%伤害),同时优于现有最优防护系统及无限制代理的任务效用。在最先进闭源模型上,其合规率从77.4%(Claude Sonnet 4.5)和83.7%(GPT-5)提升至100%,任务成功率分别从71.8%升至75.2%、66.1%升至70.6%,开创了可靠智能体推理的新基准。

原文摘要 · Abstract (English)

LLM-based agents are deployed in safety-critical applications, yet current guardrail systems fail to prevent violations of temporal safety policies, requirements that govern the ordering and sequencing of agent actions. For instance, agents may access sensitive data before authenticating users or process refunds to unauthorized payment methods, violations that require reasoning about sequences of action rather than an individual action. Existing guardrails rely on imprecise natural language instructions or post-hoc monitoring, and provide no formal guarantees that agents will satisfy temporal constraints. We present Agent-C, a novel framework that provides run-time guarantees ensuring LLM agents adhere to formal temporal safety properties. Agent-C introduces a domain-specific language for expressing temporal properties (e.g., authenticate before accessing data), translates specifications to first-order logic, and uses SMT solving to detect non-compliant agent actions during token generation. When the LLM attempts to generate a non-compliant tool call, Agent-C leverages constrained generation techniques to ensure that every action generated by the LLM complies with the specification, and to generate a compliant alternative to a non-compliant agent action. We evaluate Agent-C across two real-world applications: retail customer service and airline ticket reservation system, and multiple language models (open and closed-source). Our results demonstrate that Agent-C achieves perfect safety (100% conformance, 0% harm), while improving task utility compared to state-of-the-art guardrails and unrestricted agents. On SoTA closed-source models, Agent-C improves conformance (77.4% to 100% for Claude Sonnet 4.5 and 83.7% to 100% for GPT-5), while simultaneously increasing utility (71.8% to 75.2% and 66.1% to 70.6%, respectively), representing a new SoTA frontier for reliable agentic reasoning.

大模型代理时序安全形式验证SMT求解

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。