开发者发布神经网络形式化验证资源汇总清单

一个精选的神经网络安全形式化验证工具、基准、论文和资源列表。

神经网络形式化验证是一组技术，用于在给定范围内所有可能的输入下，数学上证明神经网络满足特定性质，如安全性、鲁棒性或公平性。这对于在自动驾驶、航空航天、机器人和医学等安全关键领域部署深度学习模型至关重要，因为这些领域中经验测试不足以保证正确性。

精确完备求解器 抽象解释与可达性分析 分支定界与加速验证器 闭环与信息物理系统 基准与竞赛 文献 综述 奠基性论文 社区 精确完备求解器 Marabou - 一个基于SMT的深度神经网络验证框架，支持通过VNN-LIB格式指定的性质。 MIPVerify.jl - 一个基于Julia的验证工具，将神经网络鲁棒性认证问题形式化为混合整数线性规划（MILP）优化问题。 Reluplex - 一个奠基性的基于SMT的求解器算法，通过扩展单纯形法来验证带有ReLU激活函数的神经网络（Marabou的前身）。 Venus - 一个可靠且完备的基于MILP的验证工具包，利用符号区间传播和输入域分割。 抽象解释与可达性分析 auto_LiRPA - 一个用于在通用计算图上自动进行基于线性松弛的扰动分析（LiRPA）的库，作为核心的边界传播后端。 ERAN - ETH神经网络鲁棒性分析器，利用带有自定义抽象域（如DeepPoly和RefineZ）的抽象解释来认证神经网络的安全性。 Neurify - 一个符号区间分析验证器，带有定向约束精化，用于高效地获得紧致边界。 NNV - 一个MATLAB工具箱，对前馈、卷积和循环架构执行基于集合的可达性分析（使用Star集、ImageStar和zonotope）。 pyNeVer - 一个用于神经网络设计、训练和形式化验证的库，使用基于星集的可达性分析算法。 分支定界与加速验证器 alpha-beta-CROWN - 一个GPU加速的神经网络验证器，将高效的线性边界传播与分支定界搜索相结合。 MN-BaB - 一个基于GPU的分支定界验证器，在DeepPoly抽象域内采用多神经元松弛约束。 nnenum - 一个高性能验证工具，利用多种抽象层次，包括zonotope、星集和LP松弛。 VeriNet - 一个完备的分支定界验证工具包，基于符号区间传播和外部LP/MIP优化。 闭环与信息物理系统 POLAR - 一个使用Taylor模型流管道对神经网络控制的连续和混合系统进行可达性分析的工具。 Verisig - 一个使用混合自动机可达性分析对带有神经网络控制器的闭环系统进行形式化验证的工具。 基准与竞赛 VNN-COMP - 国际神经网络验证竞赛的官方仓库，托管标准化基准（VNN-LIB和ONNX格式）和性能结果。 文献 综述 Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective (IEEE TDSC, 2022) - 一篇以安全为中心的综述，回顾了旨在证明网络对抗对抗攻击鲁棒性的验证方法。 Algorithms for Verifying Deep Neural Networks (Liu et al., 2019) - 一篇全面的综述，为神经网络验证提供了统一的数学框架。 Introduction to Neural Network Verification (A. Albarghouthi, 2021) - 一篇教科书式的基础综述，涵盖关键数学模型、抽象和算法。 奠基性论文 AI2: Safety Verification of Deep Neural Networks with Abstract Interpretation (Gehr et al., IEEE S&P 2018) - 开创了抽象解释在深度前馈和卷积神经网络中的应用。 An Abstraction-Refinement Approach to Verification of Artificial Neural Networks (Pulina and Tacchella, CAV 2010) - 使用反例引导的抽象精化循环，提出了早期基于SMT的神经网络验证方法。 An MIP-Based Approach for Evaluating the Robustness of Deep Neural Networks (Tjeng et al., ICLR 2019) - 展示了混合整数规划（MIP）如何执行精确的鲁棒性验证。 Certified Adversarial Robustness via Randomized Smoothing (Cohen et al., ICML 2019) - 利用随机平滑建立了针对对抗扰动的可扩展认证鲁棒性保证。 DeepPoly: An Abstract Domain for Proving Safety of Deep Neural Networks (Singh et al., POPL 2019) - 引入了DeepPoly抽象域，用于可扩展且精确的神经网络抽象解释。 Intriguing Properties of Neural Networks (Szegedy et al., ICLR 2014) - 揭示了深度神经网络对对抗样本的脆弱性，推动了认证鲁棒性领域的发展。 Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope (Wong and Kolter, ICML 2018) - 通过线性规划对偶性对凸外对抗多面体进行边界限定，提出了认证防御训练。 Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (Katz et al., CAV 2017) - 引入了Reluplex算法，扩展单纯形法以处理ReLU激活函数。 Towards Fast Computation of Certified Robustness for ReLU Networks (Weng et al., ICML 2018) - 提出了线性松弛边界（CROWN），为许多现代加速验证器奠定了基础。 社区 Neural Verification Community - 托管社区论坛、竞赛链接和协作项目的门户网站。

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）