◈ Perslis Research

机器人 / AI 系统 · 预印本 · 研究原型

可准入的运动：将安全视为运行时的准入控制问题，而非模型能力问题

一个会运动的系统，其安全性应当是运行时的属性，而非提议动作的模型的属性。我们将安全论证经由一个确定性的准入层来分解：在每个候选控制到达执行器之前，针对接地不变量对其进行验证——并证明闭环对任意控制器都保持在安全集内。

Perslis Research · kist × Perslis · 2026-09-24

下载形式白皮书（PDF，英文） ↓ 看它驾驶 — Perslis Motion ↗ 预印本 · 研究原型（仿真） · 已作护城河脱敏

实证配套：光真实驾驶仿真器上的运行时准入控制——同一准入框架在 CARLA 中、针对一个敌对控制器与方向盘处的前沿模型被测得。

与控制器无关的安全 运行时保障屏蔽 MetaDrive 演示
摘要

学习到的运动策略的安全论证，归根结底是不可证伪的：一个质量任意高的策略仍可能提议一个致命的控制，而任何量度到的能力都无法证明它不会这样做。我们主张“因为模型好所以安全”并不是一个安全论证，并给出一个真正的替代方案。我们将安全论证经由一个准入层来分解：任何控制器——随机的、基于规则的、本地模型、前沿模型，或一整套自主栈——都只是提议一个控制；一个确定性的地板在有界可达性视界上针对接地的安全不变量验证每个候选，并在其到达执行器之前决定准入、夹紧、拒绝或覆写。我们将该运行时形式化为状态 → 可达性 → 不变量 → 准入 → 执行 → 验证，并证明一个与控制器无关的前向不变性定理：若系统起始于安全集内，且每个状态都存在一个安全的回退，那么准入将使系统对每一个控制器都保持在安全集内，因为控制器从不出现在不变量之中。我们在开源的 MetaDrive 自动驾驶仿真器中实例化该架构。一个恰好破坏地板所治理通道的对抗性紧跟控制器，在地板关闭时追尾车流（在第 70 步以 70 km/h 撞入前车），而在地板开启时全程保持安全的跟车间隙——164 次刹车覆写，无撞车，且未更改控制器。模型能力决定完成多少有用工作；运行时决定什么可以被执行。这是该架构在单一仿真领域中的一次演示，而非一个车辆控制器，并且它与更广泛的 Perslis 计划中的生物与法律准入地板共用同一个引擎。

安全不应依赖于——也不应随之退化于——提议动作之物的智能。

1 · 引言

一个会运动的自主系统可能伤及他人。使此类系统安全的主流范式，是让驱动它们的策略变得更好：更多数据、更大模型、更多训练、更多评估。这改善了平均行为，且是必要的工作。但它不能，也无法，产生一个安全保证。策略是一个从状态到所提议控制的函数；关于它所量度的胜任度，没有任何东西能排除存在某个状态使它提议出灾难性的东西。“模型得分很高”是关于一个已经见过的情境分布的证据。而安全是关于一个尚未见过的情境的断言——包括对手或罕见故障有意构造出的那种。

本文的立场是：一个运动系统的安全论证应当被重新定位。我们不去要求提议者可信，而是在任何提议者与执行器之间插入一个确定性的准入层。提议者进行提议；准入层在一个有界的前瞻上针对接地的安全不变量验证每个提议，并将其准入、将其夹紧到最近的安全控制，或以一个指定的安全回退将其覆写。控制器从不被直接托付以对执行器的权限。于是安全保证经由准入映射分解，而非经由提议者——并且对每个提议者都成立，包括那些我们并未构建、也无法检视的提议者。

我们的贡献是：(i) 将运行时运动安全形式化为一个准入控制问题的形式模型，配以一个与控制器无关的前向不变性定理，并明确陈述其固有假设；(ii) 一种可达性感知形式的跟车距离不变量，其刹车足够早以保持间隙，以及对朴素反应式形式的一次观测到的失败；(iii) 在开源 MetaDrive 仿真器中的一次实证演示，其中一个对抗性控制器在地板关闭时撞车，而在地板开启时被可证明地保持安全，且未修改控制器；以及 (iv) 观察到这是一个跨领域模式的一个实例——同一条准入脊柱在生物地板中把关伪造的蛋白质事实、在法律地板中把关伪造的判例法，而在此处于一个运动地板中把关不安全的控制。

