STLCG

用於可微分訊號時序邏輯穩健度的 JAX 工具箱

授權條款

BSD-2-Clause

概述

STLCG（以 JAX 函式庫 stljax 的形式發布）是一套利用計算圖來計算訊號時序邏輯（STL）公式穩健度的工具箱。STL 是一種用來表達時空需求的形式語言，例如「在 10 秒內進入目標區域並停留 5 秒」，而它的穩健度量測則量化訊號滿足或違反規格的程度。stljax 以 JAX 重新實作 2019 年 Stanford ASL 原本以 PyTorch 撰寫的 stlcg，將循序的遞迴求值替換為可完全平行化、以遮罩為基礎的表述，在 GPU 上最多可快約 1000 倍。由於整個流程都可微分，STL 規格可以直接嵌入基於梯度的軌跡最佳化、強化學習的獎勵塑形與參數探勘中。發表於 IEEE Robotics and Automation Letters（RA-L）2025；可透過 pip 以 stljax 安裝。

stljax 讓機器人工程師能把人類可讀的時序邏輯任務規格，轉換成可微分的目標與約束項。你可以用 Expressions 與 Predicates 建立 STL 公式，在訊號或軌跡上評估其穩健度；而且由於一切都以 JAX 實作，可以透過 vmap 進行批次評估，並取得精確的梯度，供最佳化器與學習迴圈使用。關鍵的設計選擇，是以遮罩為基礎重新表述時序運算子（Always/Eventually/Until），把原本循序的遞迴計算平行化，帶來數量級的加速，同時也讓梯度在所有 min/max 運算之間正確分配。

為何重要

訊號時序邏輯為機器人提供一種精確、人類可讀的方式來規範時間與空間上的任務需求，但多年來它的穩健度計算是循序的、緩慢的，也難以微分，使 STL 無法進入現代的學習與最佳化流程。stljax 消除了這道障礙：平行化且原生支援自動微分的實作，讓 STL 快到足以用於即時控制與大批次訓練，使規格能直接作為規劃器目標、強化學習獎勵或驗證訊號。

解決的問題

先前的 STL 穩健度工具依賴循序的遞迴計算，既緩慢又難以微分，限制了形式化時序邏輯規格在基於梯度的軌跡最佳化與學習中的應用。

重點

• 以遮罩為基礎的平行 STL 穩健度計算，在 GPU 上比遞迴方法最多快約 1000 倍
• 原生 JAX：vmap 批次處理與精確梯度，並在 min/max 之間正確分配梯度
• Expression 與 Predicate API，用於建立 Always/Eventually/Until 公式
• 可微分的規格可作為軌跡最佳化與強化學習中的目標或約束
• 可透過 pip 安裝（stljax）；RA-L 2025；Stanford ASL PyTorch 版 stlcg 的後繼者

適用對象

• 運動規劃與軌跡最佳化研究人員
• 控制與形式化方法研究人員
• 強化學習獎勵設計者
• 安全自主與驗證工程師

限制

• 需要熟悉訊號時序邏輯，才能撰寫有用的規格
• 穩健度函數的平滑化／近似，會帶來精度與梯度之間的取捨
• 依賴 JAX 及其工具鏈
• 屬於規格評估函式庫，本身不包含規劃器或控制器