用大模型生成农业任务计划并自动验证，确保指令准确执行。
As You Wish: Mission Planning with Formal Verification using LLMs in Precision Agriculture
- 用自然语言描述任务，通过双大模型分工生成与验证逻辑公式。
- 引入多轮反馈机制，提升任务规划符合用户规范的可靠性。
- 适合需要高可靠性的农业自动化系统开发者参考。
尽管机器人系统已在多个行业商业化部署，但多数系统高度专业化，操作和确保按指令运行仍需专业知识。为缓解此问题，我们此前提出一种基于大模型的任务规划系统，可根据自然语言描述生成精准农业任务计划。然而，该系统受自然语言固有歧义影响。本文通过在规划架构中引入多轮反馈机制，利用线性时序逻辑（LTL）确保任务规划满足用户指定规范，同时保持自然语言输入。为降低潜在偏见，我们采用两个不同的商用大模型分别负责规范生成与验证任务。通过大量实验，揭示了将任务验证集成到全自动流程中的优势与局限，尤其关注大模型生成有效LTL公式的能力建设，并展示了所提方案如何有效应对这些问题。
原文摘要 · Abstract (English)
Though robotic systems are now being commercialized and deployed in various industries, many of these systems are highly specialized and often require an advanced skill set to operate and ensure they perform as instructed. To mitigate this problem, we recently introduced a mission planner leveraging LLMs to synthesize mission plans in precision agriculture based on mission descriptions provided in natural language. While the system demonstrates impressive performance, it also suffers from the inherent ambiguities of natural language. In this paper, we extend our system to address this issue by introducing multiple feedback loops in the planning architecture that leverage linear temporal logic (LTL) to ensure the mission planning system meets the specifications formulated by the user while still using natural language. To mitigate potential bias, this is achieved by using two different commercial LLMs in charge of the specification and verification subtasks. Through extensive experiments, we highlight the strengths and limitations of integrating mission verification into a fully autonomous pipeline, particularly regarding an LLM's ability to generate valuable LTL formulas, and show how our proposed implementation addresses and solves these challenges.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。