技术摘要：软件层面的浮点神经网络验证

问题陈述

虽然神经网络验证在为理想化的实值模型提供形式化保证方面取得了显著进展，但这些方法往往无法考虑到已部署系统的具体实现细节。在安全关键型应用（如 CPS、IoT）中，神经网络使用有限精度的浮点算术（通常为 32 位 IEEE 754）实现，并依赖于标准数学库（如 math.h）。这些底层细节引入了舍入误差和非结合性行为，可能会使基于无限精度模型的安全性证明失效。例如，本文展示了 SoftSign 激活函数在实数算术中是单调不减的，但在 32 位浮点数实现中却不再具备这一特性。

现有的尝试在软件层面验证神经网络代码的方法收效甚微。软件验证器往往难以扩展到大规模神经网络实例，迫使从业者回归到不完备的无限精度模型，或者放弃验证转而采用测试。此外，已有工具被观察到在某些设置下会产生错误结果，这使得人们对其作为浮点数实现的安全预言机（safety oracles）的可靠性产生怀疑。目前缺乏针对自动化软件验证器在神经网络代码上的严谨、标准化的评估。

方法论

为了解决这些差距，作者对八种最先进的自动化软件验证器在神经网络代码上的表现进行了严格评估。该方法论包含三个主要组成部分：

1. 基准测试构建 (NeuroCodeBench 2.0)： 作者构建了一个包含 912 个验证实例的综合基准测试。该基准涵盖：

   • 数学函数： 58 个实例，用于测试标准 math.h 函数的属性（例如单调性、周期性、线性边界）。
   • 激活函数： 57 个实例，用于测试常见激活函数（如 ReLU、TanH、SoftSign、GELU）的属性。
   • 神经网络层： 86 个实例，涵盖仿射变换、归一化、池化以及 SoftMax 层。
   • 全神经网络： 711 个实例，包括 Hopfield 网络、SAT 编码的 ReLU 网络、多项式近似网络、Lipschitz 有界网络，以及源自 VNN-COMP（概率密度和强化学习任务）的网络。
   • 地面真值 (Ground Truth)： 每个实例都通过暴力测试、穷举构造或反例生成等技术预先标记为“安全”或“不安全”，从而确保拥有用于评估的已知正确判定。

2. 标准化与兼容性： 为了确保公平比较和可重复性，作者将所有基准实例转换为国际软件验证竞赛 (SV-COMP) 使用的格式。这包括创建包含模型实现、安全性属性及必要依赖项的自包含 C 文件。工作流利用 BenchExec 框架来管理资源限制和执行，确保工具以与 2024 年 SV-COMP 版本相同的配置运行。

3. 实验评估： 本研究在两种条件下评估了八种工具（2LS、CBMC、CPAChecker、DIVINE、ESBMC、PeSCo、Pinaka、UAutomizer）：

   • 基线 (Baseline)： 在原始基准实例上运行验证器。
   • 操作模型 (Operational Models)： 提供 math.h 库的显式 C 实现（使用 MUSL 和 CORE-MATH），以观察提供函数定义是否能改善验证结果。
   • 历史分析： 作者还分析了 ESBMC 从 2018 年到 2026 年的历史性能，以观察该领域的趋势。

核心贡献

• NeuroCodeBench 2.0： 创建了一个专门用于浮点神经网络软件级验证的大规模、具有地面真值的基准测试。它包含 912 个实例，范围从简单的函数到拥有高达 17 万个参数的全神经网络。
• SV-COMP 集成： 该基准测试已格式化为与 SV-COMP 基础设施兼容，使其成为 2026 年官方基准集的一部分。这使得可以使用标准工具配置进行自动化、可重复的评估。
• 严格评估： 首次系统性地比较了八种最先进的软件验证器在神经网络代码上的表现，揭示了性能和正确性的显著差异。
• 操作模型分析： 研究了提供显式数学库实现（MUSL、CORE-MATH）是否能提高验证器性能，发现其影响取决于具体工具，且通常微乎其微或具有负面影响。

结果

评估结果揭示了当前神经网络软件验证领域的几个关键发现：

• 低正确性和低扩展性： 结果被描述为“相当令人失望”。工具在基准测试中表现出巨大的差异，表现最好的工具 (CBMC) 正确解决了 912 个实例中的 371 个，而其他工具解决的数量显著更少。不同类别的平均求解率各异，一些复杂的类别（如强化学习）求解率低至 3%。大多数工具无法同时验证超过单个神经网络层。
• 错误的判定： 几种工具产生了高比例的错误结果。例如，CBMC 产生了近 25% 的错误确定性判定（主要是假阳性），Pinaka 和 UAutomizer 也显示出显著的错误率。在解决大量实例的工具中，只有 ESBMC 没有产生错误判定。
• 操作模型的影响： 提供 math.h 的显式实现（MUSL 或 CORE-MATH）并未带来可见的整体提升。对于某些工具（CBMC、ESBMC、Pinaka），由于增加了验证库代码的复杂度，性能反而下降了。对于其他工具（CPAChecker、PeSCo），解决的实例数量增加了，但这通常伴随着错误判定的激增。
• 扩展性限制： 工具在处理全神经网络时面临巨大困难。对于复杂的类别（如强化学习和概率密度），求解率降至个位数。即使是合成网络，像 ESBMC 这样的工具在超时前也只能解决宽度极小（如宽度为 4）的实例。
• 历史进展： 对 ESBMC 从 2018 年到 2026 年的分析显示，其进步是非单调但总体呈常态化提升的。2022-2023 年间出现的错误判定激增被追溯到 k-归纳算法的一个实现错误，该错误在发布早期 NeuroCodeBench 1.0 后已得到修复。2024 年 NeuroCodeBench 1.0 的引入导致社区内错误判定大幅减少，尽管 NeuroCodeBench 2.0（2025 年底）的影响较为温和。

意义与主张

本文主张，虽然在概念上验证神经网络的软件层面是可行的，但现有的最先进软件验证器尚未准备好有效地处理这项任务。 研究强调，目前的工具无法可靠地检查超过单个层的代码，经常返回错误结果，并且缺乏对标准数学库的完整支持。

作者认为，他们的工作为验证界提供了一次必要的“现实检查”。通过提供一个具有已知地面真值的严谨基准测试，他们证明了理想化验证与软件实现之间的差距目前对于现有工具来说仍然过大，难以逾越。论文指出，NeuroCodeBench 的发布已经刺激了进展，这可以通过其初始发布后错误判定减少的现象得到证实。然而，作者总结道，针对最坏情况下的数值偏差来认证神经网络的完整实现，仍然是一个长期挑战，需要对数学库的原生支持以及针对浮点算术定制的决策程序。