Solver-Aided Verification of Policy Compliance in Tool-Augmented LLM Agents

• URL: http://arxiv.org/abs/2603.20449v1
• Date: Fri, 20 Mar 2026 19:25:43 GMT
• Title: Solver-Aided Verification of Policy Compliance in Tool-Augmented LLM Agents
• Abstract summary: We introduce an SMT solver-aided framework to enforce tool-use policy compliance in TaLLM agents.<n>Specifically, we use an LLM-assisted, human-guided approach to translate natural-language-specified tool-use policies into formal logic.<n>At runtime, planned tool calls are intercepted and checked against the constraints using the Z3 solver as a pre-condition to the tool call.
• Score: 5.90411280561446
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: 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.

Related papers

• Hybrid Analysis for Secure MCP Tool Use in LLM Agents [77.68135853475535]
  We propose a hybrid analysis-based defense framework designed to safeguard the use of MCP tools in large language model (LLM) agents.<n> MTGuard effectively mitigates multiple categories of harmful tool use across different LLM agents while maintaining performance on benign user tasks.
  arXiv  Detail & Related papers  (2026-07-28T05:17:34Z)
• Securing LLM Agents Need Intent-to-Execution Integrity [49.490963596514185]
  We argue that securing LLM agents requires defining an end-to-end correctness property that specifies when an agent's execution faithfully reflects the user's intent.<n>We observe that LLM agents are structurally analogous to compilers, where security violations correspond to mis-executions that do not preserve user intent.<n>We derive four integrity properties that must hold simultaneously: emphTool Integrity, emphInstruction Integrity, emphJudgment Integrity, and emphData Flow Integrity.
  arXiv  Detail & Related papers  (2026-05-16T12:53:31Z)
• PolicyBank: Evolving Policy Understanding for LLM Agents [51.86716874651299]
  PolicyBank maintains structured, tool-level policy insights and iteratively refines them.<n>PolicyBank closes up to 82% of the gap toward a human oracle.
  arXiv  Detail & Related papers  (2026-04-16T20:29:30Z)
• ToolRosetta: Bridging Open-Source Repositories and Large Language Model Agents through Automated Tool Standardization [51.92237664440418]
  ToolRosetta is a framework that automatically translates open-source code repositories and APIs into MCP-compatible tools.<n>Given a user task, ToolRosetta autonomously plans toolchains, identifies relevant toolchains, and converts them into executable MCP services.
  arXiv  Detail & Related papers  (2026-03-10T07:19:43Z)
• Gecko: A Simulation Environment with Stateful Feedback for Refining Agent Tool Calls [56.407063247662336]
  We introduce Gecko, a comprehensive environment that simulates tool responses using a combination of rules and LLMs.<n>GATS consistently improves the tool calling performance of various LLMs including GPT-4o, GPT-5, and Gemini-3.0-pro.
  arXiv  Detail & Related papers  (2026-02-22T15:02:00Z)
• Towards Verifiably Safe Tool Use for LLM Agents [53.55621104327779]
  Large language model (LLM)-based AI agents extend capabilities by enabling access to tools such as data sources, APIs, search engines, code sandboxes, and even other agents.<n>LLMs may invoke unintended tool interactions and introduce risks, such as leaking sensitive data or overwriting critical records.<n>Current approaches to mitigate these risks, such as model-based safeguards, enhance agents' reliability but cannot guarantee system safety.
  arXiv  Detail & Related papers  (2026-01-12T21:31:38Z)
• A-LAMP: Agentic LLM-Based Framework for Automated MDP Modeling and Policy Generation [2.5705703401045548]
  We introduce an agentic large language model (LLM)-based framework for automated MDP modeling and policy generation (A-LAMP)<n>A-LAMP translates free-form natural language task descriptions into an MDP formulation and trained policy.<n>A-LAMP consistently achieves higher policy generation capability than a single state-of-the-art model.
  arXiv  Detail & Related papers  (2025-12-12T04:21:17Z)
• MiniScope: A Least Privilege Framework for Authorizing Tool Calling Agents [13.73193852761645]
  MiniScope is a framework that enables tool calling agents to operate on user accounts while confining potential damage from unreliable LLMs.<n>Our evaluation shows that MiniScope incurs only 1-6% latency overhead compared to vanilla tool calling agents.
  arXiv  Detail & Related papers  (2025-12-11T22:10:39Z)
• Progent: Programmable Privilege Control for LLM Agents [46.31581986508561]
  We introduce Progent, the first privilege control framework to secure Large Language Models agents.<n>Progent enforces security at the tool level by restricting agents to performing tool calls necessary for user tasks while blocking potentially malicious ones.<n>Thanks to our modular design, integrating Progent does not alter agent internals and only requires minimal changes to the existing agent implementation.
  arXiv  Detail & Related papers  (2025-04-16T01:58:40Z)
• Adaptive Tool Use in Large Language Models with Meta-Cognition Trigger [49.81945268343162]
  We propose MeCo, an adaptive decision-making strategy for external tool use.<n>MeCo quantifies metacognitive scores by capturing high-level cognitive signals in the representation space.<n>MeCo is fine-tuning-free and incurs minimal cost.
  arXiv  Detail & Related papers  (2025-02-18T15:45:01Z)
• LMN: A Tool for Generating Machine Enforceable Policies from Natural Language Access Control Rules using LLMs [0.435105239054559]
  Rules or guidelines called Natural Language Access Control Policies (NLACPs) can't be directly used in a target access control model like Attribute-based Access Control (ABAC)<n> manually translating the NLACP rules into Machine Enforceable Security Policies (MESPs) is both time consuming and resource intensive.<n>We have developed a free web-based tool called LMN (LLMs for generating MESPs from NLACPs) that takes an NLACP as input and converts it into a corresponding MESP.
  arXiv  Detail & Related papers  (2025-02-18T02:45:46Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.