論文「Automated LTL Specification Generation from Industrial Aerospace Requirements」の技術的サマリー

本論文は、航空宇宙分野の安全クリティカルなソフトウェア開発において、自然言語（NL）で記述された要件から線形時相論理（LTL）仕様を自動生成するフレームワーク**「AeroReq2LTL」**を提案するものです。産業現場における形式手法の導入障壁である「要件の形式化のボトルネック」を、大規模言語モデル（LLM）とドメイン固有の知識を融合させることで解決し、実用的な検証ツールへの直接接続を実現しています。

以下に、問題定義、手法、主要な貢献、評価結果、および意義について詳細をまとめます。

---

1. 背景と問題定義

航空宇宙制御ソフトウェアの検証には、複雑なシステム特性を数学的に厳密に記述する LTL が広く用いられています。しかし、産業現場では以下の課題により、自然言語の要件を LTL に変換する作業が依然として手作業に依存し、高コストかつ誤りやすい状態にあります。

• 専門用語の曖昧さと断片化: 産業要件には高度に専門的な用語や略語が含まれており、一般的な LLM はこれらを文脈なく断片化して解釈し、意味をなさない原子命題を生成する傾向があります。
• 暗黙の時間的・論理構造: 産業ドキュメントでは、「スイッチする」「継続する」といった表現が暗黙的に時間演算子（Next, Until など）や状態遷移を意味しますが、これらが明示されていないため、LLM は重要な時間的制約を見落としたり、誤って解釈したりします。
• 文脈の欠如: 要件文単体ではなく、インターフェース定義（信号名、データ型、初期値など）や制御サイクルなどの工学的アーティファクトと照合しないと、正しい変数を特定できません。既存の NL-to-LTL ツール（NL2SPEC, NL2TL など）は、合成ベンチマークでは機能しても、このような複雑な産業ドキュメントでは精度が著しく低下します。

2. 提案手法：AeroReq2LTL フレームワーク

AeroReq2LTL は、LLM の推論能力を活用しつつ、2 つの産業向けイノベーション（SpaceKG と SpaceRDL）によって上記の課題を克服する 3 段階のワークフローを採用しています。

全体ワークフロー

1. 双ストリーム文脈再構築 (Dual-stream Context Reconstructing):
   • 要件文書から「目標ストリーム（要件パラグラフ）」と「知識ストリーム（インターフェース定義テーブル）」を抽出します。これにより、LLM が孤立した文ではなく、システムの実装コンテキスト（信号名、制御周期など）を考慮した推論を行えるようにします。
2. NL からテンプレート自然言語（TNL）への書き換え:
   • 生きた自然言語を、構造化された中間表現である「Templated Natural Language (TNL)」に変換します。この段階で、暗黙の制約を明示化し、専門用語を正規化します。
3. TNL から LTL への変換:
   • 構造化された TNL を、確率的な生成ではなく決定論的な変換ルールを用いて LTL 式に変換します。これにより、構文的に有効かつ意味的に整合性の取れた仕様を生成します。

主要な技術的貢献

(1) SpaceKG: ドメイン固有のデータ辞書（意味的グラウンディング）

• 目的: 専門用語の断片化を防ぎ、自然言語の意図をコードレベルの原子命題に正確にマッピングする。
• 仕組み: インターフェース定義テーブルから変数名、データ型、値範囲を抽出し、BERT ベースの分類と専門家によるマッピングを経て、ドメイン用語を正規化された「原子パラダイム（Atomic Paradigms）」に変換します。
  • 例：「角速度の絶対値が 0.15°/s 未満」という記述を、単なる文字列ではなく、システム変数 dwCount と閾値を用いた dwCount > 44.8s などの厳密な条件式として定義します。

(2) SpaceRDL: 構造化要件記述言語（暗黙の制約の明示化）

• 目的: 暗黙の時間的・論理的仮定を明示的な構造に変換する。
• 仕組み: 航空宇宙制御ロジックの特性に基づき、workmode, condition, timing, action などの必須フィールドを持つテンプレート言語を定義します。
  • LLM は、自由な文章をこのテンプレートに当てはめることで、「即時（immediately）」や「次のサイクル（next）」といった時間的意図を強制的に明示させられます。
  • これにより、要件文が「状態遷移」「境界チェック」「モード変更」などの明確なパターンに分類され、曖昧さが排除されます。

3. 評価結果

実世界の宇宙船制御システム（ACS-LEOS）から抽出した 79 の生産要件（SSCS モジュール）を用いて評価を行いました。

• データセット: 実際の宇宙機姿勢制御ソフトウェアの要件文書（38 ページ、79 要件）。
• ベースライン: 既存の NL-to-LTL ツール（NL2LTL, NL2SPEC）および、ゼロショットで LLM（GPT-4o, GPT-3.5, DeepSeek）に直接変換させる手法。
• 主要指標: 精度（Precision）と再現率（Recall）。

結果:

• AeroReq2LTL + GPT-4o: 精度 85%、再現率 88% を達成。
• ベースラインとの比較: 既存の最善の手法（NL2SPEC + GPT-4o）が精度 61%、再現率 61% だったのに対し、大幅に上回りました。
• アブレーション研究:
  • SpaceKG を除去した場合：精度 69%、再現率 70% に低下（用語の誤マッピングが原因）。
  • SpaceRDL を除去した場合：精度 52%、再現率 54% に激減（時間的構造の欠落や誤った演算子の使用が原因）。
  • 両者の組み合わせが精度向上に不可欠であることが証明されました。

実用性検証:
生成された LTL 仕様は、産業用検証ツール「TRACE」に直接入力され、実行トレースとの照合に成功しました。76 件の要件のうち 67 件が正しく LTL に変換され、そのうち 63 件が検証ツールによって検証可能であることが確認されました。

4. 意義と結論

本論文の提案する AeroReq2LTL は、以下の点で航空宇宙分野の形式手法実用化に重要な意義を持ちます。

1. 産業現場への適合性: 単なるテキスト変換ではなく、インターフェース定義やドメイン知識を統合した「双ストリーム」アプローチにより、実務で発生する複雑な要件の形式化を可能にしました。
2. 信頼性の向上: 確率的な LLM 生成を「構造化テンプレート（TNL）」と「決定論的変換」によって制御することで、検証ツールで直接使用可能な高品質な LTL 仕様を生成します。
3. ワークフローの自動化: 要件文書から検証ツールの入力までをエンドツーエンドで自動化し、手作業による形式化の負荷を大幅に軽減します。

今後は、自動車や医療システムなど他の安全クリティカル分野への拡張、および機能性・セキュリティ要件への対応、SpaceKG のさらに高度な形式化が今後の課題として挙げられています。本フレームワークは、航空宇宙ソフトウェアの品質保証プロセスを革新し、より厳格かつ効率的な開発を実現する道筋を示しました。