摘要:约束求解是验证神经网络的基础方法. 在人工智能安全领域, 为了修复或攻击等目的, 常常需要对神经网络的结构和参数进行修改. 面对此类需求, 本文提出神经网络的增量验证问题, 旨在判断修改后的神经网络是否仍保持安全性质. 针对这类问题, 我们基于Reluplex框架提出了一种增量可满足性模理论算法DeepInc. 该算法利用旧求解过程中关键计算格局的特征, 启发式地检查关键计算格局是否适用于证明修改后的神经网络. 实验结果显示, DeepInc的效率在大多数情况下都优于Marabou. 此外, 即使与最先进的验证工具α,β-CROWN相比, 对于修改前后均未满足预设安全性质的网络, DeepInc也实现了显著的加速.

摘要:极小不可满足子集(minimal unsatisfiable subsets, MUS)的求解是布尔可满足性问题中的一个重要子问题. 对于一个给定的不可满足问题, 其MUS的求解能够反映出问题中导致其不可满足的关键原因. 然而, MUS的求解是一项极其耗时的任务, 不同的剪枝过程将直接影响到搜索空间的大小、算法的迭代次数, 从而影响算法的求解效率. 提出一种针对MUS求解的加强剪枝策略ABC (accelerating by critical MSS), 依据MSS、MCS、MUS这3者之间的对偶性和碰集关系特点, 提出cMSS和subMUS概念, 并总结出4条性质, 即每个MUS必是subMUS的超集, 进而在避免对MCS的碰集进行求解的情况下有效利用MUS和MCS互为碰集的特征, 有效避免求解碰集时的时间开销. 当subMUS不可满足时, 则subMUS是唯一的MUS, 算法将提前结束执行; 当subMUS可满足时, 则剪枝掉此节点, 进而有效避免对求解空间中的冗余空间进行搜索. 同时, 通过理论证明ABC策略的有效性, 并将其应用于目前最高效的单一化模型算法MARCO和双模型算法MARCO-MAM, 在标准测试用例下的实验结果表明, 该策略可以有效地对搜索空间进行进一步剪枝, 从而提高MUS的枚举效率.

摘要:软件产品线测试是一项非常具有挑战性的工作. 基于相似性的测试方法通过提升测试集的多样性以达到提高测试覆盖率和缺陷检测率的目的. 因其具有良好的可拓展性和较好的测试效果, 目前已成为软件产品线测试的重要手段之一. 在该测试方法中, 如何产生多样化的测试用例和如何维护测试集的多样性是两个关键问题. 针对以上问题, 提出一种基于多样性可满足性(SAT)求解器和新颖性搜索(novelty search, NS)的软件产品线测试算法. 具体地, 所提算法同时采用两类多样性SAT求解器产生多样化的测试用例. 特别地, 为了改善随机局部搜索SAT求解器的多样性, 提出一种基于概率向量的通用策略产生候选解. 此外, 为同时维护测试集的全局和局部多样性, 设计并运用两种基于NS算法思想的归档策略. 在50个真实软件产品线上的消融和对比实验验证多样性SAT求解器和两种归档策略的有效性, 以及所提算法较其他主流算法的优越性.

摘要:人工智能技术已被广泛应用于生活中的各个领域. 然而, 神经网络作为人工智能的主要实现手段, 在面对训练数据之外的输入或对抗攻击时, 可能表现出意料之外的行为. 在自动驾驶、智能医疗等安全攸关领域, 这些未定义行为可能会对生命安全造成重大威胁. 因此, 使用完备验证方法证明神经网络的性质, 保障其行为的正确性显得尤为重要. 为了提高验证效率, 各种完备神经网络验证工具均提出各自的优化方法, 但并未充分探索这些方法真正起到的作用, 后来的研究者难以从中找出最有效的优化方向. 介绍神经网络验证领域的通用技术, 并提出一个完备神经网络验证的通用框架. 在此框架中, 重点讨论目前最先进的工具在约束求解、分支选择与边界计算这3个核心部分上的所采用的优化方法. 针对各个工具本身的性能和核心加速方法, 设计一系列实验, 旨在探究各种加速方式对于工具性能的贡献, 并尝试寻找最有效的加速策略和更具潜力的优化方向, 为研究者提供有价值的参考.

摘要:工作流可满足性是业务安全规划的基本问题, 正在面临高资源配比(资源数n显著大于步骤数k)造成的性能挑战. 在资源独立约束下, 其最高效求解途径是模式空间上的增量回溯法IPB. 为克服结点真实性验证的性能瓶颈, 它增量计算模式k指派(二部)图及其(左完备)匹配, 分别需要O(kn)和O(k2)时间. 利用父子模式的原子差异增量计算完全指派图, 只需O(n)时间, 特别是其实际性能, 将随模式块规模增长迅速提高. 但该图的O(kn)规模导致了同样的增量匹配时间. 进而引入完备k核心匹配概念, 证明其存在性等价于左完备匹配, 且其增量计算时间为O(k2). 由此, 建立了时间复杂度更低的最小增量模式回溯法. 在含互斥和两种全局值势约束而授权比例约为1/4的扩展公开实例集上进行实验, 结果表明: 当n/k=10(及n/k=100), 而k变化时, 该方法较IPB有平均超过2(及5)倍、最低1.5(及2.9)倍的性能优势; 当k=18(及k=36), 而n/k=2~4096(及n/k=2~2048)时, 该方法有平均超过2.6(及3.6)倍优势; 而较2021年Minizinc挑战赛的冠军求解器Google OR-Tools CP-SAT, 该方法最低有超过3倍优势.

