Logic-guided synthesis for evaluating implicit regulatory compliance in LLM tool calling

如何自动构造测试，检查 LLM 工具调用能否遵守未写入用户指令的法规约束。

• 场景：作者认为金融、法律、医疗和智能家居中的智能体会调用工具并执行多步目标；只完成功能不够，违规可能造成物理伤害或监管不合规。
• 现有不足：作者认为现有基准多靠人工或抓取，贵、难验证、易饱和，且主要评功能正确。法规常在长文本中，专家把规则映射到指令或轨迹的成本很高。
• 三个缺口：作者概括为 Ambiguity Gap（法规缺少可自动验证的确定性）、Validity Gap（直接生成轨迹常幻觉 API 或非法参数）和 Inference Gap（安全规则写进指令则测试过易）。
• 本文做法：作者提出 LogiSafetyGen，把法规转为有限轨迹上的 LTLf 预言，用逻辑引导模糊测试合成合规轨迹，再掩蔽安全步骤生成指令；据此建成 240 条任务的 LogiSafetyBench，并用双预言同时查功能与时序合规。作者称这是首个严格测量工具调用中隐式法规合规的评测套件。
• 评测设定：被测对象是生成 Python 程序并调用工具的 LLM，不是恶意用户攻击。系统提示含工具 schema 与法规原文，用户指令去掉显式安全步骤；通过须终态匹配，且轨迹满足隐藏 LTL。

恶意请求与一般工具安全

• AgentHarm（Andriushchenko et al., 2025；文中并引 Mazeika et al., 2024）：分析恶意用户请求下的 LLM 行为。作者认为这不同于良性条件下的规则遵守，且主要是问答。
• ToolEmu（Ruan et al., 2024）、Agent-SafetyBench（Zhang et al., 2024b）、AgentBench（Liu et al., 2024）：考察问答之外的一般工具使用安全。作者认为其中安全主要指正确操作工具，而不是解读文本法规并遵守具体规则。
• 法规锚定评测：EU-Agent-Bench（Lichkovski et al., 2025）、HSE-Bench（Wang et al., 2025a）、RuleArena（Zhou et al., 2025）、CNFinBench（Ding et al., 2025）把具体政策或真实法规写入任务。作者认为它们不要求生成满足形式化合规规则的可执行工具调用脚本。

基准如何建成

• 人工与爬取：HumanEval（Chen et al., 2021）靠人工收集；BFCL（Patil et al., 2025）爬取仓库再标注。作者引 Zhu et al.（2024），认为人工基准贵且可能被污染。
• LLM 参与生成：AutoCodeBench（Chou et al., 2025）生成代码任务，MCPBench（Wang et al., 2025c）用 LLM 辅助生成工具使用测试。作者认为生成的随机性难以保证严格正确或符合特定规则。
• 规则机制：作者称最接近本文设定的 ShieldAgent（Chen et al., 2025b）用概率规则电路约束轨迹，但是对抗攻击下的运行时防御；本文是离线合规压力测试。StateEval（Huang et al., 2025）做顺序 API 的状态感知测试生成，作者称其关注功能正确而非法规合规。

基线与对照基准

• 轨迹多样性基线：GPT-5-Mini 在与模糊器相同约束下提示生成 API 程序，比较 S.C. Cov 与 ATC。作者称符号执行原则上能产轨迹，但需大量人工适配，超出本研究范围。
• Table 1：ToolSword（对抗注入）、TAI3（意图完整性）、ToolEmu（一般风险）、Agent-SafetyBench（一般安全）。作者称它们不同时具备自动有效轨迹、隐式安全、形式化预言和可执行环境。工具规格改编自 ToolEmu。

作者把本文定位为：用 LTLf 预言和逻辑引导模糊测试，离线生成可执行、可验证的隐式法规合规测试，而不是运行时防御，也不是只评功能正确的工具调用。

整体上，LogiSafetyGen 把工具集与法规自动合成为带指令、目标状态和法规约束的测试，并同时给出一条可达该状态的合法 API 轨迹。Figure 1 分成预言机构建、轨迹生成、安全掩蔽三步。

问题设定与三种缺口

