Shepherd：一种通过形式化执行轨迹赋能元代理的运行时基底

本文提出 Shepherd，一种将元代理操作形式化为函数的函数式编程模型，核心机制在 Lean 中实现。该系统将每次交互记录为类型化事件，构建类 Git 的执行轨迹，支持状态分叉与重放，其进程分叉速度比 Docker 快五倍且提示缓存复用率超 95%。实验表明，其在运行时干预、反事实元优化及树形强化学习训练中显著提升代理性能，确立了其作为高效元代理编程基础设施的地位。