NNV：深度学习系统的形式化验证工具箱

本文介绍Vanderbilt大学VeriVITAL团队开源的MATLAB神经网络验证工具NNV，支持前馈网络、CNN、RNN、GNN等多种架构的形式化验证与可达性分析，提供统一验证框架及多种集合表示方法，最新3.0版本新增公平性验证、概率验证等模块，助力AI系统安全性保障。

原作者/维护者: VeriVITAL研究组（Vanderbilt大学） 来源平台: GitHub 原始链接: https://github.com/verivital/nnv 官方文档: https://www.verivital.com 发布时间: 持续更新

NNV（Neural Network Verification）是用于深度神经网络和学习型网络物理系统的形式化验证开源MATLAB工具箱，实现基于集合的可达性分析方法，支持Star sets等多种集合表示，可验证前馈、卷积、循环、图神经网络及神经ODE、神经网络控制系统。

支持的架构类型

• 前馈神经网络（FFNN）：标准全连接层验证
• 卷积神经网络（CNN）：ImageStar优化高维图像输入处理
• 循环神经网络（RNN/LSTM）：时序数据验证
• 图神经网络（GNN）：GraphStar支持图结构数据
• 分割网络：语义分割任务验证
• 神经ODE：连续时间神经网络验证

可达性分析方法

• Star sets：通用凸多面体表示，支持仿射变换和交集运算
• ImageStars：图像数据优化的星形集合表示
• VolumeStars：考虑体积信息的扩展表示
• GraphStars：针对GNN的集合表示

用户可根据场景选择合适的集合表示以平衡效率与精度。

最新NNV3.0版本（ATVA2026工具论文）新增功能：

• FairNNV：公平性验证模块，检测决策偏见（如敏感属性相关场景）
• ProbVer：概率验证框架，支持带随机性的神经网络（如贝叶斯网络、dropout组件）
• GNNV：图神经网络验证模块，扩展非欧几里得数据处理能力
• VideoStar：视频数据验证支持，ImageStar扩展到时间维度
• ModelStar：模型级别验证抽象，支持复杂系统级任务

这些特性扩展了NNV的应用范围与能力。

Docker部署（推荐）

提供两种许可证模式：

• 在线许可证模式：适合个人用户，浏览器登录激活
• 网络许可证模式：适合机构用户，无人值守批量运行

Docker镜像预装MATLAB R2025b和AIVL，支持GPU加速（通过--gpus all参数）。

可重复性实验

包含6个实验（FairNNV、ProbVer、GNNV、VideoStar、ModelStar、ToolComparison），分smoke测试（约30分钟）和完整运行（5-7小时）模式，可生成论文关键表格。

神经网络形式化验证能提供数学上的安全性保证，对自动驾驶、航空航天等安全关键领域至关重要。NNV作为代表性开源工具，被多篇学术论文引用，社区活跃。

NNV3.0与MathWorks AI Verification Library（AIVL）做了全面对比，涵盖验证时间、内存占用、精度等维度，通过Docker镜像自动安装AIVL依赖，用户可在相同环境下比较性能。即使无AIVL，NNV功能仍完整运行。

对于使用NNV的用户，建议：

1. 优先Docker环境：避免MATLAB安装与依赖配置复杂
2. 运行smoke测试：快速验证环境正确性
3. 阅读示例代码：项目提供丰富示例，覆盖不同架构与场景
4. 理解集合表示：选择合适表示影响验证效率
5. 关注社区更新：领域快速发展，新方法持续集成

NNV是神经网络验证领域的前沿工具，开源特性与活跃维护使其成为学术与工业界重要资源。