TriCEGAR：面向Agentic AI的轨迹驱动抽象机制

Agentic AI系统通过工具行动，并在长而随机的交互轨迹上演化其行为。这一设定使保障（assurance）复杂化，因为行为取决于非确定性环境与概率性模型输出。先前工作引入了经由动态概率保障（DPA）的agentic AI运行时验证——在线学习MDP并模型检查定量性质。一个关键局限是开发者必须手动定义状态抽象，使验证与应用特定启发式耦合，增加采纳阻力。本文提出TriCEGAR，一个从执行日志自动构建状态的轨迹驱动抽象机制，支持智能体行为MDP的在线构建。TriCEGAR将抽象表示为从轨迹学习并用反例精炼的谓词树。我们描述一个框架原生实现：(i)捕获带类型的智能体生命周期事件；(ii)从轨迹构建抽象；(iii)构建MDP；(iv)执行概率模型检查以计算Pmax(success)与Pmin(failure)等界。我们还展示运行似然如何支持异常检测作为护栏信号。