- 对象检测的形式验证
利用形式验证来确保计算机视觉模型的安全性，针对图像分类进行了拓展，提出一种一般性的方案来证明物体检测模型的鲁棒性，并提供了与最先进的验证工具兼容的实现策略。
- VeriFlow：用于神经网络验证的分布建模
通过 VeriFlow 架构，我们提出了一种以流动密度模型为基础的形式化验证方法，使任何验证方法都能限制其搜索目标数据分布，从而解决了神经网络验证中的假阳性问题。
- FVEL：基于定理证明的大型语言模型互动式形式验证环境
提出了 FVEL，一种与大型语言模型一起进行交互式形式验证的环境，通过将给定的代码转化为 Isabelle 并利用神经自动定理证明来进行验证，利用 Isabelle 中的规则和定理，通过 FVELER 数据集进行评估，结果表明 FVEL 可 - 正式验证的近似策略迭代
我们使用交互式定理证明器 Isabelle/HOL 对一种近似策略迭代算法在因子化马尔可夫决策过程上进行了形式验证。接着，我们展示了如何将形式化的算法细化为可执行的验证实现。所开发的实现方案经过了基准问题的评估，表明其实用性。作为细化的一部 - 结构化主动推理（扩展摘要）
我们介绍了结构化主动推理，这是使用范畴系统理论的一种大规模推演和形式化主动推理。我们将生成模型形式化地表现为 “在接口上” 的系统，并将接口看作通常的马尔科夫毯的组合抽象；而代理是它们生成模型的 ' 控制器 '，与它们形式上是对偶的。这为主 - 验证深度学习对于超出分布领域的泛化能力
通过使用 DNN 验证技术，我们引入了一种新的方法来识别具有稳健泛化能力的 DNN 决策规则，并在真实世界环境中进行了广泛评估，为部署 DNN 驱动系统提供了新的验证目标。
- CVPR基于线性近似的最大池化卷积神经网络的通用鲁棒性验证
使用紧密线性逼近的 MaxLin 技术，本研究提供了一种鲁棒性验证方法，可提高卷积神经网络的认证下界，并在 MNIST、CIFAR-10 和 Tiny ImageNet 数据集上显示出优于现有工具的性能提升。
- 用于安全关键设计中的顺序错误检测和纠错码（ECC）的实用形式验证
复杂纠错码核心的实际形式验证方法，使用多个复杂度降低技术和专业知识，包括使用综合序列版本的电路与 RTL 进行比较的抽象模型作为粘合逻辑，基于 k 归纳的模型检查和使用数学关系作为属性捕获来简化验证，以在 24 小时内获得无界的证明结果。
- 具有不确定节点特征和不确定图结构的图卷积网络的形式验证
该研究论文研究并解决了在安全关键环境中验证神经网络的稳健性和不确定性中的计算依赖关系问题，并使用（矩阵）多项式范围体进行可达性分析验证了其方法在三个流行基准数据集上的有效性。
- 所有人工，更少智能：形式验证透视下的 GenAI
该研究针对以大型语言模型（LLMs）为动力的再生人工智能（AI）中，用 SystemVerilog 编写的硬件设计的 CWE 进行了形式验证。研究发现，大多数 LLMs 在生成硬件代码时并不知道任何硬件 CWE，因此未考虑其安全风险。该研究 - 神经网络中的鲁棒性验证
我们研究了神经网络计算的形式验证问题，探讨了其各种鲁棒性和最小化问题。我们提供了一个理论框架，使我们能够在神经网络中转换安全性和效率问题，并分析它们的计算复杂性。我们发现，在半线性设置中，对于分段线性激活函数和使用求和或最大度量时，大多数问 - 深度强化学习中对抗输入的分析
通过正式验证的视角，我们对敌对输入的特征进行了全面分析，提出了一种新的指标 —— 敌对率，用于划分模型对此类扰动的敏感性，并提供了计算该指标的一系列工具和算法。我们的分析在实证上展示了敌对输入如何影响给定深度强化学习系统在敏感性方面的安全性 - 目标检测的验证 —— IBP IoU
我们介绍了一种新颖的区间边界传播（IBP）方法，用于形式验证物体检测模型，特别针对 IoU 指标。该方法已在名为 IBP IoU 的开源代码中实现，与流行的基于抽象解释的验证工具兼容。我们通过对着陆进场跑道检测和手写数字识别案例研究进行评估 - 神经网络验证的端到端基于集合的训练
神经网络在对抗攻击中容易受到干扰，训练和验证稳健的神经网络是有挑战的，而本论文通过采用端到端的基于集合的训练方法来解决这个问题，该方法使得训练和验证神经网络的稳健性更加简单有效。此外，通过使用集合训练的方法，可以在很多情况下比使用最先进的对 - UR4NNV：神经网络验证，欠估计可达性研究！
该研究介绍了 UR4NNV 验证框架，它首次利用了 DNN 的欠逼近可达性分析方法，针对具有 ReLU 激活函数的 DNN 并采用基于二叉树分支的欠逼近算法。UR4NNV 有效验证 DNN 属性且在达到验证轮数和未能证伪属性时提供置信水平， - 安全飞机滑行的跑道物体分类器的稳健性评估
使用形式验证方法评估了一个用于飞机滑行阶段的图像分类器深度神经网络 (DNN) 在噪声、亮度和对比度以及它们的组合等三种常见图像扰动类型下的鲁棒性，结果表明该分类器对噪声比亮度和对比度扰动更加脆弱。
- 面向 NextG 协议形式验证的自动建模：一种多模态的跨向与自标注意力大语言模型方法
利用 Auto-modeling of Formal Verification with Real-world Prompting for 5G and NextG protocols (AVRE) 系统，通过 Large Language - AAAI朝着高效量化神经网络验证迈进
量化用整数运算取代浮点算术在深度神经网络模型中，从而在设备上提供更高效的推断，降低功耗和内存需求。本文提出了一个框架用于正式验证量化神经网络的特性。我们的基准技术基于整数线性规划，保证了完备性和正确性。然后我们展示了如何利用梯度启发式搜索方 - 验证友好的深度神经网络
提出了一种生成可验证的神经网络（VNNs）的新框架，该框架通过后训练优化在保留预测性能和鲁棒性之间取得平衡，使得生成的网络在预测性能方面与原始网络相当，并且可以进行验证，以更加高效地建立 VNNs 的强大性。
- 物理信息神经网络李雅普诺夫函数：PDE 特征、学习和验证
利用物理相关的神经网络计算李雅普诺夫函数，将李雅普诺夫条件编码为偏微分方程，并使用神经网络函数进行训练，分析了李雅普诺夫和祖博夫偏微分方程的解的解析性质，提供了可以通过可满足性求解器轻松验证的学习到的神经网络李雅普诺夫函数的充分条件，使得局