Neural Network (NN) abstraction is a technique for reducing the size of an NN while ensuring that, if a property of interest holds on the smaller NN, it also holds on the original one; thus, an abstraction should provide an overapproximation of the original NN, either directly or through error bounds. This allows, for example, faster verification of NNs, as verification tools are often not scalable. Several works have been proposed for creating such abstractions. For example, [1,2] use the neuron activation values to group neurons that compute similar values for a given set of inputs. The groups of neurons are then merged. While [2] does not provide any formal guarantees, [1] provides an error estimation for a particular verification technique. Given a property, [3] can be applied such that the abstracted network will over-approximate the original network with respect to the property: for every input, if the property holds in the abstract network, it holds in the original network. This is not necessarily correct for [1] or [2].

In this thesis, we want to investigate the possibility of combining [3] with [1]. The student shall implement a new algorithm using closeness, as defined in [1], for identifying neurons to combine in the overall procedure outlined in [3]. Depending on the success of this method, we can incorporate [2], a complex improvement of [1], or work on an abstraction refinement step. Experiments shall be conducted to evaluate the improvements achieved.