arXiv:2503.03911cs.ROcs.LG2025-03被引 16

用数据驱动方法为大模型控制机器人提供安全保证,确保动作不越界。

Safe LLM-Controlled Robots with Formal Guarantees via Reachability Analysis

  • 基于历史数据构建机器人-大模型系统的可达集,无需精确物理模型
  • 通过形式化验证确保所有可能轨迹都在安全范围内,避免危险行为
  • 适合关注大模型机器人安全的开发者与研究者,尤其在未知环境中

将大语言模型(LLM)应用于机器人系统时,面临独特安全挑战,尤其在不可预测环境中。尽管LLM借助零样本学习提升了人机交互与决策能力,但其固有的概率特性及缺乏形式化保证,使安全关键应用存在隐患。传统基于模型的验证依赖精确系统模型,而真实机器人系统难以获取且易受建模误差、未建模动态或环境不确定性影响。为此,本文提出一种基于数据驱动可达性分析的安全保障框架,可确保所有可能系统轨迹保持在安全操作限内。该框架重点研究如何指令LLM引导机器人到达指定目标,并评估其生成低层控制动作以安全抵达目标的能力。通过历史数据构建机器人-LLM系统的可达状态集,本方法在不依赖显式解析模型的前提下,提供严格的运行安全性保证。实验在自主导航与任务规划中验证了框架有效性,显著降低由大模型生成指令带来的风险。该工作推进了形式化方法在大模型机器人中的应用,为下一代自主系统提供了可信赖的安全路径。

原文摘要 · Abstract (English)

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.

机器人安全大模型形式验证可达性分析

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