本文提出了一种新的基于符号区间传播和变量分裂的分支定界求解器 DPNeurifyFV，该方法采用新的启发式算法来选择区间变量，以改善变量相关性问题，在结合其他改进措施的情况下，可以显著提高深度学习神经网络验证的效率，并在空中碰撞避免网络 ACAS Xu 上实现了运行时改进。

Dec, 2022

DeepCheck 是一种基于程序分析中的符号执行核心思想的新方法，可将 DNN 翻译为一个命令式程序，并在图像分类的上下文中应用，以解决 DNN 分析中的两个有挑战性的问题：1）识别重要像素（用于属性和对抗生成）；2）创建 1 像素和 2 像素攻击，并通过 MNIST 数据集的实验结果显示，DeepCheck 的符号执行方法为 DNN 验证提供了有价值的工具。

Jul, 2018

深度神经网络在安全方面的正式验证问题已经扩展到计数版本 (DNN-Verification)，为了在给定安全属性的领域中计算不安全区域的数量。为了解决这个问题的复杂性，本研究提出了一种基于可达性分析、符号线性松弛和并行计算的新策略，以增强现有的精确和近似 DNN 计数的形式验证的效率。在标准的形式验证基准和现实的机器人场景上进行的实证评估表明，在可扩展性和效率方面都取得了显著的改进，使得这种技术能够用于复杂的机器人应用。

Dec, 2023

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

Mar, 2022

通过引入符号层，神经符号深度神经网络（NS-DNN）结合了感知和逻辑推理的人工智能任务，我们确定并形式化了一个直观的高层原则：符号正确性，该原则可以指导 NS-DNN 的设计和分析。我们证明符号正确性是 NS-DNN 可解释性和迁移学习的必要属性，并提供了一种精确推理和沟通神经符号边界上模型行为的方式，同时揭示了 NS-DNN 训练算法面临的基本权衡，并提供了支持进一步 NS-DNN 发展的框架。

Feb, 2024

利用区间算法和符号区间分析代替 SMT solver，可以更高效地实现对 DNN 的安全性质进行正式验证，ReluVal 系统相比现有最先进的 solver-based 系统 Reluplex，平均可以提升 200 倍验证效率。

Apr, 2018

本研究提出一种基于 Satisfiability Modulo Theory (SMT) 的新型自动化验证框架，旨在保证深度神经网络对于图像操作的安全性，能够发现对于给定操作范围和家族，对抗性样本是否存在，同时比较现有的相关技术。

Oct, 2016

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

Dec, 2023

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

Mar, 2018

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

Mar, 2019