给定工具集 T 与法规 P，合成 (I, S*, Φ_task)：I 是用户指令，S* 是目标状态，Φ_task 是适用约束，且 S* 由同时生成的轨迹可达。作者要越过三个缺口：法规缺少数学确定性；直接让 LLM 写轨迹会幻觉 API 或非法参数；把安全规则写进指令只剩指令跟随。

自动安全预言机构建

LLM 先把法规蒸馏成原子约束，再做 Scope Alignment 与 Constraint Deduplication，只留相关政策。逻辑不自由翻译，而限制为两种 LTLf 模板。操作限制禁止在检查 P1 成立前执行敏感动作 P2，即 ¬((¬ P₁) U P₂)；指令遵守要求触发 P1 之后出现结果 P2，即 \square(P_1 \rightarrow \diamond P_2)。前者管顺序禁止，后者管触发后的未来义务。

候选公式仍可能引用 schema 里没有的谓词。Signature Validator 删掉含未定义谓词的公式，使留下的预言可被模糊器求解。作者把模板限制追溯到先前工作里业务合规的主导形式，论文未再给其他模板。

逻辑引导轨迹生成

安全约束模糊器（作者称约 3600 行）把轨迹当作有界搜索，逐步提出动作并拒绝不满足形式规格者。每步两道边界：Vschema 要求动作在当前状态可执行；Vsafe 用运行时 LTL 监视器要求更新轨迹满足全部预言。

搜索是自底向上深度优先，只对下一步做惰性求值。业务动作违反 LTL 就剪枝并回溯，直到选中强制安全操作。作者称到达目标轨迹长度后，轨迹可解、可执行且按构造合规。论文未给出目标长度的数值。

安全掩蔽与指令合成

掩蔽函数去掉轨迹中的安全关键 API，只保留功能步骤及其顺序，再译成自然语言。指令因此只写业务目标，被测模型须从政策上下文推断被省略的合规步骤。

同一掩蔽轨迹导出两类指令。Goal-Oriented 只给最终结果，测规划时能否自行插入安全措施。Workflow-Oriented 给出业务步骤，测模型会否盲从用户顺序、仍主动插入安全检查。生成器写候选，评估器检查业务参数是否无歧义，以及有无安全提示泄漏。政策抽取与指令合成的骨干是 GPT-5-Mini。论文未写评估器是否为另一模型。

双预言与成功判定

功能预言要求最终状态与 S* 一致。安全预言要求执行轨迹满足 Φ_task 中全部 LTL。作者用二者区分单纯任务失败，与 Unsafe Success（业务逻辑正确但违反法规）。结果数字见第 4 问。

实验设置

• 被测模型：作者称评估 13 个模型，正文 Figure 2 与 Figure 3 只报告 8 个：GPT-5、GPT-5-Mini、GPT-5-Nano、Gemini-Pro、Gemini-Flash、Gemini-Lite（作者称属 Gemini-2.5 系列）、Llama-3.1-8B（图中 Llama-8B）、DeepSeek-R1-Distill-Qwen-14B（图中 DS-R1-Qwen-14B）。作者举例还包含 Qwen-Coder，未给单独数字。其余名称论文未列出。
• 任务：LogiSafetyBench 共 240 条，即 120 对；三领域各 40 对，每对含 Goal 与 Workflow，故每种指令每领域 40 条。工具规格改编自 ToolEmu。法规为 EU PSD2、USA HIPAA Security Rule、ETSI EN 303 645。安全 API 子集大小为 4、7、10（Table 2）。
• 输入：系统提示含工具 schema、原始法规和用户指令；显式安全要求已从指令去掉。模型要生成可执行的工具调用程序。
• 主指标：Pass@1，作者将其作为 Safe Success Rate：功能目标与全部隐藏 LTL 同时满足才通过。Figure 2 还分 Safe Success、Benign Failure、Unsafe Failure、Unsafe Success。
• 判定：终态匹配加运行时 LTL 监视器，不是 LLM 评审。论文未报告温度、采样次数或重复次数。
• 生成侧基线：覆盖率实验用 GPT-5-Mini 在相同约束下提示生成，每种方法 40 条轨迹。

主结果

