利用混合整数规划公式验证二值化神经网络 (BNN)，检查其可行性、MNIST 数据集和飞机冲突避免控制器中的性质，并证明相较于全精度神经网络的最先进的验证算法，通过验证 BNN 节省的时间是值得的。

Mar, 2022

本文提出了一种基于 Binarized Neural Networks（BNNs）的验证技术（EEV），可以具有可比较的鲁棒性，并且通过使用一种策略来训练鲁棒性 BNNs，可以实现更快，更准确的验证。EEV 有效，通过在 MNIST 和 CIFAR10 数据集上展示非平凡卷积 BNN 的 L-inf-bounded 对抗性鲁棒性的首个确切验证结果可以进行性能优化。

May, 2020

本研究探讨了二值化神经网络的形式验证问题，并使用硬件验证的约减方法对其进行了验证，通过证明找到最优 factor（因数）的 NP - 难度和 PTAS 可近似难度，设计出了多项式时间搜索启发式解法来生成因数解，整个框架可以应用于具有数千个神经元和输入的嵌入式设备的中等规模 BNN 的验证技术。

Oct, 2017

使用二值化神经网络 (BNNs) 的强化学习算法以提高可验证性的方法，解决了神经网络在安全关键场合应用上不可靠的问题。在训练 Atari 环境中的 BNNs 之后，我们验证了其鲁棒性属性。

Mar, 2022

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

Mar, 2018

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

Mar, 2022

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

Mar, 2019

我们介绍了两种算法，用于计算贝叶斯神经网络（BNNs）的概率鲁棒性的严格保证。

Jan, 2024

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

Sep, 2019

本文介绍了一种统一的深度学习模型形式验证的框架，利用分段线性结构和形式方法，结合现有方法的优势以实现两个数量级的加速。并提出了一组新的基准数据集，通过实验比较现有算法并确定影响验证问题难度的因素。

Nov, 2017