⚡ electrical engineering

Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial

本教程介绍了一个统一框架，该框架将控制理论与最先进的神经网络验证器 $\alpha,\!\beta$ -CROWN 相结合，从而实现对安全关键系统中基于学习的控制器进行可扩展的、形式化的安全性与稳定性属性验证。

原作者： Haoyu Li, Xiangru Zhong, Hao Cheng, Bin Hu, Huan Zhang

发布于 2026-05-27

📖 1 分钟阅读☕ 轻松阅读

原作者： Haoyu Li, Xiangru Zhong, Hao Cheng, Bin Hu, Huan Zhang

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在建造一辆自动驾驶汽车或一个通过观看视频和练习来学习行走的机器人，而不是通过严格的规则进行编程。这是一种“基于学习”的控制器。它极其智能且灵活，但有一个可怕的缺陷：我们无法确定它是否永远不会犯下致命错误。 我们可以测试它一百万次，但如果它在十亿分之一秒内失败一次，后果可能是灾难性的。

本文介绍了一种名为α,β-CROWN的“安全检查员”，用于这些人工智能大脑。不要把它想象成测试驾驶员，而应将其视为一种数学保证，它宣称：“我已经检查了该机器人可能采取的每一条路径，并保证它永远不会发生碰撞。”

以下是本文如何用简单的类比来解释这项技术：

1. 问题：“黑盒”与“无限迷宫”

基于学习的控制器就像黑盒。你输入一种情况（例如，“有行人正在过马路”），一个复杂的神经网络（数字大脑）就会输出一个动作（例如，“刹车”）。

挑战： 要证明这个大脑是安全的，你必须检查它可能面临的所有情况。由于世界是连续的且大脑是复杂的，实际上存在无限种情况。传统的数学工具要么太慢而无法检查所有情况，要么仅适用于非常简单、僵化的系统。

2. 解决方案：“智能手电筒”（α,β-CROWN）

作者将α,β-CROWN呈现为一种强大的工具，它就像黑暗、无限迷宫中的一束智能手电筒。

工作原理： 它不是试图走完迷宫中的每一条路径（这需要永远的时间），而是手电筒发出一束光，一次覆盖迷宫的整个部分。
“边界”技巧： 它不需要知道机器人确切会走哪条路径。相反，它计算出一个安全框（边界），保证该框包含机器人在该部分可能采取的所有路径。
- 如果“安全框”完全位于“安全区”内，则机器人在该部分是安全的。
- 如果“安全框”接触到“危险区”，手电筒会变得更聪明。它将那一部分分成两个更小的部分，并再次向它们照射光线。
速度： 该工具通过GPU（与视频游戏使用的相同芯片）进行了超级加速。它可以同时检查数千个这样的“部分”，使其速度快到足以处理复杂的现实世界机器人。

3. 检查员的三项主要工作

本文表明，该工具可以为控制工程师执行三项具体工作：

工作 A：“可达性”地图（我们可以去哪里？）
想象你在盒子里扔一个球。下一秒它能滚到哪里？该工具会围绕球可能最终到达的所有位置绘制一个紧密、安全的轮廓。这有助于工程师了解机器人是否会意外闯入墙壁。
工作 B：“稳定性”检查（它会倒下吗？）
想象一个球在碗里滚动。如果你推它，它会摇晃，但最终会停在底部。这就是“稳定性”。该工具从数学上证明，无论你怎么推机器人（在合理范围内），它总会重新稳定下来，永远不会失控旋转。这是通过检查“李雅普诺夫函数”来实现的，这就像一个数字能量表，其数值必须始终下降。
工作 C：“优化器”（什么是最佳动作？）
有时你希望机器人找到最佳路径，而不仅仅是安全的路径。该工具就像一个超级智能的 GPS，它不仅猜测最佳路线；它从数学上证明它所找到的路线是绝对最佳的，不会遗漏任何隐藏的捷径。

