STLCG

用于可微分信号时序逻辑鲁棒性的 JAX 工具箱

许可证

BSD-2-Clause

概述

STLCG（以 JAX 库 stljax 形式发布）是一个利用计算图来计算信号时序逻辑（STL）公式鲁棒性的工具箱。STL 是一种用于表达时空需求的形式化语言，例如“在 10 秒内进入目标区域并停留 5 秒”，其鲁棒性度量量化了信号满足或违反某个规约的强度。stljax 在 JAX 中重新实现了 Stanford ASL 于 2019 年发布的原始 PyTorch 版 stlcg，用一种完全可并行化的基于掩码的表述取代了顺序循环求值，在 GPU 上可实现最高约 1000 倍的加速。由于整个流程都是可微分的，STL 规约可以直接嵌入到基于梯度的轨迹优化、强化学习奖励塑形以及参数挖掘中。发表于 IEEE Robotics and Automation Letters（RA-L）2025；可通过 stljax 使用 pip 安装。

stljax 让机器人工程师能够将人类可读的时序逻辑任务规约转化为可微分的目标项与约束项。你可以通过 Expression 和 Predicate 构建 STL 公式，在信号或轨迹上评估其鲁棒性，并且——由于一切都基于 JAX 实现——可通过 vmap 获得批量评估，并获得用于优化器和学习循环的精确梯度。其关键设计选择是对时序算子（Always/Eventually/Until）进行基于掩码的重新表述，将原本的顺序循环计算并行化，在带来数量级加速的同时，也能在所有 min/max 运算上正确地分配梯度。

为何重要

信号时序逻辑为机器人提供了一种精确、人类可读的方式来规定时序和空间任务需求，但多年来其鲁棒性计算一直是顺序式的、缓慢且难以微分——这使得 STL 无法融入现代学习和优化流程。stljax 消除了这一障碍：一种并行化、原生支持自动微分的实现使 STL 足够快，可用于实时控制和大批量训练，从而使规约能够直接充当规划器目标、RL 奖励或验证信号。

解决的问题

以往的 STL 鲁棒性工具依赖顺序循环计算，速度慢且难以微分，这限制了形式化时序逻辑规约在基于梯度的轨迹优化和学习中的应用。

要点

• 基于掩码的并行 STL 鲁棒性计算，在 GPU 上比循环式方法最高快约 1000 倍
• 原生 JAX：支持 vmap 批处理与精确梯度，并在 min/max 上正确分配梯度
• 用于构建 Always/Eventually/Until 公式的 Expression 与 Predicate API
• 可微分规约，可在轨迹优化和 RL 中用作目标/约束
• 可通过 pip 安装（stljax）；RA-L 2025；Stanford ASL PyTorch 版 stlcg 的后继者

适用人群

• 运动规划与轨迹优化研究人员
• 控制与形式化方法研究人员
• 强化学习奖励设计者
• 安全自主与验证工程师

局限

• 需要熟悉信号时序逻辑才能编写有用的规约
• 对鲁棒性函数的平滑/近似会带来精度/梯度的权衡
• 依赖 JAX 及其工具链
• 这是一个规约评估库——本身不包含规划器或控制器