本章属专著书稿 V0.1 版,整体定格为历史快照。书稿将依据《EICPS 与具身空间 ES 理论阶段性梳理 V0.2》整体修订(三流形相乘、语义流形、Spine 单层等表述废止);修订完成前网站不逐章更新。现行口径见修订说明与各栏目 V0.2 页面。 现行口径以 V0.2 修订说明 为准。
本章从三条独立的理论演化线索出发,建立EICPS框架的理论动机。不从工程案例出发——那是验证而非来源——而是追溯AI、CPS与无人系统研究各自在理论层面遭遇的共同瓶颈,说明为什么一个统一的形式化框架是这三条线索汇合处的必然产物。
1.1 AI向物理世界的延伸:从感知推理到具身执行的理论鸿沟
人工智能向物理世界的延伸,不是一步完成的。每一次延伸都带来新的能力,也带来新的理论空白。这一节梳理三个发展阶段,定位具身智能所在的位置,以及它所暴露的根本性理论问题。
1.1.1 三阶段演化:符号推理、统计学习与具身智能
符号推理阶段(1950s–1980s)以命题逻辑与一阶谓词演算为核心,将”知识”表示为形式化规则,将”推理”处理为规则的机械演绎。这一范式在封闭的、形式化完整的领域(棋盘游戏、定理证明、专家系统的结构化知识库)中取得了令人印象深刻的成果,同时也在边界处遭遇了根本性障碍:真实世界的不完整性、模糊性与时间动态性,无法被有限的规则集完整覆盖。帧问题(frame problem)是这一局限的经典表述——如何形式化地表达”被规则未提及的事物在行动后保持不变”,至今仍无令人满意的答案。
统计学习阶段(1980s–2010s)以神经网络、支持向量机、概率图模型为代表,将”学习”从明确的规则编写转变为从数据中归纳模式。这一转变使AI系统的核心范畴从”演绎”变为”感知”:将原始信号(图像、文本、声音)映射为语义表示。深度学习的兴起(2012年后)将这种感知能力推至或超越人类水平。但统计学习的根本范畴是识别与分类——它是一个”感知机器”,不是”行动主体”。系统可以识别”这是一个危险的姿态”,但无法保证”在接下来的100ms内保持在安全区域内”。
具身智能阶段(2010s–至今)以大语言模型与物理机器人的深度融合为标志。SayCan(Ahn et al., 2022)[1]首次将LLM的语言理解能力用于机器人子任务选择,将语言模型的输出概率与机器人的动作可行性评估结合,实现”语言指导的物理执行”。RT-2(Brohan et al., 2023)[2]进一步将视觉语言模型的输出端到端地映射为机器人动作指令,消除了任务理解与动作生成之间的显式中间层。这一阶段的里程碑意义在于:语言理解能力与物理执行能力在同一系统中首次实现了功能性耦合。
表 1.1 具身AI三阶段范式演化对比
| 阶段 | 能力范畴 | 核心假设 | 典型系统 | 形式化保证 |
|---|---|---|---|---|
| 符号推理 | 演绎推理 | 世界可被有限规则完整描述 | Prolog、STRIPS | ★★★ 可判定逻辑 |
| 统计学习 | 模式感知 | 数据分布规律可泛化到新样本 | ResNet、SVM、GPT-4 | ✗ 无形式保证 |
| 具身智能 | 语言指导执行 | 大模型语言理解可迁移至物理动作 | SayCan、RT-2 | △ 经验安全 |
| EICPS(本书) | 形式化自主 | 闭合域可建立精确规约并形式验证 | Brain / Spine / Body | ★★★ V-SEM/V-PLN/V-SAF |
1.1.2 能力扩展的代价:SayCan 与 RT-2 的共同局限
SayCan与RT-2代表了不同的耦合策略,但共享一个根本性的局限:它们提供的是统计意义上的能力,而非可证明的保证。
具体表现在三个层面:
语义覆盖的统计性。 SayCan使用的语义路由基于语言模型的条件概率分布。当输入任务描述包含训练分布外的专业术语时,模型会以某个概率返回最相近的已知类型——而不是明确地说”我不知道这个词汇”。这意味着系统对任务空间的覆盖是统计性的:有足够的训练样本则覆盖率高,但永远无法排除某个低频专业词汇导致的语义误路由。
规划质量的不可验证性。 RT-2的端到端结构使得动作生成与任务理解紧密耦合,代价是中间过程变为不透明的神经网络权重。给定一个任务描述,无法在执行前验证模型生成的动作序列是否逻辑上一致、物理上可行——只能执行后观察结果。
安全约束的概率性满足。 两个系统都缺乏对物理安全约束的形式化机制。“通常不会触碰障碍物”是训练数据赋予的统计属性,不是可证明的不变性条件。在低概率但高后果的边界情形(设备故障、传感器噪声、模型分布外输入),这种统计属性提供的保护是不充分的。
上述三类局限在已有的系统性评测中均有直接记录。就语义覆盖的统计性而言,Ahn et al.(2022)[1]在补充实验中发现,当任务描述从标准表述切换为描述相同动作的非标准词汇时,SayCan的路由准确率出现显著衰减——这是语义覆盖依赖训练分布的直接实验证据,而非理论推测。就规划幻觉而言,Brohan et al.(2023)[2]在RT-2的评测中明确报告,模型在未见过的操作环境中任务成功率(约62%)显著低于已见环境(约96%),且失败案例中占多数的是”动作语义合理但物理不可执行”的幻觉规划——即模型输出了机械上不可能完成的关节指令序列,而非输出明显错误的语义。就安全约束而言,两套系统的论文均未给出安全约束满足率的形式化量化,仅以实验成功率间接替代——这一事实本身即说明了当前领域在形式化安全保证方面的理论空白:尚不存在统一的评测框架来区分”运气好没碰到危险”与”具备可证明的安全性”。
1.1.3 “统计正确”与”形式可证明”:一道认识论的断层
这不是程度的差异,而是性质的差异。
“统计正确”的命题形式是:。增大训练集、改进架构、提高精度,可以减小 ,但 永远不为零。在任何给定时刻,系统可能处于那 的概率区间内。
“形式可证明”的命题形式是:对所有合法初始状态 ,对所有时刻 ,系统轨迹满足 。这是全称量化的命题,不存在”概率区间”——要么所有情形下成立,要么不成立。
从统计命题到全称命题的跨越,不能通过在统计框架内改进参数来实现。它要求一个根本性的认识论工具替换:从数据驱动的归纳推断,到数学上可证明的不变性条件。
这一区分的历史根源。 在计算机科学发展早期,正确性的标准长期存在两条并行的路线:一条以测试(testing)为核心——通过足够多的用例证明程序通常工作;另一条以证明(proving)为核心——通过数学推导保证程序在所有情形下工作。Dijkstra(1972 年图灵奖致辞)明确指出:“程序测试只能证明缺陷的存在,不能证明缺陷的不存在(Program testing can be used to show the presence of bugs, but never to show their absence)。” Hoare(1969)的程序正确性逻辑随后提供了将函数契约(前置条件→后置条件)数学形式化的语言,使”对所有合法输入,程序都满足规约”成为可以在推理系统中被机械验证的命题。两条路线的分野,本质上是归纳推断(induction:从有限案例推广到一般)与演绎证明(deduction:从公理到全称结论)的认识论分野。
后果的不对称性决定了工具的不可替代性。 在绝大多数应用场景中,统计保证是足够的:推荐系统以 99.5% 的准确率工作,电子邮件过滤偶尔误判,这些都是可接受的代价。然而,安全关键领域中存在一类约束,其特点是:违反一次的代价等于系统失效的全部代价。飞机的操纵面控制系统不能”通常正确”——一次高曲率机动中的计算错误足以导致不可逆的事故;核电站的反应堆保护系统不能”大概率触发”——触发失效一次就是灾难。在这些场景中,把统计精度从 提高到 ,并不能将风险降至可接受范围,因为概率的尾部事件与最坏情形在时间上精确对齐。这正是 DO-178C(航空软件认证标准)将最高安全等级(DAL-A)的软件要求从测试覆盖率转向形式证明的根本原因:仅仅是”从未在测试中失败”不满足 DAL-A——系统必须证明”对所有可能的飞行状态,某些关键属性成立”。
两类保证的用途边界是清晰的,而非模糊的。 统计保证在开放世界、正态分布、连续改进的场景中是自然的选择——LLM 的语言理解、图像分类、推荐排序都在此列。形式保证在闭合世界、安全关键、不可逆后果的场景中是不可绕过的——控制系统的安全约束、软件的功能合规、协议的无死锁性都在此列。具身AI系统的独特处境,在于它同时跨越两类场景:语义理解层面对自然语言的开放世界处理(统计工具的主场),与物理执行层面对安全约束的形式保证要求(形式工具的主场),在同一系统的同一操作周期内同时激活。这种跨场景的共存,使得单纯使用任何一类工具都不充分,也使得两类工具的认识论边界必须在框架设计层面被明确划定,而非在工程实践中被模糊处理。
这一工具替换,正是具身空间框架的核心任务。§1.4 将把这一认识论区分落实为可操作的四类结构性约束,§2.2 将给出更精确的数学论证——为何 PAC 学习的天花板不是工程障碍,而是认识论障碍。
1.2 CPS→ICPS 演化轨迹:形式化能力的引入与失守
信息物理系统理论提供了将计算动力学与物理动力学统一建模的框架,也提供了形式化安全验证的工具箱。但当AI算法被嵌入CPS形成ICPS,这些工具的有效性遭到了系统性的挑战。
1.2.1 CPS 的理论奠基:混合自动机、可达性分析与 STL
CPS概念的形式化奠基,通常追溯至Lee(2008)[4]对”信息物理融合”的系统性论述。其核心贡献是将三类传统上分离处理的动力学——离散控制逻辑(计算)、连续物理过程(物理)、和通信延迟(通信)——统一在一个状态空间模型中分析。
混合自动机(Henzinger, 1996)[3]是CPS形式化建模的基础语言。它以有限个离散模式(mode)和连续状态变量(flow equation)的组合描述系统行为:在每个模式内,连续变量按微分方程演化;当满足卫式(guard)时,系统发生跳变(jump)切换到新模式。这使得”正在按直线运动”与”检测到障碍物后切换到避障模式”这样的复合行为可以在同一数学对象中被精确描述。
可达性分析(Reachability Analysis)回答”系统是否有可能进入不安全区域”的形式化问题。通过计算从所有可能初始状态出发的可达状态集合,它给出了安全性的数学证明——如果安全集与可达集不相交,则系统永远不会进入不安全区域,不依赖于任何概率假设。
信号时序逻辑(Signal Temporal Logic, STL; Maler & Nickovic, 2004)[5]为时域行为规约提供了可量化的鲁棒性度量。STL公式可以表达”在时间段 内,信号 始终满足 “这样的时域约束;其鲁棒度 量化了轨迹与规约边界之间的”余量”, 意味着满足且有余量, 提供了到边界的定量距离。
定义 1.1(混合自动机,Henzinger 1996[3]) 混合自动机是一个七元组
其中各分量的含义如下: 为有限的离散模式集(locations); 为连续状态空间; 为流方程族, 给出系统在模式 下的连续动力学; 为初始条件集; 为不变式,系统在模式 下仅当 时保持该模式; 为离散跳变边集; 为卫式,跳变 当 时使能; 为重置映射,跳变发生时连续状态更新为 。
系统的一条轨迹由连续流段(在某模式内 演化,直至不变式失效或卫式触发)与离散跳变(更新模式和状态)交替构成。可达性分析的核心问题即:从所有 出发的所有轨迹,是否始终回避不安全集 ?当可达集 时,安全性得到形式证明。
1.2.2 经典 CPS 的三个过强假设
经典CPS框架的形式化保证,建立在三个对具身AI场景而言过强的假设之上。
假设一:欧氏状态空间。 CPS的状态变量 被假定为欧氏向量,动力学方程 在线性空间中定义。这对于温度、压力、电压等标量物理量是自然的。但对于机器人的三维位姿状态——位置加旋转构成的 元素——欧氏向量表示引入了无法消除的近似误差(详见第4章)。CPS的形式化验证工具(可达性分析、STL监控)建立在欧氏度量之上;当真实状态空间是弯曲的,工具的形式化保证就不再严格成立。
假设二:完备感知。 CPS的状态估计通常假设感知模型 中的噪声 是已知分布的白噪声,状态估计的置信区间是可计算的。这在工业传感器在受控环境中的应用是合理的。但在架空线路的强电磁干扰环境下,传感器噪声模型本身是不确定的;Sim2Real Gap使得仿真中标定的噪声参数在真实环境中失效。完备感知假设的破坏,直接影响可达性分析的有效性。
假设三:预给任务规约。 CPS的形式化验证从给定的规约出发——STL公式描述的约束被视为先验已知的。但在具身AI场景中,任务规约本身是从自然语言描述动态生成的。生成过程的正确性(语言理解是否无损)和完备性(任务空间的全部约束是否被捕获)都不在经典CPS框架的假设范围内。
1.2.3 ICPS 的出现:AI 嵌入带来什么
智能信息物理系统(ICPS)的概念,大约在2015年前后随着深度学习在控制系统中的规模化应用而出现。其核心特征是:AI算法(神经网络控制器、强化学习策略、语言模型规划器)被作为CPS的计算组件嵌入,替代或辅助传统的确定性控制律。
ICPS在能力层面带来了显著提升:非线性系统的控制器可以通过强化学习端到端学习,无需显式建立物理模型;语言模型可以将高层任务描述转化为控制指令,无需专家手工编程;视觉感知模型可以处理经典滤波方法难以应对的复杂场景。
但ICPS的能力提升,是以牺牲CPS的核心优势为代价换来的。
ICPS的代表性框架,按AI组件在系统中承担的角色可分为三类。语言模型规划器类:以SayCan(Ahn et al., 2022)[1]为起点,PaLM-E(Driess et al., 2023)[6]将多模态感知与规划集成于同一大模型,进一步压缩了感知与语言推理之间的接口——这类框架将AI层定位于高层语义规划,底层执行仍依赖传统控制器,形成”语言理解→符号规划→经典控制”的松耦合链条。神经网络安全控制类:神经CBF(Dawson et al., 2022)[7]尝试用可微分神经网络替代手工设计的CBF函数,在保留前向不变性形式的同时使安全函数可由数据驱动学习;神经Lyapunov函数则以类似思路处理稳定性证书——这类框架试图同时保留形式化保证与AI的适应能力,但学习到的安全函数在分布外区域的可靠性仍是开放问题。端到端学习控制类:以RT-2(Brohan et al., 2023)[2]为代表,感知-规划-控制被整合为单一神经网络,中间层的符号表示被完全省略——这类框架能力最强,泛化最灵活,但形式化保证能力最弱,是ICPS框架中”可验证性失守”最为彻底的一端,也是本书立论的主要对话对象。
1.2.4 形式化验证能力的退化:不可监控性的根源
ICPS的核心矛盾,可以用一句话概括:神经网络的输出不是可监控的信号。
STL要求被监控的系统行为表示为有界时间域上的可测信号 ,使得鲁棒度 在每一时刻都可以被精确计算。这要求信号值是确定性的、已知精度的、与规约的语义对应关系是明确的。
语义对应关系的断裂。 在经典CPS中,被监控信号的语义是显式定义的:传感器读数 对应机械臂末端与障碍物之间的物理距离,STL公式 直接监控这个物理量。语义对应关系由系统设计者显式建立,不依赖任何统计学习。但在 ICPS 中,神经网络控制器接收传感器数据后输出的是关节角速度向量——这个向量在形式上是数值可测的,但它与任务规约(“保持安全距离”)之间的对应关系,是在训练过程中通过数百万次梯度下降隐式编码到权重矩阵中的。这个隐式对应关系在训练分布内”通常”成立,但没有任何机制保证它在新场景下仍然成立。
三层不可监控性的叠加。 ICPS 中的不可监控性并非单一问题,而是三层叠加:语义不透明——神经网络的内部状态(权重激活)不对应任何可解释的物理量,无法从中读出”系统当前对安全距离的估计是什么”;分布外不可感知——传统信号监控可以检测信号超出范围,但无法检测”当前输入对神经网络而言是否属于训练分布外区域”,而正是这类输入最可能触发安全约束违反;前向验证缺失——在经典 CPS 中,可达性分析可以在执行前验证”从当前状态出发的所有可能轨迹是否进入不安全区域”;在 ICPS 中,神经网络的输入-输出关系是高维非线性的,对其全域的前向可达集分析在计算上是不可行的。
“监控工具仍在运行”的虚假安全感。 这一点值得单独强调,因为它是 ICPS 安全验证中最容易被忽视的陷阱。当 STL 监控器挂载在 ICPS 系统上时,它会生成鲁棒度数值 ,这些数值在技术上是精确的——但精确计算的是什么?它计算的是被监控信号(通常是传感器的物理量,如距离、速度)满足规约的程度。这个计算本身没有任何问题。但它无法回答的问题是:神经网络的决策过程是否在规约的预期语义框架内运作。一个神经网络可以在物理距离信号 满足 STL 规约的同时,基于完全错误的语义理解(例如错误地识别了任务类型)生成动作指令——监控器看不到这一层,因为它只看得到物理信号。真正的安全违反,可能发生在 STL 监控器给出绿灯的几毫秒后,当错误的任务理解最终传播到物理执行层。
这种不可监控性,使得可达性分析和STL验证的形式化有效性在ICPS框架下受到根本性限制。EICPS框架的语义覆盖验证层(V-SEM)的设计动机,正是在这一缺口的上游建立可信赖的语义可见性:只有当 Brain 层的语义路由可被形式验证时,Spine 层的 STL 监控结论才是真正有效的。可监控性不是 STL 监控器本身的属性,而是系统架构在语义层提供的属性。
对这一退化,学术界已有系统性的回应纲领。Fan(范楚楚,MIT)在《Formal Methods for Safe Autonomy》(ACM Books, 2023)中将散落于时序逻辑、屏障函数、可达性分析与神经证书学习(Dawson, Gao & Fan, 2023)等方向的工作整合为 Safe Autonomy 框架,其中心命题是:自主系统应在形式化约束下运行,用数学证明而非测试统计建立行为边界。该纲领同时揭示了一个与直觉相反但在逻辑上必然的关系——自主度越高,对形式化保证的需求越强:遥操作模式下操作员本人就是每一时间步的安全兜底,系统可以没有形式化机制;当系统转向自主操作(Human-on-the-Loop,人退出实时回路只做监督)时,形式化机制必须接替人的实时安全判断,从可选项变为不可缺失项。本书与该纲领是上下游关系:Safe Autonomy 提供工具及其数学性质的证明,本书回答这些工具在一个认知-物理深度耦合的具身系统中应放在哪一层、以什么频率运行、通过什么接口交互——这正是下一节复杂系统论要展开的问题:为什么认知层与物理层之间的深度耦合,会系统性地阻碍单一层面工具的形式化效力。
1.3 具身AI的复杂系统论:认知-物理耦合复杂度的本质
理解EICPS所要处理的问题类型,需要一个比”复杂工程系统”更精确的概念框架。钱学森先生的复杂巨系统理论,提供了恰当的视角。
1.3.1 钱学森先生的复杂巨系统理论:涌现性的定义
钱学森先生将巨系统按子系统种类的多样性与层次的可知性分为两类。简单巨系统的特征是:子系统种类不多(几种、几十种),相互作用的规律清晰,还原论方法仍然适用——他本人给出的典型例子是激光系统:数以亿计的光子通过同质耦合呈现宏观相干,统计力学在此有效,全系统行为可由各局部分析的叠加重构。开放的复杂巨系统则不同:子系统种类极多,层次结构繁复,从可观测的整体到各层子系统之间,中间层次往往不为人知,甚至层次数量本身尚未厘清——系统的整体行为不能通过子系统行为的线性叠加来重构,整体性质只在子系统的深度耦合中涌现(emergent properties),在任何单一子系统中都不存在。钱学森先生称这种根本性质为涌现性(emergent non-separability),并将其定义为复杂性的本质——不是物理规模,而是层次耦合的深度与不可化约性。
钱学森先生给出的开放复杂巨系统的典型例子,涵盖了人体(分子→细胞→组织→器官→整体,各层次之间的耦合机制至今未全部厘清,意识、免疫调节等整体性质在任何单一层次中都找不到对应物)、人脑(神经网络到宏观意识的涌现)、地理-生态系统,以及社会系统。现代国家电网作为覆盖物理设备、信息控制、市场调度与运维人员认知的大型社会-技术系统,同样满足这一判定标准:发电机组、变电站控制器、调度员决策、市场机制,在多个层次上形成异质耦合,其整体行为超出了纯物理潮流计算的描述范围。2003年北美大停电,是物理网络状态、控制系统局限与人员认知判断之间多层涌现的典型案例——任何单层分析都无法预测这一级联事件。AI具身智能系统在功能上模拟人类专家的认知-行动过程,属于同一范畴:无论其实现基础是碳基的还是硅基的,其复杂性根源于认知层与物理层之间的深度耦合。
在这一框架下,更值得追问的是:EICPS的涌现性从哪个耦合界面产生,既有的工程方法是否足以处理? 电力系统工程历经数十年实践,已围绕其主要涌现机制发展出相应的方法体系(N-1安全准则、状态估计、自动发电控制等)。具身AI系统面对的是一个相对新颖的耦合界面:语义推理层(语言模型对任务意图的理解)与物理执行层(机械臂在SE(3)上的运动),通过高维、不可解释的嵌入表示相互连接。这一界面上的跨层涌现——语义层的一个隐性错误,经由控制指令链在物理空间产生的不可逆安全后果——尚缺乏成熟的形式化分析框架。EICPS理论的建设,正是从这个界面出发。
1.3.2 具身AI系统的三重复杂性
从钱学森先生的定义出发,EICPS的复杂性可以从三个相互强化的维度来理解:
认知-物理耦合的涌现性。 语言模型的推理能力、运动控制器的执行能力、传感器的感知能力,三者在具身系统中的耦合产生了不可线性叠加的系统行为。一条在语义层面看起来合理的指令(“接近10号绝缘子”),在物理执行中可能违反电气安全约束(绝缘子附近存在带电导线)——这种跨层传播是典型的涌现效应。反过来,物理层的约束(当前位姿导致机械臂不可达)也会反馈到语义层(这个子任务序列不可行,需要重新规划),形成双向耦合。
状态空间的非欧几何结构。 具身AI系统的状态,不能简单地表示为欧氏向量。物理位姿状态在 流形上演化;任务知识状态在语义嵌入空间的弯曲子流形上分布(第5章将证明架空线场景的语义流形内在维度 ,远低于嵌入维度);传感数据状态携带Sim2Real Gap的流形结构。三种非欧几何结构同时存在于同一系统中,是具身AI复杂性的数学特征。
跨域约束的同时激活。 安全关键的具身AI任务,要求四类约束在同一时间尺度上同时满足:物理安全约束(CBF前向不变性)、语义完备约束(SEC=1)、感知精度约束(EKF置信区间在阈值内)和验证可判定约束(STL鲁棒度实时可计算)。这四类约束之间的耦合——例如,感知精度下降导致CBF安全集估计偏差,进而使得形式化验证的判定结论不可靠——是涌现复杂性的具体工程表现。
1.3.3 复杂度判定准则:认知-物理集成耦合程度
基于上述分析,本书提出EICPS复杂度的判定准则:
系统的EICPS复杂度,由认知-物理集成耦合的程度决定,而非由基础设施的物理规模决定。
这一准则的可操作化形式是:当四类结构性约束(见§1.4)中有多少类在系统运行中同时激活?
- 一类激活(纯物理控制,无语义层):经典CPS,不需要EICPS框架
- 两类激活(物理+语义,无形式化执行安全层):ICPS范畴,统计保证可能足够
- 三类或四类同时激活:EICPS框架的目标范畴,形式化保证是必要的
这个准则使得”是否需要EICPS框架”成为一个可以在系统设计阶段回答的工程判定问题,而非模糊的定性描述。
复杂度判定的操作流程如下:
① 是否有 SE(3) 物理执行层? 否 → 不在 EICPS 范畴(纯软件系统)。
② 是否有语义/自然语言输入层? 否 → 经典 CPS,CBF + STL 已足够,无需 EICPS 框架。
③ 语义层是否需要覆盖行业专业词汇? 否(词汇极少且稳定)→ 规则引擎可替代 LLM,V-SEM 非必须。
④ 任务词汇表是否有限可枚举(闭合域)? 否(开放词汇表)→ 只能给出统计保证,进入 ICPS 范畴。是 → 规范闭合性可建立,V-SEM 形式等式可证明,继续 ↓。
⑤ 是否需要轨迹全程安全保证(而非仅终点精度)? 是 → 激活 CBF + STL(V-SAF 纵深防御)。
⑥ 是否需要规划质量的形式化量化(LLM 幻觉可检测)? 是 → 激活 V-PLN。
当 ①②③④⑤⑥ 全部判定为”是”时,四类结构性约束同时激活,完整 EICPS 框架是必要的。下一节将对这四类约束逐一展开分析——明确每类约束的数学本质、失效机制和对应的工具需求,是 EICPS 理论框架问题陈述的最后一步。
1.4 四类结构性约束:EICPS 理论框架的问题陈述
前三节建立了EICPS所处理的问题的来源和本质。本节将这些问题凝练为四类精确的结构性约束——这是EICPS理论框架的问题陈述,也是其数学工具选择的基本依据。
1.4.1 物理运动约束:SE(3) 流形与欧氏近似的系统性误差
刚体在三维空间中的运动由位置()和姿态()共同描述,两者的乘积空间正是特殊欧氏群 。这不是一个欧氏向量空间,而是一个6维光滑流形,同时具有李群结构(群乘法和取逆运算与流形结构相容)。
欧氏近似的代价是结构性的,而非数值性的。 用旋转矩阵的9个分量组成的向量来表示姿态,会把 (一个3维流形)嵌入 (一个9维线性空间)并施加6个非线性约束(正交性+行列式为1)。在这个嵌入空间中做线性插值(例如对两个姿态的矩阵分量做加权平均),得到的结果一般不满足这6个约束——它不是一个旋转矩阵,而是一个普通的矩阵。虽然可以通过SVD重正交化来”修复”,但这个修复引入的误差在 的高曲率区域(姿态变化剧烈时)无界增长。
更根本的问题是:CBF安全约束要求的是机械臂末端执行器与带电体之间在三维空间中的真实欧氏距离(),但安全集在 上的形状取决于 上的测地距离()。当用欧氏近似替代李群测地距离时,系统可能在欧氏度量下”满足”安全约束,而在真实几何下已经违反——这是一个无法通过参数调整消除的系统性安全漏洞。
形式化表述:物理运动约束要求安全集 中的函数 用 的内蕴度量定义,CBF的前向不变性条件需在李群结构下推导和验证。
1.4.2 语义完备性约束:从 SEC ≥ 1−δ 到 SEC = 1 的认识论鸿沟
具身AI系统的Brain层依赖语言理解来将自然语言任务描述路由到预定义的执行类型。语义覆盖率 度量的是这个路由过程对所有合法输入的覆盖程度:
其中 是任务描述空间。
统计学习方法给出的最好结果是 ,其中 是训练集覆盖不足和模型泛化误差的函数。这个界可以通过扩大训练集来减小,但不能到达零——PAC学习框架保证了,对任何固定的有限训练集,都存在以正概率出错的测试样本。
是一个完全不同性质的命题:不存在使路由出错的合法输入。它不能通过统计方法获得,因为统计方法的保证天然是概率性的。获得 的唯一路径,是对任务描述空间 的结构施加约束:当 是有限可枚举的闭合域(行业规程规定了有限的操作类型集合),且词汇表 被系统性地构造为对 的覆盖闭包时, 成为可证明的形式等式。这正是规范闭合性(Canonical Closure)的核心主张,将在第5章和第11章严格建立。
1.4.3 执行安全约束:CBF 前向不变性与轨迹全程保证
安全约束的形式化,需要区分两种保证强度:
终点精度(endpoint accuracy):系统最终到达目标位置时误差在阈值内。这是经典控制理论的稳态分析关注的问题,可以通过 Lyapunov 稳定性理论来保证。
轨迹安全(trajectory safety):系统在运动过程中的每一时刻,状态都满足安全约束。这是具身AI安全关键场景的真实需求——架空线路带电作业中,安全间距在轨迹中任何一点的瞬时违反,即构成不可逆事故,与最终到达精度无关。
控制屏障函数(Control Barrier Function, CBF)是当前处理轨迹安全问题最成熟的形式化工具。给定安全集 和候选CBF ,若存在扩展K类函数 使得所有可行控制输入 满足:
则安全集 是前向不变的——即从 内出发的任意轨迹永远不会离开 ,无论时间有多长。这是轨迹全程安全的数学保证,而非终点精度保证。
在 框架下,CBF的构造需要用李群上的 函数(而非欧氏坐标下的近似),这是物理运动约束(§1.4.1)与执行安全约束的交叉点,将在第4章和第8章详细处理。但安全约束的形式证明,还要求系统在实时且可判定的方式下被持续监控——如何在 100ms 量级控制周期内给出可信赖的在线判定,是第四类结构性约束的核心问题。
1.4.4 验证可判定性约束:STL 鲁棒度与实时量化判定
一个系统的行为是否满足规约,必须能够在有限时间内给出判定——且这个判定必须是实时的(online),而非离线的(offline),因为安全仲裁发生在任务执行过程中,不是事后分析。
从离线验证到在线监控的历史跨越。 时序逻辑的验证工具在诞生之初是离线的:模型检验(Clarke et al., 1981)在系统建模完成后,对所有可能的状态转移路径做穷举分析,给出”满足”或”不满足”的判定。这对有限状态系统是精确有效的,但有两个根本局限:第一,分析在执行前完成,无法应对执行中的动态状态更新;第二,对连续动力系统的状态空间,穷举分析遭遇无穷维度的状态爆炸。面向连续系统的在线 STL 监控,由 Maler & Nickovic(2004)奠基,Donzé & Maler(2010)系统发展——核心贡献是在每个采样时刻,用有界窗口内的实测信号替代”所有可能轨迹”,将验证问题从”模型检验”转化为”信号监控”:计算量从状态空间的指数增长降至与信号长度和公式长度线性相关的 ,使实时计算成为可能。这一工具路线的成熟,是 EICPS 能够将形式化验证嵌入 100ms 量级控制周期的技术前提。
在线判定的三个必要条件。 验证可判定性约束要求监控系统同时满足三个条件,缺一不可:可计算性——鲁棒度 必须在有限步内精确计算完毕,且计算时间有上界(STL 满足此条件,而某些高阶时序逻辑不满足);实时性——计算必须在控制周期内完成,不能阻塞后续控制决策;语义保真性——被监控的信号 必须与规约 的变量有精确的语义对应,监控的是物理量本身,而不是对物理量的统计估计。第三个条件是三者中最容易被忽视但最关键的:如果 表示”机械臂末端到带电导线的距离”,那么 的来源(传感器读数 + EKF 状态估计)的不确定性,直接决定了 STL 判定结论是否可信赖。
与感知精度约束的耦合。 一条STL规约可以监控”机械臂末端到导线的距离 “,但它要求 是一个在每个时刻都有确定数值的可测信号——这要求Body层的状态估计(EKF输出)达到足够的精度,使得 的不确定性在安全判定可接受的范围内。这一耦合意味着:感知能力的劣化(例如强电磁干扰导致传感器噪声增大)不只影响机械臂的定位精度,还会直接影响 STL 安全监控的可信赖性——即使 STL 公式本身没有任何问题,基于噪声过大的估计信号所给出的”满足安全规约”的判定也是不可信赖的。因此,感知精度约束(的状态估计不确定性)与验证可判定性约束,是 EICPS 四类约束中耦合最紧密的一对——第三部分 Spine 层的设计,将把感知不确定性显式引入 STL 鲁棒度的安全余量计算,使两类约束的耦合关系得到工程层面的明确处理。
四类约束与 EICPS 各层的对应关系如下:
表 1.2 四类结构性约束与 EICPS 层架构对应关系
| 约束类型 | 核心数学对象 | EICPS 对应层 | 主要处理章节 |
|---|---|---|---|
| 物理运动约束 | 流形;CBF | Body 层(运动执行)+ Spine 层(安全仲裁) | 第 4、8 章 |
| 语义完备性约束 | 词汇表 ;规范闭合性; | Brain 层(语义路由与任务规划) | 第 5、7、11 章(V-SEM) |
| 执行安全约束 | STL 公式 ;鲁棒度 ;CBF 前向不变性 | Spine 层(STL 监控)+ Body 层(CBF 控制律) | 第 6、9、13 章(V-SAF) |
| 验证可判定性约束 | STL 在线判定 ;形式证据链 FEP | 全层贯通:Spine 生成证据,Brain/Body 提供可测信号 | 第 10–13 章(V-SEM/V-PLN/V-SAF) |
1.5 复杂度谱系与分层设计:从理论上限到工程下限
四类结构性约束并非在所有场景中同时以最大强度激活。本节建立复杂度谱系的概念,说明EICPS框架的分层可适配性不是工程上的妥协,而是理论上的必然。
1.5.1 三个代表性复杂度层次
层次一:局部确定场景。 代表案例:架空线路单基杆塔的单机无人机巡检,或变电站内固定作业臂的预编程维护操作。
这类场景的特征是:任务类型有限(巡检路径预定义,不依赖实时语义理解)、物理约束明确(安全间距固定,导线摆动在可预测范围内)、单机操作(无跨机器协同需求)。四类约束的激活情况:物理运动约束(激活,SE(3)运动规划)、语义完备性约束(部分激活,词汇表小,可用规则系统替代LLM)、执行安全约束(激活,CBF需要)、验证可判定性约束(激活,STL在线监控)。
在这个层次上,EICPS框架以安全控制子集运行:CBF+STL构成核心,Brain层的LLM路由和HTN规划可以简化为规则引擎或有限状态机。这是框架的工程下限——在简单场景下,不强制调用全套数学深度。
层次二:区域协同场景。 代表案例:多无人机协同完成跨多基杆塔的区域巡检,或多机器人分工的变电站综合检修。
这类场景的特征是:跨机器任务分配需要语义路由(不同机器承担不同子任务类型)、机器间安全边界需要形式化(机器之间的物理距离约束)、任务复杂度上升(可能出现训练数据较少的边缘任务类型)。四类约束全部激活,但SEC的要求可能不到最强等级(词汇表较完整但不一定规范闭合)。
在这个层次上,EICPS框架激活中间层配置:Brain层的LLM路由和HTN规划全部运行,语义路由配合安全控制,但可能不需要完整的V-SEM-V-PLN-V-SAF验证链。
层次三:完整认知-物理耦合场景。 代表案例:AI具身主体在全自主模式下完成需要实时专业判断的复杂带电作业(如在检测到设备异常后动态调整作业方案),或多机协同的超复杂系统级维护任务。
这类场景的特征是:所有四类约束在最高强度下同时激活、SEC=1的形式等式是必要条件(任何词汇盲区都可能导致灾难性误判)、认知-物理耦合程度最高(语义错误在物理层的传播后果最严重)。这是EICPS框架的理论上限——三流形的完整数学深度在此才是不可省略的。
1.5.2 四类约束的分层激活模式
| 约束类型 | 层次一(局部确定) | 层次二(区域协同) | 层次三(完整耦合) |
|---|---|---|---|
| 物理运动约束 | SE(3) CBF | SE(3) CBF + 跨机器约束 | SE(3) CBF + 完整流形规划 |
| 语义完备性约束 | 规则引擎(不需要=1) | LLM路由() | 规范闭合性() |
| 执行安全约束 | STL单规约 | STL双规约 | V-SAF纵深防御 |
| 验证可判定性约束 | 在线STL监控 | 在线STL+形式证据 | 完整验证链+V-SEM-V-SAF |
框架设计原则:上层层次的框架组件,在下层层次中以降级(degraded)模式运行,而非被完全替换——这保证了跨复杂度层次的框架一致性,使得从简单场景向复杂场景的工程迁移不需要重新架构。然而,现有方法之所以无法实现这样的跨层次覆盖,恰恰是因为它们从未以这种分层原则为基础进行设计。
1.5.3 现有方法的局部性陷阱
现有的具身AI方法,普遍存在一种局部性陷阱:针对复杂度谱系的某一端进行优化,在该端取得良好结果,但在向另一端迁移时出现系统性失效。
纯AI方法(如SayCan、RT-2系列)[1,2]在复杂度谱系的高语义复杂度端表现出色:自然语言理解、多步骤任务规划、跨场景迁移。但当这些方法被部署到安全关键的物理执行环境时,它们缺乏物理安全约束的形式化机制,缺乏语义覆盖完备性的可验证保证,缺乏实时安全判定的量化工具。换言之,这些方法在谱系的”语义复杂”端做了优化,但在”物理安全”端缺乏理论基础。
纯控制方法(如经典CPS、MPC、RobotCPS框架)在复杂度谱系的高物理确定性端表现出色:精确的运动控制、可验证的轨迹安全、实时的约束满足。但当任务的语义复杂度上升(需要理解自然语言指令、处理专业领域知识、应对开放世界的任务变化),这些方法缺乏语义层的处理能力,缺乏从语言描述到形式规约的桥梁,缺乏任务知识完备性的保证机制。
局部性陷阱的危险,在于它在各自的测试环境中是不可见的。 纯AI方法在语义复杂的基准测试集上表现优异——但这些基准通常不包含带电作业场景,或者即便包含了相关图像也没有要求形式化的安全距离验证。纯控制方法在规范化物理实验中展示了可证明的轨迹安全——但实验通常假设任务类型已知,不考虑”系统不知道当前面对的是哪类任务”的情形。局部性陷阱使得在各自擅长领域的实验成绩,无法推断为在交叉场景中的可靠性。具身AI安全关键部署的核心风险,恰恰集中在这个交叉区域:语义理解需要统计学习的灵活性,同时物理执行需要形式验证的严格性,两者无法分离处理。
两类方法各自覆盖谱系一端,而EICPS框架的设计目标是覆盖整个谱系——在任何复杂度层次上,都能以该层次适当的形式化强度运行。这不是两类方法的简单叠加(分别运行一个语义层和一个控制层),而是在统一的架构和形式化证据链下,实现跨层次的可验证性:语义层的覆盖结论(SEC = 1 或 SEC ≥ 1−δ)与物理层的安全约束(CBF 不变性)必须在同一形式系统内被同时证明,才能对整个系统给出有意义的安全保证。
1.5.4 分层覆盖策略:EICPS 框架的设计原则
基于上述分析,EICPS框架的分层设计遵循以下原则:
原则一:最小激活原则。 框架在运行时按需激活组件——不在层次一场景中强制运行层次三的完整验证链,从而避免不必要的计算开销和工程复杂性。“分层”不是”降级”,而是”精确适配”。
原则二:向上兼容原则。 每个复杂度层次的组件,都是更高层次组件的严格子集。层次一的安全控制子集(CBF+STL),在层次二和层次三中以增强配置继续运行,保证跨层次的行为一致性和工程可迁移性。
原则三:形式化证据贯通原则。 无论在哪个复杂度层次上运行,Spine层生成的形式证据包都遵循统一的结构和签名机制。这使得跨层次的安全审计和合规验证可以使用同一套工具链完成。
这三个原则,将在第三部分(系统架构)和第五部分(分层验证)中分别通过设计和实验加以落实。
本章奠定了全书的问题陈述层。第2章将从认识论层面深入分析欧氏空间表示为何在结构上不足以处理认知-物理耦合复杂性,并以规范闭合性与EICPS分层框架总览作为第一部分的收束。
参考文献
-
Ahn, M., Brohan, A., Brown, N., Chebotar, Y., Cortes, O., David, B., … Zeng, A. (2022). Do As I Can, Not As I Say: Grounding Language in Robotic Affordances. arXiv preprint arXiv:2204.01691.
-
Brohan, A., Brown, N., Carbajal, J., Chebotar, Y., Chen, X., Choromanski, K., … Zeng, A. (2023). RT-2: Vision-Language-Action Models Transfer Web Knowledge to Robotic Control. Proceedings of the 7th Conference on Robot Learning (CoRL 2023), PMLR 229.
-
Henzinger, T. A. (1996). The Theory of Hybrid Automata. Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 278–292. IEEE.
-
Lee, E. A. (2008). Cyber Physical Systems: Design Challenges. Proceedings of the 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC 2008), pp. 363–369.
-
Maler, O., & Nickovic, D. (2004). Monitoring Temporal Properties of Continuous Signals. Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems (FORMATS/FTRTFT 2004), Lecture Notes in Computer Science, Vol. 3253, pp. 152–166. Springer.
-
Driess, D., Xia, F., Sajjadi, M. S. M., Lynch, C., Chowdhery, A., Ichter, B., … Florence, P. (2023). PaLM-E: An Embodied Multimodal Language Model. Proceedings of the 40th International Conference on Machine Learning (ICML 2023), PMLR 202.
-
Dawson, C., Gao, S., & Fan, C. (2022). Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction Methods. IEEE Transactions on Robotics, 39(3), 1749–1767.