研究了深度学习的形式验证以及提出了一种基于分支定界的族算法，并提出了新型的组合方法，以及新的有效的分支策略，将之用于高维输入上的问题，并提出包含以前发布的测试案例的全面测试数据集和基准测试。

Sep, 2019

本文提出了一种针对具备分段线性激活函数的前向神经网络进行验证的方法，并使用全局线性逼近对 SMT 求解器和 ILP 求解器进行推理，通过专门设计的验证算法利用推理出的相位信息对网络进行冲突检测和安全节点约束，并在碰撞避免和手写数字识别案例研究中进行了评价。

May, 2017

本文扩展了一种现有的神经网络验证技术，以支持更广泛的分段线性激活函数类别，并将原始的算法扩展以提供对以起始集表示的有界输入集的精确结果或上估计结果，并允许无界输入集。我们实施了我们的算法，并在一些案例研究中展示了它们的有效性。

Nov, 2023

本文调查了最近出现的，从可达性分析、优化和搜索中获得的洞见的方法，以确保设计的深度神经网络满足特定的输入输出属性。 我们讨论了现有算法之间的根本差异和联系。 此外，我们提供了现有方法的教学实现，并在一组基准问题上进行了比较。

Mar, 2019

我们研究了神经网络计算的形式验证问题，探讨了其各种鲁棒性和最小化问题。我们提供了一个理论框架，使我们能够在神经网络中转换安全性和效率问题，并分析它们的计算复杂性。我们发现，在半线性设置中，对于分段线性激活函数和使用求和或最大度量时，大多数问题都属于 P 类或最多属于 NP 类。

Mar, 2024

提出了一种生成可验证的神经网络（VNNs）的新框架，该框架通过后训练优化在保留预测性能和鲁棒性之间取得平衡，使得生成的网络在预测性能方面与原始网络相当，并且可以进行验证，以更加高效地建立 VNNs 的强大性。

Dec, 2023

本文提出一种基于混合整数线性规划的框架，首次在电力系统应用中验证神经网络行为，能够确定神经网络分类为安全或不安全的输入范围，并且能够系统地识别对抗性示例，从而提高神经网络在电力系统中的鲁棒性和可靠性。

Oct, 2019

本文提出了一种通用的神经网络形式验证框架，通过将验证问题转化为最优化问题，并通过我们提出的松弛算法得到可靠的上界，从而可对神经网络的输入和输出属性满足的规范进行形式化验证。

Mar, 2018

本文提出了使用神经网络控制器的分段线性系统的可达集估算和安全性验证问题，并开发了一种逐层方法来计算修正线性单位激活函数神经网络的输出可达集。基于神经网络控制器输出可达集，可以迭代地为给定的有限时间间隔估算分段线性反馈控制系统的输出可达集，并通过检查不安全区域和输出到达集的交集的存在来执行带有神经网络控制器的分段线性系统的安全性验证。

Feb, 2018

文章介绍了一种基于神经网络和逻辑规范的神经符号验证框架 Neuro-symbolic Verification，使得现有的神经网络验证基础设施可用于分析复杂的实际特性，从而避免现有神经网络验证技术的严重局限。

Mar, 2022