SoundnessBench

SoundnessBench是一个综合基准，用于彻底评估神经网络验证器的健全性。它通过提供大量带有隐藏反例的不可验证实例，来有效揭示神经网络验证器内部的错误，如果它们错误地声称这些不可验证实例是可验证的。该基准旨在支持开发者在评估和改进神经网络验证器方面的工作。

SoundnessBench is a comprehensive benchmark designed for thorough evaluation of the soundness of neural network verifiers. It effectively exposes inherent flaws of neural network verifiers by providing a substantial collection of unverifiable instances with hidden counterexamples, which allows these flaws to be uncovered when the verifiers incorrectly claim that these unverifiable instances are verifiable. This benchmark aims to support developers in evaluating and improving neural network verifiers.

原始信息汇总

SoundnessBench 数据集概述

概述

SoundnessBench 是一个用于全面评估神经网络（NN）验证器健全性的基准测试。该基准通过提供大量包含隐藏反例的不可验证实例，有效揭示 NN 验证器的内部错误，从而解决先前基准测试中缺乏真实标签的问题。

数据集下载

SoundnessBench 托管在 HuggingFace 上，可通过以下命令直接下载： bash git clone https://huggingface.co/datasets/SoundnessBench/SoundnessBench

数据集结构

下载的基准包含 26 个模型，涵盖 9 种不同的 NN 架构，具有不同的输入大小和扰动半径。以下是 9 种架构的详细信息：

名称	模型架构	激活函数
CNN 1 Conv	Conv 10 × 3 × 3, FC 1000, FC 100, FC 20, FC 2	ReLU
CNN 2 Conv	Conv 5 × 3 × 3, Conv 10 × 3 × 3, FC 1000, FC 100, FC 20, FC 2	ReLU
CNN 3 Conv	Conv 5 × 3 × 3, Conv 10 × 3 × 3, Conv 20 × 3 × 3, FC 1000, FC 100, FC 20, FC 2	ReLU
CNN AvgPool	Conv 10 × 3 × 3, AvgPool 3 × 3, FC 1000, FC 100, FC 20, FC 2	ReLU
MLP 4 Hidden	FC 100, FC 1000, FC 1000, FC 1000, FC 20, FC 2	ReLU
MLP 5 Hidden	FC 100, FC 1000, FC 1000, FC 1000, FC 1000, FC 20, FC 2	ReLU
CNN Tanh	Conv 10 × 3 × 3, FC 1000, FC 100, FC 20, FC 2	Tanh
CNN Sigmoid	Conv 10 × 3 × 3, FC 1000, FC 100, FC 20, FC 2	Sigmoid
VIT	修改后的 VIT [17]，补丁大小 1 × 1，2 个注意力头和嵌入大小 16	ReLU

每个文件夹应包含以下内容：

• model.onnx: 模型架构和参数的 ONNX 格式文件
• vnnlib/: 包含 VNN-LIB 格式的实例文件夹
• instances.csv: 包含 VNN-LIB 文件列表
• model.pt: 仅包含参数的 PyTorch 格式模型检查点（验证不需要）
• data.pt: 包含实例的原始数据（验证不需要）

基本用法

用户可以在基准测试上运行验证器，生成包含结果的 results.csv 文件。该 CSV 文件的格式应遵循 VNN-COMP 的格式。

评估脚本

提供了一个评估脚本，用于快速统计 results.csv 文件中的结果，并报告以下指标：

• clean_instance_verified_ratio
• clean_instance_falsified_ratio
• unverifiable_instance_verified_ratio
• unverifiable_instance_falsified_ratio

训练新模型

提供了一个简单的管道，供用户训练包含隐藏对抗样本的新模型。详细步骤包括：

1. 使用 synthetic_data_generation.py 生成合成数据。
2. 使用 adv_training.py 在合成数据集上训练模型。
3. 使用 cross_attack_evaluation.py 评估训练后的模型，确保反例真正隐藏，并生成 ONNX 模型和 VNNLIB 文件。

引用

如果发现 SoundnessBench 对您的工作有帮助，请引用以下论文：

