本文提出了一种通用的神经网络形式验证框架, 通过将验证问题转化为最优化问题, 并通过我们提出的松弛算法得到可靠的上界, 从而可对神经网络的输入和输出属性满足的规范进行形式化验证。
Mar, 2018
本文提出了一种新的半定松弛办法，用于证明针对任意ReLU网络的鲁棒性，显示该松弛法比先前的松弛法更严格，并在三个不同的训练对象对我们的建议松弛法不感兴趣。
Nov, 2018
本文介绍在神经网络验证中如何利用凸松弛来证明一系列比较丰富的非线性规约，包括物理系统学习到的动力学模型的能量守恒，分类器的输出标签在对抗性扰动下的语义一致性以及预测手写数字求和的系统所包含的误差等，实验验证了该方法的有效性。
Feb, 2019
通过解决凸松弛，可以证明神经网络对抗性示例的鲁棒性。最近，提出了一种基于半定编程松弛的较少保守的鲁棒性证明方法。本文提出一种几何技术，用于确定该SDP证书是否是精确的，并在单隐藏层下证明该证书的精确性，并验证其理论洞见。
Jun, 2020
我们通过一种新的被紧化的凸松弛优化算法来提高神经网络验证的效率，并针对 ReLU 神经元提出了一种新的凸松弛方案，使得我们在设计两种多项式时间算法，包括利用全面的松弛力量的基于线性规划的算法和快速传播算法时能够比类似算法更好地验证神经网络
该论文介绍了一种新的SDP算法，利用迭代特征向量方法将其各种操作表达为网络正反向传播。在MNIST和CIFAR-10数据集上的两个验证矢量网络中，将L-inf的验证鲁棒准确性从1％提高到88％和从6％提高到40％
Oct, 2020
论文提出了两种新的双重算法来解决神经网络边界问题，这些算法可以更紧密地边界和验证神经网络，同时具有之前方法的优点，可以更高效地获得更好的验证结果。
Jan, 2021
提出一种结合多神经元松弛和分支定界(并运用基于GPU的优化器)的神经网络验证器，将先前的优势综合以解决较大和较有挑战性的网络问题，并在多个基准测试中取得最新的最佳结果。
Apr, 2022
通过对常用凸松弛方法进行深入研究，我们发现：（i）更高级的松弛方法允许更多单变量函数被精确分析的ReLU网络表达，（ii）更精确的松弛方法能够允许指数级规模的解空间编码相同函数的ReLU网络，以及（iii）即使使用最精确的单神经元松弛方法，也无法构建能够精确分析多变量凸、单调的分段线性函数的ReLU网络。
Nov, 2023
该研究解决了ReLU网络在完全认证中表达能力受限的问题，通过提出基于（层级）多神经元松弛的全新方法，证明此方法可以为一般ReLU网络提供完全认证。研究发现，这一创新理论突破使ReLU网络的表达能力不再受限，对认证稳健性的实践具有重要影响。
Oct, 2024