🤖 AI

Can We Formally Verify Neural PDE Surrogates? SMT Compilation of Small Fourier Neural Operators

本文表明，通过将小尺度傅里叶神经算子的分段线性前向传播编译为 SMT 求解器，可对其物理属性（如正定性和质量守恒）进行形式化验证，从而揭示出一种明确的权衡：精确编码能提供可靠的保证但难以扩展，而近似编码虽能提升速度却以牺牲认证能力为代价。

原作者： Ali Baheri, David Millard, Ignacio Laguna Peralta

发布于 2026-05-12

📖 1 分钟阅读☕ 轻松阅读

原作者： Ali Baheri, David Millard, Ignacio Laguna Peralta

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

想象一下，你构建了一个超快、由人工智能驱动的天气模拟器。这个人工智能（称为傅里叶神经算子或 FNO）不再运行缓慢、繁重的物理方程，而是直接观察数据并瞬间预测接下来会发生什么。这就像拥有一个魔法八号球，能在刹那间预测流体流动的未来。

但有一个问题：我们并不完全信任它。

因为它是一个“黑盒”人工智能，它可能会意外地预测化学浓度变为负值（这在现实生活中是不可能的），或者能量凭空出现。在现实世界中，这些“幻觉”可能导致危险的错误。

这篇论文提出了一个简单的问题：我们能否从数学上证明这个人工智能模拟器不会违背物理定律？

以下是作者如何利用一些巧妙的技巧来解决这个问题的：

1. 将人工智能转化为数学的“魔术”

通常，人工智能模型因为使用复杂的非线性数学而显得杂乱无章且难以分析。然而，作者注意到，当这些特定的人工智能模拟器在固定网格（如像素化屏幕）上运行时，有一些特殊之处：

核心引擎是线性的： 人工智能中承担繁重工作的主要部分（即“谱卷积”）实际上只是一个巨大而复杂的乘法表。
其余部分很简单： 使其变得“非线性”的唯一因素是一个简单的开关，称为ReLU（其基本逻辑是：“如果数字为负，则将其变为零；否则保持不变”）。

基于此，作者意识到可以将整个人工智能模型转化为一个巨大而精确的数学谜题，供计算机求解器（称为Z3）完美理解。这就像将一张复杂的手绘地图转换为一个完美的、基于网格的电子表格，机器人可以阅读而不会感到困惑。

2. 检查人工智能的两种方法

团队尝试了两种不同的方法来验证人工智能，就像检查桥梁的安全性一样：

方法 A：“精确”检查（重型工具）
- 工作原理： 他们构建了人工智能的庞大、精确的数学表示。
- 好消息： 如果计算机说“安全”，那么对于所有可能的输入，它都100% 保证是安全的。如果它发现缺陷，它会给你一个具体的例子，说明人工智能究竟是如何失败的。
- 坏消息： 它非常缓慢且笨重。它非常适合小型模型（如小型一维模拟），但如果你试图将其用于巨大、高分辨率的模型，计算机会不堪重负并崩溃（超时）。
方法 B：“冻结”检查（快速近似）
- 工作原理： 他们通过将人工智能的一部分冻结为常数值来简化数学。
- 好消息： 它极其快速。它可以在不到一秒的时间内检查更大的模型。
- 坏消息： 它不再是对原始人工智能的保证。这就像检查一架模型飞机，以判断一架真正的喷气式飞机是否安全。它能给你一个提示，但并不是一份正式的证书。

3. 他们实际发现了什么？

团队在 10 个小型、玩具版本的这些人工智能模拟器（旨在模拟简单的一维流体流动）上进行了测试。结果如下：

“质量”测试（守恒）： 他们检查人工智能是否曾凭空创造或销毁物质。
- 结果： “精确”方法证明了所有 10 个模型在特定场景下都违反了这一规则。
- 额外收获： 人工智能求解器在 10 个模型中的 7 个上，发现了比标准测试方法（如随机猜测或梯度搜索）更糟糕（更危险）的违规情况。它在寻找“最坏情况”方面表现更佳。
“正性”测试（无负数）： 他们检查人工智能是否曾预测物质的数量为负。
- 结果： 对于最简单、线性的模型（没有“开关”），求解器成功证明了人工智能永远不会产生负数。这是首次对神经偏微分方程算子进行此类形式化证明。
- 局限性： 对于稍微复杂一点的模型（带有“开关”），求解器陷入困境并超时。它无法完成证明，尽管它确实找到了一个人工智能失败的具体例子。

4. 底线

这篇论文划出了一条清晰的界限：

对于小型、简单模型： 我们现在可以从数学上证明它们是安全的（或证明它们是不安全的），具有 100% 的确定性。
对于大型、复杂模型： 我们可以非常快速地找到近似答案，但我们失去了绝对真理的保证。

核心启示：
这项研究是一个“概念验证”。它表明，我们可以将这些强大的人工智能物理模拟器转化为可以验证的数学谜题。虽然我们尚未准备好验证大规模、生产级的模型，但这为未来打开了大门，届时人工智能模拟器将附带“安全证书”，而不仅仅是一个猜测。

作者 essentially 在说：“我们在人工智能和形式化数学之间架起了一座桥梁。目前它只够小型汽车（小型模型）通过，但蓝图已经存在，未来可以建造一座供卡车（大型模型）通行的桥梁。”

