下一代 AI 系统需要强有力的安全保证。本报告研究了神经网络和相关内存安全性质的软件实现，包括空指针引用、越界访问、double-free 和内存泄漏。我们旨在检测这些漏洞，并借助大型语言模型自动修复它们。为此，我们首先通过程序突变的自动化过程，将现有的神经网络代码数据集 NeuroCodeBench 的规模扩大到约 81k 个程序。然后，我们使用最先进的软件验证器 ESBMC 验证突变的神经网络实现的内存安全性。每当 ESBMC 发现漏洞时，我们会调用一个大型语言模型来修复源代码。在最新的任务中，我们比较了各种最先进的提示工程技术，以及重复调用大型语言模型的迭代方法的性能。

May, 2024

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

Mar, 2022

CTBENCH 是一个统一的库和高质量的基准测试，用于证明训练。通过在公平设置和系统调整的超参数下评估所有算法，CTBENCH 展示了几乎所有算法超越了文献中所报道的性能，并建立了新的最先进方法，同时揭示了近期算法的优势在强化基线后明显减弱。基于 CTBENCH，我们为当前的证明训练状态提供了新的见解，并提出了未来的研究方向。我们相信 CTBENCH 将成为证明训练未来研究的基准和测试平台。

Jun, 2024

利用神经网络的数学定理证明、代码验证和自动化定理证明等领域的研究，提出了一个测试用例，旨在进一步发展形式验证代码的自动定理证明。

Jun, 2024

本文提出一种基于混合整数线性规划的框架，首次在电力系统应用中验证神经网络行为，能够确定神经网络分类为安全或不安全的输入范围，并且能够系统地识别对抗性示例，从而提高神经网络在电力系统中的鲁棒性和可靠性。

Oct, 2019

本研究提出了一种通过使用过度逼近来减小神经网络规模，以提高神经网络验证技术的框架，并使用反例引导调整逼近，以验证大型神经网络。实验证明，该方法对验证大型神经网络具有很大的潜力。

Oct, 2019

本书介绍了形式验证的基本概念及其在神经网络和深度学习中的应用，以保证其安全性、健壮性和正确性。

Sep, 2021

本文介绍了神经形态计算中的基准测试 NeuroBench 及其目标，以促进该领域的技术进步和统一标准，该基准测试是由学术界和工业界的成员共同制定的。

Apr, 2023

本文介绍神经网络验证（NNV）软件工具，该工具为深度神经网络（DNN）和学习启用的控制系统（CPS）提供了一套基于集合的验证框架。NNV 的核心是一组可达性算法，这些算法利用了多种集合表示，例如，多面体、恒星集、zono topes 和抽象域表示。

Apr, 2020

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

Dec, 2023