形式化方法遇上大语言模型：面向先进AI系统合规性的审计、监控与干预
摘要
本文提出了一种将形式化方法（线性时序逻辑）与大语言模型相结合的技术，用于审计、监控和干预AI系统以确保其符合行为约束。研究表明，即便是小模型标注器在检测违规行为方面也能媲美前沿大语言模型裁判。
arXiv:2605.16198v1 公告类型：新
摘要：我们探讨了AI治理的一个特定维度：如何在AI开发全生命周期中监控和审计AI赋能的产品与服务，从部署前测试到部署后审计。通过结合形式化方法的原则与最先进的机器学习，我们提出的技术使AI产品和服务开发者，以及第三方AI开发者和评估者，能够对黑盒先进AI系统（尤其是大语言模型）进行离线审计和在线（运行时）监控，涉及产品特定的（时间延展的）行为约束，如安全约束、规范、规则和法规。我们进一步提供了预测性监控的实用技术，例如基于采样的方法，并引入了在运行时采取行动的干预监控器，以预先防范并可能减轻预测到的违规行为。实验结果表明，通过利用线性时序逻辑（LTL）的形式化语法和语义，我们提出的审计和监控技术在检测时间延展行为约束的违规方面优于LLM基线方法；采用我们的方法，即使小模型标注器也能达到甚至超越前沿LLM裁判。我们的预测和干预监控器显著降低了基于LLM的智能体的违规率，同时很大程度上保持了任务性能。我们进一步通过受控实验表明，LLM的时间推理准确性随着事件距离、约束数量和命题数量的增加而明显下降。
相似文章
连接法律解释与形式逻辑：忠实性、假设与人工智能法律推理的未来
本文指出了人工智能法律推理中法律解释与形式逻辑之间的系统性鸿沟，提出了一种神经符号方法来弥合这一鸿沟，并展示了在严格形式蕴含条件下重新标注法律自然语言推理数据时出现的显著标签偏移。
用 LLM 优化 LLM：面向测试时扩展的智能体发现方法
本文提出了 AutoTTS，这是一种环境驱动的框架，通过将测试时扩展（TTS）策略的发现过程形式化为控制器合成，自动发现用于大型语言模型（LLM）的测试时扩展策略。该框架在数学推理基准测试上展示了更优的准确率-成本权衡，且计算开销极小。
学习如何让大语言模型进行推理
OpenAI 发布了一篇文章，通过密码破译示例探索大语言模型的推理技术，展示了语言模型的逐步问题求解和模式识别能力。
全新AI范式：Ethical Immanence
介绍了Ethical Immanence，一种新型AI对齐范式，通过损失函数正则化和元认知检测将道德行为嵌入模型架构，为开源LLM带来更低成本和内在稳定性。
大语言模型能否用 TLA+ 建模实际系统？
Specula 团队的研究人员创建了 SysMoBench 基准测试，用于评估大语言模型能否准确建模实际计算系统的 TLA+ 规范，还是仅仅照本宣科地背诵教材内容。该基准测试涵盖四个阶段共 11 个系统，揭示了当前大语言模型在准确建模系统实现与参考论文方面的系统性差距。