摘要:分离逻辑是经典霍尔逻辑的针对操作指针和动态数据结构的扩展，已经广泛用于对基础软件（比如操作系统内核等）的分析与验证.分离逻辑约束自动求解是提升对操作指针和动态数据结构的程序的验证的自动化程度的重要手段.针对动态数据结构的验证一般同时涉及形状性质（比如单链表、双链表、树等）和数据性质（比如有序性、数据不变性等）.主要介绍能对动态数据结构的形状性质与数据约束进行融合推理的分离逻辑求解器COMPSPEN.首先介绍COMPSPEN的理论基础，包括能够同时描述线性动态数据结构的形状性质和数据约束的分离逻辑子集SLIDdata、SLIDdata的可满足性和蕴涵问题的判定算法.然后，介绍COMPSPEN工具的基本框架.最后，使用COMPSPEN工具进行了实例研究.收集整理了600个测试用例，在这600个测试用例上将COMPSPEN与已有的主流分离逻辑求解器Asterix、S2S、Songbird、SPEN进行了比较.实验结果表明COMPSPEN是唯一能够求解含有集合数据约束的分离逻辑求解器，而且总体来讲，能对线性数据结构上的同时含有形状性质和线性算术数据约束的分离逻辑公式的可满足性问题进行高效的求解，另外，也能对蕴涵问题进行求解.

摘要:近年来，形式化验证技术受到了越来越多的关注，它在保障安全关键领域系统的安全性和正确性方面发挥着重要的作用.模型检测作为形式化验证中自动化程度较高的分支，具有十分广阔的发展前景.研究并提出了一种新的模型检测技术，可以有效地对迁移系统进行模型检测，包括不安全性检测和证明安全性.与现有的模型检测算法不同，提出的基于不可满足核（unsatisfied core，UC）的近似逼近可达性分析（UC-based approximate incremental reachability，UAIR），主要利用不可满足核来求解一系列的候选安全不变式，直至生成最终的不变式，以此来实现安全性证明和不安全性检测（漏洞查找）.在基于SAT求解器的符号模型检测中，使用由可满足性求解器得到的UC构造候选安全不变式，如果迁移系统本身是安全的，得到的初始不变式只是安全不变式的一个近似.然后，在检查安全性的同时，逐步改进候选安全不变式，直到找到一个真正的不变式，证明系统是安全的；如果系统是不安全的，该方法最终可以找到一个反例证明系统是不安全的.作为一种全新的方法，利用不可满足核进行安全性模型检测，取得了相当好的效果.众所周知，模型检测领域没有绝对最好的方法，尽管该方法在基准的可解数量上无法超越当前的成熟方法，例如IC3，CAR等，但是该方法可以解出3个其他方法都无法解出的案例，相信本方法可以作为模型检测工具集很有价值的补充.

摘要:分布式系统在计算环境中发挥重要的作用, 其中的共识协议算法用于保证节点间行为的一致性. 共识协议的设计错误可能导致系统运行故障, 严重时可能对人员和环境造成灾难性的后果, 因此保证共识协议设计的正确性非常重要. 形式化验证能够严格证明设计模型中目标性质的正确性, 适合用于验证共识协议. 然而, 随着分布式系统的规模增大, 问题复杂度提升, 使得分布式共识协议的形式化验证更为困难. 采用什么方法对共识协议的设计进行形式化验证、如何提升验证规模, 是共识协议形式化验证的重要研究问题. 对目前采用形式化方法验证共识协议的研究工作进行调研, 总结其中提出的重要建模方法和关键验证技术, 并展望该领域未来有潜力的研究方向.

摘要:布尔可满足性求解能够验证的问题规模通常受限,因此,如何高精度地预测其可满足性既是重要的研究问题,也是一项具有挑战性的工作.相关研究工作一般使用由文字节点和子句节点组成的图来表示布尔可满足性问题的结构,但是这种表征方法缺少了变量、子句之间的重要关系信息.在所提方法中,通过将原始布尔可满足性问题实例表征为多关系异构图的方式来表达变量和句子之间的关系,并设计使用消息传递关系网络模型来捕获实例的关系信息,提取了更多的结构特征.结果表明:该模型在预测精度、泛化能力和资源需求等方面均优于现有模型,对所选数据集的平均预测精度为81%.该模型在小规模问题(变量数为100)上训练,在大规模数据集上预测的平均预测精度达到了80.8%.同时,该模型对随机生成的非均匀随机问题的预测精度达到99%,这意味着它学习了预测可满足性的重要特征.此外,模型预测所花费的时间随着问题规模的增大也只是成线性增长.总结而言,基于关系消息传递网络提出了一个预测精度更高、泛化能力更好的布尔可满足性预测方法.

摘要:信念传播算法是基于因子图模型的消息传递算法，通过图中的边，将消息从一个结点传递给另一个结点，以高概率地确定部分变量的取值，这种方法被实验证明在求解可满足性问题时非常有效.然而，目前还未对其有效性从理论角度给予解释.通过对信念传播算法的收敛性分析，试图从理论上解释算法的有效性.在信息传播算法的信息迭代方程中，参数的取值范围为（0，1），将该取值范围扩展到整个实数空间，即（-∞，+∞）.利用压缩函数的数学原理，得到了信息迭代方程收敛的判定条件.选取随机可满足性问题实例进行实验模拟，验证了结论的正确性.