本章属专著书稿 V0.1 版,整体定格为历史快照。书稿将依据《EICPS 与具身空间 ES 理论阶段性梳理 V0.2》整体修订(三流形相乘、语义流形、Spine 单层等表述废止);修订完成前网站不逐章更新。现行口径见修订说明与各栏目 V0.2 页面。 现行口径以 V0.2 修订说明 为准。
本章从认识论层面分析欧氏空间表示为何在结构上不足以支撑具身AI的形式化自主保证。以代表性系统的共同假设为切入点,说明统计近似的天花板效应,引入流形几何语言作为覆盖完整复杂度谱系的数学工具,并以规范闭合性和EICPS分层框架总览作为第一部分的收束。
2.1 SayCan · RT-2 · ProgPrompt 的共同假设与失效边界
三个代表性系统的成功,建立在一组共同的隐式假设之上。本节首先梳理三系统的发展脉络与代表性,再将这些假设显式化,分析它们在何种条件下导致系统性失效。
2.1.1 三系统的代表性与发展脉络
2022–2023年间,以大语言模型为核心的具身AI经历了从”语言规划”到”端到端感知-动作”再到”程序综合”的快速范式迭代。SayCan、RT-2、ProgPrompt 是这一迭代中的三个里程碑,分别代表三种主流技术路径。
SayCan(Ahn et al., 2022)由 Google Research 提出,是将大语言模型系统性地用于机器人任务规划的早期奠基工作。其核心思路是将语言模型的”语义相关性”与机器人的”物理可行性”以乘积形式结合:用 PaLM 给出语言分数 (哪个技能与任务描述最相关),用针对每个技能训练的价值函数给出可行性分数 (该技能在当前状态下能否执行),两者联合选出下一步动作。SayCan 在厨房场景的长程任务(如”帮我拿一块蛋白棒,然后把厨房打扫干净”)上展示了超过 80% 的任务完成率,确立了”LLM as planner”范式的可行性。
RT-2(Brohan et al., 2023)由 Google DeepMind 提出,代表了向端到端视觉-语言-动作(VLA)模型的范式跃迁。RT-2 将预训练视觉语言模型直接微调为机器人控制器:模型输入图像和自然语言指令,输出离散化的机器人动作指令(以文本 token 表示)。RT-2 的核心主张是,足够大的预训练 VLM 已经学到了可以迁移到机器人控制的”通用知识”,无需显式的中间规划表示。其在 Web 知识迁移任务(如”哪个物品应该回收?把它放到对应颜色的容器里”)上的零样本表现,成为端到端统计学习能力的标志性展示。
ProgPrompt(Singh et al., 2023)由 Stanford 与 NVIDIA 联合提出,代表”LLM 作为程序综合器”这一技术路线。给定自然语言任务描述和当前环境状态,ProgPrompt 提示 LLM 生成可执行的结构化程序,每一步骤调用预定义的原子操作(grasp(obj)、put(obj, target) 等)。程序的显式结构使条件判断、循环和错误恢复成为可能,是对 SayCan 线性动作链的结构化扩展,在 VirtualHome 和 RoboSuite 等仿真环境中的任务完成率较无结构提示方法提升 20–30 个百分点。
三个系统的发展脉络揭示了一个共同的技术信念:以更大的模型、更多的数据、更端到端的训练来扩展具身AI的能力边界——这是统计缩放律(scaling law)在机器人学中的延伸。本节的任务,恰好是追问这一信念在何处遭遇结构性的天花板——不是因为模型不够大,而是因为问题的几何和认识论本质不允许用统计逼近来解决。
2.1.2 欧氏向量假设
SayCan使用的技能价值函数 和语言分数 都将机器人状态 表示为欧氏向量。RT-2的端到端模型接受图像和语言作为输入,输出动作指令的分词表示——动作空间同样隐式地被处理为欧氏向量。ProgPrompt通过程序生成的方式组合子任务,每个子任务的前置条件和效果用欧氏向量形式的谓词表示。
这一共同假设在桌面物品操作等平坦低动态场景下是合理的近似,但在需要精确描述三维空间中刚体位姿的场景(如带电作业、精密装配)下引入了系统性的几何误差——其根本原因在第1章§1.4.1和第4章中有详细分析。
误差的性质是表示性的,而非数值性的。 欧氏向量假设带来的问题,不是”采样不够密”或”精度不够高”,而是表示空间选错了。当机械臂末端执行器需要从初始姿态旋转约 到达目标姿态时,将两个旋转矩阵在欧氏坐标上做线性插值,所得的”中间状态”矩阵的行列式趋向于零——这不是一个合法的旋转矩阵,在几何上等于将三维空间压缩到接近退化的零体积。增加采样密度、提高浮点精度,均无法修复这个问题,因为问题出在选用了平坦的欧氏度量来度量本质上弯曲的 空间。 的内蕴度量(李群测地距离)在整个姿态空间上是一致有界的,而欧氏近似的误差在高曲率区域(旋转角接近 时)没有上界。
使用边界在于旋转幅度。 当任务的旋转幅度较小(粗略地说,关节角变化量 )时, 局部曲率的影响可以忽略,欧氏近似误差有界且较小——桌面物品抓取、平面装配等场景属于此类,三个系统在这类场景上的良好表现正是建立在这一隐含条件成立的基础上。但架空线路带电作业要求机械臂在复杂立体空间中全程保持安全间距,整条轨迹上的姿态变化幅度大、高曲率区域无法回避,欧氏假设在这里从合理近似退化为系统性安全漏洞。
2.1.3 开放词汇表的语义处理假设
三个系统都默认语言模型能够处理”任意”的自然语言输入——这是大语言模型训练范式的内置假设:通过足够大的训练集和模型容量,覆盖足够广的词汇和概念。
这个假设的失效边界,在专业领域表现得尤为清晰。电力行业的专业术语——“均压环”、“防振锤”、“绝缘子串”——的使用规范和操作约束,不会出现在通用LLM的训练语料中,或出现频率极低。当任务描述包含这些术语时,系统要么以低置信度的语义近似替代,要么静默地将其映射到最相近的通用概念——两者都不是可验证的正确理解。
问题不是”数据不够多”,而是”覆盖缺口无法被证明不存在”。 即便假设我们将所有电力行业文档都纳入训练语料,PAC 学习框架的保证仍然停留在”以高概率近似正确”这一形式,而无法给出”对所有合法输入均正确路由”的形式等式。有限训练集对无限可能输入空间的覆盖,在数学上必然留有正概率的空白——这不是工程资源问题,而是统计学习方法的根本结构限制。真正的覆盖完备性(SEC = 1)只能在任务域被显式限定为有限可枚举的闭合集合时,通过形式化方法证明,而非通过增大训练集逼近。
静默失效比可见失效更危险。 当系统遇到真正不认识的输入时,一个理想的系统应该报告”覆盖缺口”。但基于统计学习的语义处理没有区分”已知答案”和”统计近似答案”的机制——它总是给出一个置信度最高的映射。“均压环”被静默映射到某个相近的通用概念后,系统会以正常的置信度继续规划和执行,不会触发任何警告。在带电作业场景中,这意味着一个基于错误语义理解的操作指令,会在没有任何错误信号的情况下传递到物理执行层。
2.1.4 感知-动作的统计对应假设
RT-2将视觉语言模型的输出token直接解码为机器人动作指令,隐含假设了从感知(视觉+语言)到动作(关节角度指令)的映射可以通过端到端的统计学习被捕获。这个假设的有效性依赖于训练分布与部署分布的足够接近(distribution shift假设),以及物理约束的统计可学习性(即安全约束可以从大量示例数据中隐式学习)。
这两个子假设在安全关键部署条件下都不成立:带电作业场景与任何现有训练数据集的分布距离极大;安全约束(法定安全间距)是离散的、绝对的条件,不是统计意义上的”通常保持距离”。
安全约束与性能指标的类型差异,是统计方法的结构性盲区。 端到端学习的工具箱——损失函数、梯度下降、概率保证——天然地处理期望值问题:让平均任务完成率更高、让平均误差更小。但法定安全间距是一个全称量词命题:“对轨迹上的每一个时刻,安全距离都不小于规定值。“这不是一个期望值,而是一个全域约束。统计学习没有机制来优化全称命题——它能给出”这类任务通常保持安全距离”的统计保证,但无法给出”这次具体执行的每一时刻都满足”的形式证明。这是类型差异,不是性能差异:不存在一个足够大的统计模型,能通过更多训练数据获得对全称安全约束的形式保证能力。
缩放律的成功强化了这一盲区。 大语言模型和视觉语言模型在语言理解、推理、跨域泛化上随规模增大而持续提升,这一经验规律让研究者有充分理由相信”足够大的模型可以学到任何感知-动作映射”。RT-2 的设计理念正是缩放律信念在机器人控制领域的延伸。但安全约束的形式可证明性,不是一个可以通过更大模型来近似的目标——它从根本上要求对可能执行路径的全域推理,而这类推理不是统计学习的能力范围,而是形式方法的能力范围。
表 2.1 将三个系统在三类假设下的失效边界并排对比,每行给出理论失效机制(为什么在结构上必然失效)和代表性文献依据。
| 系统 | 失效假设 | 理论失效机制 | 代表性文献 |
|---|---|---|---|
| SayCan | 欧氏向量假设 | 技能价值函数 将 位姿压缩为欧氏向量;六个正交性约束被隐式丢弃,高曲率区域(姿态变化快速时)的插值误差无界增长 | Ahn et al., 2022; Murray et al., 1994 |
| SayCan | 开放词汇表假设 | 语言分数 依赖通用 LLM 先验;专业术语(“均压环”、“防振锤”)在训练语料中的语义密度接近零,系统静默映射到最近通用概念而非报告覆盖缺口 | Ahn et al., 2022; Wei et al., 2022 |
| SayCan | 统计对应假设 | 技能可行性由统计估计给出;法定安全间距是离散绝对约束,统计模型无法提供零违反概率的形式保证 | Ahn et al., 2022; Robey et al., 2022 |
| RT-2 | 欧氏向量假设 | 动作指令以分词表示(离散化欧氏坐标),跳过 李群结构;离散化精度约 1 cm,不满足带电作业毫米级间距要求 | Brohan et al., 2023; Park & Bobrow, 1995 |
| RT-2 | 开放词汇表假设 | 端到端 VLM 在通用网页语料训练;电力专业术语频率极低,模型对其语义的不确定性无法量化,更无法给出覆盖闭包证明 | Brohan et al., 2023; Bommasani et al., 2021 |
| RT-2 | 统计对应假设 | 感知→动作映射完全由端到端统计学习捕获;带电作业部署环境与任何现有训练集的分布距离无上界保证,分布偏移导致安全约束静默失效 | Brohan et al., 2023; Cobbe et al., 2019 |
| ProgPrompt | 欧氏向量假设 | 前置条件与效果谓词以欧氏向量形式表示;程序拼接多步规划时无法验证 约束,误差沿执行链累积 | Singh et al., 2023; Chirikjian, 2011 |
| ProgPrompt | 开放词汇表假设 | 程序模板由 LLM 生成,假设模型理解任意任务描述;专业操作名称(“紧线”、“装设接地线”)无法通过模板匹配正确路由 | Singh et al., 2023; Liu et al., 2023 |
| ProgPrompt | 统计对应假设 | 子任务成功判断依赖 LLM 统计推断;无法处理需要精确物理量度(电气安全间距)的硬约束验证,“程序执行完成”与”约束真正满足”之间的鸿沟无法弥合 | Singh et al., 2023; Seshia et al., 2018 |
写作注 — 上表文献引用随正文写作逐步核实补全;已确认收录的条目:Ahn et al. 2022 (SayCan)、Brohan et al. 2023 (RT-2)、Singh et al. 2023 (ProgPrompt)。其余条目待系统文献梳理后补充。
2.2 统计近似的天花板:从 SEC ≥ 1−δ 到 SEC = 1 的认识论鸿沟
在进入本节论证之前,需要先界定两个核心概念的含义。
语义覆盖率(Semantic Coverage,SEC) 是本书度量具身AI系统语义完整性的核心指标。直觉上,SEC 回答这个问题:系统对任务域中所有合法的任务描述,能够给出正确的语义理解和操作路由的比例是多少?形式上,若任务域为 (所有合法任务描述的集合),系统的语义模型为 ,则
意味着对任务域的完整覆盖——系统对所有合法描述都能给出正确理解; 意味着存在覆盖盲区,系统对某些合法输入会给出错误或不确定的响应。SEC 的严格数学定义和可计算形式将在第5章展开;本章使用其直觉含义。
PAC 学习(Probably Approximately Correct learning,概率近似正确学习) 是由 Valiant(1984)建立的统计学习理论框架,它以”高概率近似正确”的形式给出学习算法的泛化保证。本节将用 PAC 框架的语言说明,统计学习方法能给 SEC 提供的最强保证是什么形式,以及这个形式为何必然停留在 (概率界),而无法到达 (形式等式)。
统计学习方法给出的最好语义覆盖保证,是概率界 。本节从PAC学习理论出发,说明这个界为什么有天花板,以及天花板在哪里。
2.2.1 PAC 学习框架的保证结构
PAC(Probably Approximately Correct)学习框架以如下形式给出保证:对任意分布 和误差参数 ,经过足够多的训练样本后,学习算法以概率至少 输出一个误差不超过 的假设。这是一个关于”高概率近似正确”的保证,其中 是保证失败的概率, 是允许的近似误差。
关键观察:即使 被训练到极小,它仍然是正概率。PAC学习的保证结构中,没有任何机制能将 降至零——因为有限训练样本对无限可能输入的覆盖,在数学上必然留有空白。
游戏类比:规则层与策略层的分裂。 游戏提供了一个干净的对照实验,因为同一个游戏里,规则层和策略层的学习性质截然不同。
棋盘上某步是否合法、某个道具能否合成——这是有限枚举的,可以形式验证,不需要任何样本,直接给出确定性答案。但”这步棋走了之后赢面有多大”——即使在完全封闭的围棋规则世界里,也是无法穷举计算的。AlphaGo 本质上就是在 CWA 规则框架内做 PAC 式的策略学习:从 局对弈样本中,学到一个策略 ,使得 。AlphaGo 下得再好,它对”某个局面下的真实胜率”的估计仍然是概率界,而不是形式等式。
| 层次 | 游戏类比 | EICPS 对应 | 可达保证 |
|---|---|---|---|
| 词汇 / 规则层 | 棋规(某步是否合法) | V-167 词汇表 | (形式验证) |
| 策略 / 规划层 | 棋力(走哪步最优) | 路径规划、优先级决策 | (PAC 学习) |
EICPS 的核心主张不是消灭 PAC 学习,而是把词汇层从 PAC 领域剥离出来放到形式验证领域——像棋规一样精确,而不是像棋力一样只能逼近。这一分层是本章论证的落脚点,也是第二部分几何理论和第四部分验证链的共同出发点。
2.2.2 天花板的数学根源:开放世界假设
统计学习的天花板,根源在于开放世界假设(Open World Assumption):训练数据覆盖的是世界的一个有限子集,而模型在推理时可能面对训练分布之外的输入。这不是算法或数据的缺陷,而是统计学习范式的本质特征。
闭合世界假设(Closed World Assumption)恰好相反:世界是有限可枚举的,所有可能的输入都可以被显式枚举和验证。在闭合世界下, 不再是统计逼近的极限,而是可以通过有限步骤验证的数学命题。
游戏软件是闭合世界假设最直观的工程实例。 游戏引擎由开发者显式枚举了所有可能的场景、道具、敌人、任务类型和动作指令。玩家的所有合法输入属于一个有限集合,游戏的语义模型对这个集合的覆盖率恰好是 。当玩家输入无效指令时,系统不会给出统计近似的模糊响应,而是明确返回”无效操作”——这正是闭合世界假设下系统行为的典型特征。
这里有一个值得辨析的术语混淆:游戏行业把《GTA》《Minecraft》这类大地图游戏称为”开放世界游戏”(Open World Game),指的是空间自由度高;但在认识论意义上,这些游戏仍然是闭合世界——《Minecraft》的地图可以接近无限延伸,但游戏引擎里所有方块类型、合成配方、生物行为都是有限枚举的。空间的开放性(大地图)与任务域的开放性(无法枚举的合法输入集合)是两个不同层次的概念。
这一区分把三类系统放在同一坐标轴上:通用 LLM(如 GPT 系列)处理自然语言,输入空间无法枚举,是认识论意义上的开放世界;游戏软件由规则引擎驱动,任务域有限枚举,是闭合世界;架空线路运检则介于两者之间——其任务域由行业规程显式定义,有限可枚举,可以像游戏引擎一样建立闭合的词汇表,进而实现 。
从开放世界到闭合世界的转变,不是数据量的问题,而是对任务空间结构的认识论承诺——承认某个应用域的合法输入集合是有限的、可枚举的。这个承诺在架空线路运检场景中是合理的:行业规程明确定义了有限的操作类型集合。
2.2.3 认识论层级的清晰化
统计命题()和形式命题()不仅在量上不同,在认识论层级上也不同。两类证明工具各有严格的历史基础和适用边界。
统计命题的证明工具,其理论基础由 Valiant(1984)奠定——PAC 学习框架首次以严格数学语言回答了”从有限样本中学到的模型可以泛化到未见数据”的条件。Vapnik 与 Chervonenkis 于 1971 年引入的 VC 维将模型复杂度与样本复杂度精确关联,使 成为可计算的理论保证。统计学习理论在学术界已高度成熟,相关工作获图灵奖认可(Vapnik 对支持向量机与统计学习理论的贡献)。然而,深度学习时代暴露了一层新的张力:大型神经网络的 VC 维远超训练样本数,按经典理论应无法泛化,但实际效果良好——这一”泛化之谜”(generalization mystery)至今是活跃研究前沿,说明统计工具的边界比理论预期更为微妙。无论如何,只要训练集有限, 是嵌入在 PAC 框架数学结构中的事实,而非工具的缺陷。
形式命题的证明工具,根基更早也更坚实。Hoare(1969)的程序正确性逻辑(霍尔逻辑,Hoare Logic)建立了形式化推理程序行为的语言;Pnueli(1977)引入线性时序逻辑(Linear Temporal Logic,LTL,线性时序逻辑),使”系统永远满足某性质”这类命题可以精确表达;Clarke、Emerson 与 Sifakis(1981)发展的模型检验(Model Checking,模型检验)使有限状态系统的形式验证自动化成为可能。Pnueli 于 1996 年、Clarke 等三人于 2007 年分别获图灵奖,标志着形式化方法在计算机科学中的权威地位。在安全关键工程领域,形式验证早已是行业标准:英特尔在奔腾浮点错误(1994)后大规模引入硬件形式验证;航空软件认证标准 DO-178C 将形式方法列为最高等级保证工具;核电控制系统普遍要求形式规约。对具身AI的直接适配工具——CBF(Ames et al., 2014)和 STL(Maler & Nickovic, 2004)——均在这一传统上发展而来,工程接受度有充分积累。
形式工具的内在限制同样明确:它们需要对系统状态空间的精确有限描述,在无界或连续域中遭遇状态爆炸(state explosion)问题。这一限制划定了形式方法的适用边界:有限可枚举的闭合域。
两种工具的认识论定位因此是互补分工,而非竞争。统计工具回答”在开放世界中学到的模型有多可靠”,形式工具回答”在闭合世界中已知规则是否被满足”:
- 统计命题的证明工具:大量训练数据 + 足够强的学习算法 + 训练-测试分布一致性
- 形式命题的证明工具:对任务空间的有限枚举 + 词汇表的覆盖闭包验证 + 规范闭合性证明
两者都有严格的数学基础,都在各自适用域内被学术界与工程界广泛接受。它们之间的鸿沟,是任务空间结构的鸿沟,而不是工具成熟度的鸿沟。无论统计工具多强大,它都无法产生形式命题;无论形式工具多严格,它都需要闭合世界假设的成立才能启动。
2.3 具身空间:覆盖完整复杂度谱系的几何语言
若欧氏空间和统计近似都不足以描述具身AI系统的状态和行为,需要什么样的语言?本节给出具身空间的非正式介绍——正式定义将在第二部分建立。
2.3.1 为什么是流形
流形(Manifold)是局部像欧氏空间、整体可能弯曲的数学对象。 是一个流形:在每个位姿的邻域内,运动的一阶近似是线性的(这让局部线性化控制成为可能),但整体上不同位姿之间的关系是非欧的(这让全局插值和路径规划需要用测地线而非直线描述)。
流形语言相比欧氏语言的优势,不在于”更精确”,而在于”诚实”——它的数学结构如实描述了问题的几何本质,而不是用近似掩盖弯曲。在诚实的语言中建立的形式化保证,才是真实有效的保证。
具体例子: 上的插值失效。 设机械臂末端执行器需要从初始姿态 (单位矩阵)运动到目标姿态 ,对应绕 轴旋转 :
欧氏插值(直接对矩阵分量做线性混合,):
验证:,而合法旋转矩阵要求 、。这个”中间姿态”将三维空间压缩到一个退化的近零体积——末端执行器的指向在数学上是未定义的。
测地线插值( 上的黎曼指数映射,):
计算结果:绕 轴旋转 的合法旋转矩阵,, 精确成立。
这个差距的本质不是数值精度问题,而是几何表示问题:欧氏插值在 的高曲率区域(旋转角度接近 时曲率趋于无穷)产生退化,而测地线插值始终停留在流形上。对 CBF(Control Barrier Function,控制障碍函数——将在第6–7章详细介绍)安全约束的影响是直接的:CBF 要求系统轨迹与障碍物之间的距离函数在整条轨迹上保持非负,这个距离必须在正确的度量下计算。若用欧氏距离度量机械臂轨迹与带电导线的间距,在高曲率姿态区域的度量误差没有上界——约束在欧氏度量下”满足”,而真实几何距离可能已经违反。这不是可以用更密的采样或更高精度的数值方法修复的,因为问题出在度量本身。然而, 仅描述了物理位姿这一个维度;具身AI系统的状态,还同时在语义空间和感知空间中演化——一个系统的完整状态,不能用单一流形表示,而需要三个独立维度的乘积结构。
2.3.2 三流形乘积结构的直觉
具身AI系统的状态,自然分解为三个独立维度:物理位姿(机器人在空间中的位置和姿态)、语义状态(任务的理解程度和执行进度)、感知数据(传感器对环境的当前表示)。每个维度有其特定的几何结构:物理位姿在 上,语义状态在嵌入空间的一个弯曲子流形上,感知数据在由传感器模型决定的流形上。
三流形乘积结构 不是三个状态向量的简单拼接,而是一个几何主张:三个分量各自的曲率被完整保留在乘积空间中。将三个流形的坐标拼接为一个欧氏向量,等于隐式地对乘积空间施加了平坦的欧氏度量,会抹去每个分量的内在弯曲——这正是第2章一直在批评的做法。
三个分量流形各有鲜明的几何特征:
继承 的李群结构。旋转部分 是紧致的三维弯曲流形(嵌入在九维矩阵空间中的三维子流形),平移部分 是平坦的。两者通过半直积组合,赋予 非交换的群乘法:先旋转后平移与先平移后旋转是不同的变换。
的嵌入维度很高(如 BERT 系列编码器的 768 维),但任务相关的语义变化实际上占据一个内在维度远低的弯曲子流形。对于架空线路运检场景,用 Two-NN 方法估计的内在维度 ——768 维空间中有 766 维对任务表示是冗余的,真正的语义几何是一个二维弯曲曲面。
由传感器模型和物理世界共同决定。仿真数据流形与真实世界数据流形之间的距离——Sim2Real Gap——可以用 Gromov-Hausdorff 距离加以几何刻画,而不是简单地用统计分布偏移来描述。
乘积结构的核心价值在于使跨流形耦合约束可表达。“在执行任务 的同时保持与带电导线的安全间距”是一个同时涉及 和 的联合约束——在单独的物理流形上无法表达(回避方向取决于任务 要求机械臂去哪里),在单独的语义流形上同样无法表达(哪些语义状态可行取决于当前物理位置)。乘积流形 是这类耦合约束的自然载体。
2.3.3 形式化自主的几何表述
“形式化自主”的几何含义是:系统的状态轨迹 始终停留在三流形各自的安全子集 中。三个安全子集在架空线路运检场景中有具体含义:
- :所有与带电导体保持法定安全间距的物理位姿——国标规定 10 kV 线路不低于 1.0 m,随电压等级递增。离开 意味着触电风险。
- :所有当前任务描述得到完整正确路由的语义状态——等价于当前任务的 已通过验证。离开 意味着系统可能在执行错误的操作。
- :传感器读数处于运行设计域(ODD,操作设计域)内——感知系统的标定和可靠性对该区域成立。离开 意味着传感器读数不可信。
不变性与终点精度的本质区别是形式化自主的核心。终点精度问的是”系统最终到达了正确目标吗”;不变性问的是”系统在整条轨迹上从未离开安全集吗”。两者的差距如同”汽车最终停到了正确位置”与”汽车整个行驶过程中从未闯红灯”——对安全关键系统而言,只有不变性才是有意义的形式保证。一个”通常安全但偶尔违反约束”的系统,在形式意义上不提供任何安全保证。
不变性安全在控制理论中有深厚的理论传承。Lyapunov(1892)建立了动力系统集合稳定性的概念框架;Blanchini(1999)系统化了正不变集(positively invariant set)理论;Ames et al.(2014)发展的控制障碍函数(CBF)提供了实时可计算的不变性证书:CBF 函数 定义安全集 ,通过约束 保证轨迹不会向内穿越边界 。在具身空间 中,形式化自主等价于 、、 三个 CBF 函数沿任何可行轨迹同时非负——这是一个可计算、可验证的几何命题。
具身空间 作为数学对象的完整定义——包括乘积度量、混合动力学、安全子集的精确刻画——将在第二部分末尾(第6章)正式给出。本节建立的几何直觉是第二部分数学建构的动机;第三、四部分的架构设计和验证链,将在这个几何基础上实现形式化自主的工程落地。
2.4 规范闭合性:开放世界到闭合域的认识论转换
规范闭合性是本书从统计保证到形式等式跨越的关键概念。本节给出非正式的动机和初步定义——严格的数学处理在第5章和第11章进行。
2.4.1 闭合域假设的工程可行性
闭合世界假设(任务空间有限可枚举)在架空线路运检场景中的可行性,来自行业规程体系的一个特殊性质:规程是规范性文件,而非描述性文件。通用 LLM 的训练语料是描述性的——它记录了人们实际说了什么,因此无法穷举。行业规程则不同:它规定了操作人员被允许做什么。《带电作业技术规程》(DL/T 966—2005)、《电力安全工作规程》(GB 26859—2011)以及 Q/GDW 系列国家电网企业标准,共同构成一套分层的规范性体系,明确定义了架空线路运检的合法作业边界。规程没有规定的操作,在法律和工程意义上均不合法——因此”合法任务的全集”恰好等于”规程覆盖的作业类型集合”。
这一规范性特征在安全关键行业中并不孤立。航空管制领域的标准通话用语(ICAO Doc 9835)将飞行员与塔台之间的合法通信限定为有限词组集合;医疗操作编码系统(ICD-10、CPT)将合法诊疗行为映射到有限分类;核电站操作规程同样使用标准化的有限指令集。这些领域独立收敛到封闭词汇的做法,印证了一个共同的工程逻辑:当操作后果涉及不可逆的安全风险时,允许的操作集合必须是有限可定义的。
V-167 的命名来源于国家电网总部科技项目指南编号 167(2026 年度课题三:输电线路检修机器人任务规划与自主决策)——以项目编号命名,并非词汇条目的数量。词汇集从适用于架空线路运检的国标(GB 系列)、行标(DL/T 系列)与企标(Q/GDW 系列)规程文本中,经 NLP 自动提取与人工专家审核,系统覆盖运检场景的全部规程定义作业类型。这一构建路径与第2.2.2节讨论的”自顶向下接地”(top-down grounding)逻辑一致:锚点来自权威规范文件,而非从感知数据自底向上学习,因此继承了规程的封闭性。规程的封闭性保证了 V-167 的可枚举性,使得”词汇表是否完备覆盖了所有合法任务”从开放性的工程判断,变为一个可回答的数学问题。
2.4.2 规范枚举协议的直觉
规范闭合性的建立,需要一个规范枚举协议(Canonical Enumeration Protocol,规范枚举协议):一套系统性步骤,保证从行业规程中提取出的词汇集确实覆盖了所有合法的任务描述。
Step A——语义空间的 Voronoi 覆盖验证。将 V-167 的各词汇条目作为语义嵌入空间中的”锚点”,每个锚点 自然定义一个 Voronoi 单元 ——即所有在语义上”最接近 “的描述构成的区域。覆盖验证的几何含义是:对任务域 中的所有合法描述 , 的嵌入向量必须落入某个 Voronoi 单元,且与锚点的距离不超过路由阈值。这是一个几何覆盖问题,而非统计估计问题——但其验证本身需要 PAC 风格的采样界(第5章给出下界: 时,322 个查询样本可以给出 95% 置信度的覆盖下界)。
Step B——对抗性边界测试。系统性地探测 Voronoi 边界:构造在语义上”介于两个词汇条目之间”的边缘情形描述,验证词汇集的路由对这些情形仍然正确。这类似于对分类器决策边界进行压力测试——“对抗性”的含义是刻意选择最容易路由出错的输入。如果在对抗性构造下路由仍然正确,则词汇边界是鲁棒的。Step B 是从统计覆盖证据(Step A)到形式充分条件的关键升级:单有统计覆盖只能给出 SEC ,对抗性测试通过才能断言边界无漏洞。
两阶段联合通过,给出规范闭合性的充分条件。Step A 提供覆盖下界的统计证据,Step B 提供边界鲁棒性的形式证据,两者缺一不可。详细的协议设计与样本复杂度分析在第11章展开。
2.4.3 从协议到定理:闭合性的形式化
规范枚举协议的通过,在数学上对应 Theorem Q-18(第5章、第11章)前提条件的满足。该定理的非正式陈述为:若词汇集 满足 Voronoi 覆盖完备性(Step A)和对抗性路由正确性(Step B),则 ——不是基于统计推断,而是基于词汇集在语义嵌入空间中的几何结构。
这个从”协议通过”到”定理结论”的推导路径,在形式化方法领域有成熟的先例。ISO 26262(汽车功能安全)、DO-178C(航空软件认证)、IEC 61508(通用功能安全)都遵循同样的模式:设计者不是对每种可能的输入逐一验证安全性,而是证明系统满足若干抽象属性,再由定理保证系统级安全性质自动成立。规范闭合性定理在 EICPS 中扮演同样的角色:Theorem Q-18 是连接”协议设计”(工程)与”SEC = 1”(数学命题)的形式化桥梁。
一个细节值得强调:Theorem Q-18 的有效性依赖语义嵌入的质量——如果嵌入空间无法区分语义上不同的任务描述,Voronoi 覆盖就失去意义。第5章将分析嵌入质量的几何条件(Lipschitz 连续性与局部等距性),并说明在满足这些条件时定理的结论如何成立。从第11章的 V-SEM 实现来看,BERT 系列在电力专业语料微调后满足这些条件。
规范闭合性的完整数学处理——从嵌入空间的几何条件到 Theorem Q-18 的形式证明——将在第5章和第11章展开。本节的目标是建立直觉:闭合域不是凭空假设的,而是从规程体系的规范性结构中自然涌现出来的,可以通过可执行的协议加以验证,并最终由定理将这种验证转化为 SEC = 1 的形式保证。
2.5 EICPS 分层框架总览:理论上限、工程下限与中间层
第一部分以 EICPS 分层框架的全局视图作为收束,为第二到四部分的逐层展开奠定结构基础。
2.5.1 为什么是三层:工程系统分层的认识论根据
“理论上限 + 中间层 + 工程下限”的三层结构并非 EICPS 的独创,而是安全关键工程系统的共同设计模式。在工业自动化领域,IEC 61512(批次控制标准,Batch Control Standard)和 ISA-88 将生产控制分解为过程层(物理约束)、协调层(任务调度)和监督层(全局优化),三层各有明确的接口合约,上层可在不改变下层的前提下独立升级。在航空电子领域,集成模块化航空电子架构(IMA,Integrated Modular Avionics)将功能分为应用层、运行时环境和硬件抽象层;DO-178C 对每一层独立认证,认证深度与功能危害等级(DAL,Development Assurance Level)挂钩——危害越高,所需验证工具越重。在通信网络领域,OSI 七层模型的工程实践收敛为应用/传输/网络三大功能域,精确对应了”端到端语义 / 可靠投递 / 物理路由”的三级关注分离。
这些领域独立收敛到三层结构,揭示了一个共同的工程逻辑:复杂系统的形式化验证需要将”理论可行性”、“工程可达性”和”最小安全下界”分别编码到不同层次,才能同时满足数学严格性与实用部署约束。单一层次无法同时满足两端:纯粹的理论框架(上层)缺乏可实现性;纯粹的工程约束(下层)缺乏覆盖保证;中间层在保留上层理论结构的前提下,实现对真实任务分布的统计逼近。
EICPS 三层框架的独特之处,在于三层之间的共享基础:Brain/Spine/Body 架构和形式化证据链在三层之间完全共用——不同层次之间的切换,不是架构替换,而是相同架构上数学工具深度的选择性激活。这与 DO-178C 的 DAL 分级逻辑高度同构:硬件不变,软件验证深度随安全需求递增。
2.5.2 框架的三层映射关系
三层在五个维度上的精确对应如下:
| 维度 | 理论上限 | 中间层 | 工程下限 |
|---|---|---|---|
| 部署场景 | 完整认知-物理耦合(带电作业全自主) | 区域协同(多机协同巡检) | 局部确定(固定杆塔单点操作) |
| 激活的数学工具 | 三流形结构 + 完整验证链 | 语义路由 + 安全控制 | CBF + STL 规范子集 |
| 形式化保证 | SEC + 下界 + 零误触 | SEC + 安全控制 | 形式化轨迹安全 |
| 验证成本 | 高(三段验证链) | 中(语义路由 + 运行时监控) | 低(单层 CBF 综合) |
| 对应书稿部分 | 第二 + 四部分 | 第三 + 四部分(局部验证链) | 第三部分 Spine 层 |
三层之间有一个关键的单调性:从工程下限到理论上限,形式化保证强度单调递增,验证成本单调递增,激活的数学工具集单调扩张。这意味着理论上限是工程下限的扩展,而非替换——工程下限的保证在理论上限中完全成立,上层增加的是覆盖广度和认知深度的保证。
单调性带来一个重要的工程含义:系统可以从工程下限起步部署,随着验证能力的积累,逐步激活更高层次。从满足 CBF 轨迹安全开始,逐步添加语义路由验证(达到中间层),最终完成 SEC 的形式证明(达到理论上限)。激活路径是增量的,而非重构的——这使得 EICPS 框架对工程实践友好,而不只是理论理想。
2.5.3 各部分的逻辑依存关系
第二到五部分之间存在严格的逻辑依存关系,不可颠倒。
第二部分(第 3–6 章)建立理论上限所需的完整几何数学语言——流形定义、黎曼度量、李群结构、三流形乘积空间 ,以及 SEC 度量的精确数学定义。没有这一层,“任务路由语义上正确”这一陈述无法精确化,后续的形式化证明没有语义基础。
第三部分(第 7–10 章)在第二部分的几何框架上实现 Brain/Spine/Body 架构,给出可计算的接口协议和语义路由算法。没有这一层,第二部分的几何结构是纯粹的数学对象,无法与真实的传感器、执行器和决策流程对接。第三部分是”将数学实例化为工程系统”的桥梁。
第四部分(第 11–13 章)在第三部分架构上建立三段形式化验证链(语义覆盖验证 V-SEM、安全行为验证 V-SAFE、端到端验证 V-E2E),将第二部分的数学命题转化为可机械检查的证明。第四部分的验证目标(SEC 、CBF 不变集、STL 规范满足)与第二部分的定理(Theorem Q-18、CBF 综合定理)精确对应——第二部分给出”什么成立”,第四部分给出”如何证明它确实成立”。
第五部分(第 14–16 章)在三个复杂度层次上用场景实例测试完整框架。第五部分在认识论上不同于前三部分:它不引入新的数学,而是回答”满足数学条件的系统在真实场景中是否如预期运行”——这是理论与实践之间的最后一道验证关口。
四部分的依存关系可以用一句话概括:几何定义正确性(Part II)→ 架构实现正确性(Part III)→ 形式证明正确性(Part IV)→ 场景验证现实性(Part V)。每一步对前一步的正确性负责,同时引入新的验证维度。
2.5.4 第一部分的张力地图
第一部分的核心贡献,不是给出答案,而是精确地提出问题——将直觉上感受到的困难(“AI 在高压线作业中不可靠”)转化为可以被数学工具回答的命题。下表列出第一部分提出的关键张力及其对应的解答位置:
| 张力 | 提出位置 | 解答章节 |
|---|---|---|
| 欧氏插值的几何失效(SO(3) 179° 例子) | §2.1 / §2.3.1 | 第 3–5 章(流形定义与 SE(3) 几何) |
| 统计近似的认识论天花板(SEC 不可突破) | §2.2 | 第 5 章 Theorem Q-18 |
| 三流形乘积空间的精确数学定义 | §2.3.2 | 第 6 章(具身空间 完整定义) |
| 安全不变集的几何形式化(、、) | §2.3.3 | 第 7 章(CBF 综合)/ 第 12 章(V-SAFE) |
| 规范闭合性的充分条件与验证协议 | §2.4.2 | 第 11 章(V-SEM 实现与样本复杂度) |
| 嵌入质量对 Theorem Q-18 有效性的依赖 | §2.4.3 | 第 5 章(Lipschitz 条件分析) |
| 框架在三个复杂度层次的实际可用性 | §2.5.2 | 第 14–16 章(分层场景验证) |
张力地图的意义是双向的:它告诉读者”每个技术难点在哪里得到回答”,也告诉作者”每个后续章节必须兑现哪些在第一部分埋下的承诺”——第一部分提问,其余各部分逐一作答。
2.5.5 第一部分的使命完成
回顾第一部分走过的思路路径。第 1 章从时间线出发,描绘了 SayCan、RT-2、ProgPrompt 三代系统的演化轨迹,以及它们在失效边界处共同遭遇的认知-物理耦合困难——这是全书的工程动机,也是出发点。第 2 章将这一感知性困难分解为三个可精确化的障碍:几何语言的不匹配(§2.1–§2.3)、统计工具的认识论天花板(§2.2)、以及任务域的开放世界假设(§2.4);并依次引出三类对应工具——流形几何、形式验证、规范闭合性。
第一部分没有解决这些问题——解决将在第二至四部分逐步完成。第一部分的使命是:将模糊的工程直觉转化为精确的数学问题陈述,使得”能否解决”本身变成一个可以被形式化回答的命题。这种”将工程问题数学化”的转化,是本书最核心的认识论主张:不是用数学装饰工程,而是让工程的困难内在地要求数学。
从第 3 章开始,我们进入数学建构的领域。
本章是第一部分的收束,同时是第二部分的引导。第 3 章将从流形的严格数学定义出发,逐步建立具身空间的完整几何基础。
参考文献
写作占位 — 本章参考文献列表(随正文写作逐步完善)