🤖 machine learning

VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification

本文提出了 VNN-LIB 2.0，这是一个经过严格形式化的神经网络验证标准，它引入了一种“网络理论”抽象，以将规范与不断演进的 ONNX 模型解耦，同时提供由 Agda 机械化的精确语法、类型系统和语义，以确保内部一致性和互操作性。

原作者： Ann Roy, Allen Antony, Andrea Gimelli, Matthew L. Daggitt

发布于 2026-05-11

📖 1 分钟阅读☕ 轻松阅读

原作者： Ann Roy, Allen Antony, Andrea Gimelli, Matthew L. Daggitt

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

想象一下，你正试图让一群不同的机器人共同解决一个谜题。在人工智能（AI）的世界里，这些“机器人”是神经网络（AI 背后的“大脑”），而“谜题”则是验证（检查 AI 是否会做出安全或正确的决策）。

长期以来，构建这些“机器人”的人与负责检查它们的人一直说着不同的语言。他们曾使用一个名为VNN-LIB 1.0的标准，但这就像一本缺失单词、没有语法规则、且定义随查看者不同而随时变化的字典。

本文介绍了VNN-LIB 2.0，这是一个全新且严谨的“语言”，旨在解决上述问题。以下是作者如何用简单概念解释它的：

1. 问题：一个坏掉的翻译器

将VNN-LIB 1.0想象成一个试图同时说两种语言却总是搞混的翻译器。

没有语法：它没有关于如何书写问题的严格规则。因此，一个机器人可能以某种方式理解一句话，而另一个机器人则可能以不同的方式理解。
词汇有限：它只能处理简单的谜题（单一输入，单一输出）。而现实世界中的 AI 往往具有复杂的输入（例如一张图片加上一些文本）和多个输出。
浮点数困惑：计算机使用“近似”数字（如 3.14159...），但旧标准并未规定应将其视为精确数学还是粗略近似。这导致了危险的错误：机器人认为自己很安全，但实际上并非如此。
“黑盒”问题：旧标准依赖一种名为ONNX（AI 的蓝图）的文件格式。但 ONNX 对其符号的含义缺乏严格、官方的定义。这就像给机器人一张用蜡笔绘制的蓝图，而这张蓝图会不断改变对“墙”的定义。

2. 解决方案：“网络理论”（通用适配器）

本文最大的创新在于一个名为网络理论的概念。

想象你在制造一个通用电源适配器。你不想为每个国家的墙壁插座（每一种 ONNX 版本）都制造一个新的适配器。相反，你创建一个通用接口，规定：“只要插座能提供电力、电压和接地，我就能插入。”

网络理论（ $\Psi$ ）：这就是那个通用接口。它并不关心 ONNX 蓝图确切是如何绘制的。它只问：“你有定义数字、形状或连接的方法吗？”
结果：VNN-LIB 2.0 现在可以与任何版本的 ONNX 对话，甚至是未来的版本，而无需重写。它将问题（查询）与蓝图（模型）分离开来，使它们能够独立演进。

3. 新语言：VNN-LIB 2.0

有了这个新基础，作者构建了一种更智能的语言，包含三大主要升级：

更丰富的句子（语法）：你现在可以询问复杂的场景。不再仅仅是检查一个机器人，你可以问：“如果机器人 A 和机器人 B 协同工作，它们是否保持安全？”你还可以窥探机器人的“大脑”，检查其隐藏的思维（隐藏层），而不仅仅是最终答案。
严格的语法（类型系统）：这种语言现在强制要求精确。如果你试图将“温度”加到“颜色”上，语言会回答：“不行，这没有意义。”这防止了计算机因混淆不同类型的数字而产生数学错误。
清晰的含义（语义）：新语言中的每个词都有经过数学证明的定义。没有猜测。如果你写下一个查询，计算机就知道确切地要求它解决什么数学问题。

4. “现实世界”与“完美数学”选项

