Paper E Experimental Task Book v2: Verification and Error Correction UAV Language Planning for AAAI

This file still uses the file name paper-e-vera-uav-experiment-taskbook-v1-20260517.md because this round requires “direct modification on the V1 version”. The text, title and release notes have all been upgraded to v2. This article is not a final paper draft, but an executable experimental task statement: clarify the research positioning of Paper E, real citable documents, algorithm solutions, data construction, comparative experiments, ablation experiments, evaluation indicators, theoretical completeness boundaries and subsequent AAAI/T-ITS promotion plans. Supplementary focus on 2026-05-19 is: data leakage prevention, failure taxonomy, parameter budgeting, indicator formulas, chart planning and AAAI compliance risks.

---

1. Research background and goals

Urban low-altitude UAV mission planning is moving from “engineer-preset routes” to “natural language mission-driven”. In actual applications, operators are more likely to give the following instructions:

• “First check the east facade of Building 3, then go to the landing point on the roof and wait.”
• “Avoid the air above the hospital and reach the temporary delivery area within 30 seconds.”
• “If the south corridor is occupied, bypass the west corridor but keep a safe distance of more than 20 meters throughout.”

These instructions simultaneously include semantic understanding, temporal order, spatial constraints, continuous trajectory safety, and reachability judgments. Large language models (LLM) are good at understanding natural language and generating candidate plans, but they cannot guarantee that the output plan is executable in physical space, nor can it guarantee that aviation safety constraints are met. Formal methods are good at giving verifiable semantics, such as Linear Temporal Logic (LTL) and Signal Temporal Logic (STL), but direct handwritten specifications require professional knowledge and are difficult to serve non-expert operators.

Existing work has proven that natural language to LTL translation can significantly reduce the threshold for writing robot task specifications. For example, Lang2LTL converts complex navigation commands into LTL and performs generalization evaluation in unseen environments [1]; NL2LTL provides an open source Python package from natural language to LTL [2]; LTLCodeGen uses code generation to improve the grammatical correctness of LTL and integrates it into robot path planning [3]; ConformalNL2LTL further attempts to use conformal prediction to guarantee translation accuracy [4]. These works provide an important foundation for this study.But for low-altitude UAV scenarios, just doing NL-to-LTL translation is not enough. UAV missions have three additional requirements:

1. Continuous safety constraints: Constraints such as flight altitude, speed, obstacle distance, time window, etc. are naturally constraints on continuous signals, and are more suitable to be evaluated by STL robustness.
2. Executable Trajectory Closed Loop: Correct specifications do not mean that the trajectory is feasible and must be verified by maps, dynamics and planners.
3. Errors can be fixed: LLM errors should not only be judged as errors, but should be converted into counterexample or robustness feedback by the verifier, and then drive LLM correction.

Therefore, this article proposes VERA-UAV: a verification and error-correcting neuro-symbolic planning framework for UAV natural language tasks. The AAAI version prioritizes answering a core question:

Given a natural language UAV mission, how can a native open source LLM generate verifiable, repairable, and executable LTL/STL mission specifications and trajectories, rather than just generating textual plans that appear reasonable but are not provably safe?

The AAAI main conference version focuses on AI planning, neuro-symbolic verification and LLM self-repair. System-level content such as AirSim, real low-altitude logistics, and multi-UAV airspace throughput will be put into subsequent T-ITS extended versions.

---

2. Problem definition and core assumptions

2.1 Input and output

Given a UAV task instance:

Among them, is the natural language task instruction, is the urban low-altitude map with semantic annotation, and is the UAV initial state. The map contains buildings, no-fly zones, passable airspace, landing points, inspection targets, dynamic obstacles and altitude levels.

System output:

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

\varphi_{\text{STL}} = G_{[0,T]}(d_{\text{obs}}(t) \ge d_{\min}) \wedge G_{[0,T]}(h_{\min} \le h(t) \le h_{\max}) \wedge F_{[0,30]}(reach(goal))

Indicates that the trajectory satisfies the specification; if , the verifier returns the violation clause, the violation time, and the minimum safety margin.

4.4 Counterexample driver repair

Instead of just returning pass/fail, the validator returns a structured diagnostic:

{
  "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’s repair prompt does not require free play, but requires it to only modify relevant fields in TaskIR:

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

The focus of this design is to reduce the search space of LLM and make the repair behavior explainable, recordable, and reproducible.

If LLM repair fails after consecutive rounds, the symbol enumeration fallback is entered. The enumeration scope is bounded by the TaskIR DSL depth, map entity set, allowed constraint template, and maximum task horizon. The enumerator prioritizes the expansion of the most relevant fields based on diagnostic results, such as safe distance, detour side, time window, target sequence, and fallback landing pad.

4.5 Trajectory generation

The AAAI version uses a lightweight reproducible trajectory generator:

• 2D grid A*: for basic reach-avoid and sequential tasks.
• 3D grid A*: used for height levels and urban low-altitude corridors.
• RRT*: for continuous spatial supplementary verification.
• MPC-lite/trajectory smoothing: used to check whether turning radius, speed change and height change satisfy simplified dynamics constraints.

The trajectory generator is not the innovation of this article. Its function is to advance the specification translation problem to the level of “whether the executable track really exists”.

---

5. Proof of theoretical properties and relative completeness

v1 only says “verification error correction can improve reliability”, but there is no mathematical boundary. v2 makes the algorithmic properties clear: VERA-UAV does not claim that LLM itself is complete, but rather claims to have relative completeness under the assumptions of a finite DSL, a decidable verifier, and a complete underlying planner.

5.1 Formal setting

Discretize the urban low-altitude map into a limited weighted map:

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

\mathcal{D}_{H,D} = {\psi: \mathrm{depth}(\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(\tau, C(\psi)) = \begin{cases} \mathrm{PASS}, & \tau \models \varphi_{\mathrm{LTL}}\ \land\ \rho(\tau,\varphi_{\mathrm{STL}})>0,\ \mathrm{FAIL}(\eta), & \text{otherwise}, \end{cases}

\tau \models \varphi_{\mathrm{LTL}} \quad \text{and} \quad \rho(\tau,\varphi_{\mathrm{STL}})>0.

\mathrm{FSR} = \frac{#{\mathrm{unsafe\ but\ returned\ as\ executable}}}{#{\mathrm{all\ returned\ executable}}}.

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: collision \lor nofly \lor altitude_violation \lor \rho(\tau,\varphi_{\mathrm{STL}})\le 0}} {#{\mathrm{returned\ trajectories}}}.

\mathrm{Gap}(\tau)=\frac{J(\tau)-J^\star}{\max(J^\star,\epsilon)}.

\mathrm{FailToPass} = \frac{#{\mathrm{initial\ fail,\ final\ pass}}} {#{\mathrm{initial\ fail}}}, \quad \mathrm{FallbackContribution} = \frac{#{\mathrm{LLM\ repair\ fail,\ symbolic\ fallback\ pass}}} {#{\mathrm{final\ pass}}}.