FMitF: Track I: Focusing Incremental Abstraction-based Verification on Neural Networks Input Distributions

FMITF：第一轨：专注于神经网络输入分布的增量抽象验证

• 批准号: 2019239
• 负责人: Matthew Dwyer
• 金额: $ 51万
• 依托单位: University of Virginia Main Campus
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-10-01 至 2024-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2019239&HistoricalAwards=false
• 关键词: FMitF; Track; Focusing; Incremental; Abstraction

The promise of machine learning is that it will improve the operation of systems across a variety of domains, such as agriculture, transportation, and medicine. With that promise comes the risk that such systems will not operate as intended, which may lead to harm to individuals or society. The project's impacts are in mitigating these risks by developing practical methods for assuring the correct operation of machine-learning systems. While risk is not unique to systems that incorporate machine learning, such systems present additional challenges to assuring their correct operation. Consider a camera-based driving system that aims to recognize a stop sign. Such a system must correctly identify a sign from among the enormous number of possible images while considering variables, such as, angle, lighting, distance, and any obstructions. Assuring such a system is correct requires evaluating the system on all such images, but it would take many years to evaluate each in turn on even the fastest computer. The project's novelties are in assuring correct behavior for groups of inputs collectively, which promises to make the assurance process practical.This project develops techniques to accelerate verification algorithms for assuring the correct operation of machine-learning models. First, these techniques exploit the fact that the system will only ever be required to consider a small fraction of the set of all possible inputs. Those inputs can be described symbolically and considered in groups to accelerate verification. Second, these techniques exploit the fact that a system may respond to different inputs by performing identical processing. Focusing verification on the processing performed by the system, rather than the inputs that are processed, allows verification to group sets of inputs to further accelerate assurance. The project develops a series of prototype implementations and benchmarks that demonstrate the utility and cost-effectiveness of the research, and that can be leveraged by the broader community for comparative evaluation.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

机器学习的前景是，它将改善农业、交通和医学等各个领域的系统运行。 伴随着这一承诺而来的风险是，这些系统将无法按预期运行，这可能导致对个人或社会的伤害。 该项目的影响是通过开发确保机器学习系统正确运行的实用方法来减轻这些风险。 虽然风险并不是包含机器学习的系统所独有的，但此类系统在确保其正确操作方面存在额外的挑战。 考虑一个基于摄像头的驾驶系统，旨在识别停车标志。 这样的系统必须从大量可能的图像中正确地识别标志，同时考虑变量，例如角度，照明，距离和任何障碍物。 要确保这样一个系统是正确的，需要在所有这些图像上评估该系统，但即使是在最快的计算机上依次评估每个图像也需要许多年。 该项目的创新之处在于确保输入组的正确行为，这有望使保证过程实用化。该项目开发了加速验证算法的技术，以确保机器学习模型的正确操作。 首先，这些技术利用了这样一个事实，即系统只需要考虑所有可能输入的一小部分。 这些投入可以象征性地加以说明，并分组审议，以加速核查。 其次，这些技术利用了这样一个事实，即系统可以通过执行相同的处理来响应不同的输入。 将验证重点放在系统执行的处理上，而不是处理的输入上，允许验证对输入集进行分组，以进一步加速保证。该项目开发了一系列原型实现和基准，展示了研究的实用性和成本效益，并可以被更广泛的社区用于比较评估。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估来支持。

项目成果

Input Distribution Coverage: Measuring Feature Interaction Adequacy in Neural Network Testing

• DOI: 10.1145/3576040
• 发表时间: 2022-12
• 期刊: ACM Transactions on Software Engineering and Methodology
• 影响因子: 4.4
• 作者: Swaroopa Dola;Matthew B. Dwyer;M. Soffa

Distribution Models for Falsification and Verification of DNNs

• DOI: 10.1109/ase51524.2021.9678590
• 发表时间: 2021-07
• 期刊: 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE)
• 作者: Felipe R. Toledo;David Shriver;Sebastian G. Elbaum;Matthew B. Dwyer

Distribution-Aware Testing of Neural Networks Using Generative Models

• DOI: 10.1109/icse43902.2021.00032
• 发表时间: 2021-02
• 期刊: 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE)
• 作者: Swaroopa Dola;Matthew B. Dwyer;M. Soffa