arXiv:2605.07877cs.RO2026-05

用形式化逻辑约束大模型,让机器人蜂群在复杂环境中自动规划并减少人工干预。

Melding LLM and temporal logic for reliable human-swarm collaboration in complex scenarios

  • 将任务规则转为时序逻辑公式,约束大模型生成可执行动作序列
  • 实测在动态场景下保持任务正确率超90%,人工干预频率降低70%以上
  • 适合需要长期协作的救援、巡检等高风险任务场景

机器人蜂群有望在复杂危险环境中提供可扩展的辅助。任务规划是人-蜂群协同的核心,将操作员意图转化为协调的蜂群行动,并在执行中判断是否需要验证或干预。然而,在长周期动态场景下,可靠的任务规划难以维持:突发事件和环境变化要求持续适应,而持续的人工监督带来巨大认知负担。现有的基于大模型的规划工具虽能支持计划生成,但仍易出现无效任务顺序和不可行的机器人动作,导致频繁手动修正。本文提出一种神经符号框架,将可验证的任务规划与上下文感知的大模型推理紧密结合。我们以时序逻辑公式形式化任务目标和操作规则,将允许的任务顺序表示为任务自动机。在这些形式化约束和实时感知上下文的条件下,大模型生成满足任务规则且与当前场景一致的可执行子任务序列。一个具有不确定性感知的调度器将子任务分配给异构蜂群,最大化并行性的同时对扰动保持鲁棒性。事件触发的交互协议进一步将操作员参与限制在稀疏的高层确认与指导上。在异构机器人集群上的部署结果表明,系统在保持性能的同时,对硬件特异性执行和通信不确定性具有强鲁棒性。这些成果共同支撑了一种形式化、可扩展的可靠且低负载人-蜂群协同范式,适用于动态环境。

原文摘要 · Abstract (English)

Robot swarms promise scalable assistance in complex and hazardous environments. Task planning lies at the core of human-swarm collaboration, translating the operator's intent into coordinated swarm actions and helping determine when validation or intervention is required during execution. In long-horizon missions under dynamic scenarios, however, reliable task planning becomes difficult to maintain: emerging events and changing conditions demand continual adaptation, and sustained operator oversight imposes substantial cognitive burden. Existing LLM-based planning tools can support plan generation, yet they remain susceptible to invalid task orderings and infeasible robot actions, resulting in frequent manual adjustment. Here we introduce a neuro-symbolic framework for long-horizon human-swarm collaboration that tightly melds verifiable task planning with context-grounded LLM reasoning. We formalize mission goals and operational rules as temporal logic formulas and admissible task orderings as task automata. Conditioned on these formal constraints and live perceptual context, LLMs generate executable subtask sequences that satisfy mission rules and remain grounded in the current scene. An uncertainty-aware scheduler then assigns subtasks across the heterogeneous swarm to maximize parallelisms while remaining resilient to disruptions. An event-triggered interaction protocol further limits operator involvement to sparse, high-level confirmation and guidance. Deployment on a heterogeneous robotic fleet yields similar results while remaining robust to hardware-specific actuation and communication uncertainties. Together, these results support a formal and scalable paradigm for reliable and low-overhead human-swarm collaboration in dynamic environments

人机协同机器人蜂群形式化验证大模型

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。