- 使用分支定界进行非线性神经网络验证
本文提出了名为 GenBaB 的通用框架，用于进行神经网络中非线性函数的分支界定与验证，并展示了其在验证各种类型的神经网络以及其他非线性计算图上的有效性。
- 可验证的强健拟合预测
使用最新的神经网络验证方法，基于 VRCP（可验证鲁棒性适应预测）框架，本文提出了一种新的方法，用于恢复在遭受对抗攻击时的预测覆盖率保证，并支持任意范数的扰动和回归任务，实验结果表明，在图像分类和强化学习环境的回归任务中，VRCP 方法达到 - 验证神经压缩感知
我们首次开发了自动验证算法生成的可证明正确性的神经网络，在计算任务中，我们使用精确的正确性概念，通过训练和验证，成功地实现了从少于向量维数的测量中回复稀疏向量的任务，并且在问题维度较小的情况下，网络的复杂性可以根据问题难度进行调整，解决了传 - 学习神经网络验证的最小 NAP 规范
给定一个神经网络，找到足以形式验证网络鲁棒性的最小（最粗略）NAP。
- 高效编译表达性问题空间规范为神经网络求解器
最近的研究描述了神经网络验证中的嵌入间隙存在。在间隙的一侧是高级规范，由领域专家根据可解释的问题空间编写。在另一侧是逻辑上等价的一组可满足性查询，以适合神经网络求解器的不可解释的嵌入空间形式表达。本文描述了一种将前者编译为后者的算法。我们探 - 具分布鲁棒性的不精确神经网络统计验证
为高维自主系统提供行为保证是人工智能安全领域中的一个特别具有挑战性的问题。本文提出了一个基于主动学习、不确定性量化和神经网络验证的新方法，其中的核心是一种称为不精确神经网络的集成技术，它提供了用于引导主动学习的不确定性。通过在多个物理模拟器 - 使用超属性验证全局神经网络规范
本研究引入超属性形式主义，提供了表达全局规范的方法，可以通过利用验证通用计算图形的能力验证全局规范，从而扩大了使用现有方法提供的保证范围。
- 神经网络中的原像逼近
研究了神经网络的全局鲁棒性问题，提出了一种在量化验证中高效的、基于线性松弛的生成符号下逼近的先验图像的算法。
- 类型化仿射决策结构的威力：一个案例研究
本文介绍了 TADS (紧凑型白盒神经网络表示) 在神经网络验证中的应用，结合 PCA 降维技术，提出了 Precondition Projection 技术用于描述神经网络的行为，可以用于诊断网络错误并提供紧凑和明确的解释，以及用于网络调 - 可微逻辑的逻辑：朝向 DL 统一语义的发展
本文介绍了一种名为 Differentiable Logics 的方法，它使用神经网络满足逻辑规范。作者提出了一种元语言，称为 Differentiable Logics 的逻辑，它可以定义 Differentiable Logics 中的 - 第三届神经网络验证大赛（VNN-COMP 2022）：概述与结果
这篇文章总结了第三届国际神经网络验证竞赛（VNN-COMP 2022），它是第 5 届面向机器学习自主系统的形式方法研讨会（FoMLAS）的一部分，旨在促进当前最先进的神经网络验证工具的公平客观比较，鼓励工具接口的标准化，并聚集神经网络验证 - MMCheckINN：Imandra 中的宽范围神经网络验证（扩展版）
本文介绍了如何使用 Imadra 编程语言和定理证明器来设计开发适用于神经网络验证的 CheckINN 库。
- ICML通过预测选择切平面：基于模仿学习的切割技能培养
本文提出了一种名为 NeuralCut 的新型神经网络进行割平面选择，该方法基于对专家的模仿学习而设计，能够在 MILPs 的切割选择中实现性能优异的表现，且在验证神经网络时表现出很大潜力。
- 凸松弛屏障的重新审视：用于神经网络验证的单神经元更紧凑的松弛方法
我们通过一种新的被紧化的凸松弛优化算法来提高神经网络验证的效率，并针对 ReLU 神经元提出了一种新的凸松弛方案，使得我们在设计两种多项式时间算法，包括利用全面的松弛力量的基于线性规划的算法和快速传播算法时能够比类似算法更好地验证神经网络
- NNV: 面向深度神经网络和学习增强型的网络物理系统的神经网络验证工具
本文介绍神经网络验证（NNV）软件工具，该工具为深度神经网络（DNN）和学习启用的控制系统（CPS）提供了一套基于集合的验证框架。NNV 的核心是一组可达性算法，这些算法利用了多种集合表示，例如，多面体、恒星集、zono topes 和抽象 - 神经网络验证的 Lagrangian 分解
通过 Lagrangian 分解，提出了一种新的神经网络验证方法，其在 GPU 上实施时可提供有效的结果，以推测最大化值的边界，并且可以随时停止，可用于推导形式化验证。
- 通过安全区域的线性逼近验证飞机防撞神经网络
该研究将飞机避碰系统问题定义为马尔科夫决策过程，并使用动态规划进行警告逻辑的优化，使用神经网络压缩以便在有限的硬件上运行，通过神经网络验证工具进行安全性检查的结果发现成千上万个不安全的反例。
- ICLR神经网络非线性规范的验证
本文介绍在神经网络验证中如何利用凸松弛来证明一系列比较丰富的非线性规约，包括物理系统学习到的动力学模型的能量守恒，分类器的输出标签在对抗性扰动下的语义一致性以及预测手写数字求和的系统所包含的误差等，实验验证了该方法的有效性。
- 通过诱导 ReLU 稳定性进行更快的对抗鲁棒性验证训练
本篇论文研究神经网络验证中的协同设计概念，并通过改进权重稀疏性和 ReLU 稳定性的方法，将计算困难的验证问题转化为可处理的问题，并改善了验证的速度，该方法具有普适性。