NL2SpaTiaL：自然言語から操作タスク向けの幾何学的時空間論理仕様を生成する

概要: 時相論理（Temporal Logic）はロボティクスに対する厳密な検証の枠組みを提供しますが、通常は軌道（トラジェクトリ）レベルの信号に対して動作し、操作の中心となる対象中心の幾何学的関係を本来的に表現することはできません。時空間論理（Spatio-Temporal Logic, SpaTiaL）は、幾何学的な空間要件を明示的に捉えることでこれを克服し、操作タスクの検証に自然な形式主義を提供します。その結果、自然言語（NL）を検証可能な SpaTiaL の仕様へ翻訳することは重要な目的です。しかし、既存の NL-to-Logic 手法では仕様を平坦な列（フラットなシーケンス）として扱うため、入れ子になった時間的スコープと空間関係が絡み合い、深いネストのもとでは性能が急激に低下してしまいます。私たちは、仕様を階層的論理木（Hierarchical Logical Trees, HLT）としてモデル化する枠組み NL2SpaTiaL を提案します。式を単発で、構造化された HLT として生成することで、私たちの手法は意味のパースと構文上のレンダリングを切り離し、人間の合成的（コンポジショナル）な空間推論に整合します。これを支えるため、私たちの知る限り、論理を起点とした合成（synthesis）パイプラインによる明示的な階層的監督を備えた、最初の NL-to-SpaTiaL データセットを構築します。オープンウェイトの LLM による実験では、提案する HLT の定式化が、論理の深さがさまざまな場合において、平坦生成のベースラインを大幅に上回ることを示しています。これらの結果は、スケーラブルな NL-to-SpaTiaL 翻訳には、明示的な HLT 構造が不可欠であることを示しており、最終的に、言語条件付ロボティクスにおいて候補となる軌道を検証するための厳密な「生成してテストする（generate-and-test）」パラダイムを可能にします。プロジェクトのウェブサイト: https://sites.google.com/view/nl2spatial