二元神经网络属性验证的混合整数规划方法
本研究提出一种使用布尔可满足性对深度神经网络的属性进行验证的严格方法，并构建了一种创建二元化神经网络布尔公式的表示方法来验证其强健性，是深度神经网络验证方面的一项重要贡献。
Sep, 2017
本研究探讨了二值化神经网络的形式验证问题，并使用硬件验证的约减方法对其进行了验证，通过证明找到最优 factor（因数）的 NP - 难度和 PTAS 可近似难度，设计出了多项式时间搜索启发式解法来生成因数解，整个框架可以应用于具有数千个神经元和输入的嵌入式设备的中等规模 BNN 的验证技术。
Oct, 2017
本文提出了一种基于混合整数规划的验证方法，对分段线性神经网络进行验证，以评估其对于对抗样本的脆弱性；通过紧凑的非线性公式和新颖的预处理算法实现了两到三个数量级的计算速度提升，并成功确定了 MNIST 分类器对于一定幅值下的对抗精度，相较于同类算法提供更好的证明。
Nov, 2017
本文研究了使用组合和整数优化来攻击二值化神经网络的问题，提出一种混合整数线性规划（MILP）的解决方案。实验表明，与标准梯度攻击（FGSM）相比，所提出的 IProp 算法表现良好，同时超越了 MILP 的限制。
Oct, 2018
本文提出了一种基于 Binarized Neural Networks（BNNs）的验证技术（EEV），可以具有可比较的鲁棒性，并且通过使用一种策略来训练鲁棒性 BNNs，可以实现更快，更准确的验证。EEV 有效，通过在 MNIST 和 CIFAR10 数据集上展示非平凡卷积 BNN 的 L-inf-bounded 对抗性鲁棒性的首个确切验证结果可以进行性能优化。
May, 2020
研究了深度学习的形式验证以及提出了一种基于分支定界的族算法，并提出了新型的组合方法，以及新的有效的分支策略，将之用于高维输入上的问题，并提出包含以前发布的测试案例的全面测试数据集和基准测试。
Sep, 2019
使用二值化神经网络 (BNNs) 的强化学习算法以提高可验证性的方法，解决了神经网络在安全关键场合应用上不可靠的问题。在训练 Atari 环境中的 BNNs 之后，我们验证了其鲁棒性属性。
Mar, 2022
量化用整数运算取代浮点算术在深度神经网络模型中，从而在设备上提供更高效的推断，降低功耗和内存需求。本文提出了一个框架用于正式验证量化神经网络的特性。我们的基准技术基于整数线性规划，保证了完备性和正确性。然后我们展示了如何利用梯度启发式搜索方法和边界传播技术来提高效率。我们通过在 PyTorch 中量化感知网络来评估我们的方法。结果表明，与现有技术相比，我们能够以更好的可扩展性和效率验证量化网络。
Dec, 2023
通过将训练二值化神经网络的问题重新定义为一个混合整数规划的亚可加性对偶问题，我们展示了二值化神经网络具有一种平滑可控的表示形式，从而使得在二值化神经网络的背景下可以使用 Bolte 等人的隐式微分的框架，为实际实现反向传播提供了可能。此方法还可以应用于更广泛的混合整数规划类问题，包括在人工智能及其他领域中遇到的符号方法。
Oct, 2023