一句话：提出 HOBAT 框架，通过将一批同构神经网络中同位置神经元抽象为单个神经元并迭代精化，实现批量形式化验证。
持续学习使神经网络能不断纳入新数据并更新，但同时会产生一批候选网络用于软件迭代。现有方法多依赖经验性精度测试来筛选，缺乏对整批网络的形式化保证，尤其在对抗样本下。基于约束求解、区间传播和线性近似的验证技术虽能提供形式保证，却只针对单个网络。本文分析若干非传统机器学习范式对应的批量验证问题，提出 HOBAT 框架：在同构结构神经网络的合理假设下，将一批网络中相同位置的神经元抽象为单个神经元，再通过迭代精化恢复精度，直至满足待验证属性。该方法与单网络上的边界传播验证正交。作者将其与边界传播验证集成，实验表明相比原始方法有显著提升，并展现出大数据时代验证大批量网络的巨大潜力。
The rapid development of deep learning has significantly transformed the ecology of the software engineering field. As new data continues to grow and evolve at an explosive rate, the challenge of iteratively updating software built on neural networks has become a critical issue. While the continuous learning paradigm enables networks to incorporate new data and update accordingly without losing previous memories, resulting in a batch of new networks as candidates for software updating, these approaches merely select from these networks by empirically testing their accuracy; they lack formal guarantees for such a batch of networks, especially in the presence of adversarial samples. Existing verification techniques, based on constraint solving, interval propagation, and linear approximation, provide formal guarantees but are designed to verify the properties of individual networks rather than a batch of networks. To address this issue, we analyze the batch verification problem corresponding to several non-traditional machine learning paradigms and further propose a framework named HOBAT (BATch verification for HOmogeneous structural neural networks) to enhance batch verification under reasonable assumptions about the representation of homogeneous structure neural networks, increasing scalability in practical applications. Our method involves abstracting the neurons at the same position in a batch of networks into a single neuron, followed by an iterative refinement process on the abstracted neuron to restore the precision until the desired properties for verification are met. Our method is orthogonal to boundary propagation verification on a single neural network. To assess our methodology, we integrate it with boundary propagation verification and observe significant improvements compared to the vanilla approach. Our experiments demonstrate the enormous potential for verifying large batches of networks in the era of big data.