FMitF: Track I: Generative Neural Network Verification in Medical Imaging Analysis

医学图像，如计算机断层扫描（CT）和磁共振成像（MRI）扫描，通常使用计算机和软件进行转换和分析。医学图像越来越多地使用人工智能和机器学习方法（如深度神经网络）进行处理和分析。在这些安全关键领域，严格保证这些机器学习方法的行为是必不可少的，但最近的许多研究表明，这些方法存在风险，例如缺乏鲁棒性和偏见。神经网络形式化验证正在成为一种为这些机器学习模型提供保证以精确表征其行为的方法。本项目的新颖之处在于为医学图像分析任务开发一个神经网络形式规范和验证框架，将其应用于确保整个医学图像分析技术堆栈的规范，并在两个特定的医学图像分析任务上对其进行评估。第一个图像分析任务是从多发性硬化症患者的mri中分割脑病变，这是将mri的不同区域自动表征为相应的解剖结构的过程。第二个图像分析任务是图像合成，用于对视网膜的光学相干断层扫描（OCT）进行降噪。该项目的影响是通过正式验证增强对机器学习模型的信心，从而实现医学成像分析。除了将这些正式方法开发和应用于医学成像分析之外，该项目的结果可能会提高其他领域的可信度，例如自主系统中的感知和传感组件。目前开发的大多数神经网络验证方法仅适用于简单的计算机视觉任务，如图像分类，而医学图像分析通常需要更复杂的生成计算机视觉方法来解决更复杂的任务，如语义分割、实例分割和图像合成。在医学影像分析的背景下，为这些生成式计算机视觉任务开发正式的方法是这个项目的核心。该项目的第一个主要目标是开发一个鲁棒性规范框架，建立在对抗扰动的鲁棒性、规范挖掘和用于生成任务的计算机视觉度量的基础上。第二个主要目标是开发形式验证方法，建立在神经网络的可达性分析的基础上，特别是开发生成模型中使用的上采样层的可达性方法。第三个主要目标是考虑图像合成生成模型的鲁棒性，例如通过生成对抗网络（GAN）过程训练的模型。第四个主要目标是评估这些规范和验证方法对MS病变分割和OCT图像合成去噪任务的影响。研究人员将组织相关的竞赛和挑战，例如继续进行神经网络验证竞赛（VNN-COMP）和IEEE ISBI纵向MS病变分割挑战赛，并将基于该项目的研究和结果为形式方法、机器学习、计算机视觉和医学成像分析研究社区制定基准。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Medical images, such as computed tomography (CT) and magnetic resonance imaging (MRI) scans, are routinely transformed and analyzed using computers and software. Medical images are increasingly processed and analyzed with artificial-intelligence and machine-learning methods, such as deep neural networks. In such safety-critical domains, stringent guarantees on the behaviors of these machine-learning methods are essential, but many recent studies have shown risks with these methods, such as lack of robustness and bias. Neural-network formal verification is emerging as an approach to provide guarantees on these machine-learning models to precisely characterize their behaviors. This project's novelties are to develop a neural-network formal-specification and -verification framework for medical-image analysis tasks, apply it to ensure specifications across the medical-image-analysis technology stack, and evaluate it on two specific medical-imaging analysis tasks. The first image-analysis task is the segmentation of brain lesions from MRIs of multiple-sclerosis patients, which is the process of automatically characterizing different regions of the MRIs into corresponding anatomic structures. The second image-analysis task is image synthesis for denoising optical-coherence-tomography (OCT) scans of the retina. The project's impacts are to enable medical-imaging analysis by enhancing confidence in the machine-learning models through formal verification. Beyond the development and application of these formal methods to medical-imaging analysis, the results of this project may enhance trustworthiness in other domains, such as perception and sensing components in autonomous systems.Most neural-network verification methods developed so far are applicable only to simple computer-vision tasks, such as image classification, whereas medical image analysis typically requires more sophisticated generative computer-vision methods to solve more sophisticated tasks, such as semantic segmentation, instance segmentation, and image synthesis. Developing formal methods for these generative computer-vision tasks in the context of medical-imaging analysis is the core of this project. The first major objective of the project is to develop a robustness-specification framework, building on robustness to adversarial perturbations, specification mining, and metrics from computer vision used for generative tasks. The second major objective is to develop the formal-verification methods, building on reachability analysis of neural networks, specifically developing reachability methods for up-sampling layers used in generative models. The third major objective is to consider the robustness of generative models for image synthesis, such as those trained through generative-adversarial-network (GAN) processes. The fourth major objective is to evaluate these specification and verification methods on the MS lesion segmentation and OCT image-synthesis denoising tasks. The researchers will organize relevant competitions and challenges, such as continuing the Verification of Neural Networks Competition (VNN-COMP) and the IEEE ISBI Longitudinal MS Lesion Segmentation Challenge, and will develop benchmarks for the formal-methods, machine-learning, computer-vision, and medical-imaging-analysis research communities based on the research and results of this project.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.