用分层符号框架让大模型在物理系统中更安全,避免胡说八道。
SafePilot: A Framework for Assuring LLM-enabled Cyber-Physical Systems
- 分层规划+判别器判断任务难易,复杂任务拆解处理
- 大模型输出自动转为形式化约束并验证,不合规就改提示重算
- 支持属性和时间约束,适合机器人、自动驾驶等高风险场景
大型语言模型(LLM)通常拥有超过100亿参数,正被逐步集成到机器人、工业自动化和自动驾驶等网络物理系统(CPS)中。利用其抽象知识与推理能力,用于规划与导航等任务。然而,LLM容易产生‘幻觉’——输出看似合理但事实错误或上下文不当,可能导致系统产生危险行为。为此,本文提出SafePilot,一种新型分层神经符号框架,根据属性和时序规范实现对LLM驱动的CPS端到端保障。给定任务及规范后,该框架首先通过判别器评估任务复杂度:若可处理,则直接交由内置验证机制的LLM任务规划器;否则采用分而治之策略,将任务分解为子任务分别规划并合并。规划器将自然语言约束转化为形式化规范,并验证输出。一旦发现违规,定位问题,调整提示,重新调用LLM。该过程持续迭代直至生成有效计划或达到预设上限。框架支持属性与时间约束,通过两个案例研究验证了其有效性与适应性。
原文摘要 · Abstract (English)
Large Language Models (LLMs), deep learning architectures with typically over 10 billion parameters, have recently begun to be integrated into various cyber-physical systems (CPS) such as robotics, industrial automation, and autopilot systems. The abstract knowledge and reasoning capabilities of LLMs are employed for tasks like planning and navigation. However, a significant challenge arises from the tendency of LLMs to produce "hallucinations" - outputs that are coherent yet factually incorrect or contextually unsuitable. This characteristic can lead to undesirable or unsafe actions in the CPS. Therefore, our research focuses on assuring the LLM-enabled CPS by enhancing their critical properties. We propose SafePilot, a novel hierarchical neuro-symbolic framework that provides end-to-end assurance for LLM-enabled CPS according to attribute-based and temporal specifications. Given a task and its specification, SafePilot first invokes a hierarchical planner with a discriminator that assesses task complexity. If the task is deemed manageable, it is passed directly to an LLM-based task planner with built-in verification. Otherwise, the hierarchical planner applies a divide-and-conquer strategy, decomposing the task into sub-tasks, each of which is individually planned and later merged into a final solution. The LLM-based task planner translates natural language constraints into formal specifications and verifies the LLM's output against them. If violations are detected, it identifies the flaw, adjusts the prompt accordingly, and re-invokes the LLM. This iterative process continues until a valid plan is produced or a predefined limit is reached. Our framework supports LLM-enabled CPS with both attribute-based and temporal constraints. Its effectiveness and adaptability are demonstrated through two illustrative case studies.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。