本研究提出了一种基于 Markov 决策过程、混合整数线性规划、熵式细化和概率模型检验的抽象方法，用于验证深度强化学习中的概率策略，并在一些强化学习基准测试上验证了其有效性。
Jan, 2022
本文提出了一种通用的神经网络形式验证框架，通过将验证问题转化为最优化问题，并通过我们提出的松弛算法得到可靠的上界，从而可对神经网络的输入和输出属性满足的规范进行形式化验证。
Mar, 2018
本文调查了最近出现的，从可达性分析、优化和搜索中获得的洞见的方法，以确保设计的深度神经网络满足特定的输入输出属性。 我们讨论了现有算法之间的根本差异和联系。 此外，我们提供了现有方法的教学实现，并在一组基准问题上进行了比较。
Mar, 2019
用具有适当启发式条件的一组算法基于神经网络的输出分布来验证其概率，同时计算和迭代优化神经网络输出概率的下界和上界，并通过应用非概率性神经网络验证中的最先进的边界传播和分支约束技术，显著提高了解决时间。
May, 2024
本研究提出了一种新颖的深度概率模型的生成式公式，该公式实现了对其函数动态的 “软” 约束。通过随机变分推断建模的函数及其给定阶数的导数受到不等式或等式约束，进而表征模型和约束参数的后验分布，使得所提出的方法可以准确可伸缩地量化预测和所有参数的不确定性。在普通微分方程模型的参数推断和计数数据单调回归问题中，展示了等式约束和不等式约束的应用。该方法在多种实验环境中进行了广泛测试，并在具有挑战性的建模应用中取得了非常有竞争力的结果，同时提供了高度的表达性、灵活性和可伸缩性。
Feb, 2018
应用深度生成模型通过物理学定理来传递极高复杂物理系统中的不确定性。我们构建出一个隐式变分推断公式，并顺利地运用物理学原理作为模型输出的约束条件。这让模型在面对高成本数据采集以及通常小型训练数据集的物理系统建模时具备了一种可扩展的方法来描述随机输入或观测和物理系统输出的不确定性，并以传输动态为规范示例来验证了方法的有效性。
Dec, 2018
提出了一种生成可验证的神经网络（VNNs）的新框架，该框架通过后训练优化在保留预测性能和鲁棒性之间取得平衡，使得生成的网络在预测性能方面与原始网络相当，并且可以进行验证，以更加高效地建立 VNNs 的强大性。
Dec, 2023
本文介绍了一种统一的深度学习模型形式验证的框架，利用分段线性结构和形式方法，结合现有方法的优势以实现两个数量级的加速。并提出了一组新的基准数据集，通过实验比较现有算法并确定影响验证问题难度的因素。
Nov, 2017
本文分析了得分估计器作为最基础和多功能的变分推理算法，并利用语义学和程序分析中的工具来阐述这个算法在程序中的作用，揭示出算法所做假设的内在局限性，提出了证明这些假设的规则，并用非平凡的连续数学事实来代替假设中的积分要求，最终发展了一种运用静态程序分析来满足假设条件的方法，并应用于 Pyro 中的八个代表性模型中，表明这种方法是可行的。
Jul, 2019
该研究提出了一种概率证明框架 PROVEN，用于验证神经网络在输入加噪时的鲁棒性，可证明分类器的 top-1 预测在受限的 Lp 范数扰动下不会发生改变，证书是基于现有的神经网络鲁棒性验证框架，该方法在 MNIST 和 CIFAR 神经网络模型的实验中取得了 75% 的提升。