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

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

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.