TriCEGAR：一种面向智能体AI的轨迹驱动抽象机制

智能体AI系统通过工具进行交互，并在长期、随机的交互轨迹中演化其行为，这使得其行为保障变得复杂，因其依赖于非确定性环境和概率性模型输出。先前工作通过动态概率保障（DPA）引入了运行时验证方法，在线学习马尔可夫决策过程（MDP）并进行量化属性的模型检测。然而，该方法要求开发者手动定义状态抽象，导致验证过程与特定应用启发式紧密耦合，增加采用难度。本文提出TriCEGAR，一种从执行日志自动构建状态抽象的轨迹驱动机制，支持在线构建智能体行为MDP。TriCEGAR将抽象表示为从轨迹中学习并利用反例精化的谓词树。我们描述了一个原生框架实现，可捕获类型化的智能体生命周期事件、从轨迹构建抽象、构造MDP，并执行概率模型检测以计算如最大成功概率Pmax(success)和最小失败概率Pmin(failure)等边界。此外，运行似然性还可作为护栏信号用于异常检测。