Compressing neural networks via formal methods

Advancements in Neural Networks have led to larger models, challenging implementation on embedded devices with memory, battery, and computational constraints. Consequently, network compression has flourished, offering solutions to reduce operations and parameters. However, many methods rely on heuristics, often requiring re-training for accuracy. Model reduction techniques extend beyond Neural Networks, relevant in Verification and Performance Evaluation fields. This paper bridges widely-used reduction strategies with formal concepts like lumpability, designed for analyzing Markov Chains. We propose a pruning approach based on lumpability, preserving exact behavioral outcomes without data dependence or fine-tuning. Relaxing strict quotienting method definitions enables a formal understanding of common reduction techniques.