Verification of Neural Reachable Tubes via Scenario Optimization and Conformal Prediction
University of Southern California（南加州大学）
针对DeepReach等神经可达管难以验证的问题，提出基于鲁棒场景优化与保形预测的概率安全验证方法，并证明二者等价及异常值调整可恢复安全体积。
2024-04-10 cs.AI cs.LG cs.RO
Learning Neural Networks under Input-Output Specifications
Virginia Tech（弗吉尼亚理工大学）；University of California, Berkeley（加州大学伯克利分校）
在本文中，我们研究了一个重要的问题，学习神经网络，可证明满足一定的规格的输入输出行为。我们的策略是找到一个内部近似的一组容许的政策参数，这是凸的变换空间。为此，我们解决了凸化神经网络的验证条件，这是通过抽象的非线性规范和激活函数与二次约束的关键技术挑战。特别是，我们提出了一种基于循环变换的原始神经网络的重新参数化方案，这导致了在学习过程中可以强制执行的凸条件。这种理论构造在一个实验中得到了验证，该实验指定了不同输入区域的可达集。
2022-02-23 cs.LG cs.SY eess.SY
A Dual Approach to Scalable Verification of Deep Networks
DeepMind
本文讨论了形式化验证神经网络的期望性质的问题，即，获得神经网络满足与其输入和输出相关的规范的可证明保证（例如，对有界范数对抗扰动的鲁棒性）。大多数以前的工作在这个主题是有限的，其适用性的网络，网络架构的大小和复杂性的属性进行验证。相比之下，我们的框架适用于一般类的激活函数和规范的神经网络的输入和输出。我们制定验证作为一个优化问题（寻求找到最大的违反规范），并解决拉格朗日松弛的优化问题，以获得最坏情况下违反规范的上限进行验证。我们的方法是任何时候，即它可以在任何时候停止，并可以获得最大违规的有效界限。我们开发了专门的验证算法，在特殊的假设下，可证明的紧密性保证，并证明了我们的一般验证方法对各种验证任务的实际意义。
2018-08-03 cs.LG stat.ML
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
Probabilistically Tightened Linear Relaxation-based Perturbation Analysis for Neural Network Verification
Department of Computer Science, University of Verona（计算机科学系，威尼斯大学）
PT-LiRPA通过概率紧缩线性松弛扰动分析提升神经网络验证的鲁棒性证书，显著提高验证正确性的概率保证。
2025-12-31 cs.AI cs.LG
Learning Density Distribution of Reachable States for Autonomous Systems
MIT（麻省理工学院）；UIUC（伊利诺伊大学厄巴纳-香槟分校）；Ford（福特汽车公司）
与最坏情况可达性相反，状态密度分布可用于安全相关问题，以更好地量化潜在危险情况的风险可能性。在这项工作中，我们提出了一种数据驱动的方法来计算非线性甚至黑箱系统可达状态的密度分布。我们的半监督方法从轨迹数据中学习系统动力学和状态密度，这是由状态密度演化遵循Liouville偏微分方程这一事实指导的。借助神经网络可达性工具，我们的方法可以估计所有可能的未来状态的集合以及它们的密度。此外，我们可以进行在线安全验证与不安全行为发生的概率范围。我们使用了一组广泛的实验来表明，我们学习的解决方案可以产生一个更准确的估计密度分布，并可以量化风险更少的保守性和灵活性相比，最坏情况下的分析。
2021-09-14 cs.AI cs.LG
Constraint-Aware Refinement for Safety Verification of Neural Feedback Loops
Massachusetts Institute of Technology（麻省理工学院）
本文提出约束感知精化验证方法 CARV，通过显式利用安全约束仅在必要位置精化可达集过近似，从而高效降低保守性并验证神经反馈回路安全性。
2024-09-30 cs.LG cs.RO cs.SY
Warming up recurrent neural networks to maximise reachable multistability greatly improves learning
针对循环神经网络学习长时间依赖困难的问题，本文提出通过 warmup 初始化最大化可达多稳定性，并设计部分预热的双层架构，在多类基准上显著提升学习速度与性能且保持精度。
2023-07-20 cs.LG
Vertex-based reachability analysis for verifying ReLU deep neural networks
神经网络在不同的任务上实现了高性能，即图像识别、话音识别和其他应用。尽管取得了成功，但这些模型在小扰动方面仍然很脆弱，可以用来制作所谓的对抗性例子。已经提出了不同的方法来规避它们的脆弱性，包括形式化验证系统，它采用各种技术，包括可达性，优化和搜索过程，以验证模型满足某些属性。在本文中，我们提出了三种新的可达性算法，用于验证具有ReLU激活的深度神经网络。第一个和第三个算法计算可达集的过近似，而第二个算法计算精确可达集。与以前提出的方法不同，我们的算法以V-多面体作为输入。我们对ACAS徐问题的实验表明，在这项工作中提出的精确多面体网络映射（EPNM）的可达性算法超过了国家的最先进的结果，从文献中，特别是在有关其他可达性方法。
2023-01-27 cs.LG
Safety Verification of Neural Network Control Systems Using Guaranteed Neural Network Model Reduction
Augusta University（奥古斯塔大学）；Southwest Jiaotong University（西南交通大学）
为了提高神经网络控制系统安全性验证的计算效率，提出了一种保证神经网络模型降阶方法。首先，提出了模型降阶精度的概念来描述神经网络的输出与其降阶后的输出之间的保证距离。提出了一种基于可达性的模型降阶精度计算方法。然后，通过将一个尺寸减小的神经网络控制器替换到闭环系统中，开发了一种计算原系统的可达集的算法，该算法能够支持计算效率更高的安全验证过程。最后，将所提出的方法应用于带有神经网络控制器的自适应巡航控制系统的实例研究中，结果表明，该方法可以显著减少安全验证的计算时间，从而验证了该方法的有效性。
2023-01-17 cs.AI cs.LG
Certified Approximate Reachability (CARe): Formal Error Bounds on Deep Learning of Reachable Sets
TU Delft（代尔夫特理工大学）；University of Oxford（牛津大学）
本文提出 CARe 框架，通过引入 epsilon-近似 HJ-PDE 建立训练损失与真实可达集准确性的关系，并利用 SMT 求解器和 CEGIS 闭环微调神经网络，首次为连续动力系统的深度学习可达集提供形式化正确性保证。
2025-03-31 cs.LG cs.SY eess.SY
Verification of Visual Controllers via Compositional Geometric Transformations
Northeastern University（东北大学）
本文提出一种通过组合几何变换建模视觉不确定性的验证框架，为基于感知的控制器生成可达集外近似，并在基准环境中验证了其安全性认证效果。
2025-07-06 cs.LG cs.RO
What's Producible May Not Be Reachable: Measuring the Steerability of Generative Models
Harvard University（哈佛大学）；MIT（麻省理工学院）；Cornell University（康奈尔大学）
本文针对生成模型评估仅关注可生成性的不足，提出“可引导性”概念并给出数学分解量化方法，通过用户重现任务构建基准，发现现有模型可引导性差，且验证了简单图像引导机制能实现超2倍的改进。
2025-11-12 cs.AI cs.CV cs.HC
Neural Network Verification with PyRAT
针对关键领域AI系统的安全可信需求，提出基于抽象解释的神经网络安全与鲁棒性验证工具PyRAT，介绍其核心抽象方法与特性，该工具在VNN-Comp 2024中获第二名，已在多项合作中提供安全保障。
2025-09-05 cs.AI cs.LG
Scalable Data-Driven Reachability Analysis and Control via Koopman Operators with Conformal Coverage Guarantees
Georgia Institute of Technology（佐治亚理工学院）；School of ECE（电子工程学院）；Schools of Cybersecurity & Privacy & Aerospace Eng（网络安全与隐私及航空航天工程学院）
本文提出基于Koopman算子的可扩展数据驱动可达性分析与控制方法，通过符合预测保证系统覆盖，提升高维任务的可达集覆盖率和计算效率。
2026-01-03 cs.AI cs.LG cs.RO
Robust Training and Verification of Implicit Neural Networks: A Non-Euclidean Contractive Approach
Georgia Institute of Technology（佐治亚理工学院）；University of California, Santa Barbara（加州大学圣巴巴拉分校）
提出了一种基于非欧收缩理论的隐式神经网络训练和鲁棒性验证的理论和计算框架。其基本思想是将神经网络的鲁棒性分析转化为可达性问题，并利用$\ell_{\infty}$ -范数输入输出Lipschitz常数和网络的紧包含函数过逼近其可达集。首先，对于一个给定的隐式神经网络，我们使用$\ell_{\infty}$ -矩阵措施，提出了它的适定性的充分条件，设计了一个迭代算法来计算其不动点，并提供其$\ell_\infty$ -范数输入输出Lipschitz常数的上界。其次，我们介绍了一个相关的嵌入式网络，并表明嵌入式网络可以用来提供一个$\ell_\infty$ -范数盒过逼近的可达集的原始网络。此外，我们使用嵌入式网络设计了一个迭代算法来计算原系统的紧包含函数的上界。第三，我们利用Lipschitz常数的上界和紧包含函数的上界设计了两个隐式神经网络的训练和鲁棒性验证算法。最后，我们应用我们的算法训练隐式神经网络的MNIST数据集和比较我们的模型的鲁棒性，通过现有的方法在文献中训练的模型。
2022-08-08 cs.LG cs.SY eess.SY
Safety Verification of Model Based Reinforcement Learning Controllers
School of Aeronautics and Astronautics（航空航天学院）；Purdue University（普渡大学）
基于模型的强化学习（RL）已经成为开发用于现实世界系统的控制器的有前途的工具（例如，机器人、自动驾驶等）。然而，实际系统往往有约束强加在他们的状态空间，必须满足，以确保系统及其环境的安全。为RL算法开发验证工具是具有挑战性的，因为神经网络的非线性结构阻碍了对此类模型或控制器的分析验证。为此，我们提出了一种新的基于模型的RL控制器使用可达集分析的安全验证框架。所提出的框架可以有效地处理使用神经网络表示的模型和控制器。此外，如果控制器不能满足一般的安全约束，所提出的框架也可以用来识别的初始状态的子集，从该控制器可以安全地执行。
2020-10-21 cs.LG cs.RO cs.SY
Reachable Sets of Classifiers and Regression Models: (Non-)Robustness Analysis and Robust Training
Technical University of Munich（慕尼黑工业大学）
神经网络在分类和回归任务中实现了出色的准确性。然而，理解它们的行为仍然是一个开放的挑战，需要解决预测的鲁棒性，可解释性和可靠性问题。我们通过计算神经网络的可达集来回答这些问题，即由连续输入集产生的输出集。我们提供了两种有效的方法，导致过和下近似的可达集。正如我们所展示的，这个原则是高度通用的。首先，我们使用它来分析和增强分类器和回归模型的鲁棒性。这与现有的主要侧重于分类的工作形成对比。具体来说，我们验证（非）鲁棒性，提出了一个强大的训练过程，并表明我们的方法优于对抗攻击以及最先进的方法验证分类器的非范数界扰动。其次，我们提供了区分未标记输入的可靠和不可靠预测的技术，以量化每个特征对预测的影响，并计算特征排名。
2021-05-12 cs.CV cs.LG stat.ML
Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers
Georgia Institute of Technology（佐治亚理工学院）
本文提出一种基于区间分析的框架，通过将神经网络控制器与非线性系统嵌入更大系统并利用单轨迹计算和划分策略，实现闭环系统可达集的高效严格过近似验证。
2023-08-07 cs.LG cs.SY eess.SY
Constrained Feedforward Neural Network Training via Reachability Analysis
Stanford University（斯坦福大学）
神经网络最近在各种各样的用途中变得流行，但是在安全关键领域（诸如人类附近和周围的机器人）中的应用有限。这是因为训练神经网络以服从安全约束仍然是一个公开的挑战。大多数现有的安全相关方法只试图验证已经训练好的网络是否遵守约束，需要交替训练和验证。相反，这项工作提出了一种约束方法，同时训练和验证前馈神经网络与整流线性单元（ReLU）的非线性。通过计算网络的输出空间可达集并确保其不与不安全集相交来执行约束;通过制定可达集与输出空间的不安全部分之间的新型冲突检查损失函数来实现训练。可达集和不安全集表示的约束zonotopes，凸多面体表示，使可微碰撞检查。所提出的方法是成功地证明了一个非线性层和大约50个参数的网络。
2021-07-16 cs.AI cs.LG cs.RO
Out of the Shadows: Exploring a Latent Space for Neural Network Verification
Technical University of Munich（慕尼黑工业大学）
本文提出了一种基于潜在空间的神经网络验证方法，通过迭代细化减少验证子问题数量，利用矩阵运算实现高效GPU加速，提升了验证性能。
2026-02-09 cs.LG
Shared Certificates for Neural Network Verification
ETH Zurich（苏黎世联邦理工学院）；Nostic Solutions AG（诺斯蒂克解决方案公司）；University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；VMware Research（威睿研究院）
针对神经网络验证中从头独立证明导致开销高昂的问题，提出共享证书概念，利用中间层抽象的重叠特性跨输入复用证明工作，在不损失精度的前提下有效降低整体验证成本。
2023-11-23 cs.CR 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
Scalable Surrogate Verification of Image-based Neural Network Control Systems using Composition and Unrolling
Stony Brook University（石溪大学）；Massachusetts Institute of Technology（麻省理工学院）；Clemson University（克莱姆森大学）
针对基于图像的神经网络控制系统验证中的过度过近似问题，提出通过组合系统动力学与网络并展开多步控制循环的方法，显著提升了可达集计算的准确性和可扩展性。
2025-04-29 cs.LG cs.RO cs.SY
Formal Verification of Input-Output Mappings of Tree Ensembles
Saab AB（萨博集团）；Linköping University（林雪平大学）
机器学习和人工智能的最新进展现在正在考虑安全关键的自主系统，其中软件缺陷可能会对人类和环境造成严重伤害。这些领域的设计组织目前无法提供令人信服的论据，证明当使用机器学习算法来实现其软件时，他们的系统可以安全运行。本文提出了一种从决策树和树集成中提取等价类的有效方法，并形式化地验证它们的输入输出映射是否符合要求。这个想法是，鉴于安全需求可以追溯到系统输入输出模式的理想属性，我们可以在安全参数中使用积极的验证结果。本文介绍了该方法的实施工具投票（树集成验证器），并评估其可扩展性的两个案例研究，在当前文献中。我们证明了我们的方法是实用的树集成训练低维数据高达25决策树和树深度高达20。我们的工作还研究了高维数据的方法的局限性，并初步探讨了大量的树和验证所需的时间之间的权衡。
2020-03-23 cs.LG stat.ML
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
On The Verification of Neural ODEs with Stochastic Guarantees
我们表明，神经常微分方程，一类新兴的时间连续神经网络，可以通过解决一组全局优化问题进行验证。为此，我们引入随机拉格朗日可达性（SLR），一种基于抽象的技术，用于构建一个紧密的Reachtube（在给定的时间范围内的一组可达状态的过度近似），并提供随机保证的形式的置信区间的Reachtube边界。SLR本质上避免了臭名昭著的包装效应（过度近似误差的积累），通过执行局部优化步骤来扩展安全区域，而不是像确定性可达性方法那样重复向前传播它们。为了实现快速局部优化，我们引入了一种新的前向模式伴随灵敏度方法来计算梯度，而无需反向传播。最后，我们建立了SLR的渐近和非渐近收敛速度。
2020-12-16 cs.LG cs.NE cs.SY
Bridging Neural ODE and ResNet: A Formal Error Bound for Safety Verification
Univ Gustave Eiffel（法国埃菲尔大学）
本文通过界定神经常微分方程与残差网络之间的近似误差，提出一种形式化误差界限，使两者能互为验证代理，从而无需重复验证即可保证安全性属性在两模型间相互成立。
2025-10-11 cs.AI cs.LG
Fundamental Limits in Formal Verification of Message-Passing Neural Networks
University of Kassel（卡塞尔大学）
输出可达性和对抗鲁棒性是神经网络最相关的安全属性之一。我们表明，在消息传递神经网络（MPNN）的背景下，一个常见的图神经网络（GNN）模型，形式化验证是不可能的。特别是，我们表明，输出可达的图分类MPNN，工作在图的无界大小，非平凡程度和充分表达节点标签，不能正式验证：有没有算法，正确回答（是或否），给定一个MPNN，是否存在一些有效的输入MPNN，使相应的输出满足给定的规格。然而，我们也表明，输出的可达性和对抗性的鲁棒性节点分类MPNN可以正式验证时，输入图的程度的限制是先验的。我们讨论了这些结果的影响，为了获得一个完整的图片的原则可能性，正式验证GNN，根据所涉及的GNN模型和输入输出规格的表现力。
2022-10-04 cs.LG cs.LO
A Simple and Efficient Sampling-based Algorithm for General Reachability Analysis
Stanford University（斯坦福大学）；Harvard University（哈佛大学）；University of Paris-Saclay（巴黎萨克雷大学）；CNRS（法国国家科学研究中心）；CentraleSupélec（中央理工-高等电力学院）
在这项工作中，我们分析了一个有效的基于采样的通用可达性分析算法，这仍然是一个众所周知的挑战性问题，从神经网络验证到动力系统的安全分析的应用。该算法通过对输入进行采样，在真可达集上估计其图像，并将其$ε$填充凸包作为集合估计器，适用于一般的问题设置，实现简单。我们的主要贡献是使用随机集理论的渐近和有限样本精度保证的推导。这种分析通知算法设计，以获得一个$ε$接近可达集近似的概率高，提供了洞察可达性问题是最具挑战性的，并激励安全关键的应用程序的技术。在一个神经网络验证任务中，我们证明了这种方法比以前的工作更准确，速度也更快。根据我们的分析，我们还设计了一个鲁棒模型预测控制器，我们在硬件实验中证明。
2022-04-13 cs.AI cs.LG cs.RO
Set-Based Training for Neural Network Verification
Technical University of Munich（慕尼黑工业大学）
本文提出一种基于集合的训练方法，通过计算输出集合和梯度集合来减小输出包络，提升神经网络鲁棒性并简化形式化验证，实验证明其性能具有竞争力且可用多项式时间算法验证。
2025-08-05 cs.CR cs.LG cs.LO
Formal Safety Verification and Refinement for Generative Motion Planners via Certified Local Stabilization
Georgia Institute of Technology（佐治亚理工学院）
提出一种通过小型神经跟踪控制器稳定GMP采样参考并应用神经网络验证的方法，实现生成式运动规划器的形式化安全验证，在不重训练下提升仿真与硬件上的安全性。
2025-09-24 cs.LG cs.RO cs.SY
Generating Formal Safety Assurances for High-Dimensional Reachability
University of Southern California（南加州大学）
针对高维系统下HJ可达性分析维度灾难与DeepReach神经求解器无安全保证的问题，提出误差界计算与场景优化方法，实现高维场景下概率安全的可达管近似。
2023-06-10 cs.AI cs.LG cs.RO
Hierarchical End-to-End Taylor Bounds for Complete Neural Network Verification
Johns Hopkins University（约翰霍普金斯大学）
本文提出HiTaB框架，利用二阶光滑性及Hessian和其Lipschitz常数，通过分层方法改进神经网络可达集分析，提供更精确的安全性证明。
2026-05-11 cs.LG cs.SY eess.SY
LLM-Assisted Dynamic Threat Analysis for Attacker-Reachable Software Weaknesses in Autonomous Vehicles
The University of Alabama（阿拉巴马大学）；Department of Civil, Construction & Environmental Engineering, The University of Alabama（阿拉巴马大学土木、建筑与环境工程学院）；Department of Computer Science, The University of Alabama（阿拉巴马大学计算机科学学院）
该研究针对自动驾驶车辆软件弱点的动态威胁分析难题，探究LLM辅助Autoware的自动化测试工件生成，发现构建集成是核心障碍，推理模型编译测试用例的表现优于代码专用模型。
2026-08-14 cs.CR cs.LG cs.SE
Verification of Non-Linear Specifications for Neural Networks
DeepMind
关于神经网络验证的先前工作集中于作为网络输出的线性函数的规范，例如，在输入的对抗扰动下分类器输出的不变性。在本文中，我们扩展验证算法，能够证明更丰富的神经网络的属性。要做到这一点，我们介绍了类的凸松弛规格，构成非线性规格，可以使用凸松弛验证。我们表明，一些重要的属性感兴趣的可以在这一类建模，包括能量守恒的物理系统的学习动力学模型;语义一致性的分类器的输出标签下的对抗扰动和边界错误的系统，预测手写数字的总和。我们的实验评估表明，我们的方法是能够有效地验证这些规格。此外，我们的评估暴露了模型中无法验证以满足这些规范的失效模式。因此，强调训练模型的重要性不仅要适合训练数据，而且要与规范一致。
2019-02-25 cs.LG stat.ML
A Note on Non-Composability of Layerwise Approximate Verification for Neural Inference
Tel Aviv University（特拉维夫大学）
本文指出分层近似验证在神经推断中不可靠，通过反例证明对抗性误差可导致最终输出任意变化。
2026-02-17 cs.CR cs.LG
DiFR: Inference Verification Despite Nondeterminism
harvard（哈佛大学）
DiFR通过比较生成token与可信参考实现预测，验证推理过程的正确性，能有效检测采样错误、模拟bug和模型量化，提升推理验证的效率与准确性。
2025-11-25 cs.AI cs.LG
Enabling Verification of Deep Neural Networks in Perception Tasks Using Fuzzy Logic and Concept Embeddings
Continental AG（大陆集团）；University of Bamberg（班贝格大学）
用于安全关键应用的深度卷积神经网络（CNN）的一个主要缺点是其黑盒性质。这使得在已经训练好的计算机视觉CNN上很难验证或监控复杂的符号要求。在这项工作中，我们提出了一个简单而有效的方法来验证一个CNN符合与视觉概念相关的符号谓词逻辑规则。这是第一个：（1）不修改CNN，（2）可以使用没有CNN输入或输出特征的视觉概念，以及（3）可以利用连续的CNN置信度输出。为了实现这一目标，我们新结合了可解释的人工智能和逻辑的方法：首先，使用监督概念嵌入分析，CNN的输出是事后丰富的概念输出。其次，来自先验知识的规则被建模为接受CNN输出的真值函数，并且可以以很少的计算开销进行评估。我们在这里研究模糊逻辑的使用，即，连续的真值，以及适当的输出校准，这在理论上和实际上都显示出轻微的好处。在三个验证用例的最先进的对象检测器上证明了适用性，其中对违反规则的监控可以揭示检测错误。
2022-03-13 cs.CV cs.LG cs.LO
Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis
Stanford University（斯坦福大学）；NASA Jet Propulsion Laboratory（美国宇航局喷气推进实验室）
本文提出RoVer-CoRe框架，利用汉密尔顿-雅可比可达性分析对感知系统进行鲁棒验证，通过整合控制器、观测函数和状态估计模块，实现对非线性、非凸、学习驱动等复杂系统的安全性和性能验证。
2026-04-15 cs.LG cs.RO cs.SY
2L-3W: 2-Level 3-Way Hardware-Software Co-Verification for the Mapping of Deep Learning Architecture (DLA) onto FPGA Boards
Tennessee Tech University（田纳西理工大学）
FPGA已成为部署深度学习架构（DLA）的热门选择。有许多研究人员已经探索了DLA在FPGA上的部署和映射。然而，越来越需要对这些部署进行设计时硬件-软件协同验证。据我们所知，这是第一个提出2级3路（2L-3 W）硬件-软件协同验证方法的工作，并为FPGA板上DLA的成功映射，部署和验证提供了一个分步指南。2级验证是为了确保每个阶段（软件和硬件）的实现都遵循所需的行为。3路协同验证提供了跨范例（软件、设计和硬件）的逐层参数检查，以确保DLA在FPGA板上的正确实现和映射。建议的2L-3 W的共同验证方法已在几个测试用例进行了评估。在每种情况下，将PYNQ FPGA板（硬件）上部署的DLA的预测和逐层输出与Vivado HLS上实现的DLA的逐层输出的中间设计结果以及软件级别（Caffe深度学习框架）的预测和逐层输出进行比较，以获得逐层相似性得分。比较是使用完全自动化的Python脚本实现的。该比较提供逐层相似性分数，该分数通知我们DLA映射到FPGA的成功程度，或者帮助在设计时识别在映射不成功的情况下要调试的层。我们在LeNet DLA和Caffe启发的Cifar-10 DLA上展示了我们的技术，并且共同验证结果产生了99%准确度的逐层相似性得分。
2019-11-14 cs.LG stat.ML
Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound
Department of Computer and Information Science, University of Konstanz, Konstanz, Baden-Würtemberg, Germany（计算机与信息科学系，康斯坦茨大学，康斯坦茨，巴登-符腾堡，德国）
提出基于界限传播和分支定界的算法解决神经网络概率验证问题，显著缩短求解时间并保证可靠性与完备性。
2025-07-10 cs.AI cs.LG
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
Reachability Analysis of Deep Neural Networks with Provable Guarantees
University of Oxford（牛津大学）；University of Liverpool（利物浦大学）
深度神经网络（DNN）的正确性是具有挑战性的。我们研究了前馈DNN的通用可达性问题，对于给定的网络输入集和其输出上的Lipschitz连续函数，计算函数值的上下界。因为网络和函数是Lipschitz连续的，所以在下界和上界之间的区间内的所有值都是可达的。我们展示了如何获得的安全验证问题，输出范围分析问题和鲁棒性措施，通过实例化的可达性问题。我们提出了一种新的算法，基于自适应嵌套优化来解决可达性问题。该技术已在一系列DNN上实施和评估，证明了其效率，可扩展性和处理比最先进的验证方法更广泛的网络类别的能力。
2018-05-06 cs.CV cs.LG stat.ML
Training-free LLM Verification via Recycling Few-shot Examples
Yonsei University（延世大学）；KAIST（韩国科学技术院）
针对LLM推理随机性与结论不一致的问题，提出无需训练的ReFeri框架，结合前向置信得分与后向重构惩罚，在7项任务上使3种LLM准确率平均提升8.2%。
2026-09-01 cs.AI cs.LG
Verification of deep probabilistic models
DeepMind（深度思维）
概率模型是现代深度学习工具箱的关键部分-从生成模型（VAE，GANs），用于机器翻译和语音处理的序列到序列模型，到函数空间模型（条件神经过程，神经过程）。考虑到这些模型的大小和复杂性，在应用程序中安全地部署它们需要开发工具来严格分析它们的行为，并提供一些保证，这些模型与期望的属性或规范列表一致。例如，机器翻译模型应该为模型输入中的无害变化产生语义上等效的输出。学习单调函数分布的函数回归模型应该在较大的输入下预测较大的值。这些属性的验证需要一个新的框架，超越了确定性前馈网络中研究的验证概念，因为在概率模型中要求最坏情况的保证可能会产生保守或空洞的结果。我们提出了一种新的验证公式，用于深度概率模型，该模型在产生输出的过程中接受条件输入和样本潜变量：我们要求模型的输出在潜变量的采样上满足高概率的线性约束，并且对于模型的条件输入的每个选择。我们表明，严格的下限的概率约束得到满足，可以有效地获得。神经过程的实验表明，几个感兴趣的属性，而建模功能空间可以在这个框架内建模（单调性，凸性），并有效地验证使用我们的算法
2018-12-06 cs.LG stat.ML
The Cost of Relaxation: Evaluating the Error in Convex Neural Network Verification
Foundation for Research and Technology – Hellas（希腊基础研究与技术研究所）；University of Crete（塞萨洛尼基大学）；Catalan Institution for Research and Advanced Studies（加泰罗尼亚研究与高级研究机构）；University of Lleida（莱里达大学）
研究凸松弛在神经网络验证中的误差，分析其在深度和输入半径下的指数增长特性，并通过实验验证结果。
2026-04-20 cs.AI cs.LG
Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systems
Georgia Institute of Technology（佐治亚理工学院）
针对神经网络控制非线性系统的鲁棒可达集估计，本文提出收缩引导的自适应划分算法，通过解耦验证与划分以低计算成本显著提升精度，并给出混合单调可达性保证。
2023-12-10 cs.LG cs.SY eess.SY
Verification and Validation of Physics-Informed Surrogate Component Models for Dynamic Power-System Simulation
Department of Wind and Energy Systems, Technical University of Denmark (DTU)（风能与能源系统系，丹麦技术大学）
本文探讨了物理信息代理组件模型在动态电力系统仿真中的验证与验证问题，提出了一种有限时间界限，用于连接允许的组件输出误差与代数耦合灵敏度、动态误差放大和仿真时间 horizon。通过模型基于验证和数据基于验证两种设置，研究了同步机模型的代理模型。
2026-03-18 cs.LG cs.SY eess.SY
Correctness Verification of Neural Networks
Massachusetts Institute of Technology（麻省理工学院）
我们提出了一个新的框架，指定和验证的正确性全局神经网络的感知任务。感知任务的神经网络验证大多集中在鲁棒性验证上。与鲁棒性验证不同，鲁棒性验证旨在验证网络的预测在标记点周围的某些局部区域中是稳定的，我们的框架提供了一种在整个目标输入空间中全局指定正确性的方法，并验证网络对所有目标输入都是正确的（或找到网络不正确的区域）。我们通过1）由世界的所有相关状态组成的状态空间和2）从世界的状态产生神经网络输入的观察过程来提供规范。用有限数量的瓦片平铺状态和输入空间，从状态瓦片获得地面真值边界，从输入瓦片获得网络输出边界，然后比较地面真值和网络输出边界，为任何感兴趣的输入提供网络输出误差的上限。所提出的框架还可以检测非法输入--不包含在（或接近）由状态空间和观察过程定义的目标输入空间中的输入（神经网络不是设计来处理它们的），这样我们就可以在没有保证时进行标记。两个案例研究的结果突出了我们的技术在整个目标输入空间验证误差界的能力，并显示了误差界在状态和输入空间的变化。
2022-08-23 cs.CR cs.CV cs.LG
Generative Models Erode Human Temporal Learning Through Market Selection
Independent Researcher（独立研究者）
本文论证现代生成模型在亚AGI能力水平上通过市场选择机制侵蚀人类时间学习，提出价值崩溃路径并用昂贵检验框架形式化，跨领域证据显示验证侵蚀四阶段。
2026-06-04 cs.AI cs.CY cs.LG