本文承认了一个棘手的情况：有些机器人是使用“完美数学”（实数）进行检查的，而实际运行的机器人则使用“近似数学”（浮点数）。

旧方式：这是一个隐藏的危险。检查器会说“安全”，但真实的机器人可能会崩溃。
新方式：VNN-LIB 2.0 允许你明确说明：“我知道这使用的是近似数学，但我仍希望使用完美数学来检查它。”它给查询贴上了警告标签：“请谨慎操作，这可能略有不准。” 这使得研究人员能够使用强大的工具，而无需在数学并不完美的情况下假装它是完美的。

5. “黄金标准”证明

为了确保在编写这种新语言时没有犯错，作者不仅仅是将其写下来，而是将其编程到了一个名为 Agda 的数学证明机器人中。

把 Agda 想象成一个超级严格的编辑，它会检查新语言的每一条规则，以确保没有任何逻辑漏洞。
由于该语言在 Agda 中实现了“机械化”，任何人都可以利用这一证明来验证他们自己的工具（求解器）是否正常工作。它将标准从一种“建议”转变为一种“数学上保证的契约”。

总结

简而言之，VNN-LIB 2.0是一种新的、严格的且灵活的语言，用于提出 AI 安全问题。它修复了过去破碎的语法，允许提出关于多个 AI 模型的复杂问题，并提供了一个经过数学证明的基础。因此，当某个工具声称“此 AI 是安全的”时，我们可以真正信任它所说的就是其确切含义。

技术摘要：VNN-LIB 2.0：神经网络验证的严谨基础

问题陈述

神经网络验证社区日益依赖 VNN-LIB 标准（1.0 版）以促进求解器与高层工具之间的互操作性。然而，1.0 版存在四个关键缺陷，使其无法作为严谨的形式化基础：

缺乏形式化语法：1.0 版未形式化定义查询语言语法，导致不同求解器实现之间互不兼容。
表达能力有限：该标准假设单个网络仅具有单个输入和输出。它无法原生支持多个网络、多个输入/输出或隐藏层访问，迫使人工合并模型，从而模糊了已验证工件与部署模型之间的关系。
缺乏类型系统：没有机制指定数值类型（例如浮点数与实数），当求解器将有限精度算术视为实数运算时，会造成歧义并可能导致非健全性（unsoundness）。
缺乏语义：该标准缺乏形式化语义，使得无法形式化证明求解器、查询生成器或转换的正确性，并阻碍了证明证书的开发。

VNN-LIB 面临的一个独特挑战（使其区别于 SMT-LIB 等标准）是：查询并非自包含的；它们指定了外部神经网络模型（通常为 ONNX 格式）的属性。由于 ONNX 本身缺乏形式化语义且持续演进，定义严谨的 VNN-LIB 标准需要在保持兼容性的同时，将查询语言与特定 ONNX 版本解耦。

方法论

作者通过开发 VNN-LIB 2.0 的理论基础来解决这些挑战。核心方法论创新是引入了网络理论（ $\Psi$ ）。

1. 网络理论抽象

作者将“网络理论”定义为一种抽象规范，捕捉了为定义 VNN-LIB 所需的神经网络模型格式的最小语法、类型判断和语义。

解耦： $\Psi$ 充当接口。 $\Psi$ 的具体实现（例如针对 ONNX v1.20.0）提供了元素类型、张量表示、模型结构和节点输出引用的具体定义。
模块化：VNN-LIB 2.0 是相对于抽象 $\Psi$ 定义的。这使得标准即使在 ONNX 演进时也能保持稳定；对于新的 ONNX 版本，只需更新 $\Psi$ 的实例化，而无需更新 VNN-LIB 标准本身。
形式化：整个标准（包括语法、类型和语义）均在Agda交互式定理证明器中进行了机械化，以确保内部一致性并排除歧义。

2. 形式化语法与表达能力