4. 构建方式：“乐高”方法

本文解释说，该工具将机器人的大脑（神经网络）和世界的物理特性视为一个巨大的计算图。

将机器人的决策过程想象成一串乐高积木。有些积木是简单的数学运算（加法），有些是“开关”（如果灯是红色的，就停止），有些是复杂的曲线（正弦波）。
α,β-CROWN 知道如何为每一个单独的乐高积木套上“安全包装”。然后，它将这些包装连接在一起，以查看整个链条的安全性。如果某个积木太复杂而无法完美包装，它会将该积木分解成更小的部分，然后包装这些部分。

5. 教导机器人变得“可验证”

最后，本文讨论了如何训练这些机器人，使其更易于检查。

旧方法（CEGIS）： 你训练机器人，检查它是否安全，发现错误，然后告诉它再试一次。这就像学生猜测答案直到答对为止。
新方法（认证训练）： 该工具在训练期间给机器人一个“提示”。它告诉机器人：“如果你这样调整大脑权重，安全包装就会变得更紧。”机器人学会塑造自己的大脑，以便安全检查员可以轻松证明它是安全的。本文声称，这使得最终机器人的验证速度比旧方法快5 倍。

总结

简而言之，本文介绍了一种用于 AI 控制机器的通用安全检查员。它使用一种巧妙的方法，在复杂的数学问题周围绘制“安全框”，并将它们分割，直到小到足以证明。通过使用强大的计算机芯片（GPU），它可以以足够快的速度完成这项工作，使其适用于自动驾驶汽车和电网等现实世界应用，确保这些智能机器不仅在经验上是好的，而且在数学上是安全的。

技术摘要：利用神经网络验证器 $\alpha,\beta$ -CROWN 架起控制与验证的桥梁

问题陈述

基于学习的神经网络（NN）控制器在自动驾驶、机器人和电力系统等安全关键领域已展现出高表达性和强大的实证性能。然而，仅凭实证性能不足以支持在这些场景中的部署。对闭环属性（包括稳定性（如李雅普诺夫稳定性）、安全性（如屏障函数）和可达性）进行形式化验证存在迫切需求。

现有的验证方法面临显著局限：

可扩展性：传统方法（如 SMT 求解器（例如 dReal、Z3）、混合整数线性规划（MILP）和凸优化（SDP、SOS））往往扩展性较差，特别是对于高维系统或深度网络，这归因于其利用 GPU 加速和并行计算的能力有限。
结构僵化：许多方法依赖于特定的结构假设，例如具有 ReLU 激活函数的浅层分段线性网络或多项式系统，这使得它们难以在不同的控制设置或证书类别之间迁移。
证书特异性：近期面向控制的验证方法往往利用特定于证书的结构性特征（例如符号边界传播），这限制了它们对不同类别证书的直接适用性。

方法论

本文介绍了一个统一框架，将控制理论与最先进的神经网络验证器 $\alpha,\beta$ -CROWN 相结合。核心方法论在于将控制问题视为计算图上的验证或优化任务。

1. $\alpha,\beta$ -CROWN 验证器

$\alpha,\beta$ -CROWN 是一个用于表示为计算图的非线性函数的通用边界引擎。其运行涉及：

计算图：该框架将系统动力学 $f$ 、控制器 $\pi$ 和证书（例如李雅普诺夫函数 $V$ ）建模为由基本操作（仿射映射、非线性函数如 ReLU、sin、乘法等）组成的有向无环图（DAG）。
自动线性松弛（auto LiRPA）：验证器将可靠的线性过近似（边界）沿计算图向后传播。对于任意输入域 $B$ ，它计算一个仿射下界 $F(x) \geq a^\top x + b$ 。该过程完全可微且高度向量化，允许在 GPU 上高效执行。
分支定界（BaB）：为了处理线性边界无法得出结论的情况，该框架采用输入域分支定界法。它递归地将输入域划分为子域。随着域缩小，局部线性松弛收紧，过近似误差减小。
雅可比矩阵处理：对于需要梯度边界（例如 $\nabla V \cdot f$ ）的连续时间系统，该框架扩展计算图，通过链式法则显式编码梯度计算，将雅可比矩阵计算视为另一个算子。

