该论文介绍了一种名为CROWN的通用框架，可以证明具有一般激活函数的神经网络分类器对于给定的输入数据点是健壮的，通过绑定给定激活函数的线性和二次函数，从而可以处理包括但不限于ReLU、tanh、sigmoid和arctan在内的一般激活函数，同时在可比的计算效率下，在ReLU网络上CROWN可以显着提高认证下限，同时CROWN能够展示其对包括tanh、sigmoid和arctan在内的具有一般激活函数的网络的有效性和灵活性。
Nov, 2018
本文介绍一种基于凸松弛框架的神经网络强鲁棒性验证算法，通过大量实验发现该算法在已有松弛算法上并没有显著提高，提示了一类算法具有固有的严格验证难度。
Feb, 2019
本文介绍在神经网络验证中如何利用凸松弛来证明一系列比较丰富的非线性规约，包括物理系统学习到的动力学模型的能量守恒，分类器的输出标签在对抗性扰动下的语义一致性以及预测手写数字求和的系统所包含的误差等，实验验证了该方法的有效性。
研究了深度学习的形式验证以及提出了一种基于分支定界的族算法，并提出了新型的组合方法，以及新的有效的分支策略，将之用于高维输入上的问题，并提出包含以前发布的测试案例的全面测试数据集和基准测试。
Sep, 2019
本文介绍了深度神经网络的鲁棒性的重要性及其应用场景，探讨了Sigmoid激活函数作为近似函数的限制，提出了全面的神经网络紧度定义方法，实现了证明下限稳健性的大幅改善。通过提高识别网络的准确度，使得卷积神经网络获得了明显更精确的验证结果。
Aug, 2022
本文提出了一种紧线性逼近方法(Ti-Lin)来验证卷积神经网络的稳健性，使用MNIST，CIFAR-10和Tiny ImageNet数据集对Ti-Lin进行评估，结果表明Ti-Lin明显优于其他五种最先进的方法，对纯CNN具有Sigmoid/Tanh/Arctan函数和具有Maxpooling功能的CNN的稳健性边界水平提高了最多63.70％和253.54％。
Nov, 2022
本文研究了神经网络鲁棒性的形式化验证，提出了一种新的双重逼近方法，利用激活函数的低估区间来定义紧逼近边界，并将其实现到了名为DualApp的工具中，在不同体系结构的深度神经网络基准测试中，DualApp方法得到了明显的优化
May, 2023
我们研究了神经网络计算的形式验证问题，探讨了其各种鲁棒性和最小化问题。我们提供了一个理论框架，使我们能够在神经网络中转换安全性和效率问题，并分析它们的计算复杂性。我们发现，在半线性设置中，对于分段线性激活函数和使用求和或最大度量时，大多数问题都属于P类或最多属于NP类。
Mar, 2024
本研究旨在解决现有Sigmoid激活函数松弛过松的问题，从而提高形式验证的效率。我们提出了一种基于超平面的调优方法（$\alpha$-sig），可实现Sigmoid激活函数的最紧凑的凸松弛，并在大规模验证任务中嵌入这种松弛。实验结果显示，该方法的性能优于目前的主流验证工具LiRPA和$\alpha$-CROWN。
Aug, 2024
本研究针对形式验证中深度神经网络的非凸性问题，提出了一种新的方法，通过调整超平面紧密地包围sigmoid激活函数。该方法称为α-sig，可以有效地在形式验证框架中引入sigmoid函数的紧凑凸放松，显著提高了验证效率。实验结果显示其优于现有的LiRPA和α-CROWN方法。