The deployment of Large Language Models (LLMs) in robotic systems presents unique safety challenges, particularly in unpredictable environments. Although LLMs, leveraging zero-shot learning, enhance human-robot interaction and decision-making capabilities, their inherent probabilistic nature and lack of formal guarantees raise significant concerns for safety-critical applications. Traditional model-based verification approaches often rely on precise system models, which are difficult to obtain for real-world robotic systems and may not be fully trusted due to modeling inaccuracies, unmodeled dynamics, or environmental uncertainties. To address these challenges, this paper introduces a safety assurance framework for LLM-controlled robots based on data-driven reachability analysis, a formal verification technique that ensures all possible system trajectories remain within safe operational limits. Our framework specifically investigates the problem of instructing an LLM to navigate the robot to a specified goal and assesses its ability to generate low-level control actions that successfully guide the robot safely toward that goal. By leveraging historical data to construct reachable sets of states for the robot-LLM system, our approach provides rigorous safety guarantees against unsafe behaviors without relying on explicit analytical models. We validate the framework through experimental case studies in autonomous navigation and task planning, demonstrating its effectiveness in mitigating risks associated with LLM-generated commands. This work advances the integration of formal methods into LLM-based robotics, offering a principled and practical approach to ensuring safety in next-generation autonomous systems.

翻译：在机器人系统中部署大型语言模型（LLM）带来了独特的安全挑战，尤其是在不可预测的环境中。尽管LLM通过零样本学习增强了人机交互与决策能力，但其固有的概率特性及缺乏形式化保证，对安全关键型应用构成了重大隐患。传统的基于模型的验证方法通常依赖于精确的系统模型，然而这类模型难以从实际机器人系统中获得，且可能因建模误差、未建模动态或环境不确定性而无法被完全信任。为应对这些挑战，本文提出一种基于数据驱动可达性分析的LLM控制机器人安全保证框架，该形式化验证技术可确保所有可能的系统轨迹均保持在安全运行范围内。本框架具体研究了指令LLM引导机器人抵达指定目标的问题，并评估其生成底层控制动作以安全引导机器人成功抵达目标的能力。通过利用历史数据构建机器人-LLM系统的状态可达集，本方法在不依赖显式解析模型的前提下，为防范不安全行为提供了严格的安全保证。我们在自主导航与任务规划的实验案例研究中验证了该框架，证明了其在缓解LLM生成指令相关风险方面的有效性。本研究推动了形式化方法在基于LLM的机器人学中的集成，为保障新一代自主系统的安全性提供了一种原则性且实用的途径。