形式化方法遇上大语言模型：面向先进AI系统合规性的审计、监控与干预

arXiv:2605.16198v1 公告类型：新 摘要：我们探讨了AI治理的一个特定维度：如何在AI开发全生命周期中监控和审计AI赋能的产品与服务，从部署前测试到部署后审计。通过结合形式化方法的原则与最先进的机器学习，我们提出的技术使AI产品和服务开发者，以及第三方AI开发者和评估者，能够对黑盒先进AI系统（尤其是大语言模型）进行离线审计和在线（运行时）监控，涉及产品特定的（时间延展的）行为约束，如安全约束、规范、规则和法规。我们进一步提供了预测性监控的实用技术，例如基于采样的方法，并引入了在运行时采取行动的干预监控器，以预先防范并可能减轻预测到的违规行为。实验结果表明，通过利用线性时序逻辑（LTL）的形式化语法和语义，我们提出的审计和监控技术在检测时间延展行为约束的违规方面优于LLM基线方法；采用我们的方法，即使小模型标注器也能达到甚至超越前沿LLM裁判。我们的预测和干预监控器显著降低了基于LLM的智能体的违规率，同时很大程度上保持了任务性能。我们进一步通过受控实验表明，LLM的时间推理准确性随着事件距离、约束数量和命题数量的增加而明显下降。