形式化方法遇见LLM：面向高级AI系统合规的审计、监控与干预

我们考察AI治理的一个特定维度：如何在AI开发生命周期全程（从部署前测试到部署后审计）监控和审计AI赋能的产品与服务。我们将形式化方法的原理与最先进的机器学习相结合，提出一系列技术，使AI产品与服务的开发者以及第三方AI开发者和评估者，能够针对黑盒高级AI系统（尤其是LLM），对产品特定的（时间延展的）行为约束（如安全约束、规范、规则与法规）执行离线审计与在线（运行时）监控。我们进一步提供了预测性监控的实用技术（如基于采样的方法），并引入干预型监控器，在运行时采取行动，以预先阻止并可能缓解预测到的违规。实验结果表明，通过利用线性时序逻辑（LTL）的形式语法与语义，我们提出的审计与监控技术在检测时间延展行为约束违规方面优于LLM基线方法；采用我们的方法，即便是小模型标注者也能媲美或超过前沿LLM评判者。我们的预测性与干预性监控器显著降低了基于LLM的智能体的违规率，同时基本保持了任务性能。我们还通过受控实验表明，随着事件距离、约束数量与命题数量的增加，LLM的时序推理准确率出现显著退化。