- 使用高效的边界传播和并行计算扩展深度神经网络验证工具的规模
深度神经网络在安全方面的正式验证问题已经扩展到计数版本 (DNN-Verification)，为了在给定安全属性的领域中计算不安全区域的数量。为了解决这个问题的复杂性，本研究提出了一种基于可达性分析、符号线性松弛和并行计算的新策略，以增强现 - 基于状态转换的形式化验证长短期记忆音频分类器
通过使用基于星集的形式验证方法验证音频分类系统，本研究旨在简化长短时记忆结构和卷积变体在音频分类领域中的可及性分析，从而在实际应用中确保准确的信号分类，强调了在噪声对输出分类准确性产生影响的情况下，鲁棒性验证对于确保精确可靠的预测的必要性。
- 比较可微分逻辑用于学习系统的研究预览
通过将背景知识编码为逻辑约束，用可微分逻辑指导学习过程，创造性地满足约束的机器学习模型进行了比较和评估，并提出了未来工作的开放问题。
- 利用大型语言模型发现归纳循环不变量
本文通过使用大语言模型，探索了在自动程序验证中找到归纳循环不变量的新方法，并证明了其可以改进目前的技术水平。
- 在 Rust 中利用大型语言模型进行自动证明合成
基于大型语言模型（LLMs）和静态分析相结合，开发了一个基于 Rust 的形式验证框架 Verus 的原型。通过将验证任务分解为多个较小的任务，迭代地查询 GPT-4，并将其输出与轻量级静态分析相结合，这个原型显著减少了编写入门级证明代码的 - 关于直觉性计算树逻辑的推理
本文定义了直觉主义版本的计算树逻辑，解释了直觉主义逻辑的语义特征，并研究了其在形式验证中的应用，进而定义了直觉主义版本的 CTL 的语法和语义，并研究了该逻辑的一些简单性质。最后，我们证明了在我们定义的直觉主义版本的 CTL 中，一些 CT - 可证明安全系统：控制可达人工通用智能的唯一路径
通过利用先进的人工智能进行形式验证和机械解释，我们描述了人类安全繁荣与强大人工通用智能（AGIs）共存的路径，并主张这是唯一能确保安全可控 AGI 的途径，提出了一系列能推动这个积极结果的挑战问题，并邀请读者一同参与这项工作。
- numpy 快速区间算术工具箱及其在神经网络控制系统形式验证中的应用
本文介绍了一个基于 numpy 的区间分析工具箱，用于神经网络控制系统的形式验证，利用自然包容函数系统地构建了一般映射的区间边界，并通过自然包容函数的组合，提供了一种用于动态神经网络控制器的形式验证的方法。
- 原有表征定理的 Isabelle 形式化
本篇论文基于 Isabelle-verified 事件结构枚举算法，通过对巨大数据库进行跨站数据挖掘，发现了连接看似不相关的数学对象（并发理论中的事件结构和计算生物学中的完整图）的新定理，并通过 Isabelle/HOL 定义和定理进行了形 - 用于验证学习增强自主系统的假设生成
介绍了一种利用自动综合假设的方法，对基于深度神经网络的自主系统的安全属性进行形式化验证，生成最弱的假设并将其用作运行时监视器以保证整个系统的安全性，在一个来自自主飞行器领域的复杂视觉感知 DNN 案例上实现了该方法。
- MULTIGAIN 2.0: 面向多个平均回报、LTL 和稳定状态约束的 MDP 控制器合成
MULTIGAIN 2.0 是 MultiGain 的一个扩展工具，它基于概率模型检查器 PRISM，并在多目标控制器合成方面进行了扩展，不仅支持多维长期平均奖励结构、稳态约束和线性时间逻辑属性的概率系统的形式验证和合成，还提供了寻找有限内 - 两种近似算法的故事：通过欠 - 过估算收紧 DNN 的稳健性验证
本文研究了神经网络鲁棒性的形式化验证，提出了一种新的双重逼近方法，利用激活函数的低估区间来定义紧逼近边界，并将其实现到了名为 DualApp 的工具中，在不同体系结构的深度神经网络基准测试中，DualApp 方法得到了明显的优化
- 软件安全新时代：基于大型语言模型和形式验证的自愈软件
利用大型语言模型和形式验证策略结合的新颖解决方案，自动检测和修复 C 程序中的软件漏洞，成功率高达 80％。
- 基于规格的神经网络简化用于可扩展形式验证
本文提出了一种保守的神经网络缩减方法，该方法能够在验证减小的网络的同时，确保验证原始网络，可以适用于任何类型的激活函数，使得网络能够被缩小到不到原来的 5% 的大小，从而显著减少了验证时间。
- 基于机器学习的密码协议安全验证框架
本文提出了一种利用机器学习进行密码协议安全验证的框架，使用神经网络处理密码协议的结构特征，自动生成数据并利用形式化验证工具分配安全标签。经测试，该方法适用于实际密码协议的验证。
- 神经网络控制器到决策树控制器的精确且具有成本效益的自动转换
将基于神经网络的控制器转换为等效的软决策树控制器，以提高可验证性且减小意外行为的风险。在包含 ReLU 激活函数和 argmax 操作的离散输出 NN 控制器上，提出了一种自动剪枝的精确且高效的转换算法。以 OpenAI Gym 环境中的两 - 可证明边界的神经网络原像
本文介绍了第一个有效的边界传播算法 INVPROP，用于在神经网络的线性约束输出集的原像上验证属性，并可以与分支和限制相结合以实现完整性。我们的算法在安全控制区域量化和神经网络中检测超出分配的输入方面具有应用价值，并且在相同硬件上比先前的工 - 基于 ILP 的量化神经网络形式化验证方法 QVIP
本文提出了一种基于整数线性约束的编码形式，以有效地验证 QNN 的正确性和局部稳健性，从而提高其能源效率和减少计算量。实验证明该方法比现有技术更快两个数量级且可处理更多的验证任务。
- 验证可逆编程用于验证无损压缩
本文介绍了一种基于对称数字系统的无损压缩方法，特别是它们共享编码器和解码器之间的结构，使得可以使用单一可逆函数同时指定两者。我们提出了一种可逆语言 Flipper，它嵌入在 Agda 中，以支持对程序属性的形式化验证。通过 Flipper， - 高维可达性形式化安全保证生成
提供自治系统的正式安全性和性能保证变得越来越重要，本文提出一种提供可达管的可证安全近似解的方法，该方法可以通过计算 DeepReach 解的误差界来进行可达管的修正，并通过基于情景优化的方法来推导 DeepReach 解的误差界等.