⚡ electrical engineering

Certified Neural Approximations of Nonlinear Dynamics

本文介绍了一种新颖、自适应且可并行化的验证方法，该方法为非线性动力系统的神经网络近似提供了形式化误差界限，从而使其能够在安全至关重要的场景中进行安全部署，并在包括神经网络压缩和基于 Koopman 算子的轨迹预测在内的多种基准测试中优于现有最先进的方法。

原作者： Frederik Baymler Mathiesen, Nikolaus Vertovec, Francesco Fabiano, Luca Laurenti, Alessandro Abate

发布于 2026-06-04

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Frederik Baymler Mathiesen, Nikolaus Vertovec, Francesco Fabiano, Luca Laurenti, Alessandro Abate

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

想象一下你拥有一个非常复杂、难以预测的机器——比如喷气发动机或天气系统。为了理解它、预测它的未来或确保它的安全，工程师通常需要一个数学模型。但这些现实世界的模型往往非常混乱且具有非线性（扭曲、弯曲、难以计算），导致计算机很难验证它们是否安全。

为了解决这个问题，科学家们经常使用一种“简化模型”，比如神经网络（一种类型的 AI），来模仿真实的机器。你可以把神经网络看作是真实喷气发动机的一个**“卡通版本”**。比起复杂的蓝图，计算机更容易读取这个卡通版本。

问题所在：
危险在于，这个卡通版本在大部分时间看起来可能没问题，但在某个微小的关键点上可能会失效。如果你用这个卡通版本来控制真实的喷气发动机，那个微小的失效可能会导致坠毁。在过去，检查这个卡通版本是否“足够接近”真实情况，需要一台超级强大且缓慢的计算机（称为 SMT 求解器），它会尝试检查每一个可能的情况。这就像是为了查看一片沙滩是否安全，而去试图逐一数清沙滩上的每一粒沙子。这太慢了，而且无法处理大型复杂系统。

解决方案：“认证神经近似”（Certified Neural Approximations）
本文介绍了一种更快的方法，用于检查 AI 卡通版本是否安全可用。以下是他们是如何实现的，使用了简单的类比：

1. “局部地图”策略（一阶模型）

他们并没有试图一次性理解整个扭曲复杂的机器，而是将机器的行为分解成许多微小、易于处理的块。

类比： 想象你正在攀登一座非常陡峭且弯曲的山。一次性预测整个路径很难。但如果你把注意力集中在脚下的方寸之间，地面看起来就是平坦的。
方法： 他们将整个“山峦”（系统的所有可能状态）划分为一个个微小的矩形方块。在每个微小的方块内部，他们假定复杂的曲线实际上是一条直线（即“一阶模型”）。这使得计算变得简单得多。然后，他们在那个直线周围增加了一个“安全缓冲带”（误差界限），以考虑到真实的地面实际上是弯曲的。

2. “智能细化”（自适应划分）

有时，一条直线并不是对非常弯曲部分的良好预测。

类比： 如果你在平坦的路上行走，一张大地图就足够了。但如果你遇到了陡峭的悬崖或扭曲的转弯，你就需要放大并针对那个特定的位置绘制一张更详细的地图。
方法： 如果计算机发现某个地方的“直线”预测与真实机器偏差过大，它会自动将该方块一分为二，并尝试使用更小、更详细的方块再次进行尝试。它只在真正需要的地方进行“放大”，从而节省了大量时间。

3. “并行团队”（并行化）

类比： 与其让一个人独自检查整座山，不如想象有一个由 8 名徒步旅行者组成的团队。每位徒步旅行者同时检查山脉的不同部分。
方法： 作者使他们的算法具备了“可并行化”的特性，这意味着它可以同时利用多个计算机处理器来检查系统的不同部分。这使得验证过程变得极其迅速。

他们取得了什么成就

通过使用这种“放大、直线、团队检查”的方法，他们实现了：

速度更快： 他们验证系统的速度比之前的最佳方法快了高达 820 倍。
规模更大： 他们可以处理比以往方法所放弃的更大型、更复杂的系统（高达 7 个维度）。
精度更高： 他们不仅仅是简单地说“安全”或“不安全”，他们还能精准地指出哪里是安全的，以及哪里可能会失效，即使整个系统并不完美。

两个新的冒险

作者还展示了该方法在两个棘手的新任务中的应用：

压缩 AI： 他们将一个巨大的、臃肿的 AI 模型（像一本巨型百科全书）缩减为一个微小的版本（像一本口袋指南），同时证明了这个微小版本的功能几乎与巨型版本完全一致。
使用 Koopman 算子预测轨迹： 他们使用该方法来检查一个能够一次性预测系统整个未来路径（例如一个小球滚下山坡的过程）的 AI，而不仅仅是预测下一步。这对于引导航天器或控制机器人非常有用。

总结：
本文提供了一种全新的、超快速的方法，用以证明 AI 对复杂机器的“卡通版”是否足够安全。他们没有使用缓慢的暴力破解法去一次性检查整个系统，而是将其分解成微小的碎片，用简单的数学检查这些碎片，并在必要时进行放大。这使我们能够在以前无法实现的安全性要求极高的场景中，信任 AI 的应用。

技术摘要：非线性动力学的认证神经近似

问题陈述

非线性动力系统是网络物理系统（Cyber-Physical Systems）的基础，但直接对其进行验证和控制非常困难。一种常见的策略是构建抽象（Abstraction）——即一个近似原始系统的简化模型。神经网络已成为这一领域的有效工具，能够隐式地划分状态空间并学习简化的动力学特性。

