一张图读懂 EICPS 理论框架

这张图从上到下呈现了一条完整的推导链：工程问题触发数学诊断，诊断推导理论框架，框架决定工具选型，工具落地为系统架构，架构输出可审计的安全证明。六层之间不是并列关系，每一层都是下一层存在的前提。

第一层：工程问题

Prj167（500 kV 架空输电线路智能作业机器人）是整个框架的起点。当前系统依赖遥操作——操作员实时发送指令，自身充当安全兜底。研究目标是把它升级为自主操作（Human-on-the-Loop），让 AI 做决策，操作员只监督。

这个转变打开了一个缺口：遥操作中由操作员承担的实时安全判断，在自主操作中没有人来承担。需要形式化机制来填补。这个缺口就是 Safe Autonomy 问题——图中紫色虚线框标注的学术框架背书（Fan, ACM Books 2023）——但 EICPS 要做的不是引用一个框架，而是解决这个框架要求的底层数学结构。

第二层：状态空间数学诊断

“直接给旧方案加形式化验证”行不通。诊断首先要回答：为什么行不通，行不通在哪里？

具身系统的状态由数学性质根本不同的异质分量组成（V0.2： $X_0 = X_{phy} \times X_{cyb} \times X_{task} \times X_{norm}$ ，各分量用各自合适的数学，不强行统一为流形）：

$X_{phy}$ （物理域）：关节位姿和力矩，用 SE(3) / 配置流形描述——这部分用流形是恰当的。状态是有限维向量，动力学有解析形式，CBF 和 STL 的代数前提在这里成立。

$X_{task}$ （任务域）：任务意图和 AI 规划输出，是图结构的纯离散切换空间。没有连续演化，只有节点跳转——它不是流形，用自动机/任务网络描述。

$X_{cyb}$ （信息域）：感知状态、环境状态、人的意图估计——不可直接观测但影响行为的量。用信念状态与概率空间描述，EKF 处理高斯近似，PINN 处理物理约束下的非线性估计。

旧方案的失败根因：机械臂（有限维 ODE）与导线（三维连续体 PDE，状态 $\mathbf{w}(\cdot,t) \in [L^2([0,L])]^4$ ）耦合后，合并状态空间变成无穷维，CBF 的李导数和 STL 的鲁棒度都无法在有限时间内计算（→ 详细论证）。

第三层：ES 组织框架

诊断给出了设计约束，理论框架把约束转化为结构。

接口的结构保持要求：语义层合法的操作序列可能对应物理上不可行的状态——这就是物理幻觉（语义规划结果违反物理可行集）。因此语义到物理的映射必须显式检查结构保持性，范畴论在此仅作为接口组合的描述语言使用，不构成安全性证明（V0.2 修订，见修订说明第 3 条）；实际安全兜底由可行集校验与 CBF 承担（→ 详细定义）。

Flow-Jump 混合动力系统： $H = (C, f, D, g)$ ，连续作业阶段为 Flow，锁紧 / 换装 / FAILSAFE 触发为 Jump。这套语言（Goebel, Sanfelice & Teel 2012）把模态切换纳入正式数学描述，而不是作为异常处理。

分离式硬件设计：这是状态空间结构诊断直接推导出的硬件方案，不是经验选择。它满足形式化可处理性的三个充分条件：① 各作业阶段状态为有限维向量；② 动力学有解析形式（ $\dot{x} = f(x,u)$ ，李导数可计算）；③ CBF-QP 在控制周期内可求解。这三个条件是必要的，满足它们的方案是充分的（→ 推导过程）。

第四层：形式化工具

异质状态分量的数学结构决定了工具的配置方式，不是先选工具再凑框架：

STL（Maler & Nickovic 2004）：写安全规约，实时计算鲁棒度 $\rho$ 。正值表示满足，负值表示违反，是 Brain 层向 Spine 层传递安全要求的语言。

CBF（Nagumo 1942 / Ames et al. 2017）：实时 QP 过滤。把 Nagumo 不变集条件转化为 1kHz 频率下的有限维优化问题，是 Spine 层的执行核心（→ 形式化验证历史来龙去脉）。

HTN（Erol, Hendler & Nau 1994）：在 $\mathcal{M}_{sem}$ 上做任务分解，生成工具切换序列，输出给接口 A。

EKF（Kalman 1960）：在 $\mathcal{M}_{lat}$ 上做状态估计，为 CBF 提供可靠的有限维状态向量输入。

图中的 Safe Autonomy 框（虚线紫色） 刻意与四个工具框区分——它是这套工具选型的学术框架上游，不是同级别的工具，也不是 EICPS 的贡献。EICPS 的贡献是说清楚为什么这四个工具的组合能完整覆盖工程约束空间，以及每个工具在哪一层工作（→ 为什么是这七个工具）。

第五层：分层架构（V0.1 三层 → V0.2 六层）

三类处理频率的物理约束要求必须分层；层数是设计决定——图中为 V0.1 三层（Brain-Spine-Body），V0.2 已细化为六层（Spine 拆为合规门控/确定性执行器/最小安全内核，见修订说明第 5 条），推导图待按六层重绘。以下为 V0.1 三层的频率分工（作为历史口径保留）：

Brain（≈1 Hz）：大模型推理无法实时化，这是物理约束，不是工程选择。负责语义规划和 HTN 任务分解，输出 STL 规约包给接口 A。不要求 AI 绝对正确。

Spine（≈1 kHz）：CBF-QP 必须在控制周期内完成，无法等待大模型。负责安全过滤、STL 监控、EKF 估计，输出经形式化检验的运动指令给接口 B。不依赖 AI 正确性——这是架构设计的关键：可靠性来自下游形式化机制（V0.2 中由安全内核与门控分担），不来自 Brain 的准确率。

Body（μs 级）：硬件时序，软件层无法介入。接收 Spine 的实时指令，回传传感器数据。

接口 A（Brain→Spine）传递的是 STL 规约，接口 B（Spine→Body）传递的是经过 CBF 过滤的运动指令。这两个接口在时间尺度和内容类型上都截然不同（→ 为什么要分层？从三层到六层）。

第六层：EvidencePack

每次任务执行后，Spine 层将安全验证结果打包为机器可读的结构：

$\{P,\; A,\; x_{act},\; \varphi,\; \rho^*,\; v\} \quad \rho^* \geq 0 \implies \text{安全规约满足}$

六个字段分别是：任务场景规约、执行动作序列、实际状态轨迹、安全规约 STL 公式、最小鲁棒度、验证标识符。 $\rho^* \geq 0$ 是安全性成立的充要条件，机器可验证，不依赖人工判断。

EvidencePack 把”安全性已被验证”从声明变为可追溯的数学事实，是 EICPS 区别于纯工程实现的核心输出（→ 什么是 EvidencePack？）。

这张图的推导逻辑

从上到下每一层都是下一层的充分条件，不是平行选项：

没有工程问题，就没有动力去做数学诊断
没有数学诊断，分离式设计就是经验猜测，工具选型就是任意凑合
没有理论框架，Brain-Spine-Body 就是生物类比，不是可证明的工程架构
没有形式化工具，EvidencePack 就是空洞的声明