技术摘要：小型傅里叶神经算子的 SMT 编译

问题陈述
傅里叶神经算子（FNOs）为偏微分方程（PDE）模拟提供了显著的加速，但往往缺乏关于物理约束（如质量守恒或浓度非负性）的形式化保证。虽然标准验证依赖于蒙特卡洛（MC）测试或基于梯度的证伪，但这些方法仅采样特定输入，无法在连续输入区域上提供详尽的保证。现有的神经网络验证工具主要面向分类器或控制策略设计，无法原生处理谱卷积、函数空间输入或 PDE 特有的属性（如守恒律）。

方法论
作者提出将训练好的 FNO 编译为可满足性模理论（SMT）求解器（具体为 Z3），以实现形式化验证。核心洞察在于：在固定网格和固定训练权重下，FNO 中的谱卷积是一个线性映射。因此，带有 ReLU 非线性的 FNO 是一个分段线性映射，可以在 Z3 的线性实数算术中精确表示，而无需近似前向传播过程。

该方法涉及两种主要的编码策略：

精确编码：通过将操作应用于标准基向量，将谱卷积编译为显式稠密矩阵（ $W^{spec}$ ）。完整的前向传播被表示为仿射映射与逐坐标 ReLU 函数的复合。这种编码是可靠的（sound），即"UNSAT"结果证明该属性对所有允许输入均成立，而"SAT"结果则提供有效的反例。然而，其复杂度按 $O(N^2H^2L)$ 增长，限制了其仅适用于小网格尺寸（ $N \le 32$ ）。
冻结编码：为了扩展到更大网格（ $N \le 64$ ），将谱路径替换为源自参考输入的常数。这将复杂度降低至 $O(NH^2L)$ 并实现亚秒级检查。然而，这是一种近似；"UNSAT"结果仅认证冻结的代理模型，而非原始 FNO，且"SAT"结果需要在原始模型上进行验证。

实验聚焦于具有周期性边界条件的 1 维平流 - 扩散 - 反应（ADR）方程。研究验证了两个属性：

质量非增加：检查输出的离散质量是否超过输入质量超过容差 $\epsilon = 0.05$ 。
非负性：检查非负输入是否在所有网格点产生非负输出。

主要贡献

精确编译：本文通过构建显式谱矩阵，首次实现了固定网格 FNO 到 Z3 线性实数算术的精确编译。
首个形式化证明：它为神经 PDE 算子提供了首个可靠的形式化证明，具体为网格尺寸高达 16 的线性（无 ReLU）FNO 生成了非负性证书。
比较分析：该工作在 10 个小模型（85–117 个参数）上比较了 Z3 与基于梯度的证伪及蒙特卡洛测试。
可靠性与可扩展性边界：作者刻画了精确验证与可扩展性之间的权衡，表明精确编码支持小型线性模型的证明及中等规模 ReLU 模型的反例，而近似编码虽能进一步扩展，但会丧失对原始模型的形式化可靠性。

结果

质量非增加：使用精确编码，Z3 为所有 10 个模型找到了可靠的质量违反反例。在 10 个模型中的 7 个上，Z3 发现的违反程度比基于梯度的证伪和 MC 测试更为严重。对于线性模型，Z3 通过全局优化发现了更深层的违反；对于 ReLU 模型，梯度搜索仍具有竞争力。
非负性：
- 线性模型（L=1）：Z3 生成了 2 个可靠的非负性证明（针对网格尺寸 $N=8$ 和 $N=16$ ），并在其他线性模型上发现了 4 个可靠反例。
- ReLU 模型（L=2）：Z3 找到了 1 个可靠反例，但由于激活模式组合爆炸（ $2^{NH}$ ），其余 3 个非负性查询超时。梯度证伪成功在所有 4 个 ReLU 模型上发现了违反，且严重程度往往高于 Z3。
冻结编码：该方法成功验证了 8 个较大模型（ $N=32$ 至 $64$）的非负性，并在其中 4 个模型上发现了质量反例。然而，这些结果是近似的；非负性证明仅适用于冻结代理模型，且质量反例需要在原始模型上重新验证（3 个确认，1 个未确认）。

意义与主张
本文将其定位为概念验证，而非生产级验证的解决方案。作者明确指出，其结果并未解决大规模 FNO 验证问题；所测试的模型是“玩具级”的，具有冻结的隐藏层和有限的参数。

其意义在于证明了：

FNO 可以被精确编译为分段线性形式，从而能够利用 SMT 求解器处理物理驱动的属性。
形式化验证对于小型线性神经算子是可行的，并为此类系统生成了首个可靠证书。
存在明确的边界：精确证明目前仅适用于小型线性模型，而精确反例可扩展至中等规模的 ReLU 模型。更大的算子将需要近似编码，或与专门的、可扩展的神经网络验证器（如 $\alpha$ - $\beta$ -CROWN）集成，而非通用 SMT 求解器。

作者总结道，这项工作鼓励形式化验证社区参与神经 PDE 代理的研究，并建议算子学习社区将可验证性视为设计标准。

1. 将人工智能转化为数学的“魔术”

2. 检查人工智能的两种方法

3. 他们实际发现了什么？

4. 底线

技术摘要：小型傅里叶神经算子的 SMT 编译

类似论文