Source-linked AI summary
Solver-Aided Verification of Policy Compliance in Tool-Augmented LLM Agents
Cailin Winston, Claris Winston, René Just
TL;DR
TaLLM agents need more reliable compliance with domain-specific tool-use policies than prompt-based guidance provides. The paper translates policies into logical constraints and checks planned calls with an SMT solver before execution. On the τ2 benchmark, solver-aided checking reduced invalid tool calls and improved consistency, while policy encodings still required human review.
Problem
Existing TaLLM policy-enforcement approaches lack deterministic guarantees that policy-violating actions will be prevented.
Method
The framework uses LLM-assisted, human-guided policy translation into logical constraints and checks planned tool calls against them at runtime with an SMT solver.
Results
Solver-aided checking reduced invalid write tool calls to 29% while maintaining similar overall task success and improving consistency across repeated executions.
Takeaways & Limitations
Runtime solver checks provide a policy-enforcement mechanism that reduces policy-violating calls and improves consistency across repeated executions.
Takeaways & Limitations
Policy encodings require manual review because automatic translation can be incomplete or semantically underconstrained.
Abstract
from arXiv · showhide
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.
1 Introduction
TaLLMs increase autonomy by invoking external tools, but existing prompt-based and heuristic safeguards do not reliably prevent policy violations. The paper proposes formal, solver-aided runtime checking of tool calls, with policies encoded as logical constraints through an LLM-assisted, human-guided process.
- TaLLMs can query information and take real-world actions, increasing the need for strict adherence to operational policies.
- Existing prompt-based, heuristic, and human-in-the-loop mechanisms lack reliable guarantees or scalability for preventing policy violations.
- Tool-call compliance can be modeled as satisfiability over agent-observable state, policies, and planned tool arguments.
- The framework encodes tool-use policies as logical constraints and checks planned calls with an SMT solver before execution.
- The evaluation targets whether solver-aided checking reduces policy-violating calls while preserving task success.
- Policy documents are translated into formal encodings using an LLM-assisted, human-guided, and human-reviewed approach.
2 Logical Encoding of Natural Language Policies
The paper treats tool-use policies as constraint systems over observable state and tool arguments. Their logical encoding represents relevant values, categories, policy predicates, and assertions, while validation schemas connect each tool to the variables and predicate needed for compatibility checking.
- Prompt-based policy guidance becomes brittle as policies grow longer and interact across conversations and tool invocations.
- Policy compliance is modeled as satisfiability over variables representing relevant state and possible tool calls.
- A domain expert converts natural-language policies into logical encodings containing constants, sorts, predicates, functions, and assertions.
- Each tool validation schema specifies the typed policy variables to instantiate and the predicate whose satisfiability determines permission.
3 Solver-Aided Policy Compatibility Checking
The runtime checker intercepts candidate tool calls, instantiates policy constraints from observable context and call arguments, and submits them to an SMT solver. Satisfiable calls proceed; unsatisfiable calls are blocked and may trigger bounded replanning.
- The checker intercepts each planned call, constructs assertions from current state and call details, and tests satisfiability against the policy encoding.
- The checker observes the tool name, arguments, and preceding conversation while leaving the agent’s internal reasoning unchanged.
- A language model extracts required variable values from conversation history and tool arguments for SMT-LIB constraint construction.
- SAT permits the invocation because a consistent assignment exists, whereas UNSAT identifies a policy violation and blocks the call.
- Blocked calls receive an unsatisfiable-core explanation and up to three replanning attempts are allowed.
4 Evaluation Setup
The evaluation uses the airline domain of the τ2 benchmark to test policy adherence, task performance, and consistency. It measures repeated-task success with pass_k across four trials and poses research questions about translation, policy violations, and overall accuracy.
- Evaluation Setup: The airline evaluation includes 50 tasks, 13 tools, and a 1242-word policy document covering cancellations, re-bookings, and compensation eligibility.
- Evaluation Setup: pass_k measures the probability that all k independent trials of a task succeed, averaged across tasks.
- Evaluation Setup: Higher pass_k scores indicate greater consistency and reliability across independent trials.
- Evaluation Setup: Experiments use k=4 trials, with GPT-4.1 for customer and service agents and GPT-4o for tool-call validation.
- Research Questions: The evaluation asks how policy translation, solver-aided checking, policy-violating calls, task accuracy, and consistency are affected.
5 Results
The evaluation found that policy encoding quality varied substantially across generation designs, while runtime policy checking reduced invalid write calls and preserved similar overall task success with improved consistency.
- Policy Translation Designs: Fully automated Proof-of-Thought generation failed on realistic policies because outputs contained syntax errors, undefined symbols, and incomplete rule structures.The design was therefore not viable for policy verification.
- Policy Translation Designs: Iterative generation and repair produced syntactically correct SMT-LIB but omitted essential constraints, resulting in underconstrained policies and incorrect behavior.The approach performed better with Z3-Python code than with raw SMT-LIB.
- Policy Translation Designs: The AWS Bedrock automated-reasoning approach achieved around 95% judged coverage but still left rules underconstrained, allowing policy-violating invocations.The cancellation encoding failed to explicitly prohibit cancellations outside the permitted 24-hour window.
- Policy Translation Designs: Across designs, policy encoding faced recurring challenges in syntactic correctness, semantic completeness, and constraint tightness.Implicit negation and exclusivity assumptions could leave models underconstrained.
- Policy Translation Designs: Manual review and targeted tuning were required because automatically translating natural-language policies into complete logical constraints remained difficult.The authors treated policy encodings as explicit, reviewable artifacts rather than relying solely on fully automated translation.
- Policy-Checking Results: 29% of write tool calls were invalid with the policy checker, compared with a roughly equal valid-invalid split for the baseline.The checker improved precision but slightly reduced recall by producing fewer correct write calls overall.
- Policy-Checking Results: The policy checker achieved similar overall task success and improved consistency, with success decreasing 26% as k increased versus 40% for the baseline.The comparison used the pass_k metric across airline-domain tasks at k = 4.
6 Related Work
Related work shows that TaLLM agents can use external domain-specific tools but commonly fail through incomplete planning, incorrect invocations, and execution errors. This paper addresses policy adherence by integrating solver-checked formal verification directly into the tool-use planning loop.
- Tool-Augmented LLMs: TaLLM systems extend language models with external domain-specific tools, differing in how tools are provisioned and executed.Examples include prompt-documented compositional tools and fine-tuned tool-selection models.
- Tool-Augmented LLMs: Prior benchmarks and analyses identify incomplete planning, incorrect tool invocations, and tool execution errors as common TaLLM failures.These studies characterize failures across multiple domains and task capabilities.
- Policy Enforcement: Policy adherence is a key failure mode because prompt-based and postprocessing approaches lack deterministic guarantees and cannot prevent violating actions before execution.The limitation is highlighted in both prior work and the Tau-bench benchmark.
- Formal Verification: Although formal methods can provide hard policy guarantees, prior work had not integrated formal verification directly into TaLLM tool-use planning.This paper bridges that gap by incorporating proof-based reasoning into the action-planning loop.
7 Conclusion
The paper presents a solver-aided framework that compiles natural-language operational policies into logical constraints for runtime enforcement in TaLLM agents. Evaluations show reduced policy-violating tool calls, while manual or semi-structured policy encoding remains necessary for constraint correctness and tightness.
- The framework compiles natural-language operational policies into logical constraints and checks proposed tool invocations at runtime.This provides policy enforcement independent of agent reasoning variability.
- Evaluations on the 𝜏2 benchmark show fewer policy-violating tool calls and more consistent behavior across repeated executions.
- Manual or semi-structured policy encoding remains necessary to ensure constraint correctness and tightness.
- The paper identifies further automation of policy encoding and improved policy checking as directions for future research.