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.