Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations
School of Mechatronic Engineering and Automation, Shanghai University, Shanghai, China（机械电子工程与自动化学院，上海大学，上海，中国）；Beijing Institute of Control Engineering, Beijing, China（北京控制工程研究所，北京，中国）
本文提出LightCROWN方法，利用激活函数的分析特性计算更紧的雅可比界，提升神经控制屏障函数的验证效率和可扩展性。
2026-05-08 cs.LG
Hybrid Zonotopes Exactly Represent ReLU Neural Networks
The University of Texas at Dallas（德克萨斯大学达拉斯分校）
本文提出利用混合zonotope等价表示ReLU前馈全连接神经网络，证明二元变量复杂度随网络规模线性增长，并通过非线性函数逼近、MPC闭环可达性与验证及MNIST分类鲁棒性案例验证了该方法的实用性。
2023-04-05 cs.LG cs.SY eess.SY
Static analysis of ReLU neural networks with tropical polyhedra
LIX, Ecole Polytechnique, CNRS and Institut Polytechnique de Paris（巴黎综合理工学院与巴黎综合理工学院联盟计算机科学实验室）；University of Colorado at Boulder（科罗拉多大学博尔德分校）
本文研究了前馈神经网络的极差分析问题，它是研究神经网络的鲁棒性、规范遵从性和神经网络反馈系统的可达性分析等应用的基础。我们的方法专注于ReLU（整流线性单元）前馈神经网络，这些网络存在特定的困难：利用导数的方法通常不适用，即使对于小型网络，神经元激活模式的数量也可能相当大，凸近似通常过于粗糙。在本文中，我们采用基于集合的方法和抽象的解释，已经非常成功地应对类似的困难，在经典的程序验证。我们提出了一种使用热带多面体抽象ReLU前馈神经网络的方法。我们表明，热带多面体可以有效地抽象ReLU激活函数，同时能够控制由于线性计算而导致的精度损失。我们展示了ReLU网络和热带有理函数之间的联系如何为ReLU神经网络的范围分析提供方法。
2021-08-23 cs.AI cs.LG
Fully Automatic Neural Network Reduction for Formal Verification
Technical University of Munich（慕尼黑工业大学）
本文提出一种基于可达性分析的全自动可靠神经网络缩减方法，在验证过程中在线缩减网络规模，适用于ReLU、sigmoid、tanh及卷积网络，显著缩短形式化验证时间。
2025-07-07 cs.LG
Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq
Technische Universität Berlin（柏林工业大学）
神经网络的验证依赖于激活函数是分段仿射的（pwa）--使得定理证明者能够对验证问题进行编码。在本文中，我们提出了第一个形式化的pwa激活函数的交互式定理证明器，用于验证神经网络内Coq库Coquelicot真正的分析。作为概念验证，我们构建了流行的pwa激活函数ReLU。我们将我们的形式化到一个Coq模型的神经网络，并设计了一个验证的转换从一个神经网络N到一个PWA功能表示N组成PWA功能，我们构造的每一层。这种表示使编码证明自动化，例如Coq的战术lra -线性实数算术的决策过程。此外，我们的形式化铺平了道路，集成Coq的框架中的神经网络验证作为后备证明时，自动证明失败。
2023-01-30 cs.LG
Neural Network Verification as Piecewise Linear Optimization: Formulations for the Composition of Staircase Functions
Rice University（莱斯大学）；Google Research（谷歌研究院）
我们提出了一种技术，神经网络验证使用混合整数规划（MIP）配方。我们使用分段线性激活函数为网络中的每个神经元导出一个\emph{strong formulation}。此外，在一般情况下，这些公式可能需要指数数量的不等式，我们还推导出一个分离过程，在输入维的超线性时间运行。我们首先介绍并开发了我们在\emph{staircase}函数类上的技术，该技术概括了ReLU、二进制化和量化的激活函数。然后，我们使用楼梯激活函数的结果，得到一般分段线性激活函数的分离方法。从经验上讲，使用我们的强大的配方和分离技术，我们可以减少计算时间在精确的验证设置的基础上MIP和提高假阴性率依赖于松弛的MIP配方的不精确的验证。
2022-11-27 cs.LG math.OC
Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation
The Robotics Institute, Carnegie Mellon University（卡内基梅隆大学机器人研究所）
本文提出一种基于符号导数边界传播的高效验证框架，用于验证基于ReLU的神经控制屏障函数，在多种机器人动力学实验中验证率和验证时间均优于区间算术基线方法。
2024-10-04 cs.LG cs.RO cs.SY
Permutation Invariance of Deep Neural Networks with ReLUs
Chennai Mathematical Institute（钦奈数学研究所）；TCS Research（TCS研究院）
考虑一个深度神经网络（DNN），它被用来建议飞机必须转向的方向，以避免与入侵飞机发生可能的碰撞。非正式地说，如果当入侵者从左（右）方向接近时，它要求自己的船右转（左），那么这样的网络是行为良好的。考虑另一个网络，它接受四个输入--在一场桥牌游戏中发给玩家的牌--并决定哪支球队可以出价。不严格地说，如果你交换伙伴的手（北方和南方，或东方和西方），决定不会改变。然而，如果你把北牌换成东牌，情况就会改变。对于输入和输出层的某些排列，这种排列不变性是这些网络的正确性和鲁棒性的核心。本文提出了一种合理的、基于抽象的技术，以ReLU作为激活函数，在DNN中建立置换不变性。该技术计算可达状态的过度近似和安全状态的欠近似，并将此信息向前和向后跨层传播。我们的方法的新颖之处在于一个有用的领带类分析，我们介绍了前向传播，和一个可扩展的2-多面体下近似方法，逃避指数爆破的区域数量在向后传播。实验比较表明，我们的算法的效率验证置换不变性作为一个两个安全属性（使用FFNN验证两个副本的网络）。
2021-10-18 cs.LG cs.LO
Training for Faster Adversarial Robustness Verification via Inducing ReLU Stability
Massachusetts Institute of Technology（麻省理工学院）
我们探讨的概念协同设计的背景下，神经网络验证。具体来说，我们的目标是训练深度神经网络，不仅对对抗性扰动具有鲁棒性，而且其鲁棒性可以更容易地验证。为此，我们确定了网络模型的两个属性--权重稀疏性和所谓的ReLU稳定性--这两个属性会显著影响相应验证任务的复杂性。我们证明，提高权重稀疏性本身已经使我们能够把计算上棘手的验证问题变成易于处理的问题。然后，提高ReLU稳定性会导致验证时间增加4- 13倍。我们的方法的一个重要特点是它的“普遍性”，也就是说，它可以与广泛的培训程序和核查办法一起使用。
2019-04-23 cs.CR cs.LG cs.NE
Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation
Department of Computer Science University of Oxford（牛津大学计算机科学系）；St Hugh’s College University of Oxford（牛津大学圣希利学院）；Delft Center for Systems and Control TU Delft（代尔夫特理工大学系统与控制中心）；Dep. of Computer Science & Inst. for Data Science in Mech. Eng RWTH Aachen University（亚琛工业大学计算机科学系及机械工程数据科学研究所）；AI4I Italy（意大利AI4I）
本文提出一种基于线性边界传播的神经控制屏障函数验证方法，通过计算梯度边界和McCormick松弛，实现对神经网络作为控制屏障函数的有效验证，适用于任意控制-affine系统和多种非线性激活函数。
2026-04-14 cs.LG cs.RO cs.SY
NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems
Vanderbilt University（范德堡大学）；University of Pennsylvania（宾夕法尼亚大学）
本文介绍了神经网络验证（NNV）软件工具，这是一个基于集合的验证框架，用于深度神经网络（DNN）和支持学习的网络物理系统（CPS）。NNV的核心是一系列可达性算法，这些算法使用了各种集合表示，如多面体、星集、zonotopes和抽象域表示。NNV支持精确（健全和完整）和过近似（健全）可达性算法，用于验证具有各种激活函数的前馈神经网络（FFNN）的安全性和鲁棒性。对于具有学习能力的CPS，例如包含神经网络的闭环控制系统，NNV为线性对象模型和具有分段线性激活函数（例如ReLU）的FFNN控制器提供精确和过近似的可达性分析方案。对于类似的神经网络控制系统（NNCS），而不是具有非线性的植物模型，NNV支持过近似分析相结合的星集分析用于FFNN控制器与zonotope-based分析的非线性植物动态CORA建设。我们使用两个真实案例研究来评估NNV：第一个是ACAS Xu网络的安全性验证，第二个是基于深度学习的自适应巡航控制系统的安全性验证。
2020-04-12 cs.LG cs.SY eess.SY
DiffRNN: Differential Verification of Recurrent Neural Networks
University of Southern California（南加州大学）
诸如长短期记忆（LSTM）网络的循环神经网络（RNN）在诸如图像处理、数据分类、语音识别的各种应用中以及作为自治系统中的控制器已经变得流行。在实际环境中，通常需要在资源受限的平台（如移动电话或嵌入式设备）上部署此类RNN。由于这些组件的内存占用和能耗成为瓶颈，因此有兴趣使用一系列启发式技术来压缩和优化这些网络。然而，这些技术不能保证优化网络的安全性，例如，对抗对抗性输入，或者优化网络和原始网络的等价性。为了解决这个问题，我们提出了RNN，RNN的第一个差分验证方法，以证明两个结构相似的神经网络的等价性。基于ReLU的前馈神经网络的差分验证的现有工作不适用于RNN，其中无法避免非线性激活函数，如Sigmoid和Tanh。RNN还带来了独特的挑战，例如处理顺序输入，复杂的反馈结构以及门和状态之间的相互作用。在RNN中，我们通过用线性约束非线性激活函数，然后求解约束优化问题来计算高维空间中非线性表面上的紧密边界框来克服这些挑战。然后使用dReal SMT求解器证明这些边界框的合理性。我们在各种基准测试中证明了我们的技术的实际有效性，并表明RNN优于POPQORN等最先进的RNN验证工具。
2020-07-20 cs.LG stat.ML
Neural Network Verification with Branch-and-Bound for General Nonlinearities
University of California, Los Angeles（加州大学洛杉矶分校）；University of Michigan（密歇根大学）；Carnegie Mellon University（卡内基梅隆大学）；Columbia University（哥伦比亚大学）；University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
针对现有神经网络验证分支定界主要局限于ReLU等分段线性激活的问题，本文提出通用框架GenBaB，通过线性边界传播、新型分支启发式与预优化分支点查找表，支持Sigmoid、Tanh、Sine、GeLU及LSTM/ViT中的多维非线性运算，并能验证ACOPF等一般非线性计算图。
2025-02-07 cs.AI cs.LG
Formal Verification of Stochastic Systems with ReLU Neural Network Controllers
Duke University（杜克大学）
在这项工作中，我们解决了配备ReLU神经网络（NN）控制器的随机网络物理系统（CPS）的正式安全验证问题。我们的目标是找到一组初始状态，在预定的置信度下，系统在指定的时间范围内不会达到不安全的配置。具体来说，我们考虑离散时间线性时不变系统与高斯噪声，我们抽象的一个合适的图。然后，我们制定了一个可满足性模凸（SMC）的问题，估计上界的转移概率在图中的节点之间。使用这个抽象，我们提出了一种方法来计算紧边界上的节点的安全概率在这个图中，尽管这些节点之间的转移概率可能过近似。此外，使用建议的SMC公式，我们设计了一个启发式方法来细化系统的抽象，以进一步提高估计的安全界限。最后，我们证实了所提出的方法的有效性与仿真结果考虑机器人导航的例子和比较对国家的最先进的验证计划。
2021-03-08 cs.LG cs.SY eess.SY
Complexity of Injectivity and Verification of ReLU Neural Networks
Technische Universität Berlin, Faculty IV Institute of Software Engineering and Theoretical Computer Science, Algorithmics and Computational Complexity（柏林技术大学，第四学院软件工程与理论计算机科学研究所，算法与计算复杂性）；Technische Universität Berlin, Faculty II, Institute of Mathematics, Combinatorial Optimization and Graph Algorithms（柏林技术大学，第二学院数学研究所，组合优化与图算法）
本研究证明ReLU网络单射性判定为coNP完全，提出输入维度参数化算法，并证明网络验证为coNP难，同时刻画满射性与计算凸性的联系。
2025-06-19 cs.CC cs.DM cs.LG
From Approximation Rates to Loss-Landscape Barrier Decay in Shallow ReLU Networks
Independent Researcher（独立研究者）
本研究探讨了过参数化单隐藏层 ReLU 网络中 Lipschitz 损失景观的渐近平滑特性，通过理论证明和实验验证，发现网络宽度增加时损失景观趋于平滑，局部和全局极小值之间的能量间隙减小。
2026-08-14 cs.LG
ReluDiff: Differential Verification of Deep Neural Networks
University of Southern California（南加利福尼亚大学）
随着深度神经网络越来越多地被部署在实践中，其效率已成为一个重要问题。虽然存在用于减小网络的大小、能量消耗和计算要求的压缩技术，但它们仅凭经验证明不存在准确性损失，但缺乏压缩网络的正式保证，例如，在对抗性的例子面前。现有的验证技术，如Reluplex，ReluVal和DeepPoly提供了形式化的保证，但它们是为分析单个网络而不是两个网络之间的关系而设计的。为了填补这一空白，我们开发了一种新的方法，用于两个密切相关的网络的差分验证。我们的方法包括一个快速但近似的前向区间分析，然后是一个向后的过程，迭代地细化近似，直到验证所需的属性。我们有两个主要的创新。在前向传递过程中，我们利用两个网络的结构和行为相似性来更准确地限制两个网络的输出神经元之间的差异。然后在向后传递中，我们利用梯度差来更准确地计算最有益的细化。我们的实验表明，与最先进的验证工具相比，我们的方法可以实现数量级的加速，并证明比现有工具更多的属性。
2020-01-29 cs.LG cs.LO cs.SE
Probabilistic Verification of ReLU Neural Networks via Characteristic Functions
Georgia Institute of Technology（佐治亚理工学院）；University of New Mexico（新墨西哥大学）
由于神经网络在许多工程应用中的日益普遍性，因此优化神经网络的输入-输出关系以实现某些期望的性能规范是困难的，但却是重要的问题。我们在频域中使用概率论的思想为ReLU神经网络提供概率验证保证。具体来说，我们将（深度）前馈神经网络解释为有限时域上的离散动力系统，该系统形成初始状态的分布，并使用特征函数通过网络传播输入数据的分布。使用逆傅立叶变换，我们获得了输出集的相应累积分布函数，该函数可用于检查网络是否按预期执行，给定输入集中的任何随机点。所提出的方法不要求分布具有定义良好的矩或矩生成函数。我们证明了我们提出的方法上的两个例子，并比较其性能相关的方法。
2022-12-03 cs.LG cs.SY eess.SY
Robustness Verification of Recurrent Neural Networks with Abstraction Refinement
National Science and Technology Council (NSTC), Taiwan（台湾国家科学与技术委员会）
提出抽象精化框架，通过分割预激活区间消除非线性松弛误差，并利用SHAP引导的时间步选择策略降低组合成本，显著提升RNN鲁棒性验证成功率。
2026-06-12 cs.LG
Abstract Neural Networks
University of California, Davis（加州大学戴维斯分校）
深度神经网络（DNN）正迅速应用于无人机和飞机控制等安全关键领域，激发了验证其行为安全性的技术。不幸的是，DNN验证是NP难的，当前的算法随着DNN中节点的数量呈指数级增长。本文介绍了抽象神经网络（ANN）的概念，它可以用来在使用较少节点的情况下完全过度逼近DNN。ANN类似于DNN，除了权重矩阵被给定抽象域中的值所取代。我们提出了一个由抽象域和DNN中使用的激活函数参数化的框架，可以用来构建相应的ANN。我们提出了DNN激活函数的必要和充分条件，以使所构建的ANN完全过逼近给定的DNN。先前关于DNN抽象的工作仅限于区间域和ReLU激活函数。我们的框架可以用其他抽象域（如八边形和多面体）以及其他激活函数（如Leaky ReLU、Sigmoid和Hyperbolic Tangent）来实例化。
2020-09-11 cs.LG cs.PL stat.ML
Random Parameter Noise Does Not Make Exact ReLU Verification Easy
University of Illinois Chicago（伊利诺伊大学芝加哥分校）
研究对抗性平滑模型中ReLU网络精确验证，表明在NP⊈BPP假设下，不存在预期运行时间为多项式的可靠完备验证器，通过结合精确间隙嵌入等方法证明，指出参数非退化不能为精确验证提供通用平滑多项式保证。
2026-07-17 cs.CC cs.LG
Vertex-based reachability analysis for verifying ReLU deep neural networks
神经网络在不同的任务上实现了高性能，即图像识别、话音识别和其他应用。尽管取得了成功，但这些模型在小扰动方面仍然很脆弱，可以用来制作所谓的对抗性例子。已经提出了不同的方法来规避它们的脆弱性，包括形式化验证系统，它采用各种技术，包括可达性，优化和搜索过程，以验证模型满足某些属性。在本文中，我们提出了三种新的可达性算法，用于验证具有ReLU激活的深度神经网络。第一个和第三个算法计算可达集的过近似，而第二个算法计算精确可达集。与以前提出的方法不同，我们的算法以V-多面体作为输入。我们对ACAS徐问题的实验表明，在这项工作中提出的精确多面体网络映射（EPNM）的可达性算法超过了国家的最先进的结果，从文献中，特别是在有关其他可达性方法。
2023-01-27 cs.LG
Expediting Neural Network Verification via Network Reduction
National University of Singapore（新加坡国立大学）
本文提出验证前的网络约简预处理，通过消除稳定 ReLU 神经元并转换为 ReLU/Affine 序列化结构，显著提升 alpha-beta-crown、VeriNet 和 PRIMA 的验证速度与适用范围。
2023-08-14 cs.AI cs.LG cs.SE
ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs
Stanford University（斯坦福大学）
深度神经网络通常缺乏在安全关键系统中部署所需的安全性和鲁棒性保证。形式化验证技术可以用来证明网络的输入输出安全性质，但当性质难以确定时，我们依赖于各种优化问题的解决方案。在这项工作中，我们提出了一种名为ZoPE的算法，该算法解决了具有低维输入的前馈ReLU网络输出的优化问题。该算法急切地分裂的输入空间，边界的目标使用zonotope传播在每一步，并提高了计算效率相比，现有的混合整数规划方法。我们演示了如何制定和解决三种类型的优化问题：（i）最小化输出空间上的任何凸函数，（ii）最小化两个网络的输出上的凸函数，在它们之间的层中具有对抗性扰动，以及（iii）最大化两个网络之间的输出差异。使用ZoPE，我们观察到与几个最先进的验证器相比，ACAS Xu神经网络验证基准的属性$1$的$25\times$加速，以及与混合整数编程基线相比，一组线性优化问题的$85\times$加速。我们通过投影到生成对抗网络的范围并可视化压缩和未压缩网络之间的差异来展示优化器在分析网络方面的多功能性。
2022-05-16 cs.AI cs.LG math.OC
Verification-Aided Learning of Neural Network Barrier Functions with Termination Guarantees
Microsoft Research（微软研究院）；Johns Hopkins University（约翰斯·霍普金斯大学）
针对验证辅助学习框架无终止保证、找有效屏障函数成功率低的问题，提出先学习神经网络基函数再利用凸性与验证反例微调的方法，具备有限步终止保证，可显著提升框架性能。
2024-03-12 cs.AI cs.LG cs.SY
Global Optimization of Objective Functions Represented by ReLU Networks
Stanford University（斯坦福大学）；The Hebrew University of Jerusalem（耶路撒冷希伯来大学）
神经网络可以学习复杂的非凸函数，并且在安全关键环境中保证其正确行为是具有挑战性的。存在许多方法来发现网络中的故障（例如，对抗性的例子），但这些不能保证没有失败。验证算法解决了这一需求，并通过回答“是或否”的问题来提供关于神经网络的正式保证。例如，它们可以回答是否在一定范围内存在违规行为。然而，个别的“是或否”问题不能回答定性的问题，如“在这些界限内最大的误差是什么”;这些问题的答案在于优化领域。因此，我们提出了扩展现有验证器的策略来执行优化并找到：（i）给定输入区域中的最极端故障和（ii）导致故障所需的最小输入扰动。一个天真的方法，使用二分搜索与现成的验证结果在许多昂贵的和重叠的调用验证。相反，我们提出了一种方法，紧密集成的优化过程中的验证过程，实现更好的运行时性能比天真的方法。我们评估我们的方法实现的扩展Marabou，一个国家的最先进的神经网络验证，并比较其性能与二分法和MIPVerify，基于优化的验证。我们观察到Marabou和MIPVerify扩展之间的互补性能。
2021-09-09 cs.LG math.OC
Interior-Point Vanishing Problem in Semidefinite Relaxations for Neural Network Verification
Institute of Science Tokyo（东京科学研究所）；Keio University（庆应大学）
该研究发现用于神经网络验证的SDP松弛存在内点消失问题，会随网络深度增加丧失严格可行性，提出五种解决方案可解决41%的总问题，同时指出传统ReLU上下界约束有害于可行性，为深度网络SDP验证提供了实用方案。
2025-06-12 cs.LG math.OC
Bounding the Complexity of Formally Verifying Neural Networks: A Geometric Approach
University of California, Irvine（加州大学欧文分校）
在本文中，我们考虑形式化验证整流线性单元（ReLU）神经网络（NN）行为的计算复杂性，其中验证需要确定NN是否满足凸多面体规范。具体来说，我们表明，对于两种不同的神经网络架构-浅NN和两级格（TLL）NN-验证问题（凸）多面体约束是多项式的神经网络中的神经元的数量进行验证，当所有其他方面的验证问题保持固定。我们实现这些复杂性的结果，展示明确的（但类似的）验证算法的每种类型的架构。这两种算法都有效地将NN参数转换为NN输入空间的分区，通过超平面;这具有将原始验证问题划分为多项式的许多子验证问题的效果，这些子验证问题来自神经元的几何形状。我们表明，这些子问题可以选择，使神经网络是纯粹的仿射在每个，因此每个子问题是可解的多项式时间通过线性规划（LP）。因此，可以使用用于枚举超平面布置中的区域的已知算法来获得用于原始验证问题的多项式时间算法。最后，我们适应我们提出的算法验证动态系统，特别是当这些神经网络架构被用作LTI系统的状态反馈控制器。我们进一步评估这种方法的可行性数值。
2021-03-25 cs.LG
Value Functions are Control Barrier Functions: Verification of Safe Policies using Control Theory
University College London（伦敦大学学院）
本文提出将价值函数与控制屏障函数建立理论联系，通过控制理论验证方法为强化学习策略提供安全证书，并给出验证指标与实现细节，推动安全可验证的RL控制系统设计。
2023-12-05 cs.AI cs.LG cs.RO
Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features
Vanderbilt University（范德堡大学）
本文提出GraphStar集扩展NNV框架，实现GNN形式化验证，在电力系统任务和图分类基准上提供更紧致的鲁棒性保证。
2026-09-25 cs.AI cs.LG
Learning Lookahead Lemmas for Neural Network Verification
本文提出一种前瞻驱动的神经网络验证内处理框架，将其应用于Marabou和α-β-CROWN两款验证器，可提升性能，最多多证明34%的不可满足实例。
2026-08-03 cs.AI cs.LG cs.LO
DeepAbstract: Neural Network Abstraction for Accelerating Verification
Technical University of Munich（慕尼黑工业大学）；Audi AG（奥迪股份公司）
虽然抽象是一个经典的验证工具，可以扩展它，但它并不经常用于验证神经网络。然而，它可以帮助完成将现有算法扩展到最先进的网络架构的仍然开放的任务。我们介绍了一个抽象的框架，适用于全连接前馈神经网络的基础上聚类的神经元，在一些输入的行为相似。对于ReLU的特定情况，我们还提供了抽象所引起的错误范围。我们展示了抽象如何减少网络的大小，同时保持其准确性，以及如何将抽象网络上的验证结果传输回原始网络。
2020-06-24 cs.AI cs.LG cs.LO
Classification of Data Generated by Gaussian Mixture Models Using Deep ReLU Networks
Georgia Institute of Technology（佐治亚理工学院）
本文针对无界域 GMM 二分类，利用高斯分布性质证明深度 ReLU 网络可取得与维度无关的超额风险收敛率，并给出解析函数的新型 ReLU 逼近误差界。
2023-08-15 cs.LG math.ST stat.ML
A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks
Microsoft Research AI（微软研究院人工智能部门）；UCLA（加州大学洛杉矶分校）
神经网络的验证使我们能够衡量它们对对抗攻击的鲁棒性。验证算法分为两类：在指数时间内运行的精确验证器和有效但不完整的松弛验证器。在本文中，我们统一了所有现有的LP松弛验证，尽我们所知，在一个一般的凸松弛框架。该框架适用于具有不同架构和非线性的神经网络，并涵盖了鲁棒性验证的原始和对偶视图。我们进一步证明了强对偶的原始和对偶问题在非常温和的条件下。接下来，我们进行了超过22个CPU年的大规模实验，以获得在我们的ReLU网络框架中最优的凸松弛问题的精确解。我们发现，对于在MNIST和CIFAR数据集上正常或鲁棒训练的各种网络，精确的解决方案并没有显着改善PGD和现有松弛验证器之间的差距。我们的研究结果表明，对于我们的框架捕获的大类方法，严格验证存在固有的障碍。我们讨论了这种障碍的可能原因以及绕过它的潜在未来方向。我们的代码和训练模型可以在http://github.com/Hadisalman/robust-verify-benchmark上找到。
2020-01-10 cs.AI cs.CR cs.CV
Fast Neural Network Verification via Shadow Prices
University of California at Berkeley（加州大学伯克利分校）；Facebook AI Research（脸书人工智能研究院）；University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
为了在安全关键设置中使用神经网络，提供运行时操作的保证至关重要。最近关于ReLU网络的工作试图验证属于有界框的输入是否会产生一些不期望的输出。输入分裂过程是一种特殊类型的验证机制，它通过递归地将输入集划分为更小的集合来实现。这些方法的效率很大程度上取决于盒子在验证属性之前必须经历的分裂次数。在这项工作中，我们提出了一种新的技术的基础上，充分利用影子价格的问题，产生一个更有效的生成分裂比国家的最先进的信息。机载防撞系统（ACAS）基准验证任务的结果显示，产生的分区，大大减少了计算时间的相当大的减少。这些结果为包括视觉和控制在内的各种机器学习应用程序的改进验证方法打开了大门。
2021-06-21 cs.LG stat.ML
Boosting the Robustness Verification of DNN by Identifying the Achilles's Heel
National University of Defense Technology（国防科技大学）
深度神经网络（DNN）是一种广泛使用的深度学习技术。如何保证DNN系统的安全性是DNN研究和应用的关键问题。鲁棒性是DNN的重要安全属性。然而，现有的验证DNN的鲁棒性的工作是耗时的，并且难以扩展到大规模DNN。在本文中，我们提出了一种用于DNN鲁棒性验证的提升方法，旨在更早地找到反例。我们的观察是DNN的不同输入有不同的可能性存在反例，并且最大输出值和第二大输出值之间的差异很小的输入往往是DNN的阿基里斯之踵。我们已经实现了我们的方法，并将其应用于最先进的DNN验证工具Reluplex和四种DNN攻击方法。在两个基准上的实验结果表明了该方法的有效性。
2018-11-17 cs.CR cs.LG
A Unified View of SDP-based Neural Network Verification through Completely Positive Programming
Stanford University（斯坦福大学）；MIT（麻省理工学院）
确保神经网络的输入-输出关系符合规定的操作规范是将这些网络部署在安全关键应用中的关键推动因素。基于半定规划（SDP）的ReLU网络验证方法将这个问题转化为最优化问题，其中任何此类公式的准确性反映了神经网络计算如何表示的保真度水平，以及棘手约束的放松。虽然文献包含了在保持可处理性的同时改进SDP公式的紧密性的许多进展，但相对较少的工作致力于另一个极端，即，如何在SDP松弛之前最准确地捕获原始验证问题。在这项工作中，我们开发了一个精确的，凸的验证公式作为一个完全积极的程序（CPP），并提供分析表明，我们的公式是最小的-任何约束的去除从根本上歪曲了神经网络计算。我们利用我们的配方提供了一个统一的观点，现有的方法，并在某些情况下观察到的大弛豫间隙的来源给予洞察力。
2022-03-06 cs.LG math.OC
FROAV: A Framework for RAG Observation and Agent Verification -- Lowering the Barrier to LLM Agent Research
AetheTech
FROAV提供了一个开源平台，通过可视化工作流编排、评估框架和Python集成，降低LLM代理研究的门槛，使研究人员能更专注于算法创新。
2026-01-12 cs.LG cs.SE
Data-Driven Safety Verification using Barrier Certificates and Matrix Zonotopes
Technical University of Munich（慕尼黑工业大学）
针对信息物理系统因模型不可靠或难以获取导致的安全验证难题，提出基于矩阵 zonotopes 和障碍证书的数据驱动框架，通过构建包含真实模型的模型集并集成障碍证书，实现无需显式模型的严格安全验证，数值实验验证了有效性。
2025-04-14 cs.FL cs.LG cs.SY
Expressiveness of Multi-Neuron Convex Relaxations in Neural Network Certification
Department of Computer Science（计算机科学系）；Department of Information Technology and Electrical Engineering（信息科技与电气工程系）
本研究首次严格分析了多神经元松弛的表达性，发现其本质上不完整，但通过增加神经元或划分输入域可实现完整性，为认证鲁棒性提供了新方向。
2026-11-03 cs.AI cs.LG
Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings
School of Computing, Newcastle University（纽卡斯尔大学计算机学院）；Imperial College London（帝国理工学院）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）
本文提出一种数据驱动的分布鲁棒安全性验证方法，利用屏障证书和条件均值嵌入，无需精确模型，通过平方和优化高效求解，降低样本复杂度。
2024-03-15 cs.LG cs.SY eess.SY
OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems
Stanford University（斯坦福大学）
深度学习方法可用于生成控制策略，但证明其安全性具有挑战性。由此产生的网络是非线性的，并且通常非常大。为了应对这一挑战，我们提出了OVERT：一个健全的算法的安全性验证的非线性离散时间闭环动态系统的神经网络控制策略。OVERT的新颖之处在于将经典形式化方法文献中的思想与较新的神经网络验证文献中的思想相结合。OVERT的核心概念是抽象非线性函数，并给出一组最优紧的分段线性边界。这种分段线性边界被设计用于无缝集成到ReLU神经网络验证工具中。OVERT可以通过计算可达集或直接求解可行性查询来证明有界时间安全性。我们展示了几个经典基准测试示例的安全验证的各种示例。OVERT在计算时间和可达集的紧密性方面都优于现有的方法。
2021-08-03 cs.LG cs.LO cs.SY
Neural Networks with Small Weights and Depth-Separation Barriers
Weizmann Institute of Science（魏茨曼科学研究所）
在研究神经网络的表达能力时，一个重要的问题是是否存在只能由足够深的网络来近似的函数，假设它们的大小是有界的。然而，对于恒定深度，现有结果仅限于深度$2$和$3$，并且实现更高深度的结果一直是一个重要的开放问题。在本文中，我们专注于前馈ReLU网络，并通过简化为开放问题和电路复杂性中的自然证明障碍，证明了在深度$4$之外证明此类结果的基本障碍。为了证明这一点，我们研究了一个看似无关的问题的独立利益：即，是否有多项式有界的功能，需要超多项式的权重，以近似与恒定深度的神经网络。我们对这个问题提供了一个否定的和建设性的答案，通过表明如果一个函数可以用具有任意大权重的多项式大小、恒定深度的$k$网络来逼近，那么它也可以用多项式大小、深度的$3k+3$网络来逼近，其权重是多项式有界的。
2020-12-27 cs.CC cs.LG stat.ML
The Off-Support Barrier: Why Semantic Safety Constraints Are Not Learning-Problem Invariants, and What Follows for Prior Design, Containment, and Verification
该研究提出语义安全约束是离支撑对象，基于奇异学习理论推导得出多项推论，以2026年7月OpenAI与Hugging Face评估事件为案例，为AI安全的先验设计、约束验证等问题提供理论启示。
2026-08-13 cs.AI cs.LG
UR4NNV: Neural Network Verification, Under-approximation Reachability Works!
National University of Defense Technology（国防科技大学）；Chinese Academy of Sciences（中国科学院）；University of Chinese Academy of Sciences（中国科学院大学）
本文提出 UR4NNV 框架，首次利用基于二叉树分支的欠近似可达性分析验证 ReLU 深度神经网络，以有效证伪属性并缓解过近似方法的“未知困境”。
2024-01-23 cs.AI cs.LG
PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier
University of California, Irvine（加州大学尔湾分校）
神经网络（NN）具有与其在现实世界应用中的扩散相称的日益明显的安全性影响：意外的以及对抗性的错误分类都可能导致致命的结果。因此，形式化验证技术已被公认为是设计和部署安全神经网络的关键。在本文中，我们介绍了一种新的方法来正式验证ReLU NN最常见的安全规范-即网络输入和输出的多面体规范。像其他一些方法一样，我们使用一个放松的凸规划来减轻问题的组合复杂性。然而，我们的方法的独特之处在于，我们不仅使用凸解算器作为线性可行性检查器，而且还作为惩罚解决方案中允许的松弛量的手段。特别地，我们通过通常的线性约束对每个ReLU进行编码，并将其与凸目标函数相结合，该凸目标函数对每个神经元的输出与其松弛之间的差异进行惩罚。该凸函数进一步构造成迫使最大弛豫出现在最接近输入层的地方;这提供了进一步的好处，即当逐层调节时，尽可能早地调节最有问题的神经元。可以利用这种范例来创建一种验证算法，该算法不仅在一般情况下比竞争方法更快，而且还能够验证更多的安全属性;我们在标准MNIST鲁棒性验证套件上评估了PEREGRiNN，以证实这些声明。
2021-04-18 cs.FL cs.LG stat.ML
Optimized Symbolic Interval Propagation for Neural Network Verification
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
神经网络越来越多地应用于安全关键领域，因此其验证变得越来越重要。目前证明前馈神经网络输入输出关系的算法中有一大类是基于线性松弛和符号区间传播的。然而，由于变量的依赖性，近似随着网络深度的增加而恶化。在本文中，我们提出了DPNeurifyFV，这是一种用于低维输入空间的ReLU网络的新型分支定界求解器，它基于具有新鲜变量和输入分裂的符号区间传播。一个新的启发式选择新鲜的变量可以改善依赖性问题，而我们的新的分裂启发式，结合其他几个改进，加快了分支定界过程。我们评估我们的方法在空中防撞网络ACAS徐和演示运行时的改进相比，国家的最先进的工具。
2022-12-15 cs.AI cs.CR cs.LG
BaB-prob: Branch and Bound with Preactivation Splitting for Probabilistic Verification of Neural Networks
School of Aerospace Engineering（航空航天工程学院）；Institute for Robotics and Intelligent Machines（机器人与智能机械研究所）；Georgia Institute of Technology（佐治亚理工学院）
本研究将带预激活分裂的分支定界框架拓展至神经网络概率验证场景，提出BaB-prob方法及两种高效分裂策略变体，证明了其在前馈ReLU网络上的可靠性与完备性，在多类测试基准的中高维输入问题上性能优于现有最优方法。
2025-09-30 cs.AI cs.LG stat.ML
E-Globe: Scalable $ε$-Global Verification of Neural Networks via Tight Upper Bounds and Pattern-Aware Branching
University of Texas at Austin（德克萨斯大学奥斯汀分校）；Los Alamos National Laboratory（洛斯阿拉莫斯国家实验室）；University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
E-Globe通过紧上界和模式感知分支实现神经网络的高效ε-全局验证，显著提升验证速度和精度。
2026-02-04 cs.AI cs.LG
Parameterized Hardness of Zonotope Containment and Neural Network Verification
Technische Universität Berlin（柏林技术大学）；Max Planck Institute for Mathematics in the Sciences（马克斯·普朗克数学研究所）；University of Technology Nuremberg（纽伦堡技术大学）
研究探讨了2层ReLU网络函数的正性判定问题，证明其在参数d下属于W[1]-难问题，并展示了Zonotope包含、Lp-Lipschitz常数近似等任务的计算复杂性，揭示了这些基础问题的最优解法。
2026-09-04 cs.CC cs.DM cs.LG
Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models
University of Oxford（牛津大学）；Amazon Inc（亚马逊公司）
我们介绍了一种自动化的，正式的，基于反例的方法来合成屏障证书（BC）的连续和混合动力学模型的安全验证。该方法的基础是一个归纳框架：这是一个学习者之间的顺序循环，它操纵一个候选BC结构为神经网络，和一个声音验证器，它要么证明候选人的有效性或生成反例，以进一步指导学习者。我们将该方法与最先进的技术进行比较，在多项式和非多项式动态模型上：结果表明，我们可以更快地合成声音BC高达两个数量级，特别是在验证引擎上有明显的加速（少五个数量级），同时需要更小的数据集（少三个数量级）用于学习部分。除了对现有技术的改进之外，我们还进一步挑战了混合动力学模型和更大维度模型的新方法，并展示了我们算法和代码库的数值鲁棒性。
2020-10-19 cs.LG cs.LO cs.SY
Learning Safe Neural Network Controllers with Barrier Certificates
Southwest University（西南大学）；University of Surrey（萨里大学）；University of York（约克大学）
针对非线性连续动力系统，提出了一种新的控制器设计方法。控制器是基于神经网络（NN）。为了证明安全性，我们利用障碍函数，这是由神经网络以及表示。我们同时训练障碍神经网络和神经网络，实现了验证在环合成。我们提供了一个原型工具nncontroller与一些案例研究。实验结果证实了该方法的可行性和有效性。
2020-09-18 cs.AI cs.LG cs.SY
Neural Network-assisted Interval Reachability for Systems with Control Barrier Function-Based Safe Controllers
Boston University（波士顿大学）；University of Colorado Boulder（科罗拉多大学博尔德分校）
本文提出用预训练神经网络近似基于CBF的优化控制器，并结合混合单调理论与神经网络验证算法构造嵌入系统，通过单条轨迹高效过近似系统可达集，用于性能与稳定性验证。
2025-04-11 cs.LG cs.SY eess.SY
Strong mixed-integer programming formulations for trained neural networks
Google Research（谷歌研究院）；MIT（麻省理工学院）
我们提出了一个理想的混合整数规划（MIP）制定的整流线性单元（ReLU）出现在一个训练有素的神经网络。我们的公式需要一个单一的二进制变量，除了ReLU的输入和输出变量之外，没有其他连续变量。我们对比它与一个理想的“扩展”配方与线性数量的额外的连续变量，通过标准技术。一个明显的缺点是，我们制定的是，它需要一个指数数量的不等式约束，但我们提供了一个例程来分离的不等式在线性时间。我们还证明了这些指数多约束是温和的条件下的小面定义。最后，我们研究了网络验证问题，并观察到从指数不等式中动态分离1）比扩展公式更具有计算效率和可扩展性，2）在较小的实例上将最先进的MIP求解器的求解时间减少了7倍，以及3）在较硬的实例上几乎匹配最先进的MIP求解器的对偶边界，在几轮分离之后，并且在数量级上更少的时间。
2019-02-28 cs.LG math.OC
