STLCG

微分可能な信号時相論理（STL）ロバストネスのための JAX ツールボックス

ライセンス

BSD-2-Clause

概要

STLCG（JAXライブラリ stljax として配布）は、計算グラフを用いて信号時相論理（Signal Temporal Logic, STL）式のロバストネスを計算するためのツールボックスです。STLは「10秒以内に目標領域に進入し、5秒間とどまる」といった時空間的要求を表現するための形式言語であり、そのロバストネス尺度は、信号が仕様をどれだけ強く満たす、または違反するかを定量化します。stljax は、2019年に Stanford ASL が開発したオリジナルの PyTorch 版 stlcg を JAX で再実装したもので、逐次的な再帰評価を完全に並列化可能なマスキングベースの定式化に置き換え、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 への依存とそのツールチェーン
• 仕様評価ライブラリであり、プランナーやコントローラ自体は含まれない