支持黑盒模型输入约束形式化验证与确认的负选择方法
机器学习
2022-09-07 v1
摘要
从划分的输入空间生成不安全子需求,以支持黑盒模型形式化验证的验证引导测试用例,对研究者而言是一个具有挑战性的问题。搜索空间的大小使得穷举搜索在计算上不可行。本文研究了一种元启发式方法,用于在划分的输入空间中搜索不安全候选子需求。我们提出一种负选择算法(NSA)用于在给定的安全属性内识别候选不安全区域。NSA 算法的元启发式能力使其能够在验证这些区域的子集时估计广阔的不安全区域。我们利用划分输入空间的并行执行来生成安全区域。基于安全区域先验知识的 NSA 用于识别候选不安全区域,随后使用 Marabou 框架验证 NSA 结果。我们的初步实验与评估表明,当使用 Marabou 框架以高精度验证时,该过程能找到候选不安全子需求。
引用
@article{arxiv.2209.01411,
title = {Negative Selection Approach to support Formal Verification and Validation of BlackBox Models' Input Constraints},
author = {Abdul-Rauf Nuhu and Kishor Datta Gupta and Wendwosen Bellete Bedada and Mahmoud Nabil and Lydia Asrat Zeleke and Abdollah Homaifar and Edward Tunstel},
journal= {arXiv preprint arXiv:2209.01411},
year = {2022}
}