🤖 AI

Formal Methods Meet LLMs: Auditing, Monitoring, and Intervention for Compliance of Advanced AI Systems

本文提出了一种结合形式化方法（具体为线性时序逻辑）与机器学习的混合框架，以实现对黑盒人工智能系统的有效离线审计与在线运行时监控，并证明这些技术在检测时序约束违规方面优于大语言模型基线，同时能在保持任务性能的前提下主动缓解风险。

原作者： Parand A. Alamdari, Toryn Q. Klassen, Sheila A. McIlraith

发布于 2026-05-18

📖 1 分钟阅读☕ 轻松阅读

原作者： Parand A. Alamdari, Toryn Q. Klassen, Sheila A. McIlraith

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你雇佣了一位才华横溢但略显混乱的厨师（即人工智能）来经营一家餐厅。这位厨师几乎能烹饪任何菜肴，但他们并不总是遵循食谱，有时会忘记洗手，或者可能将菜肴端错桌子。你需要确保他们遵守规则，但你无法窥探他们的大脑以了解他们的思考过程。

本文旨在构建一位智能保安，从外部监视这位厨师，将其行为与规则手册进行核对，甚至在厨师犯错之前介入阻止。

以下是他们解决方案的分解，采用简单的类比：

1. 问题：“时间旅行”盲区

作者发现，虽然人工智能厨师擅长烹饪，但他们极不擅长记住随时间推移的事件序列。

类比：想象一条规则规定：“如果你拿了一个鸡蛋，你就必须最终将其敲开。”
人工智能的困境：如果厨师拿了一个鸡蛋，然后谈论了 10 分钟的天气，最后才敲开它，标准的“人工智能法官”可能会感到困惑。它可能会想：“他们拿了一个鸡蛋，但没有立刻敲开，所以他们违反了规则！”或者，如果他们等待太久，人工智能会完全忘记这种关联。
发现：本文证明，即使是最聪明的人工智能法官，随着事件之间的间隔变长，或随着规则数量的增加，它们在识别这些“时间延迟”规则方面的表现也会变差。它们会不堪重负。

2. 解决方案："TRAC"系统

作者创建了一个名为TRAC（时间规则评估与合规）的系统。将 TRAC 想象为一位专门的保安，它不试图像厨师那样“思考”，而是使用严格的数学清单。

标记器（翻译者）：首先，一个较小的人工智能（标记器）将厨师混乱的行为翻译成简单的“是/否”标志。
- 厨师说：“我要去拿鸡蛋，然后也许稍后再敲开它。”
- 标记器说：“动作：拿起了鸡蛋。状态：真。”
监控器（数学引擎）：这是核心。TRAC 不使用人工智能来猜测规则是否被违反，而是使用线性时序逻辑（LTL）。
- 隐喻：想象一个倒计时器或进度条。当厨师拿起鸡蛋时，“敲开鸡蛋”的计时器开始运行。监控器并不关心厨师在中间做了什么；它只检查数学逻辑：“计时器是否已过期？敲开的动作发生了吗？”
- 因为这是基于数学而非“感觉”，所以它永远不会疲倦，永远不会遗忘，并且能够完美地识别在长时间内发生的规则。

3. 升级：“预测性”保安（TRACP+I）

作者不仅希望在错误发生后将其抓获，更希望在错误发生之前将其阻止。他们将 TRAC 升级为TRACP+I。

水晶球（预测）：系统观察厨师当前的行为，并模拟未来几步。它会问：“如果厨师继续沿着这条路径走下去，他们是否会在 3 步之后违反规则？”
干预（制止之手）：如果系统预见到违规即将发生，它不会仅仅大喊“你违反了规则！”。它会立即采取行动。它有三种修复方式：
1. 重采样：它说：“再试一次那个动作，但换一种方式”，并选择一个更安全的版本。
2. 提示：它向厨师低声提醒：“嘿，记得关于敲开鸡蛋的规则！”
3. 切换：如果厨师真的陷入困境，它会在那一刻将厨师替换为一个“更安全”版本的厨师。

4. 结果：小工具胜过大脑

最令人惊讶的发现是关于谁做得最好。

旧方法：使用庞大且极其昂贵的人工智能充当法官（即“作为法官的大语言模型”）。
新方法：仅使用一个微小、廉价的人工智能将动作翻译成“是/否”标志，然后使用基于数学的 TRAC 系统进行实际判断。
结果：“小人工智能 + 数学”团队每次都击败了“超级人工智能”团队。庞大的人工智能不断因时间间隔而陷入困惑，而小人工智能加数学系统则完美无缺。这意味着公司无需花费数百万美元购买最大的人工智能模型来确保安全；它们可以使用更小型、更廉价的工具，并结合这种基于数学的保安。

总结

本文认为，为了保持先进人工智能的安全，我们不应依赖人工智能来监管自身（因为它不擅长记住长期规则）。相反，我们应该采用混合方法：

让一个小人工智能将大人工智能正在做的事情翻译成简单的事实。
使用严格的、基于数学的“规则引擎”（TRAC）来监视这些事实。
如果数学引擎预测到错误，它将介入以阻止其发生。

这构建了一个安全网，其速度更快、成本更低、准确性更高，比试图让人工智能“思考”着摆脱困境更为有效。

技术摘要：形式化方法与大语言模型的融合

问题陈述

本文针对人工智能治理中的一个关键缺口：缺乏在AI 赋能产品与服务的整个开发生命周期中对其进行监控、审计和干预的稳健机制。尽管大量精力被投入到前沿 AI 模型的安全性上（例如通过安全框架和红队测试），但中小企业（SMEs）和第三方开发者往往缺乏确保其部署的、黑盒 AI 系统（特别是大语言模型或 LLMs）符合特定产品、特定行业及特定司法管辖区法规的工具。

