Ensuring Machine Learning Generalization in Avionics Using Formal Methods

Generalization in machine learning refers to the ability of a model to perform well on unseen data—that is, input data it has not encountered during training. Establishing a bound on generalization error is important for ensuring the absence of unintended behaviors—an essential requirement in safety-critical systems and software. While such bounds are typically derived through statistical methods with associated confidence levels, this session explores a formal approach that offers rigorous mathematical guarantees.

Specifically, Collins Aerospace presents a method to evaluate the generalization capability of machine learning models—particularly neural networks approximating functions over low-dimensional, well-defined, and bounded input spaces—using formal verification techniques. This approach involves iteratively partitioning the input space into regions at various resolutions. For each region, a property is defined asserting that the neural network’s error at any point within the region remains below a specified threshold. Verifying this property constitutes a formal guarantee of generalization within that region.

An abstract interpretation solver was used to verify these properties across the entire partitioned input space. Regions where verification fails are refined by sampling or generating new data, creating more granular partitions guided by heuristics that minimize data generation. The effectiveness of this method is demonstrated by formally verifying the generalization of a neural network–based avionics function.