LLMs Meet Formal Methods for Robot Swarms: Reliable, Explainable and Human-in-the-loop Planning in Open Environments

Multi-robot systems including unmanned aerial vehicles, ground robots, and legged platforms are increasingly deployed to assist humans in complex collaborative missions such as disaster response. However, in open, unknown and dynamically evolving environments, manually coordinating a fleet of robots under real-time constraints poses severe physical and cognitive burdens on human operators, e.g., for scene understanding, task decomposition, task assignment and progress monitoring. While large language models (LLMs) have shown promising roles in multi-robot coordination by processing multimodal inputs and assisting decision making, their susceptibility to hallucinations and logical inconsistencies remains a critical bottleneck for long-term and complex missions. To address this challenge, we introduce the novel framework that adopts the rigorous and explainable algorithmic structure of formal methods, as a backbone to specify, decompose, assign and monitor the contingent tasks. Meanwhile, the intermediate outputs from LLMs such as semantic labels, task strategies and execution progress are grounded, verified and supervised within different stages of the framework. Thus, the operator is required only high-level confirmations at key events, while being fully aware of how the LLMs outputs are ultilized and whether they are aligned with the current objective. Lastly, to enable this real-time, online and highly interactive framework, a cloud-edge-end software architecture is developed that streamlines the information flow among the base station, the operator-fleet teams, andtherobots,withformalmethods-basedplanningmodulesandLLMsdeployed across all layers. The proposed frameworkpreservestheopen-worldreasoningcapabilities of LLMs while leveraging the rigorous guarantees of formal methods, It is validated through large-scale human-in-the-loop simulations and physical deployments involving 40 robots and 160 long-term tasks. Reliability, explainability and efficiency have been evaluated throughly and all shown significant improvements. We anticipate that our system will pave the way for more effective human-fleet teaming in safety-critical real-world scenarios.