一个被识别的核心挑战是，许多合规要求具有时间延展性。这些是行为约束，其中事件之间的关系跨越时间，例如“如果收到发票，则最终必须支付”，或“在确认付款之前不要发货”。作者认为，目前依赖LLM 作为裁判（LLM-as-a-Judge）方法进行审计是不足的，因为 LLM 难以推理这些时间模式，特别是在事件之间的时间间隔变化、约束数量增加或每一步的命题数量增长时。

方法论

作者提出了一种框架，将形式化方法（特别是线性时序逻辑 LTL）与机器学习相结合，以构建一个黑盒监控和审计系统。核心方法涉及分解问题：利用 LLM 对事件进行标记（从未结构化文本中提取原子命题），并利用形式化逻辑对这些事件序列进行推理。

TRAC 框架

作者引入了TRAC（时间规则评估与合规性），这是一组专为黑盒 AI 系统设计的算法家族：

标记函数（ $L$ ）： 一个 LLM（或其他分类器）将输入和输出的序列映射为一组在给定时间步成立的命题符号（原子事实）。
LTL 推进（LTL Progression）： 系统不使用静态自动机编译约束，而是采用LTL 推进。该技术根据当前的真值分配 $\sigma_t$ $σ_{t}$ 重写 LTL 公式 $\psi$ $ψ$ ，生成剩余公式 $\psi_{t+1}$ $ψ_{t + 1}$ ，描述轨迹剩余部分必须满足的条件。
- 这允许对时间属性进行动态、增量的评估。
- 它保留了约束的符号结构，使得能够生成可解释的“见证”（执行轨迹），以解释为何发生违规。
算法：
- TRAC： 用于实时监控和离线审计的基础算法。它输出裁决（违规、满足或尚未确定）以及见证。
- TRACR（带重置的 TRAC）： 扩展 TRAC 以处理连续监控。如果检测到违规或满足，系统将公式重置为其初始状态，从而能够检测随后的违规（适用于嘈杂环境或重复任务）。
- TRACP+I（带预测和干预能力的 TRAC）：
  - 预测性监控： 使用基于采样的方法估计在时间范围 $k$ 内发生未来违规的概率。
  - 干预： 如果预测风险超过阈值，系统触发黑盒干预。策略包括：
    - 拒绝采样： 重新采样模型的输出，直到找到合规的输出。
    - 约束引导提示： 将剩余 LTL 公式（以自然语言形式）注入提示中，以引导模型。
    - 模型替换： 切换到更安全的替代模型来生成输出。

主要贡献

数学框架： 为评估黑盒 AI 系统提供了形式化定义，使其能够针对用户指定的、用自然语言或形式化逻辑（LTL）表达的行为要求进行评估。
TRAC 算法： 一套算法（TRAC、TRACR、TRACP+I），利用 LTL 推进来检测违规、 pinpoint 源头并提供解释性见证。论文证明了在标记函数完美的条件下，基于 LTL 推进的算法具有可靠性（soundness）。
优于 LLM 裁判： 实证证据表明，在检测时间延展性违规方面，TRAC 的表现显著优于作为基线的 LLM 裁判。值得注意的是，在 TRAC 框架内用作标记器的较小模型，其表现与作为独立裁判的前沿 LLM 相当甚至更优。
预测与干预监控： 引入了 TRACP+I，通过主动干预在不显著降低任务性能的情况下，降低了基于 LLM 的智能体的违规率。
LLM 局限性表征： 受控实验揭示，LLM 的时间推理准确性随以下因素可预测地下降：
- 相关事件之间的距离增加（时间弹性）。
- 同时存在的约束数量增加。
- 每个时间步的命题数量增加。

实验结果

作者在三个环境中评估了他们的方法：IPC-Trucks（物流规划）、TextWorld（烹饪任务）和ScienceWorld（科学推理）。

审计性能： 在审计任务中，TRACR + LLM（作为标记器） 在所有环境中均取得了最高的 F1 分数。即使是小型标记模型（例如 Qwen-7B）与 TRACR 结合，其表现也优于用作零样本或少样本裁判的大型前沿模型（例如 GPT-4.1、Gemini-2.5-Pro）。
时间推理限制： 合成轨迹的实验证实，LLM 在处理时间模式方面存在困难。随着事件间隔的增加（对于简单公式，小型模型从约 10 步下降到前沿模型的约 1000 步）以及公式复杂度（约束/命题数量）的增加，准确率显著下降。
干预有效性： TRACP+I 框架成功降低了所有模型和环境中的约束违规率。干预措施（重采样、提示引导、替换）有效地引导智能体走向合规，同时保持了与基线相当的任务性能（累积奖励）。

意义与主张

本文主张，经典形式化方法对于 AI 监督仍然具有重要价值，但需要针对基于语言的系统进行调整。其主要意义在于提出的分解策略：利用 LLM 在语义标记（提取命题）方面的优势，同时依赖形式化方法（LTL 推进）在推理时间模式方面的优势。

作者强调，这种方法：

使合规审计变得触手可及，无需前沿模型所需的预算。
通过见证提供可解释性，这对于调试和问责至关重要。
通过预测性监控和干预实现主动治理，超越了事后诊断。
解决了代理型 AI 系统（Agentic AI systems）特有的治理挑战，即行为在长时间范围内演变，而部署前的评估往往不足以应对这一领域。

论文最后谦逊地承认了局限性：黑盒监控无法检测所有故障模式，标记函数可能引入错误，并且将模糊的自然语言要求转化为精确的 LTL 公式仍然是一个受“形式化陷阱”影响的社会技术挑战。最终，TRAC 被呈现为更广泛的 AI 问责生态系统中的一个可部署工具。