論文 E 実験タスクブック v2: AAAI の検証とエラー修正 UAV 言語計画

このラウンドでは「V1 バージョンでの直接修正」が必要なため、このファイルは依然として「paper-e-vera-uav-experiment-taskbook-v1-20260517.md」というファイル名を使用しています。テキスト、タイトル、リリース ノートはすべて v2 にアップグレードされました。この記事は最終的な論文草案ではなく、実行可能な実験課題の記述です。論文 E の研究の位置づけ、実際に引用可能な文書、アルゴリズムのソリューション、データ構築、比較実験、アブレーション実験、評価指標、理論的完全性の境界、およびその後の AAAI/T-ITS 推進計画を明確にします。 2026 年 5 月 19 日の補足的な焦点は、データ漏洩の防止、障害分類、パラメータの予算編成、指標の式、チャートの計画、および AAAI コンプライアンス リスクです。

---

1. 研究の背景と目的

都市部の低高度 UAV ミッション計画は、「エンジニアが事前に設定したルート」から「自然言語ミッション主導型」に移行しつつあります。実際のアプリケーションでは、オペレーターは次のような指示を与える可能性が高くなります。

• 「まず3号館東側ファサードを確認してから、屋上の着陸地点に行ってお待ちください。」
• 「病院上空を避け、30秒以内に臨時分娩エリアに到達してください。」
• 「南通路が占有されている場合は、西通路を迂回してください。ただし、全体を通して 20 メートル以上の安全な距離を保ちます。」

これらの指示には、意味の理解、時間的順序、空間的制約、連続軌道の安全性、および到達可能性の判断が同時に含まれます。大規模言語モデル (LLM) は、自然言語を理解して候補計画を生成することに優れていますが、出力計画が物理空間で実行可能であることは保証できませんし、航空安全上の制約が満たされていることも保証できません。形式的手法は、線形時相論理 (LTL) や信号時相論理 (STL) など、検証可能なセマンティクスを与えるのに適していますが、直接手書きで仕様を作成するには専門知識が必要であり、専門家以外のオペレーターが対応するのは困難です。

既存の研究では、自然言語から LTL への翻訳により、ロボット タスク仕様を作成するしきい値を大幅に下げることができることが証明されています。たとえば、Lang2LTL は複雑なナビゲーション コマンドを LTL に変換し、目に見えない環境で汎化評価を実行します [1]。 NL2LTL は、自然言語から LTL までのオープンソース Python パッケージを提供します [2]。 LTLCodeGen は、コード生成を使用して LTL の文法の正確さを改善し、それをロボットの経路計画に統合します [3]。 ConformalNL2LTL はさらに、翻訳精度を保証するために等角予測の使用を試みます [4]。これらの研究は、この研究の重要な基盤を提供します。しかし、低高度 UAV シナリオの場合、NL から LTL への変換を行うだけでは十分ではありません。 UAV ミッションには 3 つの追加要件があります。

1. 継続的な安全制約: 飛行高度、速度、障害物距離、時間枠などの制約は、当然連続信号に対する制約であり、STL の堅牢性によって評価するのがより適しています。
2. 実行可能な軌道閉ループ: 仕様が正しいことは、軌道が実行可能であることを意味するものではなく、マップ、ダイナミクス、プランナーによって検証される必要があります。
3. エラーは修正可能: LLM エラーはエラーとして判断されるだけでなく、検証者によって反例または堅牢性フィードバックに変換され、LLM 修正が実行される必要があります。

したがって、この記事では、VERA-UAV: UAV 自然言語タスク用の検証およびエラー修正神経記号計画フレームワークを提案します。 AAAI バージョンでは、次のような重要な質問に答えることが優先されます。

自然言語による UAV ミッションが与えられた場合、ネイティブのオープンソース LLM は、合理的に見えても安全であることが証明されていないテキストの計画を生成するだけでなく、検証可能、修復可能、実行可能な LTL/STL ミッションの仕様と軌道をどのように生成できるのでしょうか?

AAAI のメインカンファレンスバージョンは、AI プランニング、神経記号検証、LLM 自己修復に焦点を当てています。 AirSim、実際の低空物流、複数の UAV 空域スループットなどのシステム レベルのコンテンツは、後続の T-ITS 拡張バージョンに組み込まれる予定です。

---

2. 問題の定義と中心となる前提

2.1 入力と出力

UAV タスク インスタンスを指定すると、次のようになります。

このうち、 は自然言語タスク命令、 はセマンティック アノテーションを備えた都市低空地図、 は UAV の初期状態です。マップには、建物、飛行禁止区域、通行可能な空域、着陸地点、検査対象、動的障害物、高度レベルが含まれています。

システム出力:

\varphi_{\text{LTL}} = G(\neg 衝突) \wedge F(reach(goal)) \wedge G(\neg enter(no_fly_zone))

\varphi_{\text{STL}} = G_{[0,T]}(d_{\text{obs}}(t) \ge d_{\min}) \ウェッジ G_{[0,T]}(h_{\min} \le h(t) \le h_{\max}) \ウェッジ F_{[0,30]}(リーチ(目標))

