Gaussian Mixture Models (GMMs) are powerful tools for representing arbitrary distributions or data sets, especially in complex non-linear systems. They are often used as approximators due to their flexibility. However, in many cases, such as for dynamical systems, these must be propagated through non-linear functions. How we can do this is still an open problem.
In this work, we propose a scalable method for quantizing GMMs with formal bounds on the approximation error using the Wasserstein distance. This ensures the method is suitable for safety-critical applications such as autonomous vehicles and UAVs, where formal guarantees are essential. Our approach, called the multi-grids method, constructs local grids at locations of high density, which are identified using clustering techniques. Around each cluster, a hyperrectangular grid is formed, and the locations are placed ensuring minimal error in terms of the Wasserstein distance. This design allows the method to scale efficiently to GMMs of large sizes in terms of both the dimension and the number of components, a known limitation of existing methods.
We validate our method against the state of the art, across various settings, demonstrating significantly lower approximation errors in terms of the Wasserstein distance. Even at higher dimensions of 60 it can still find efficient quantizations with little computational costs. Additionally, we apply the multi-grids method to the uncertainty propagation problem in dynamical systems, including the benchmark Dubins Car, highlighting its practical effectiveness in real-time systems.

Bayesian Neural Networks (BNNs) offer uncertainty quantification but are computationally expensive, limiting their practical deployment. This paper introduces a neuron-level pruning framework that reduces BNN complexity while preserving predictive performance. Unlike existing weight-level pruning techniques, our approach removes entire neurons, enabling significant memory savings and inference speedups without requiring specialized hardware. We propose a pruning loss based on the Wasserstein distance, balancing model sparsity and predictive accuracy. Our method is fully automatic, eliminating the need for manual hyperparameter tuning. Experimental results on UCI regression and Fashion MNIST datasets demonstrate that our framework can prune over 80% of neurons while maintaining predictive distribution integrity. Additionally, we validate the Lottery Ticket Hypothesis in the Bayesian setting, showing that pruned subnetworks retain performance and learn faster when retrained. This work represents a step toward making BNNs more scalable for real-world applications.

The use of machine learning (ML), especially neural networks, in modeling control systems has shown promise, particularly for systems with complex physics. However, applying these models in safety-critical areas requires reliable verification and control synthesis methods due to their inherent complexity. Formal methods, using stochastic finite state models like interval Markov decision processes (IMDPs), provide a way to analyze and verify these systems against detailed safety and performance specifications defined using linear temporal logic over finite traces (LTLf). Abstraction of ML models into such IMDPs, allows the deriving of formal guarantees on the IMDP that carryover to the underlying ML model.

This thesis focuses on designing a switched controller for a cart-pendulum system using neural network dynamic models (NNDM) by formal control synthesis, validating it through formal verification methods. The methodology includes modeling the system behavior under different controllers, abstracting these models into IMDPs, applying the respective formal methods, and validating the approach through experiments. The aim is to demonstrate the framework's utility in a practical context, comparing different neural network architectures and researching the applicability of formal guarantees to both the models and the actual system.

The main contributions are a practical application of the framework to a specific system, a comparison of neural network architectures for dynamic modeling, and an experiment-based validation of the framework's effectiveness. It confirms that the formal guarantees for abstracted models are relevant to the actual system, providing insights into the framework's potential for real-world applications. The findings suggest areas for further research, particularly in making such frameworks more accessible for practical deployment in safety-critical systems.