CheckINN：Imandra 中的宽范围神经网络验证（扩展版）
本文介绍了一种基于 Imandra 的 DNN 验证证明检查器的新实现，该实现通过使用 Imandra 的两个关键功能：无限精度实数算术和形式化验证基础设施来提高数字稳定性和验证性能，并在实现验证正确性属性和性能优化方面继续开展工作。
Jul, 2023
该研究提出了一种基于新颖理论、数据结构和算法设计的增量和完全的 DNN 验证框架，旨在提高完全验证器在更新后的 DNN 上的验证效率。将其实现在名为 IVAN 的工具中，可以在 MNIST 和 CIFAR10 分类器上实现总体几何平均加速比为 2.4 倍，在 ACAS-XU 分类器上实现总体几何平均加速比为 3.8 倍。
Apr, 2023
深度神经网络验证技术的验证进展为 DNN 验证器的广泛应用开辟了道路，提出了在 Marabou DNN 验证器的基础上以 Imandra 为实现语言进行形式保证的 Marabou 证明检查算法的替代实现。
May, 2024
本文介绍了一种针对神经网络控制系统（NNCS）安全验证的新方法，利用归纳不动点方法，并配合自动推断必要的分解谓词的算法，将验证过程从数小时（甚至超时）缩短至几秒钟，在案例研究中显著提高了验证性能。
Dec, 2023
本文讨论了神经网络在安全和保密方面应用的局限性，提出了一些自动推理技术来提供神经网络性能的保障，并且对现有的神经网络自动验证方法进行了综合分类和阐述，同时讨论了存在的局限性以及未来研究的方向。
May, 2018
本研究提出了一种通过使用过度逼近来减小神经网络规模，以提高神经网络验证技术的框架，并使用反例引导调整逼近，以验证大型神经网络。实验证明，该方法对验证大型神经网络具有很大的潜力。
Oct, 2019
提出了一种生成可验证的神经网络（VNNs）的新框架，该框架通过后训练优化在保留预测性能和鲁棒性之间取得平衡，使得生成的网络在预测性能方面与原始网络相当，并且可以进行验证，以更加高效地建立 VNNs 的强大性。
Dec, 2023
为高维自主系统提供行为保证是人工智能安全领域中的一个特别具有挑战性的问题。本文提出了一个基于主动学习、不确定性量化和神经网络验证的新方法，其中的核心是一种称为不精确神经网络的集成技术，它提供了用于引导主动学习的不确定性。通过在多个物理模拟器上对经过增强学习的控制器进行评估，证明了我们的方法可以为高维系统提供有用且可扩展的保证。
Aug, 2023
使用二值化神经网络 (BNNs) 的强化学习算法以提高可验证性的方法，解决了神经网络在安全关键场合应用上不可靠的问题。在训练 Atari 环境中的 BNNs 之后，我们验证了其鲁棒性属性。
Mar, 2022