Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs

技術要約：階層的意味論分解による自然言語と形式仕様の架け橋

問題提起
自然言語（NL）によるソフトウェア要件を、線形時相論理（LTL）などの形式仕様へと正確かつ自動的に翻訳することは、航空宇宙分野のような安全性が極めて重要な産業領域において、形式検証をスケールアップさせる際の決定的なボトルネックとなっている。現在の業界慣行は、人間の専門家による手動の翻訳に大きく依存しており、このプロセスは時間がかかる上に誤りが生じやすい。ルールベースの手法から学習ベースの手法に至る既存の自動化アプローチは、一定の自動化を実現しているものの、重大な限界に直面している。ルールベースの手法は柔軟性に欠け、自然言語の多様性に苦慮する。一方で、学習ベースのアプローチは、訓練データを超えた汎化に失敗することが多い。また、近年の大規模言語モデル（LLM）は、意味抽出には長けているものの、実世界の産業要件に特有の、暗黙的な時相意味論、深くネストされた論理構造、およびコンテキスト固有の制約への対応に苦慮している。LLMを直接適用すると、「サイレント・フェイラー（静かなる失敗）」、すなわち、生成された数式は構文的には正しいものの、エラーの累積や構造的検証の欠如により意味論的に誤っているという事態を招くことが多い。

手法：REQ2LTLフレームワーク
これらの課題に対処するため、著者らは、新しい階層的中間表現であるOnionLを通じてNLとLTLを橋渡しするモジュール式フレームワークであるREQ2LTLを提案する。本フレームワークは、LLMの意味抽出能力と、決定論的なルールベース合成による構造的保証を組み合わせた、2段階のパイプラインによって動作する。

1. 中間表現（OnionL）：
   OnionLは、時相意味論、スコープ、および論理関係を明示的にエンコードするように設計された、ツリー構造の中間言語である。これは、要件を以下の3つの構成要素に分解する。

   • 原子命題（APs）： セマンティックなサブフィールド（コンポーネント、変数、関係、数式）が付加された述語レベルの事実。
   • スコープ： 単項演算子（例：Globally、Eventually、Next）またはモードベースの前件に対応する文脈的境界。
   • 関係： サブフォーミュラを接続する論理的または時相的な依存関係（例：And、Or、Implies、Until）。
     この構造はLTLの構成的構文を反映しており、LLMが局所的な意味解析に集中し、グローバルな論理構成をルールベースのメカニズムに委ねるためのセマンティックな架け橋として機能する。

2. 第1段階：REQ2ONIONL（意味論的分解）：
   このモジュールは、プロンプト誘導型のLLMを利用して、自由形式のNL要件を構造化されたOnionLツリーへと変換する。ここでは、BUILDING-ONIONLと呼ばれる特定の思考連鎖（Chain-of-Thought）アルゴリズムを採用しており、以下の2段階で動作する。

   • マクロ構造の抽出： グローバルな時相またはモードベースのスコープを特定し、トップレベルのノードを構築する。
   • 再帰的な節の分解： 節を、入れ子になったスコープ、関係、および正規化された原子命題へと再帰的に分解する。
     このプロセスは、OnionLの再帰的文法を定義する知識リポジトリによってガイドされ、産業パターンに関する数ショットの例示によって強化される。

3. 第2段階：ONIONL2LTL（ルールベース合成）：
   このモジュールは、検証されたOnionLツリーから標準化されたLTL数式への、決定論的かつルールベースの翻訳を行う。

   • 検証： 翻訳の前に、深さ優先探索を実行して、構造的な適格性（例：演算子の正しいarity、有効なスコープのネスト）を検証する。安全性が重要なアプリケーション向けに、本フレームワークは、エンジニアによる検査と修正のためにOnionL構造を可視化（Mermaidダイアグラム経由）する「ヒューマン・イン・ザ・ループ」メカニズムをサポートしている。
   • 翻訳： ポストオーダー（後順）走査により、各ノードを対応するLTL構文（例：Globallyを$\text{G}$へ、Impliesを$\rightarrow$へマッピング）に変換する。このプロセスにより、出力が構成的に構文的に正しいことが保証される。

主な貢献

• OnionL中間表現： 時相意味論と論理関係を明示的にエンコードし、NLとLTLの間の堅牢なセマンティック・ブリッジとして機能する階層的言語。
• 階層的意味論分解： 要件を体系的に分解する、プロンプト駆動型の2段階アルゴリズム（BUILDING-ONIONL）により、構造的完全性と意味的精度を大幅に向上させる。
• REQ2LTLフレームワーク： LLMベースの分解と、決定論的なルールベースの翻訳および検証を組み合わせた自動化パイプライン。既存の手法と比較して、優れた精度と完全な構文的正確性を達成する。

実験結果
著者らは、学術的ベンチマーク（Circuit、Navigation、Office Email）と、112個の航空宇宙要件からなる実世界の産業データセットの両方を用いてREQ2LTLを評価した。

• 産業における性能： 航空宇宙データセットにおいて、REQ2LTLは88.4%の意味的精度（Exact Match）と100%の構文的正確性を達成した。これは、入れ子状の論理や暗黙的な時相の手がかりに苦慮し、Exact Match率が55%から65%の間であった最先端のベースライン（例：NL2SPEC、NL2LTL、NL2TL）を大幅に上回る結果となった。
• 学術的性能： 学術的ベンチマークにおいて、REQ2LTLは一貫して高いパフォーマンス（Binary Accuracy >94%、BLEU >0.97）を示し、曖昧さの少ない設定においても効果的に汎化できることを示した。
• アブレーション研究： 実験により、構造化モデリング（OnionL）、段階的なプロンプティング、および検証フィードバックの組み合わせが不可欠であることが確認された。構造化された中間表現を削除すると、意味的精度は65.2%に低下し、段階的なプロンプティングを削除すると58.9%に低下した。
• エラー分析： 本フレームワークは、ゼロショットや他のベースライン手法で頻発していた、時相の誤解釈、条件の混乱、およびネストの喪失に関連するエラーを効果的に排除した。残存するエラーは、主に、入力要件に内在する言語的な曖昧さに起因していた。

意義と主張
本論文は、REQ2LTLが非形式的な自然言語要件と形式仕様の間の溝を効果的に埋め、安全性が重要な産業システムにおけるスケーラブルな採用のための実用的な基盤を提供することを主張している。構造化された中間表現と、LLMとルールベースのハイブリッドアーキテクチャを導入することで、本フレームワークは直接的なLLM翻訳の限界、特に暗黙的な時相意味論と深い論理ネストの問題に対処している。著者らは、ルールベースの合成を通じて100%の構文的正確性を保証する能力と、高い意味的忠実度を組み合わせることで、REQ2LTLが産業用検証ワークフローにおける実行可能なツールとなることを強調している。さらに、可視化されたヒューマン・イン・ザ・ループの検証ステップを含めることで、言語的な曖昧さの問題に対処し、エンジニアが自動化パイプラインを壊すことなく、効率的に意味的エラーを修正できるようにしている。著者らは、現在の研究はLTLに焦点を当てているが、将来的にはSignal Temporal Logic (STL) や Metric Temporal Logic (MTL) のような、より表現力の高い時相論理への拡張が可能であると述べている。