FEARL 的关键不是“让大模型变小”，而是“让需要证明的部分足够小”。这件事要从机器人真正看到的东西说起。论文把机器人在时刻 t 的观测写成三元组：图像 I、语言指令 g，以及低维安全传感器 s。前两者是“任务语义”，后者是“物理边界”。想去拿杯子，得看图听话；但会不会撞墙、会不会越界，往往只需要看激光雷达、位姿或边界距离。于是 FEARL 把职责拆开：Controller（C）吃进高维输入 (I, g)，吐出一个被限制在 [-1, 1]dc 的上下文向量 z；Safety module（S）再把 s 和 z 拼起来，输出最终动作。这里的核心不是“谁更强”，而是“谁该被证明”。大模型继续负责理解世界，小模块负责接受审查，像是把家里最复杂的账本交给会计，把门禁密码交给保安。表1：不同环境下的模块配置与训练设置。可以看到，FEARL 并不迷信单一骨架，既能接自定义的 BERT+ViT，也能接现成的 SmolVLA，还能在室内、室外和二维玩具场景里切换训练方式。这里的 dc 是上下文嵌入维度，ds 是安全传感器维度，|A| 是动作空间大小。说白了，C 可以“很会看”，S 只要“会把关”。这个设计还有一个很重要的边界条件：上下文向量必须有界。论文用 tanh 把它压到有限区间里，因为验证工具不是算命先生，它需要在一个清清楚楚、边界明确的输入空间里工作。若上下文向量无限大，验证问题就会从“难”直接升级成“别闹”。因此，FEARL 不是简单把大模型接上小模块，而是先把接口“规矩化”，再谈安全证明。
安全不靠“手感”：形式化验证如何划定“免屏蔽”安全区？
很多机器人安全方案喜欢说“我已经训练得很安全了”，但训练出来的安全，通常更像“平时没出事”。FEARL 更偏执一点：它要的是能写进证明里的安全。论文把安全要求写成对 S 的约束，也就是在某个安全传感器区域 R 内，模块 S 的输出不能落入危险动作集合 Yunsafe(R)。这类约束非常适合写成“碰撞避免”“边界不越界”“姿态不乱跑”这样的物理规则。接下来就是验证工具出场。论文使用扩展后的 ϵ-ProVe 去扫描模块 S 的输入空间，把它分成两块：一块是已经证明安全的区域，另一块是暂时不能证明的区域。注意，这里的“不能证明”不等于“不安全”，只是验证器还没拿到足够强的证据。这个区分非常关键，因为它直接决定了运行时是否需要屏蔽器介入。论文把这套流程叫做 verification-guided shielding，中文可理解为“验证引导的屏蔽”。离线阶段先把安全区域尽量证出来；在线阶段，只有当当前状态落在未认证区域时，屏蔽器才会接管动作。这样一来，屏蔽器不再像“全天候保安”，而更像“只在危险角落上岗”的特勤队，既保安全，也少打扰策略本身的动作选择。表4：Indoor Navigation 的安全约束定义。这里列的是激光雷达条件下哪些动作在什么距离区间内会被判为危险。读起来像一份“机器人版交通法规”，只不过执法依据不是红绿灯，而是传感器数值。论文之所以能做验证，根本原因就在于这些安全规则都能落到低维、可解释的传感器上，而不是漂浮在高维图像语义里。论文还给出了几个理论结果，核心意思很朴素：认证区域越大，屏蔽器越少出手；屏蔽器越少出手，性能损失越小。 这和直觉一致，但论文把它写成了可分析的形式。也就是说，验证不仅是在证明“安全”，还在量化“安全证明到底覆盖了多少真实运行状态”。这点很实用，因为如果认证区域太小，屏蔽器就会频繁插手，机器人就会像被家长一路拎着走，动作别扭，任务也容易掉链子。表3：使用 ϵ-ProVe 的离线验证结果。可以看到，二维玩具任务的可认证体积接近满分，室内和室外任务也能证出相当可观的安全区域，只是维度一高、约束一多，验证时间就开始变长。这个现象不奇怪：验证器面对的是组合爆炸，不是“多跑几轮就能解决”的普通训练问题。
Davide Corsi, Kyungmin Kim, Roy Fox. Verifiable Foundation Models for Robot Safety. arXiv:2606.26093v1, 2026.D. Corsi et al. Verification-guided shielding for deep reinforcement learning. RLC, 2024.H. Wu et al. Marabou 2.0: A versatile formal analyzer of neural networks. CAV, 2024.
