NNV3：将神经网络验证扩展到新架构和新领域
NNV3: Expanding Neural Network Verification to New Architectures and Domains
- Vanderbilt University（范德堡大学）
- The University of Texas at Dallas（德克萨斯大学达拉斯分校）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
NNV3扩展了神经网络验证工具，引入新星集成员（ModelStar、VolumeStar、GraphStar）、概率可达性模式及公平性验证，并新增多个领域基准，使NNV成为全面、健壮的AI系统验证工具。
AI中文摘要：
我们介绍NNV3，这是神经网络验证（NNV）工具的最新版本，一个用于深度学习模型和学习型信息物理系统形式验证的MATLAB框架。基于NNV 1.0（前馈神经网络、卷积神经网络、神经网络控制系统）和NNV 2.0（循环神经网络、状态空间神经网络、神经常微分方程）的基于集合的可达性基础，NNV3引入了星集家族的新成员：ModelStar用于验证权重扰动下的网络，VolumeStar用于视频和3D体积输入，GraphStar用于图神经网络。一种基于共形推断的概率可达性模式补充了确定性验证难以处理的问题的健全性分析，而FairNNV在连续输入区域上认证反事实和个体公平性属性。NNV3引入了用于恶意软件检测、基于图的电力系统模型、医学成像、变长时间序列数据和动作识别的新基准。NNV3还通过统一的文档站点整合了教程和开发者指南。本文详细介绍了这些重大更新，展示了NNV成熟为一个全面、健壮且易于访问的验证工具，适用于各种AI系统。
英文摘要：
We present NNV3, the latest version of the Neural Network Verification (NNV) tool, a MATLAB framework for formal verification of deep learning models and learning-enabled cyber-physical systems. Building on the set-based reachability foundation of NNV 1.0 (FFNNs, CNNs, NNCS) and NNV 2.0 (RNNs, SSNNs, neural ODEs), NNV3 introduces new members of the Star-set family: ModelStar for verifying networks under weight perturbation, VolumeStar for video and 3D volumetric inputs, and GraphStar for graph neural networks. A conformal-inference-based probabilistic reachability mode complements sound analysis for problems where deterministic verification is intractable, while FairNNV certifies counterfactual and individual fairness properties over continuous input regions. NNV3 introduces new benchmarks for malware detection, graph-based power-system models, medical imaging, variable-length time series data, and action recognition. NNV3 also incorporates tutorials and developer guides through a unified documentation site. This paper details these major updates, demonstrating NNV's maturation into a comprehensive, robust, and accessible verification tool for a diverse range of AI systems.