2. 控制问题的重构

本教程展示了如何将经典控制理论问题重构为 $\alpha,\beta$ -CROWN 友好的、基于盒域（box domains）的可满足性或优化问题：

可达性分析：通过界定闭环映射 $g(x)$ 在输入盒上的输出，计算可达集的安全过近似。
稳定性验证（李雅普诺夫）：将李雅普诺夫函数沿轨迹递减的要求转化为可满足性问题。对于离散时间系统，这涉及在次水平集上验证条件（如 $V(g(x)) - (1-\kappa)V(x) \leq 0$ ），并将其重构为周围盒上的逻辑蕴含。针对连续时间系统也提供了类似的重构，包括处理盒边界上的前向不变性。
安全性验证（屏障函数）：通过检查屏障函数导数上的条件，验证安全集的前向不变性。对于控制仿射系统，控制输入上的上确界被转换为多面体顶点上的最大值。
收缩分析：将基于矩阵的收缩条件重构为涉及黎曼度量的标量可满足性问题。
优化（MPC）：利用验证器作为模型预测控制（MPC）的全局优化器，在非线性动力学和约束条件下最小化成本函数，并由认证的 lower bound 引导。

3. 训练与综合

本文讨论了控制器与证书协同综合的框架：

反例引导的归纳综合（CEGIS）：一种迭代方法，利用验证过程中发现的反例作为训练数据。
认证训练：一种范式，将 $\alpha,\beta$ -CROWN 生成的可微下界直接纳入训练损失函数。这使得基于梯度的优化能够最大化规范的可认证下界，从而产生本质上“易于验证”的模型。

主要贡献

统一框架：本文提出了一种统一方法，将 $\alpha,\beta$ -CROWN 应用于多种控制任务，包括可达性、稳定性、安全性和优化。
通过 GPU 并行化实现可扩展性：通过在 GPU 上利用边界传播和分支定界的高效并行特性，该框架实现了优于传统基于 SMT 或 MILP 方法的扩展性，特别是对于高维和复杂非线性系统。
通用适用性：与局限于特定网络架构或证书类型的方法不同， $\alpha,\beta$ -CROWN 能够处理表示为计算图的通用非线性函数，支持广泛的算子（三角函数、分段线性函数等）。
可微性：线性边界传播完全可微，使得验证约束能够直接集成到训练循环中（认证训练）。
实际实现：本教程提供了详细的编程接口（API）和代码示例，演示如何定义计算图、使用领域特定语言（DSL）构建约束，以及执行验证、边界计算和优化任务。它还提供了与 dReal API 兼容的即插即用层。

结果与主张

本文声称，所提出的流程在传统方法具有挑战性的验证和优化问题上展现了卓越的可扩展性。

效率：在 GPU 上同时处理数万个子域的能力，使得能够快速修剪大区域，并在微小域上通过粗略边界进行认证。
多功能性：该框架通过将各种控制规范（包括李雅普诺夫稳定性、屏障函数安全性和收缩度量）重构为盒域上的可满足性问题，成功处理了这些规范。
训练优势：本文指出，在二维四旋翼飞行器环境中，使用认证训练方法训练的模型比使用 CEGIS 训练的模型验证速度快 5 倍，这表明训练目标直接提高了可验证性。

意义

这项工作的意义在于其试图架起控制理论与可扩展神经网络验证之间的桥梁。通过提供一个统一、高效且通用的框架，作者旨在使形式化认证成为基于学习的控制设计中更实用且不可或缺的组成部分。本教程旨在降低将严格验证技术应用于复杂、已学习的控制策略的入门门槛，超越实证测试，为安全关键系统提供形式化保证。