然而，为了使这些神经抽象在关键应用中保持安全，它们必须具备关于其与真实系统接近程度的形式化保证。具体而言，必须能够认证神经网络 $N(x)$ 在给定定义域内与真实动力学 $f(x)$ 的误差在有界范围 $\epsilon$ 内（即 $\|f(x) - N(x)\|_\infty \le \epsilon$ ）。

现有的验证方法严重依赖于 SMT（满足性模理论）求解器（例如 dReal）来处理非线性实数算术。虽然这种方法是可靠的，但这些求解器面临着严重的扩展性限制，通常无法在合理的时间内验证较大的网络或更高维度的系统。这种计算瓶颈限制了神经抽象在复杂、高维场景中的实际应用。

方法论

作者提出了一种新型的可扩展验证框架，该框架消除了对昂贵的非线性算术 SMT 求解器的依赖。相反，该方法利用了认证一阶泰勒模型（Certified First-Order Taylor Models）和可并行化的自适应划分策略。

1. 认证一阶泰勒模型

该方法并非直接验证非线性谓词 $\exists x : \|f(x) - N(x)\| > \epsilon$ ，而是利用一阶泰勒展开式在局部近似真实的动力学 $f(x)$ 。

局部线性化： 将输入定义域 $X$ 划分为超矩形。在以 $c$ 为中心的超矩形 $H_\delta(c)$ 内，动力学由一个线性函数加上一个余项来界定：
$f(x) \in (f(c) + J_f(c)(x - c)) \oplus R$
其中 $J_f(c)$ 是雅可比矩阵， $R$ 是基于拉格朗日误差界（针对光滑函数）或 CROWN（针对 ReLU 网络）得出的认证误差界。
通过线性求解器进行验证： 这种转换将验证问题转化为检查线性不等式的满足性。作者使用 Marabou 2.0（一种基于线性界限传播的神经网络验证工具）来验证这些条件。这避免了非线性算术推理的计算开销。

2. 自适应证书细化

为了解决线性近似引入的保守性问题（即误差界 $R$ 可能过大），该框架采用了自适应细化策略：

划分准则： 当满足以下条件时，会对超矩形进行拆分：
1. 泰勒余项界限过于保守（ $R_{max} - R_{min} > \epsilon$ ）。
2. 求解器发现的潜在反例不满足真实的误差条件（由于线性化导致的“伪”反例）。
目标化划分： 划分轴的选择基于输入维度对近似误差的贡献，优先考虑涉及非线性项的维度。这使得实现输出依赖型细化成为可能，即不同的输出维度可能需要不同层级的划分。
并行化： 验证过程通过一个被多个工作进程访问的共享栈（深度优先搜索）进行并行化处理。每个工作进程负责处理一个超矩形，要么对其进行认证，要么将其拆分并将其子区域重新压入栈中。

3. 训练

神经网络的训练旨在最小化平均平方误差以及采样输入的最大 $L_\infty$ 误差。损失函数包含一项针对最坏情况误差的项，以提高样本效率。

核心贡献

无 SMT 验证： 引入了一种基于认证线性化的方法，消除了先前方法中的主要计算瓶型（即非线性实数算术推理）。
自适应并行细化： 一种可扩展的策略，能够实现具有非均匀精度的自适应验证，在不牺牲可靠性的前提下显著降低了保守性。
可扩展性： 能够处理高达 7 维的系统以及比现有技术方法规模大得多的神经网络。
新颖的应用： 将神经抽象扩展到了两个此前难以处理的场景：
- 神经网络压缩： 验证压缩后的网络是否仍与较大的“教师”网络保持 $\epsilon$ 以内的接近度。
- Koopman 算子发现： 验证轨迹级预测，其中网络输出代表未来状态序列（最终层包含超过 100 个状态）。

实验结果

该方法在既有文献的基准测试（如 WaterTank、JetEngine、Van der Pol Oscillator）以及新的挑战性任务上进行了评估。

性能对比现有技术： 与基于 dReal 的方法（Abate 等人，2022）相比，所提方法展示了显著的加速。例如，在 WaterTank 基准测试中，新方法的速度快了约 820 倍。当 dReal 在大多数大型模型（如 JetEngine 的 3x[64] 架构、SteamGovernor）上因超时（1 小时限制）而失败时，该方法成功认证了所有测试模型的 100% 定义域，包括像低推力航天器（Low Thrust Spacecraft）这样的高维系统。
Koopman 算子： 该框架成功验证了一个基于 Koopman 理论的轨迹预测网络。尽管该网络在验证集上的平均平方误差很低，但验证过程识别出了特定情况下误差超过容差（ $\epsilon=0.1$ ）的反例。至关重要的是，它认证了 99.03% 的输入定义域，提供了关于模型在何处可靠的细粒度见解，而传统方法只能返回单个反例。
神经压缩： 该方法验证了一个近似 Lorenz 吸引器动力学的压缩网络（参数量从 420 万减少到 6.7 万，降幅达 98.4%）。验证过程检查了超过 350 万个超矩形，耗时约 89 小时，证明了处理大规模、非解析动力学的可行性。

重要性与主张

本文声称其主要意义在于解决了神经抽象验证的可扩展性瓶颈。通过将神经网络的验证（由线性求解器处理）与非线性动力学的验证（通过局部线性化和细化处理）解耦，作者使得验证复杂的、高维的系统成为可能，而这些系统此前是难以处理的。

作者强调，其方法提供的形式化误差界允许将神经近似作为带有有界扰动的代理模型安全地使用。这种可靠性使得在抽象模型上验证的属性（如安全性或可达性）可以严谨地迁移到具体系统中。这项工作还突显了该框架的通用性，表明其不仅可以应用于标准的动力学系统，还可以应用于通用的函数近似任务，如网络压缩和用于算子理论的深度学习架构。