文档中心 / 研究问答 Q-24

旧方案形式化验证失败是工程能力不足，还是结构性失败？

一句话回答

是结构性失败。 旧方案的形式化障碍来自数学前提不成立，不是算力不够、工具不对、或实现难度太高。换更好的芯片、更快的 QP 求解器都无法解决这个问题。

旧方案是什么

Prj167（500 kV 架空输电线路智能作业机器人）的原始作业设计：

  • 机械臂持续施力于导线（夹持 / 沿线滑动 / 连续接触工具操作）
  • 机械臂与导线保持力学耦合，导线随之振动
  • 在此状态下执行精细操作任务（除冰、线夹更换等）

这个方案的直觉是合理的——模仿人工高压作业的持续接触模式。但当我们尝试为它建立形式化安全验证时，遇到了三道独立的数学障碍。

第一道障碍：状态空间维度爆炸

架空导线在空间中做三维运动，需要四个分量才能完整描述其位移状态：

分量符号物理含义
竖向（面内）wz(x,t)w_z(x,t)重力方向的横向位移
水平（面外）wy(x,t)w_y(x,t)垂直于竖直面的横向位移
纵向u(x,t)u(x,t)沿导线轴向的拉伸位移
扭转θ(x,t)\theta(x,t)绕导线轴的扭转角

这四个分量各自满足偏微分方程，其中横向两个分量的方程形如：

ρA∂2wi∂t2+EI∂4wi∂x4−T(x)∂2wi∂x2=qi(x,t)−Fi(t) δ(x−x0),i∈{y,z}\rho A \frac{\partial^2 w_i}{\partial t^2} + EI \frac{\partial^4 w_i}{\partial x^4} - T(x)\frac{\partial^2 w_i}{\partial x^2} = q_i(x,t) - F_i(t)\,\delta(x - x_0), \quad i \in \{y, z\}

其中 T(x)T(x) 是沿线分布的张力（高压线悬链线形态下 T(x)T(x) 非均匀），F(t)=(Fy,Fz,Fu)\mathbf{F}(t) = (F_y, F_z, F_u) 是机械臂施加的三维接触力。不同振动模式激励不同方向：微风振动（Aeolian vibration）主要激励竖向 wzw_z；导线舞动（Galloping）同时激励 wyw_y 和 wzw_z，轨迹为椭圆；机械臂的接触力是三维向量，原则上可以激励全部模态。

每个分量的完整状态都是连续区间 [0,L][0,L] 上的函数，而不是有限个数字。 四个分量合在一起，导线的完整状态是向量值函数：

w(⋅, t):  [0,L]  →  R4,w(⋅,t)  ∈  [L2([0,L])]4\mathbf{w}(\cdot,\, t):\; [0,L] \;\to\; \mathbb{R}^4, \quad \mathbf{w}(\cdot,t) \;\in\; \bigl[L^2([0,L])\bigr]^4

这是无穷维 Hilbert 空间中的一个元素。将机械臂的有限维状态 q∈Rnq \in \mathbb{R}^n 与导线的无穷维状态 w(⋅,t)\mathbf{w}(\cdot,t) 耦合后，整个系统的状态不再可以表示为任何有限维向量。

形式化验证的前提条件——有限维状态表示——不成立。

第二道障碍：CBF 屏障函数不可定义

CBF（Control Barrier Function）的核心不等式要求计算李导数：

dhdt(x)=∂h∂x⋅f(x,u)≥−α(h(x))\frac{dh}{dt}(x) = \frac{\partial h}{\partial x} \cdot f(x, u) \geq -\alpha(h(x))

当状态包含 w(⋅,t)∈[L2([0,L])]4\mathbf{w}(\cdot,t) \in [L^2([0,L])]^4 时，∂h∂w\frac{\partial h}{\partial \mathbf{w}} 是无穷维空间到实数的线性泛函（Fréchet 导数），ff 是作用在函数空间上的 PDE 算子。两者的”内积”即便在形式上可以写出，也没有有限维度内的数值实现——这不是精度问题，而是这个对象根本不是有限维向量，QP 的决策变量 uu 无法从一个没有闭合形式的梯度中构造出来。

QP 优化问题的建立依赖这一计算，QP 建不起来，CBF 机制完全失效。四分量向量场比标量位移更难处理，障碍只会更高，不会更低。

第三道障碍：STL 鲁棒度无法实时计算

安全规约用 STL 表达，例如：

φ=□[0,T]  min⁡x∈[0,L]∥FK(q(t))−w(x, t)∥R3  ≥  dsafe\varphi = \square_{[0,T]}\; \min_{x \in [0,L]} \bigl\|\mathrm{FK}(q(t)) - \mathbf{w}(x,\, t)\bigr\|_{\mathbb{R}^3} \;\geq\; d_\mathrm{safe}

即”在整个作业时段内，机械臂末端（由正运动学 FK 给出）到导线上任意一点的三维欧氏距离始终不小于安全间距”。这里 w(x,t)∈R3\mathbf{w}(x,t) \in \mathbb{R}^3 是导线上 xx 处的空间坐标，由参考位置加上三个位移分量给出。

实时计算鲁棒度 ρ(φ,t)\rho(\varphi, t) 需要知道 w(⋅,t)\mathbf{w}(\cdot, t) 的当前完整三维形态。但 w(⋅,t)\mathbf{w}(\cdot, t) 是四分量 PDE 系统的解——没有解析形式，每步数值求解需要空间离散化（有限元或谱方法）和时间积分，计算代价远超毫秒级控制周期。更重要的是，min⁡x\min_{x} 操作本身需要在连续区间上搜索，即便导线形态已知，求解最近点也是额外的计算负担。

STL 实时监控的前提——规约信号的在线可计算性——不成立。

三个障碍同时存在，互相独立

障碍根源能否绕过
状态维度无穷导线三维连续体：w(⋅,t)∈[L2]4\mathbf{w}(\cdot,t) \in [L^2]^4不能（模态截断引入的高频误差无法在安全证明中被计入）
CBF 李导数不可算Fréchet 导数作用在函数空间上，无有限维闭合形式不能（不是计算速度问题，是代数对象类型问题）
STL ρ 不可实时评估三维形态依赖 PDE 数值解，min⁡x\min_x 搜索额外开销不能（即使忽略 PDE 求解，min⁡x\min_x 本身也无法在控制周期内完成）

三个障碍来自同一个根因（三维连续体与有限维 ODE 的耦合），但各自阻断了不同的形式化工具链，且彼此独立——解决其中一个不会缓解另外两个。

诊断的正确结论

失败的原因不是：

  • 算法没选对（换 MPC / 换神经网络不能解决这个问题）
  • 算力不够（更快的处理器不改变代数结构）
  • 工程实现不够精细（不是实现层的问题）

失败的原因是：旧方案使得系统状态空间结构与形式化验证工具所要求的代数前提不兼容。这是数学上的结构性障碍，必须从根本上改变作业设计，而不是优化现有方案。

这个诊断直接推导出分离式设计的必要性（→ 分离式设计为什么是数学必要条件？），也是具身空间 ES 强调”异质状态各用合适数学、物理域保持有限维可解析”的直接理由（→ 从 EST 到 ES：概念演进）。

→ CBF 与 MPC 的比较 · STL 规约与鲁棒度 · 什么是 EvidencePack？