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

机器学习的前景是，它将改善各种领域的系统运行，如农业、交通和医学。这一承诺带来的风险是，这些系统可能无法按预期运行，从而可能对个人或社会造成伤害。该项目的影响在于通过开发确保机器学习系统正确运行的实用方法来降低这些风险。虽然风险并不是包含机器学习的系统所独有的，但这类系统为确保其正确运行带来了额外的挑战。考虑一个基于摄像头的驾驶系统，它的目标是识别停车标志。这样的系统必须在考虑角度、光线、距离和任何障碍物等变量的同时，从大量可能的图像中正确地识别出一个标志。确保这样的系统是正确的，需要在所有这样的图像上评估系统，但是即使在最快的计算机上轮流评估每个图像也需要很多年的时间。项目的新颖之处在于确保输入组的正确行为，这保证了保证过程的实用性。该项目开发了加速验证算法的技术，以确保机器学习模型的正确运行。首先，这些技术利用了这样一个事实，即系统只需要考虑所有可能输入集合中的一小部分。这些输入可以用符号来描述，并分组考虑以加速验证。其次，这些技术利用了一个事实，即系统可以通过执行相同的处理来响应不同的输入。将验证集中在系统执行的处理上，而不是被处理的输入上，允许验证对输入集进行分组，以进一步加速保证。该项目开发了一系列原型实现和基准，展示了研究的效用和成本效益，并可由更广泛的社区用于比较评估。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.