2 · 问题：能力不是一个安全论证

考虑一个学习到的策略 \(\pi\)，它已在一个大型测试集上被评估并表现良好。我们确立了什么？确立了 \(\pi\) 在从评估分布抽取的状态上倾向于提议好的控制。而我们真正需要用于安全的性质在种类上是不同的：对于所有可达状态，被执行的控制都使系统免于碰撞、不驶出路肩、处于限速之内、并在地理围栏之内。能力度量是对情境的聚合；安全性质是对情境的全称量化。没有任何有限的评估能弥合这道鸿沟，而对手或一次不走运的传感器故障能把系统驱向恰恰是评估从未采样到的那个状态。

这正是为什么“因为模型好所以安全”并不像安全断言所必须的那样可证伪。没有任何单独针对策略的实验，其失败能让我们断定该策略在一般意义上不安全，也没有任何实验，其成功能让我们断定它在一般意义上安全；状态空间太大，而危害正栖身于尾部。认证与保险需要一个能针对不变量与证据来兑现的断言，而非一个关于模型平均胜任度的断言。因此我们干脆不再要求提议者承载安全论证。

3 · 反转——一个准入层

这一步是把提议者与准入分离。提议者的职责是有用：取得进展、保持车道、完成路线。准入的职责则狭窄而确定：给定当前状态与一个所提议的控制，决定什么——如果有的话——被允许到达执行器。我们把运行时排布为一条流水线：

\[ \text{State} \;\rightarrow\; \text{Reachability} \;\rightarrow\; \text{Invariants} \;\rightarrow\; \text{Admission} \;\rightarrow\; \text{Actuation} \;\rightarrow\; \text{Verification} \]

提议者位于这条流水线之前，只提供一个候选。不变量编码了安全集。可达性把候选在一个有界视界上向前投影。准入即决策——准入、夹紧或覆写——它是唯一对执行器拥有权限之物。验证记录被准入了什么以及为何，因此每次覆写都是一张可检视的收据：动作在其行动之前被验证。这是运行时保障 / Simplex 一脉 [1]，以及来自安全强化学习的屏蔽一脉 [6]；我们所强调的是，安全论证完全由准入映射承载，因而对上游是哪个提议者无动于衷。

控制器只是提议。一个确定性的地板决定什么可以被执行。

4 · 形式模型

设世界状态为 \(x \in \mathcal{X}\)——位置、速度、朝向、近邻物体、边界与执行器状态——控制为 \(u \in \mathcal{U}\)，具有离散动力学 \(x_{t+1} = f(x_t, u_t)\)。安全集由不变量谓词 \(g_i(x) \le 0\) 定义——在路上、限速、跟车距离、地理围栏、间距、执行器限制：

\[ \mathcal{S} = \{\, x \in \mathcal{X} : g_i(x) \le 0 \ \ \forall i \,\}. \]

定义视界 \(H\) 上的可达集：

\[ \mathrm{Reach}_H(x, u) = \{\, x' : x'\ \text{reachable from}\ x\ \text{under}\ u\ \text{within}\ H\ \text{steps} \,\}. \]

于是准入映射 \(A : \mathcal{X} \times \mathcal{U} \to \mathcal{U}\) 为

