第四部分导言

一条链的强度，由它最弱的一环决定。如果”语义理解”这一环是统计性的，那么即使后续的”规划质量”和”执行安全”都是形式化保证的，整条链的保证等级也只能是统计性的。端到端的形式化自主，要求链上每一环都达到形式等式的强度。

为什么需要一条链

在第三部分建立的Brain/Spine/Body架构中，一个具身AI系统的完整执行过程经历三个阶段：Brain层将自然语言任务描述转化为结构化的执行计划（语义理解阶段）；Spine层对Brain层的计划进行质量评估，并将高质量计划编译为STL规约（规划质量阶段）；Body层在CBF安全层的监护下执行具体的物理动作（物理执行阶段）。

如果我们希望对整个过程给出形式化的自主性保证，那么这三个阶段必须逐一处理——任何一个阶段的保证缺失，都会使整体保证退化为统计断言。

这就是”验证链”这一概念的核心含义：它不是三个独立贡献的并列，而是对同一保证目标的三段串行证明。V-SEM的输出是V-PLN的前提，V-PLN的输出是V-SAF的前提，三段合在一起，才能给出从”任务被完整理解”到”执行过程物理安全”的端到端形式化保证。

第四部分依次建立这三段证明。

第一环：语义完备性（V-SEM）

问题的精确表述。 Brain层调用大语言模型进行语义路由——将自然语言任务描述中的关键词映射到预定义的任务类型集合中。这个映射依赖语言模型对词汇表的覆盖能力。如果任务描述中出现了词汇表中不存在的专业术语，语言模型将面临”词汇盲区”：它可能沉默（返回空结果）、可能猜测（返回最相近但语义错误的结果）、或可能幻觉（返回语义上完全错误的结果）。三种情形在安全关键场景中都是不可接受的。

SEC从不等式到等式的跨越。 语义覆盖率 $\mathrm{SEC}$ 的统计定义给出 $\mathrm{SEC} \geq 1-\delta$，意味着以概率 $1-\delta$ 覆盖任务空间。这个界可以通过增加训练数据、增大词汇表来收紧 $\delta$，但它永远无法到达 $\mathrm{SEC}=1$——因为统计界本质上是开放世界假设下的近似，任何有限样本都无法排除”下一个见到的词汇超出覆盖范围”的可能性。

规范闭合性（Canonical Closure）提供了跨越这道鸿沟的唯一路径：当且仅当任务知识域是有限可枚举的（闭合域假设），且词汇表 $\mathcal{V}^L_{167}$ 通过系统性的词汇枚举协议构成对该域的覆盖闭包，$\mathrm{SEC}=1$ 才成为可证明的形式等式而非统计近似。

第11章构建并证明这一协议，对V-167词汇集进行两阶段验证（Step A：向量覆盖验证，Step B：边缘案例对抗测试），给出Theorem Q-18的完整证明，并分析从开放世界到闭合域的认识论转换条件。$\mathrm{SEC}=1$ 的建立，是第二环和第三环的形式化前提——如果语义层存在盲区，后续两环的所有努力都建立在不稳固的基础上。

第二环：规划质量（V-PLN）

语言模型幻觉的几何本质。 Brain层依赖大语言模型（LLM）进行规划。即使在 $\mathrm{SEC}=1$ 的条件下（语义覆盖完备），LLM仍然可能产生幻觉：生成在形式上合法（符合词汇表）但在内容上错误的任务计划——步骤顺序颠倒、物理约束被忽略、任务类型被错误组合。

第12章提出，幻觉在语义流形 $\mathcal{M}_{\mathrm{sem}}$ 上有一个精确的几何解释：LLM输出的语义嵌入向量与参考任务计划的语义嵌入向量之间，存在一个可度量的语义分歧度 $d_{\mathrm{Sem}}$。高幻觉率对应高 $d_{\mathrm{Sem}}$；零幻觉对应 $d_{\mathrm{Sem}} < \epsilon_{\mathrm{thr}}$（在语义流形上的邻域内）。

