NL2STL:CCG解析・意味合成を用いた確率付き信号時相論理仕様候補の生成

信号時相論理（SignalTemporalLogic:STL）を含む時相論理（TemporalLogic:TL）は，「いつ」「どの状態が」「どの順序で」成立すべきか，といった時間的・空間的な制約を厳密な形式で記述することができる．ロボティクスや自律システムを扱う工学分野では，TL/STL仕様に基づく経路計画や制御器設計の手法が数多く検討されている．一方で，TL/STLのシンタックスに基づいた仕様記述には一定の専門知識が求められるため，最近では自然言語（NaturalLanguage:NL）仕様からTL/STL仕様へ自動変換する枠組み（NL-to-TL/STL）が注目されている．例えば，先行研究[1]では，大規模言語モデル（LargeLanguageModels:LLMs）を用いて大規模な{NL,TL}のペアデータを構築し，テキスト変換モデルを教師あり学習する枠組みを提示している．このようなLLMを用いた学習型アプローチは，十分なデータがある状況では高精度化が期待でき，実用に向けた重要な方向性である．しかしながら，自然言語に基づく仕様の生成では，自然言語の意味曖昧性に由来する解釈の不確定性が残る．より具体的には，自然言語文は，同一の表現であっても複数の妥当な解釈を許すことがあり，STLのように作用域（scope）や入れ子構造が意味に直結する形式仕様へ変換する際に，その不確定性が顕在化しやすい．例えば，Within10seconds,reachBorreachCwhileavoidingA.という文では，whileavoidingAがreachCのみに係る（局所スコープ）解釈と，reachBorreachC全体に係る（大域スコープ）解釈の双方が成立し得る．このような場合において，どちらか一方のみを「正解」とみなすことは必ずしも適切ではなく，むしろ複数の妥当な仕様候補を提示し，人間（仕様設計者）が選択・検証できる形にすることは，システムの信頼性や安全性を担保するうえで非常に重要である．そこで本研究では，曖昧なNL入力に対して複数の解釈候補に対応するSTL仕様候補集合を生成し，さらに各候補に確率（重み）を付与して提示する枠組みを構築する．具体的には，組合せ範疇文法（CombinatoryCategorialGrammar:CCG）に基づく構文解析から得られる𝑛-best構文木（parsetree）を用いて複数の統語構造をもとに，ccg2lambda[2]により意味合成（semanticcomposition）を行うことにより，NLの解釈候補を明示的に列挙し，曖昧性が生じる箇所（例：修飾句の係り先）を候補分岐として保持したまま複数のSTL候補を得ることを目指す．本研究の主な貢献は以下のとおりである．•STL仕様生成に適したsemantictemplate（語彙・構文範疇への意味付与）を設計し，CCGに基づく構文解析に沿って意味合成できる形に整理する．•𝑛-best解析により同一のNLから複数の妥当な解釈構造を導出し，曖昧性をSTL候補集合として扱う枠組みを示す．•候補に対してスコアに基づく重み（確率）を付与し，さらに同一STL（あるいは同一の構造パターン）に対応する導出を集約することで，曖昧性を確率として提示できることを示す．Thisworkispublishedwithoutpeerreviewandislicensedbytheauthor(s)underCCBY4.0(https://creativecommons.org/licenses/by/4.0/).org/licenses/by/4.0/).集合と導出確率を得て，各構文木に対してsemantictemplateに基づく意味合成を行い，得られた意味表現をSTLへ変換したうえで同一性判定のために正準化する．最後に，同一のSTL・構造パターンについて集約して，𝑆(ℓ)を構成する．3.3原子命題とタスク表現本稿ではSTLの原子命題を𝜙𝑅で統一し（式(3)），到達・回避などのタスクを式(4)–(5)のように表す．これにより，NL側の語彙（reach,avoid,within,or,whileなど）が最終的にどの時相演算子（F,G,U）とどの原子命題（𝜙𝐴,𝜙𝐵,𝜙𝐶）へ変換されるかが明確になる．3.4CCGによる𝑛-best構文解析入力文ℓに対して，CCGparserにより上位𝐾個の構文木˜T𝐾(ℓ)={(𝑇𝑖,˜𝑞𝑖)}𝐾𝑖=1(9)を得る．ここで𝑇𝑖は構文木，˜𝑞𝑖はparserが出力する導出確率（導出スコアに基づいて変換された確率）である．𝑛-best解析では，∑𝐾𝑖=1˜𝑞𝑖≤1となり得る．以降では，𝑛-bestの範囲で確率が総和1となるように𝑞𝑖:=˜𝑞𝑖∑𝐾𝑘=1˜𝑞𝑘(𝑖=1,...,𝐾)(10)で再正規化した𝑞𝑖を用いる．3.5semantictemplateと意味合成区間を引数に取る中間表現自然言語に現れる時間表現（例：within10seconds）を一貫して扱うため，本研究では文（あるいはVP）レベルの意味を，時間区間𝐼を受け取りSTLを返す関数𝑓:I→STLとして表す中間表現を導入する．ここでIは時間区間の集合であり，例えばI={[𝑎,𝑏]|0≤𝑎≤𝑏}のような有界区間全体を想定する．例えば「reach𝑅」は𝐼上での到達制約F𝐼𝜙𝑅を返す関数として表される．この型付けにより，within節は「区間𝐼=[0,𝑇]を導入して𝑓(𝐼)を評価する演算」として自然に合成できる．構文木に沿った意味合成各構文木𝑇𝑖に対して，ccg2lambdaに基づき意味合成を行う．語彙項目（または構文範疇）にSTL指向のsemantictemplate（𝜆式）を割り当て，構文木に沿って関数適用（および簡約）を実行することで，文全体の意味表現𝑀𝑖を語彙項目（例）semantictemplate（𝜆式）reach𝜆𝑅.𝜆𝐼.F𝐼𝜙𝑅avoid𝜆𝑅.𝜆𝐼.G𝐼¬𝜙𝑅or𝜆𝑓.𝜆𝑔.𝜆𝐼.𝑓(𝐼)∨𝑔(𝐼)and𝜆𝑓.𝜆𝑔.𝜆𝐼.𝑓(𝐼)∧𝑔(𝐼)while𝜆𝑓.𝜆𝑔.𝜆𝐼.𝑓(𝐼)∧𝑔(𝐼)within𝜆𝑇.𝜆𝑓.𝑓([0,𝑇])得る：𝑀𝑖=Comp(𝑇𝑖;Θ),(11)ここでΘはsemantictemplateの集合である．修飾句の係り先の違い（例：while節の付加位置）は，どの部分式にsemantictemplateが適用されるかの違いとして現れ，結果としてSTLのスコープの違いに対応する．semantictemplateの例紙面の都合上，主要語彙の代表例のみを表1に示す．以下では型注釈を簡略化して記す（𝑅は領域ラベル，𝑇は時間長）．例えばWithin10seconds,reachBorreachCwhileavoidingA.に対して，while節がreachCに付加される構文ではor(reach(𝐵),while(reach(𝐶),avoid(𝐴)))が構成され，while節が選言全体に付加される構文ではwhile(or(reach(𝐵),reach(𝐶)),avoid(𝐴))が構成される．両者にwithin10が適用されることで，第2章で示した例（局所／大域スコープ）に対応するSTL候補へ変換される．3.6STL候補の同定と確率集約STLへの変換と正準化構文木ごとに得た意味表現𝑀𝑖をSTLへ変換し，正準化することでˆ𝜑𝑖を得る：ˆ𝜑𝑖=Cano(𝑀𝑖).(12)ここでCano(·)は，例えば以下を含む：•中間表現が𝑓:I→STLの形であれば，既定の区間𝐼defを適用して閉じたSTLを得る（within節が存在する場合はその指定区間が優先される）．•∧/∨の結合順の統一，冗長な括弧の除去，重複部分式の簡約．これにより，異なる構文木から得られた式が同一STLに対応する場合に，機械的に同定できるようにする．org/licenses/by/4.0/).SemantictemplatesforSTL同一STLへの集約異なる構文木が同一のSTLへ変換される場合があるため，導出確率をSTL側で集約する．候補STL𝜑の確率を𝑃(𝜑|ℓ)=∑𝑖:ˆ𝜑𝑖=𝜑𝑞𝑖(13)で定義する．得られた𝑚個の異なる候補{𝜑𝑗}𝑚𝑗=1（𝑚≤𝐾）に対し，（𝑛-best近似や失敗導出の除外等に備えて）再正規化した確率𝑝𝑗=𝑃(𝜑𝑗|ℓ)∑𝑚𝑘=1𝑃(𝜑𝑘|ℓ)(14)を用いて𝑆(ℓ)を構成する．4実験4.1設定本章では，図1で示した提案手法が，曖昧な自然言語仕様ℓから複数のSTL候補を生成し，式(8)の形式で確率付き候補集合𝑆(ℓ)を得られることを，代表例により確認する．CCG構文解析には確率的CCGパーサの一つであるdepccgを用い，入力文ℓに対して上位𝐾=50個の構文木集合˜T𝐾(ℓ)={(𝑇𝑖,˜𝑞𝑖)}𝐾𝑖=1を取得した．スコア˜𝑞𝑖は式(10)により正規化し，意味合成（式(11)），正準化（式(12)），集約（式(13)–(14)）を行った．そして，自然言語仕様ℓを次のように与えた：ℓ=Within10seconds,reachBorreachCwhileavoidingA.前述のとおり，この文はwhileavoidingAの作用域により局所／大域スコープの2通りの妥当な解釈を許すものである．4.2生成されたSTL候補および確率本稿の記法に従い，到達はF[0,10]𝜙𝑅，回避はG[0,10]¬𝜙𝐴と表す．このとき，局所／大域スコープに対応する代表的なSTL候補は，第2章で導入した式(6),(7)で与えられる．NLspecificationSemanticCompositionCanonicalizationAggregationInputOutputCCGparser(n-best)STLspecificationSTL候補確率𝜑local0.5935𝜑global0.4065提案手法では，各構文木𝑇𝑖から得られるˆ𝜑𝑖を正準化して同一性判定を行い，式(13)により同一STLに確率を集約する．本例では，𝐾=50個の導出は最終的に2種類のSTLに集約され，候補数は𝑚=2となった．ここで，正準化後のSTL候補が𝜑local（局所）または𝜑global（大域）のいずれに一致するかにより，導出インデックス集合を𝐼local:={𝑖|ˆ𝜑𝑖=𝜑local},𝐼global:={𝑖|ˆ𝜑𝑖=𝜑global}と定義する．このとき，式(13)に基づく確率は𝑃(𝜑local|ℓ)=∑𝑖∈𝐼local𝑞𝑖=0.5935,(15)𝑃(𝜑global|ℓ)=∑𝑖∈𝐼global𝑞𝑖=0.4065,(16)となった．したがって，最終出力は式(8)の形式で𝑆(ℓ)={(𝜑local,0.5935),(𝜑global,0.4065)}(17)と与えられる．結果は表2に示すとおりである．4.3まとめ本例では，式15–16より，曖昧な自然言語仕様から2つのSTL仕様候補とその確率が得られた．このように，提案手法はSTL仕様を一意に定めるのではなく，妥当な解釈候補を複数保持し，複数のSTL仕様とその確率を提示できることを確認した．5おわりに本稿では，曖昧なNL入力に対して複数の解釈候補に対応するSTL仕様候補集合を生成し，さらに各候補に確率（重み）を付与して提示する枠組みを構築した．org/licenses/by/4.0/).