\[ A(x,u) = \begin{cases} u & \text{(ALLOW) if } \mathrm{Reach}_H(x,u) \subseteq \mathcal{S},\\[4pt] u' & \text{(CLAMP) nearest } u' \text{ with } \mathrm{Reach}_H(x,u') \subseteq \mathcal{S},\\[4pt] u_{\mathrm{safe}}(x) & \text{(DENY / EMERGENCY) otherwise — brake, hover, halt.} \end{cases} \]

在任意控制器 \(\pi\) 下的闭环为

\[ u_t = A\big(x_t,\, \pi(x_t)\big), \qquad x_{t+1} = f(x_t, u_t). \]

注意 \(\pi\) 只进入 \(A\) 的实参之内，并且每当准入夹紧或覆写时即被丢弃。这正是定理所利用的结构性事实。

5 · 安全定理

定理 1（与控制器无关的前向不变性）。 假设 (a) \(x_0 \in \mathcal{S}\)；(b) 每个状态都存在一个安全的回退，即 \(\forall x \in \mathcal{S},\ \mathrm{Reach}_H\big(x, u_{\mathrm{safe}}(x)\big) \subseteq \mathcal{S}\)；且 (c) 准入 \(A\) 在每一步都被施用。那么对所有 \(t \ge 0\) 且对每一个控制器 \(\pi\)，都有 \(x_t \in \mathcal{S}\)。
证明梗概。 对 \(t\) 作归纳。基例：由 (a) 有 \(x_0 \in \mathcal{S}\)。归纳步：设 \(x_t \in \mathcal{S}\)。准入返回三个值之一。若它 ALLOW \(u\)，则由 ALLOW 条件有 \(\mathrm{Reach}_H(x_t,u) \subseteq \mathcal{S}\)，故尤其有 \(x_{t+1} \in \mathcal{S}\)。若它 CLAMP 到 \(u'\)，则由 CLAMP 条件有 \(\mathrm{Reach}_H(x_t,u') \subseteq \mathcal{S}\)，故 \(x_{t+1} \in \mathcal{S}\)。若二者皆不存在，准入执行 \(u_{\mathrm{safe}}(x_t)\)，并由 (b) 有 \(\mathrm{Reach}_H(x_t, u_{\mathrm{safe}}(x_t)) \subseteq \mathcal{S}\)，故 \(x_{t+1} \in \mathcal{S}\)。在每个分支中都有 \(x_{t+1} \in \mathcal{S}\)。控制器 \(\pi\) 从不出现在不变量之中；它只影响选择哪一个集内控制，而从不影响所选控制是否使系统保持在 \(\mathcal{S}\) 内。\(\square\)
推论（模型无关性）。 该安全保证对 \(\pi\) 不变。将随机 → 基于规则 → 学习到的 → 前沿相互替换，改变的是被准入行为的质量，而非在 \(\mathcal{S}\) 中的归属。模型能力决定完成多少有用工作；运行时决定什么可以被执行。

我们直白地陈述这些固有假设，因为它们恰恰是一次物理部署所必须兑现的接口。定理 1 假设：喂给不变量的状态 \(x_t\) 是精确的；执行器有足够的权限去实现 \(u_{\mathrm{safe}}\)（例如足够的刹车以在可用间隙内停下）；并且不变量 \(g_i\) 正确地编码了意图中的安全集。在这些成立之处，安全是一条定理。在它们不成立之处，该保证只与最弱的接口一样好——而那是一个关于感知、执行与规格说明的断言，而非关于提议者的断言。孤立出这一事实正是本文的要点。

6 · 使跟车距离不变量具备可达性感知

我们把一个不变量端到端地做完：在一辆前车之后保持一个安全的跟车间隙。设前车处于距离 \(d\)、本车速度 \(v\)、前车速度 \(v_\ell\)、接近速率 \(c = v - v_\ell\)。一条纯反应式规则保持间隙

\[ g_{\mathrm{safe}} = \max\big(d_{\min},\ v\,\tau\big) \]

其中 \(\tau\) 为车头时距，并按车辆已经处于 \(g_{\mathrm{safe}}\) 内多深来成比例刹车。这种形式介入得太晚：一旦紧跟者已经积累了速度，它必须挽回的间隙就超过了刹车在时限内所能买到的，于是车辆即便一边记录着覆写也依然撞车。我们观测到的正是这一点——一个反应式的间隙保持器尽管约有 120 次准入覆写却仍然撞车——这促成了一种可达性感知的形式。

可达性形式提出一个前瞻性的问题：需要多大的恒定减速度，才能在间隙落到 \(d_{\min}\) 之前停止接近？对 \(c > 0\)，

\[ a_{\mathrm{req}} = \frac{c^2}{2\,(d - d_{\min})}. \]

地板于是命令一个刹车幅度

\[ b = \min\!\left(1,\ \max\!\left(\frac{g_{\mathrm{safe}} - d}{g_{\mathrm{safe}}} + 0.3,\ \ \frac{a_{\mathrm{req}}}{a_{\max}}\right)\right), \]

这样，只要所需减速度一接近执行器的权限 \(a_{\max}\)，刹车便随之升高，而不仅仅是等到间隙已经被违反之后。这就在所假设的权限之下保证了投影出的间隙从不落到 \(d_{\min}\) 之下。

不变量会组合，而组合的顺序至关重要。限速上限与跟车刹车按序施用：限速把油门上限压到零，但并不抢占跟车刹车。一个早期版本曾让限速守卫短路整条流水线并压制刹车命令——这是我们找到并修复的一个缺陷，做法是让这些守卫相互组合而非相互竞争。这是一条一般义务的一个小实例：当若干不变量治理同一个执行器时，准入必须尊重它们全部，而非最先触发的那一个。

7 · 实证演示（图 1–2）

参考实现 drive_floor 运行在开源的 MetaDrive 自动驾驶仿真器 [9] 之上。提议者是一个 SymbolicDriver——几何式车道保持外加自适应巡航，不含任何深度网络——以及两个对手，一个 Tailgater（紧跟者）和一个 Drifter（漂移者），其中每一个都恰好破坏一个通道，使得所诱发的失败恰恰是地板所治理的那个不变量。这是一个刻意的实验选择：我们在引入任何精巧模型之前，先用一个攻击其所负责通道的对手来测试地板，这样通过就不可能是一次侥幸的错失。地板是一个 SafetyShield.verify 调用，它返回最近的安全动作外加一条被记录的覆写——在行动之前被验证。已接入的不变量是在路上、限速与跟车距离。

图 1 — 交互式。 在同一条 MetaDrive 高速公路上的头条结果。对抗性紧跟者在地板关闭时追尾车流，而在地板开启时保持一个安全间隙——两行中的控制器完全相同。

运行撞车地板覆写次数结果
紧跟者 · 地板关闭是——第 70 步，以 70 km/h 撞入前车0追尾车流
紧跟者 · 地板开启否164全程保持一个安全间隙
符号式驾驶者 · 地板开启否15行驶干净，极少需要地板

两行紧跟者的差别仅在于是否施用准入；控制器逐字节完全相同。地板在未更改控制器的情况下把一个会撞车的控制器变得安全。符号式驾驶者那一行展示了互补的一点：一个已经尊重不变量的控制器很少被触及——15 次覆写——因此地板在一个胜任的提议者身上几乎不施加代价，同时仍然待命。

图 2 — 交互式。 来自我们受控复现的纵向准入轨迹。地板关闭时间隙坍缩到零（碰撞）；地板开启时，屏蔽在间隙收窄时刹车并保持一个稳定的跟车距离。

为了在更高分辨率下检视该机制，我们构建了一个受控的纵向复现，承载同一个不变量（安全间隙、可达性感知刹车），其中 \(a_{\max}^{\text{brake}} = 9\ \mathrm{m/s^2} > a_{\max}^{\text{acc}} = 3\ \mathrm{m/s^2}\)。紧跟者全程提议全油门。地板关闭时，间隙收窄到零，车辆相撞。地板开启时，屏蔽在间隙收窄时刹车，将本车从 \(15.3\ \mathrm{m/s}\) 减到 \(6.3\ \mathrm{m/s}\) 以匹配前车，并以约 400 次准入覆写全程保持一个约 \(9.7\ \mathrm{m}\) 的间隙；接近速率稳定到约为零。无撞车。该轨迹具体地展示了定理的机制：每一步，提议者的全油门命令都被丢弃，取而代之的是一个被准入的刹车，而间隙不变量从未被违反。

8 · 可达性与模型替换不变性（图 3–4）

图 3 — 交互式。 在固定接近速率下，所需减速度 \(a_{\mathrm{req}} = c^2 / \big(2(d - d_{\min})\big)\) 作为间隙的函数。一旦 \(a_{\mathrm{req}}\) 越过一个阈值，地板即介入，保证投影出的间隙保持在 \(d_{\min}\) 或以上；一个纯反应式的间隙保持器介入得太晚，即便记录了覆写也仍然撞车。

图 3 为可达性形式提供了论据。在固定接近速率下，所需减速度随间隙收缩而急剧增长；一条等到间隙已经进入 \(g_{\mathrm{safe}}\) 之内才动作的反应式规则，是在曲线的平坦部分介入的，一旦 \(a_{\mathrm{req}}\) 已经爬升过执行器的权限就无法挽回。可达性形式在 \(a_{\mathrm{req}}\) 首次越过一个低于 \(a_{\max}\) 的阈值时介入，这恰恰是使投影出的间隙保持在 \(d_{\min}\) 或以上之物。反应式间隙保持器尽管约有 120 次覆写却仍观测到撞车，正是这条曲线的实证投影：覆写触发了，但太晚而无济于事。这是把可达性分析的纪律 [4][5] 施用于单一标量不变量。

图 4 — 交互式。 概念性：撞车率对控制器（规则 / 随机 / 对手），地板关闭对地板开启。地板关闭时，撞车率随提议者剧烈变动且对手撞车；地板开启时，它沿提议者轴平坦地为零。安全不随控制器而移动；只有工作质量在移动。

图 4 是被画成一幅图的推论。沿提议者轴——基于规则、随机、对抗——地板关闭的撞车率从可容忍摆动到必然。地板开启的撞车率是平坦的：安全性质不随控制器改变而移动，因为控制器不在不变量之中。沿那条轴确实移动的，是所完成有用工作的量，而运行时刻意不去治理它。这正是本文所主张的分离，被可视化了：一条轴用于能力，一个正交的保证用于安全。

9 · 一个引擎：汽车、无人机、机器人

第 4–5 节中没有任何东西是汽车特有的。准入映射是在一个抽象状态 \(x\)、一个抽象控制 \(u\) 与一组不变量谓词 \(g_i\) 之上定义的；定理只用到存在一个安全回退，以及准入在每一步都被施用。要把该引擎移到无人机，只需替换状态（加入高度与姿态）、不变量（间距、地理围栏、最小高度、回航电量）与回退（\(u_{\mathrm{safe}}\) 变为悬停并保持）。要把它移到机械臂，不变量变为关节限制、工作空间边界与人机间距，回退变为停止。提议者可自由更换；准入脊柱是同一种代码形状。

这也为任何新领域固定了实验方法：对抗通道规划者。在引入任何精巧模型之前，用一个恰好破坏地板所治理通道的对手来测试地板。若地板能顶住一个专门为违反其所保护不变量而构建的提议者，那么通过就是一个真实的结果而非一次侥幸的擒获——只有到那时，才值得去衡量一个有能力的提议者在其之上把有用工作做得多好。

10 · 面向模型中介系统的准入控制

运动地板是一个贯穿整个 Perslis 计划的模式的一个实例：一个学习到的或以其他方式不受信任的组件，唯有通过一个它无法作弊的确定性验证器才能赢得权限。该验证器在每个领域都提出同一种形状的问题——此物可否进入受信任状态？——并针对接地不变量、而绝不针对提议者的自信来作答。

同样的反转贯穿了该计划的推理放置工作：一个学习到的组件被授予的权限，只与某个验证器的准入成比例，而非与该组件自身的能力成比例。在每种情形下，安全或完整性论证都经由准入映射、而非提议者来分解——正是这一点，让同一个论证能够在提议者升级时被复用。在这个框架中，准入控制就是模型中介系统的信任层，而运动是执行器把利害关系变得物理化的那一种情形。

11 · 局限与范围

这是对一种架构——运行时保障屏蔽——在单一仿真领域中的演示：MetaDrive 纵向控制外加我们受控的纵向复现。它不是一个车辆控制器，也不用于任何真实汽车。跟车距离不变量被端到端地展示；在路上与限速守卫已接入，但驶出道路的演示需要我们尚未构建的单车道几何（未来工作）。

贯穿全文的接地都是仿真器的真值状态。一次真实部署没有这份奢侈：不变量必须由经过验证的感知来喂给，而这在此处超出范围，也正是那些困难的物理问题所栖居之处——传感器不确定性、时延、执行器故障、时序、冗余与认证。定理 1 的假设（精确状态、足够的回退权限、正确的不变量）恰恰是这样一次部署所必须兑现的接口；我们并不声称已经兑现了它们，也不声称地板是一个更好的驾驶者。地板根本不是一个驾驶者。它是一个包裹在任何驾驶者外面的保证，强制执行它被给定的那个安全集。若安全集是错的，地板就会忠实地强制执行那个错误的东西。本文的贡献在于孤立出软件控制的那个问题——一个运行时能否不论提议者为何都使系统保持在给定的安全集内？——并独立于模型地回答它，从而使剩下的问题被诚实地命名，并被留在它们所归属之处。

12 · 结论

我们主张一个运动系统的安全应当是运行时的属性，而非提议动作的模型的属性，并将其落到实处。通过在任何提议者与执行器之间插入一个确定性的准入层，并把每个候选控制针对接地不变量向前投影，闭环对每个控制器都可证明地保持在安全集内——提议者从不出现在不变量之中。在 MetaDrive 仿真器中，一个在地板关闭时撞车的对抗性控制器，在地板开启时被保持安全，且对控制器没有任何更改。模型能力决定完成多少有用工作；运行时决定什么被允许发生。这一分离，正是那使得一个生物地板能拒绝伪造事实、一个法律地板能拒绝伪造引证的同一个分离——准入控制作为模型中介系统的信任层，如今在门的另一侧带着一个执行器。

地板并不造就一个更好的驾驶者。它造就一个环绕任何驾驶者都成立的保证。

参考文献

  1. L. Sha. "Using Simplicity to Control Complexity." IEEE Software, 18(4):20–28, 2001.
  2. A. D. Ames, X. Xu, J. W. Grizzle, and P. Tabuada. "Control Barrier Function Based Quadratic Programs for Safety Critical Systems." IEEE Transactions on Automatic Control, 62(8):3861–3876, 2017.
  3. A. D. Ames, S. Coogan, M. Egerstedt, G. Notomista, K. Sreenath, and P. Tabuada. "Control Barrier Functions: Theory and Applications." European Control Conference (ECC), 2019.
  4. I. M. Mitchell, A. M. Bayen, and C. J. Tomlin. "A Time-Dependent Hamilton–Jacobi Formulation of Reachable Sets for Continuous Dynamic Games." IEEE Transactions on Automatic Control, 50(7):947–957, 2005.
  5. M. Althoff. "An Introduction to CORA 2015." Proc. Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH), 2015.
  6. M. Alshiekh, R. Bloem, R. Ehlers, B. Könighofer, S. Niekum, and U. Topcu. "Safe Reinforcement Learning via Shielding." AAAI Conference on Artificial Intelligence, 2018.
  7. S. Shalev-Shwartz, S. Shammah, and A. Shashua. "On a Formal Model of Safe and Scalable Self-Driving Cars." arXiv:1708.06374, 2017.
  8. E. Bartocci and Y. Falcone (eds.). Lectures on Runtime Verification: Introductory and Advanced Topics. Springer LNCS 10457, 2018.
  9. Q. Li, Z. Peng, L. Feng, Q. Zhang, Z. Xue, and B. Zhou. "MetaDrive: Composing Diverse Driving Scenarios for Generalizable Reinforcement Learning." IEEE Transactions on Pattern Analysis and Machine Intelligence, 2022.

如何引用

@techreport{perslis2026motion,
  title       = {Admissible Motion: Runtime Safety as an Admission-Control
                 Problem, Not a Model-Capability Problem},
  author      = {{Perslis Research}},
  institution = {Perslis Research},
  year        = {2026},
  month       = {9},
  note        = {Preprint, research prototype (simulation). Moat-scrubbed.},
  url         = {https://research.perslis.com/motion.html}
}