@misc{zhou2024testingneuralnetworkverifiers, title={Testing Neural Network Verifiers: A Soundness Benchmark with Hidden Counterexamples}, author={Xingjian Zhou and Hongji Xu and Andy Xu and Zhouxing Shi and Cho-Jui Hsieh and Huan Zhang}, year={2024}, eprint={2412.03154}, archivePrefix={arXiv}, primaryClass={cs.LG}, url={https://arxiv.org/abs/2412.03154}, }

搜集汇总

数据集介绍

构建方式

SoundnessBench数据集的构建旨在填补神经网络验证器基准测试中缺乏真实标签的空白。通过提供大量包含隐藏反例的不可验证实例，该数据集能够有效揭示神经网络验证器内部的潜在错误。具体而言，数据集包含了26个模型，涵盖9种不同的神经网络架构，每种架构具有不同的输入尺寸和扰动半径。这些模型以ONNX格式存储，并附带VNN-LIB格式的实例文件，确保了数据集的标准化和可复现性。

特点

SoundnessBench数据集的主要特点在于其设计的高度针对性和复杂性。通过引入隐藏的反例，该数据集能够更精确地评估验证器的鲁棒性和准确性。此外，数据集支持多种神经网络架构，包括卷积神经网络（CNN）和多层感知机（MLP），以及不同的激活函数，如ReLU、Tanh和Sigmoid，从而提供了广泛的测试场景。

使用方法

使用SoundnessBench数据集时，用户可以通过下载数据集并运行验证器来生成结果文件。结果文件应遵循VNN-COMP的格式，每行包含一个实例的验证结果。数据集还提供了一个评估脚本，用于计算验证结果的各项指标，如可验证实例的验证率、不可验证实例的验证率等。此外，数据集支持用户训练新的模型，并提供了详细的训练和评估流程，确保用户能够生成包含隐藏反例的新模型。

背景与挑战

背景概述

SoundnessBench，由Xingjian Zhou、Hongji Xu、Andy Xu、Zhouxing Shi、Cho-Jui Hsieh和Huan Zhang等研究人员于2024年创建，是一个旨在全面评估神经网络验证器（NN Verifiers）健全性的综合基准。该数据集的核心研究问题在于解决先前基准中缺乏真实标签的问题，通过提供包含隐藏反例的不可验证实例，有效揭示NN验证器内部的潜在错误。SoundnessBench不仅填补了这一领域的空白，还为开发者提供了评估和改进NN验证器的重要工具，对神经网络验证领域产生了深远影响。

当前挑战

SoundnessBench在构建过程中面临的主要挑战包括：1) 如何生成包含隐藏反例的不可验证实例，以确保验证器的评估准确性；2) 如何设计多样化的神经网络架构，涵盖不同的输入尺寸和扰动半径，以全面测试验证器的鲁棒性。此外，数据集的评估标准和方法也需精心设计，以确保能够准确捕捉验证器的健全性问题，如非零的`unverifiable_instance_verified_ratio`指标，这直接反映了验证器的不健全结果。

常用场景

经典使用场景

SoundnessBench 数据集的经典使用场景主要集中在神经网络验证器的评估与改进。通过提供包含隐藏反例的不可验证实例，该数据集能够有效揭示神经网络验证器内部的潜在错误，从而帮助开发者识别和修正这些错误。具体操作包括使用数据集中的模型和实例进行验证测试，生成结果文件，并通过提供的评估脚本分析验证器的性能指标，如可验证实例的验证率、不可验证实例的验证率等。

解决学术问题

SoundnessBench 数据集解决了神经网络验证器评估中缺乏真实标签的学术问题。传统基准测试中，验证器的评估往往依赖于可验证实例，而忽略了不可验证实例中的潜在错误。该数据集通过引入隐藏反例，填补了这一空白，使得研究者能够更全面地评估验证器的鲁棒性和准确性，推动了神经网络验证技术的发展。

衍生相关工作

SoundnessBench 数据集的发布催生了一系列相关研究工作。例如，基于该数据集的验证器评估方法被广泛应用于神经网络鲁棒性研究中，推动了新型验证技术的开发。同时，该数据集也为对抗样本生成和检测提供了新的思路，促进了对抗攻击防御技术的发展。此外，SoundnessBench 的成功应用还激发了其他领域对类似基准测试数据集的需求和研究。