Pass@1 是主指标。正文只写出一处精确对比：Smart Home IoT 上 GPT-5 从 Workflow-Oriented 的 75% 降到 Goal-Oriented 的 28%（对应 Figure 2）。Figure 2 其余堆叠分段与四类结果无法可靠对齐，不转写，因而不能从正文补出最差模型的 Pass@1。下表是 Figure 3 对 Goal-Oriented 的 Instruction Adherence 违规率（%），八个模型都列出。列顺序按图底从左到右，且 Tele-Healthcare 上 Gemini-Pro 的 57 与正文一致；同图 Semantic 行的 50、80 也与正文一致。

| 模型 | Financial | Tele-Healthcare | Smart Home | | GPT-5 | 0 | 12 | 45 | | GPT-5-Mini | 10 | 15 | 28 | | GPT-5-Nano | 38 | 25 | 75 | | Gemini-Pro | 2 | 57 | 20 | | Gemini-Flash | 18 | 32 | 8 | | Gemini-Lite | 28 | 60 | 28 | | DeepSeek-R1-Distill-Qwen-14B | 22 | 40 | 30 | | Llama-3.1-8B | 30 | 5 | 0 |

据 Figure 3。

• 作者的总判断：作者称能力与合规大体正相关，前沿商业模型优于开放权重模型；但扩大规模改善推理，并不消除隐式合规失败，模型常把完成任务放在安全之前。
• API 密度与指令类型：作者把 API Density 定义为场景中不同安全关键工具数。金融服务有 4 个，作者称 GPT-5 near-perfect，正文未给该格精确 Pass@1；智能家居有 10 个，作者称规划更深。作者称有工作流脚手架时更稳，去掉后下降，且更多转向不安全行为。Tele-Healthcare 上，作者称 Gemini-Pro 换成 Goal 后 Unsafe Success Rate 上升，论文未给该比率。
• 与上表的关系：作者称 GPT-5 系列更强的模型往往更少安全违规。表中金融与远程医疗符合该方向，Smart Home 上 GPT-5 高于 GPT-5-Mini。作者称 Gemini-Pro 经常差于 Gemini-Flash，并举远程医疗的遵守违规为例；同表金融列上 Pro 低于 Flash。

轨迹生成覆盖率

S.C. Cov 是轨迹覆盖的安全关键 API 比例。ATC 是相邻 API 对的种类数，除以唯一 API 集合大小的平方。

| 场景 | 子集大小 | GPT-5-mini ATC | GPT-5-mini S.C. Cov | Ours ATC | Ours S.C. Cov | | Tele-Healthcare | 7 | 28.4% | 85.7% | 42.6% | 100% | | Financial Services | 4 | 23.4% | 100% | 85.6% | 100% | | Smart Home IoT | 10 | 30.1% | 80% | 63.3% | 100% |

据 Table 2。

• 作者称模糊器在三领域都达到 100% S.C. Cov，并称 LLM 基线更低，举例 Smart Home 漏掉 20% 安全 API，与表中 80% 相符。Financial Services 的 S.C. Cov 双方都是 100%。
• 作者称 Ours 的 ATC 在三领域都更高，并称最大提升在 Tele-Healthcare（23.4% 对 85.6%）。Table 2 里这两个数在 Financial Services 行；Tele-Healthcare 的 ATC 是 28.4% 与 42.6%。按表，ATC 差距最大的是 Financial Services。
• 作者认为这与 LLM 测试生成的 Sampling Bias 一致：把轨迹生成当作约束满足而非文本生成，才能探索 API 组合边界。

失败模式的其余观察

Figure 3 只分析 Goal-Oriented，另外三类是 Syntax Error、Semantic Error（API 幻觉）和 Operational Restriction（顺序错误）。作者称没有跨领域或模型族通用的失败模式，合规失败依赖上下文。

• 语义：作者称 Syntax Error 可忽略，但前沿模型仍有 Semantic Error。正文给出 Gemini-Pro 在 Financial Services 为 50%，Gemini-Flash 在 Smart Home IoT 为 80%。作者称高推理能力并不保证 API 落地。
• 语法行：Figure 3 的 Syntax 标注可见 0 与 2。该行末端可能与色标粘连，不逐格转写。
• 顺序违规行：Operational Restriction 的文本抽取比 8×3 多出一个数，不转写。

其他消融与分析

