用形式化验证确保工具增强型大模型不违规操作。
Solver-Aided Verification of Policy Compliance in Tool-Augmented LLM Agents
- 将自然语言政策转为逻辑约束，运行时用SMT求解器检查。
- 在TauBench上测试，违规率下降且任务准确率不变。
- 适合对合规性要求高的客服与自动化场景。
工具增强型大语言模型（TaLLMs）通过调用外部工具实现与真实环境交互，但其在客户服务和业务流程自动化等敏感场景中面临工具使用与行为合规性问题。现有方法仅通过上下文注入政策描述进行引导，无法保证合规。本文提出基于SMT求解器的框架，采用人工引导的LLM辅助方式，将自然语言定义的工具使用策略转换为SMT-LIB-2.0格式的逻辑约束，覆盖代理可观测状态与工具参数。运行时拦截计划中的工具调用，利用Z3求解器验证是否违反约束，违规调用被阻止。在TauBench基准上的实验表明，该方法显著降低策略违规率，同时保持任务整体准确性。结果表明，将形式化推理集成到TaLLM执行流程中可有效提升工具调用合规性与系统可靠性。
原文摘要 · Abstract (English)
Tool-augmented Large Language Models (TaLLMs) extend LLMs with the ability to invoke external tools, enabling them to interact with real-world environments. However, a major limitation in deploying TaLLMs in sensitive applications such as customer service and business process automation is a lack of reliable compliance with domain-specific operational policies regarding tool-use and agent behavior. Current approaches merely steer LLMs to adhere to policies by including policy descriptions in the LLM context, but these provide no guarantees that policy violations will be prevented. In this paper, we introduce an SMT solver-aided framework to enforce tool-use policy compliance in TaLLM agents. Specifically, we use an LLM-assisted, human-guided approach to translate natural-language-specified tool-use policies into formal logic (SMT-LIB-2.0) constraints over agent-observable state and tool arguments. At runtime, planned tool calls are intercepted and checked against the constraints using the Z3 solver as a pre-condition to the tool call. Tool invocations that violate the policy are blocked. We evaluated on the TauBench benchmark and demonstrate that solver-aided policy checking reduces policy violations while maintaining overall task accuracy. These results suggest that integrating formal reasoning into TaLLM execution can improve tool-call policy compliance and overall reliability.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。