基于网络理论，作者定义了 VNN-LIB 2.0 的形式化语法，显著扩展了表达能力：

多网络：查询可以声明多个网络，支持如师生验证或编码器 - 解码器架构等场景。
网络等价性：该标准引入了 equal-to（引用完全相同的模型文件）和 isomorphic-to（引用具有相同图结构但权重可能不同的模型）声明。这使得求解器能够在网络副本之间共享推论（例如变量边界）。
隐藏节点：declare-hidden 构造允许对中间层输出施加约束，这对于推理编码或注意力机制至关重要。
多维输入/输出：支持任意数量的输入和输出，以适应多模态网络。

3. 类型系统与语义

类型判断：形式化类型系统强制数值健全性。它确保算术运算和比较在兼容的类型上执行（例如，防止在没有显式强制转换规则的情况下混合 float32 和 int32）。类型系统依赖于底层网络理论 $\Psi$ 提供的判断。
语义：查询的语义被定义为数学可满足性问题。给定一组模型 $M$ （从 $\Psi$ 实例化）和输入赋值 $X$ ，语义确定是否存在一个赋值使得所有断言评估为真。
实值查询：为了适应将模型视为实数（ $\mathbb{R}$ ）上函数的现有求解器，该标准引入了“实值查询”机制。通过使用特殊的 real 类型，查询作者明确授权求解器在 $\mathbb{R}$ 上解释模型，同时承认由于浮点不精确性可能导致的非健全性。这是通过从基础理论派生特定的网络理论 $\Psi_{\mathbb{R}}$ 来实现的。

主要贡献

网络理论（ $\Psi$ ）：引入了一种新颖的抽象，定义了模型格式所需的最小语义接口，使 VNN-LIB 能够独立于特定 ONNX 版本进行定义。
形式化语法与文法：为 VNN-LIB 2.0 定义了精确的上下文无关文法，支持多网络、隐藏层和复杂的输入/输出结构。
形式化类型系统：一个相对于网络理论强制数值类型健全性的类型系统，解决了数值表示中的歧义问题。
形式化语义：由网络理论参数化的查询语义的严谨数学定义，使得能够对消费或生成 VNN-LIB 的工具进行正确性形式化证明。
机械化：整个标准已在 Agda 中形式化，提供了规范参考实现和机器检查证明的基础。
实值扩展：一种通过派生网络理论支持实值分析的模块化方法，在健全性需求与当前求解器能力的现实之间取得平衡。

结果与验证

内部一致性：Agda 形式化验证了语法、类型和语义的内部一致性，确保该标准不存在 1.0 版中存在的歧义。
表达能力演示：论文展示了如何通过对网络理论 $\Psi$ 进行简单变换，得到实值查询的完整实例，展示了该抽象的灵活性。
社区采纳：该标准收到了验证社区的积极反馈。领先的求解器团队已承诺支持 VNN-LIB 2.0，新标准计划用于 VNN-COMP 2026 竞赛。
工具支持：作者发布了一个高性能 C++ 库（附带 Python 和 Julia 绑定），实现了符合新标准的解析器和类型检查器，以及 Agda 形式化代码。

意义

本文声称 VNN-LIB 2.0 为可信的神经网络验证提供了稳健且严谨的基础。其意义在于两个互补的领域：

实际互操作性：通过扩展表达能力（多网络、隐藏节点）并标准化语法，它使社区能够以统一的方式指定和验证更丰富的属性，促进更好的基准测试和工具比较。
理论严谨性：通过提供形式化语义和类型系统，它在工具与求解器之间建立了“严谨的契约”。这使得工具本身（求解器、优化器、证明检查器）的形式化验证成为可能，并解决了关于数值健全性的微妙问题（例如区分实值语义与浮点语义）。

作者强调，虽然这项工作具有理论性质，但它具有具体的后果：它确保查询的无歧义解释，提供解决技术问题的语言，并为未来形式化验证的证明证书奠定基础。