軌道 が仕様を満たすことを示します。 の場合、検証者は違反条項、違反時間、および最小安全マージンを返します。

4.4 反例のドライバーの修復

バリデーターは単に「pass/fail」を返すのではなく、構造化された診断を返します。

{
  "status": "FAILED",
  "stage": "STL_ROBUSTNESS",
  "violated_clause": "G[0,T](distance_to_obstacle >= 10)",
  "counterexample_trace": [
    {"t": 14.2, "x": 38, "y": 51, "z": 30, "distance_to_obstacle": 6.4}
  ],
  "robustness": -3.6,
  "repair_hint": "Increase safety margin or route around building_7 west side."
}

LLM の修復プロンプトではフリー プレイは必要ありませんが、TaskIR の関連フィールドを変更することのみが必要です。

你生成的 TaskIR 在 STL 验证中失败。
失败子句：G[0,T](distance_to_obstacle >= 10)
反例：t=14.2s 时距离 building_7 仅 6.4m。
请只修改 route constraint 或 safety margin，不要改变用户原始目标。
输出新的 TaskIR JSON。

この設計の焦点は、LLM の検索スペースを削減し、修復動作を説明可能、記録可能、および再現可能にすることです。

連続した ラウンド後に LLM 修復が失敗した場合、シンボル列挙フォールバックに入ります。列挙スコープは、TaskIR DSL の深さ、マップ エンティティ セット、許可される制約テンプレート、および最大タスク範囲によって制限されます。列挙子は、安全な距離、迂回側、タイム ウィンドウ、ターゲット シーケンス、フォールバック ランディング パッドなどの診断結果に基づいて、最も関連性の高いフィールドの拡張を優先します。

4.5 軌道の生成

AAAI バージョンでは、軽量で再現可能な軌道ジェネレーターを使用します。

• 2D グリッド A*: 基本的なリーチ回避タスクおよび連続タスク用。
• 3D グリッド A*: 高さレベルと都市の低高度の廊下に使用されます。
• RRT*: 継続的な空間補足検証用。
• MPC-lite/軌跡スムージング: 回転半径、速度変化、高さ変化が単純化された力学制約を満たしているかどうかを確認するために使用されます。

軌道ジェネレーターはこの記事の革新的なものではありません。その機能は、仕様の変換の問題を「実行可能トラックが本当に存在するかどうか」というレベルまで進めることです。

---

5. 理論的特性と相対的な完全性の証明

v1 には「検証エラーの修正により信頼性が向上する」とだけ書かれていますが、数学的な境界はありません。 v2 はアルゴリズムの特性を明確にします。VERA-UAV は、LLM 自体が完全であるとは主張しませんが、有限の DSL、決定可能な検証者、および完全な基礎となるプランナーの仮定の下で 相対的な完全性 があると主張します。

5.1 正式な設定

都市の低高度マップを限定された重み付きマップに離散化します。

\tau = (v_0, v_1, \ldots, v_T), \quad (v_t,v_{t+1})\in E.

\mathcal{D}_{H,D} = {\psi: \mathrm{深さ}(\psi)\le D,\ \mathrm{horizon}(\psi)\le H,\ \mathrm{entities}(\psi)\subseteq \mathcal{E}(\mathcal{M})}。

C(\psi)=(\varphi_{\mathrm{LTL}},\varphi_{\mathrm{STL}})。

V(\タウ, C(\psi)) = \begin{ケース} \mathrm{PASS}, & \tau \models \varphi_{\mathrm{LTL}}\ \land\ \rho(\tau,\varphi_{\mathrm{STL}})>0,\ \mathrm{FAIL}(\eta)、& \text{そうでない場合}、 \end{件}

\tau \models \varphi_{\mathrm{LTL}} \quad \text{および} \quad \rho(\tau,\varphi_{\mathrm{STL}})>0。

\mathrm{FSR} = \frac{#{\mathrm{安全ではない\ しかし\ 実行可能ファイルとして\ 返されました}}}{#{\mathrm{すべて\ 返された\ 実行可能ファイル}}}。

P = \frac{|\hat{\mathcal{C}}\cap \mathcal{C}^\star|}{|\hat{\mathcal{C}}|}, \quad R = \frac{|\hat{\mathcal{C}}\cap \mathcal{C}^\star|}{|\mathcal{C}^\star|}, \quad F1 = \frac{2PR}{P+R}。

\mathrm{SVR} = \frac{#{\tau: 衝突 \lor nofly \lor 高度_violation \lor \rho(\tau,\varphi_{\mathrm{STL}})\le 0}} {#{\mathrm{返された\ 軌道}}}。

\mathrm{ギャップ}(\tau)=\frac{J(\tau)-J^\star}{\max(J^\star,\epsilon)}。

\mathrm{FailToPass} = \frac{#{\mathrm{最初\ 失敗、\ 最終\ 合格}}} {#{\mathrm{初期\ 失敗}}}、 \クアッド \mathrm{フォールバックコントリビューション} = \frac{#{\mathrm{LLM\修復\失敗、\シンボリック\フォールバック\パス}}} {#{\mathrm{最終\パス}}}。