$\mathcal{M}_{\mathrm{sem}}$ 结构约束下的对齐。 通用LLM的语义分歧度高，是因为它的训练目标是覆盖尽可能广的语义空间，而非在专业任务的语义流形结构上精确对齐。QLoRA微调将通用LLM的语义输出拉向 $\mathcal{M}_{\mathrm{sem}}$ 的低曲率区域——专业任务的密集分布区——幻觉率的降低（16.5倍）在几何上对应语义嵌入向量的方差被 $\mathcal{M}_{\mathrm{sem}}$ 的局部曲率约束所收紧。

形式质量下界 $Q(f)$。 $\Delta_{\mathrm{align}}$ 度量微调前后语义分歧度的降幅，由此给出规划质量函数 $Q(f)$ 的形式下界 $Q(f) \geq 0.944$。这个下界的意义在于：它不是在说”LLM在90%以上的情况下能产生正确计划”，而是在说”在 $\mathcal{M}_{\mathrm{sem}}$ 的结构约束下，LLM输出与参考计划之间的形式距离被控制在可接受的上界以内”——两者的保证强度不在同一认识论层级上。

第三环：执行安全（V-SAF）

最后一道防线的设计挑战。 假设V-SEM保证了语义完备，V-PLN保证了规划质量，但执行过程中仍然可能出现安全威胁——不是因为语义错误，而是因为物理世界的不确定性：导线的实时摆动超出预测模型的范围、突发的风速变化、传感器噪声导致的状态估计偏差。这些情形无法在语义层或规划层预防，必须在物理执行层实时拦截。

第13章设计纵深防御架构：L1层（STL在线监控）持续评估当前轨迹是否满足时域安全规约；L2层（CBF仲裁）在L1发现违规风险时，通过QP求解器实时修正控制输入以恢复安全；L3层（FAILSAFE模式）在L2无法恢复时触发停机。三层递进，每层都对应一个形式化可判定的条件。

跨域正交化：为什么CBF能抵抗语义错误的传播。 物理流形 $\mathcal{M}_{\mathrm{phy}}$ 上的CBF安全约束，与语义流形 $\mathcal{M}_{\mathrm{sem}}$ 上的语义错误，在数学上是正交的——CBF检验的是机械臂末端在三维空间中与带电导线的物理距离，这个检验对”上游语义是否正确”完全不敏感。即使Brain层的某条指令携带了V-PLN未能完全过滤掉的语义错误，只要该错误导致的物理轨迹违反了CBF安全集，L2层会在轨迹执行过程中实时拦截。这种跨域正交化，是纵深防御的数学基础。

零误触保证。 50场景仿真验证（涵盖正常作业、极端风速、传感器降级、指令异常等边界情形）给出零误触（false activation）的形式证明：在满足V-167词汇集闭合性的任务类型范围内，STL-101与STL-102双规约的联合约束不会在合法操作上触发L2干预，同时不会在任何违规轨迹上放行。布里丹之驴定理（Theorem BD）给出了两规约之间约束冲突的精确形式化分析与消解条件。

三环相互依存的保证结构

验证链的整体保证，强于任何单环的独立贡献，这值得明确陈述：

V-SEM给出的 $\mathrm{SEC}=1$，保证了V-PLN中幻觉度量框架的词汇前提——如果词汇表不完备，幻觉检测本身就是不完备的（因为存在不在词汇表内的错误）。V-PLN给出的 $Q(f) \geq 0.944$，保证了V-SAF中STL规约的输入质量——如果Brain层的计划质量太低，Spine层的CBF仲裁将被迫过于频繁地干预，使得任务难以完成。V-SAF给出的零误触保证，保证了在V-SEM和V-PLN条件下，执行安全的最终判定不依赖任何统计近似，而是在每一时刻、每一状态上都成立的形式不变性。

三段链条合在一起，构成从”任务描述进入系统”到”物理执行完成”的完整形式化自主保证——这正是本书标题中”形式化自主”（Formal Autonomy）的精确含义。

本部分对应 LaTeX 文档的 Part IV（第11–13章）。三章的核心数学结果分别对应三篇系列论文（V-SEM: IEEE RA-L，V-PLN: IEEE RA-L，V-SAF: IEEE T-ASE），各章末尾给出论文结论与书中理论的对应关系。