• 安全预言核验：全体作者独立审三轮，只留一致同意，三领域合计接受率 73.9%（Section 4.2）。
• 指令与掩蔽核验：每人负责一个场景，直到 40 对有效样本；接受率 70.6%，得到 240 条（Section 4.2）。论文未报告一致性系数。
• 覆盖率实验每种方法、每个领域 40 条轨迹（Section 5.2）。
• 论文未报告 Pass@1 的重复次数、解码温度、查询次数或耗时。
• 设定是良性指令下的隐式合规，论文未把该评测写成自适应攻击实验。

作者指出的局限与后续方向

• 预言只覆盖时序（Limitations）：为自动合成 LTL，预言限制为 Operational Restriction 与 Instruction Adherence。它只刻画 API 调用顺序，不能分析参数是否安全，例如转账金额是否在限额内，或合法调用中的恶意载荷。需要深查参数值或概率判断的政策无法形式化。作者提出后续可设计更细的逻辑，以覆盖数据流和参数级约束。
• 生成器先验（Limitations）：测试场景的初始多样性部分受播种用骨干 LLM 的创造先验限制。人工核验保证最终质量，但作者观察到纯自动生成在没有人工引导时仍难产生极端结构新意。作者预期基础模型继续扩大后，生成器能更自主地提出边界情况，从而减少高风险基准对 human-in-the-loop 的依赖。

实验覆盖范围

• 作者称评测 13 个 LLM；Figure 2 与 Figure 3 报告其中 8 个，论文未列出其余名称，也未报告 Qwen-Coder 的单独结果。
• 场景为金融服务、远程医疗、智能家居，各 40 对样本、两种指令，合计 240 条。工具规格改编自 ToolEmu，法规为 PSD2、HIPAA Security Rule、ETSI EN 303 645。
• 轨迹覆盖的对照是 GPT-5-Mini 提示生成，每种方法 40 条轨迹（Section 5.2）。作者称符号执行需要大量人工适配，超出本研究范围。
• 失败模式分析只做 Goal-Oriented（Figure 3）。通过判定是状态匹配加 LTLf 监视器，不是 LLM 评审。系统提示含法规原文，省略的是指令中的安全步骤。
• 论文未报告 Pass@1 的重复次数、解码温度、查询次数或耗时。人工核验给出三轮一致同意，以及接受率 73.9% 和 70.6%，未报告一致性系数。

LogiSafetyGen 用时序逻辑预言和约束搜索，自动生成检查工具调用是否遵守隐含法规的测试，并实例化为 LogiSafetyBench。

• 问题：高风险工具调用不能只看功能是否完成。法规写在长文本里，现有基准又偏功能正确、难扩展。作者要得到可执行、可验证、且不把安全步骤写进用户指令的测试。
• 做法：法规收成两种 LTLf 模板并经签名校验；模糊器在可执行性与安全约束下自底向上搜索，得到按构造合规的轨迹；安全 API 被掩蔽后，合成只写结果的 Goal 指令和给出业务步骤的 Workflow 指令。通过须终态匹配且轨迹满足全部 LTL。政策抽取与指令合成使用 GPT-5-Mini。
• 数据：三领域分别锚定 PSD2、HIPAA Security Rule 和 ETSI EN 303 645。人工核验后为 240 条任务。预言接受率 73.9%，指令接受率 70.6%。
• 生成质量：Table 2 中模糊器三领域 S.C. Cov 均为 100%；GPT-5-mini 为 85.7%、100%、80%。ATC 上 Ours 为 42.6%、85.6%、63.3%，GPT-5-mini 为 28.4%、23.4%、30.1%。
• 模型行为：系统提示含法规原文。正文写出的 Pass@1 中，GPT-5 在 Smart Home IoT 从 Workflow 的 75% 降到 Goal 的 28%。作者称更大模型功能更好，仍常优先完成任务；Goal 条件下失败原因随领域变化，没有统一模式。
• 作者结论：作者认为现有模型能执行已经给出的工作流，但缺少自行推断隐含安全约束的自主性，并把该基准当作衡量、改进自主智能体法规合规的基础。作者同时指出预言不含参数级约束，生成多样性仍部分依赖骨干模型与人工筛选。