Defended dissertations

Collective decision-making plays a vital role in multi-agent systems, political science, and economics. From voting systems and resource allocation to team formation, these problems share a common structure: a group of agents, each with individual preferences, must reach a joint decision. The field of (computational) social choice offers a rigorous mathematical framework for analyzing such processes and formalizing what constitutes a best outcome, while also investigating the computational challenges involved. Given the inherent complexity of aggregating diverse---and sometimes conflicting---preferences, it is no surprise that many of these problems are computationally intractable. Yet, because they arise in practical and socially significant contexts, finding viable solutions remains essential. Various approaches exist to address their complexity. This dissertation thesis builds on the observation that not all instances of hard problems are equally difficult. We adopt the lens of parameterized complexity, a framework that provides tools to identify (structural) restrictions under which efficient algorithms are possible. Our main contribution is a detailed parameterized analysis of five foundational problems in computational social choice. We begin with control by deleting projects in participatory budgeting---a generalization of multiwinner voting. Next, we investigate the fair assignment of delivery orders in the modern gig economy. Then, we study two classes of coalition formation games, each reflecting distinct facets of collective decision-making. Finally, we propose a computational model for assigning refugees to communities in a way that respects the preferences of both the newcomers and the inhabitants already living in the city.

Virtual reality is one of the fastest-growing fields in today's technology. The visual quality, the field of view, the time-warping, it all gets better and better every day. However, there is also one other important aspect of virtual reality that is not talked about that often, and yet it should – user interface. After several decades of being dependent only on a mouse and keyboard – devices which prevailed as controllers for personal computers – we finally can use other methods of input. To control the virtual environment, we can even use other parts of our body than hands – for example, utilize eyesight for eye-tracking or let our own feet carry us around the virtual world. This dissertation thesis deals with hand-tracking controllers for virtual reality. The goal is to create an intuitive controller with the use of optical sensors so the user does not have to hold or wear any device to interact with the virtual world. We proposed and implemented a set of algorithms to fuse the tracking data from multiple optical hand-tracking sensors that provide greater precision and tracking possibilities than a single optical sensor ever could. We tested our approach both in terms of precision and speed of algorithms and its usability in real-life scenarios. In all the tests, our approach outperformed the current state-of-the-art.

There is a lot of data everywhere, on the internet, in science, etc. But unannotated data themselves are of little value. The goal of this dissertation is to improve active deep learning for eicient and reliable annotation of large data sets, with a particular emphasis on astronomical spectra. To validate the suitability of active deep learning for large data sets of astronomical spectra, we applied an active deep learning method to discovery of rare astronomical objects. This method, which combines a convolutional neural network with active learning, successfully discovered a number of new objects, even though we did not have a large and representative training set. The success of active deep learning depends on predictive uncertainties, so we next explored methods for quantifying them. We developed two probabilistic methods: one for predicting spectroscopic redshift using the Monte Carlo dropout and the other for predicting the atmospheric properties of exoplanets using the deep ensemble method. However, predictive uncertainties must be reliable. Therefore, we have developed a method that facilitates the diagnosis of the causes of potential problems with these predictive uncertainties. This method uses an interpreter of a probabilistic integral transform histogram to facilitate this diagnosis. Overall, this dissertation advances the field of active deep learning and predictive uncertainties evaluation with potential applications beyond astronomy to any field with large data sets.

Recommender systems play a pivotal role in managing and personalizing vast amounts of data across domains such as e-commerce, entertainment, and social media. This thesis addresses two critical challenges in modern recommender systems: scalability in linear shallow autoencoders and the integration of semantic and interaction-based similarities using Transformer architectures. Building on the Embarrassingly Shallow Autoencoder (EASE), we introduce ELSA, a scalable linear shallow autoencoder designed to overcome the limitations of EASE on datasets with a large number of items. By leveraging a low-rank decomposition of the weight matrix and gradient descent-based optimization, ELSA demonstrates remarkable scalability and applicability to industrial-scale datasets. The second contribution extends ELSA to Transformer architectures, resulting in the development of beeFormer, a framework that effectively combines interaction data with semantic and vision representations. We demostrate, that training Transformers with interaction data can transfer knowledge between datasets while outperforming not only semantic similarity-based Transformers but also traditional collaborative filtering methods. Additionally, the thesis explores cross-domain recommendation, revealing the potential of Transformer models to transfer knowledge between domains like books, movies, and fashion. The use of Large Language Model (LLM)-generated descriptions is shown to improve cross-domain recommendations.

This dissertation thesis is focused on formal verification of machine-code systems using model checking with abstraction. The background and state of the art of machine-code model checking are presented, and weaknesses of previous approaches are noted. The author's research described in this dissertation thesis and previous conference proceedings articles presents novel solutions to the major problems of previous research: the systems are described in the Rust programming language and are inherently simulable, automatically converted to verification equivalents and verified within a novel framework based on Three-Valued Abstraction Refinement. Special care is taken to allow efficient verification of variables based on bit-vectors. The author has created a formal verification tool implementing the introduced techniques, and its performance is evaluated in the thesis. The tool can be used to verify arbitrary finite-state digital systems, with a special focus on systems with behaviour determined by machine-code programs. The created tool is free, open-source, and publicly available.