Summarising patient interactions creates a huge workload for the healthcare professionals. This research finds that patient interactions contain a lot of noise that is subjective of nature. To explore the problem area interviews with a summarisation prototype have been conducted to extract system requirements and validate those by implementing them in the prototype. Filtering noise, reinforcement learning and numerical factual correctness are of paramount importance to a successful summarisation system.

Computers have become an essential part of modern life. They are used in a wide range of applications, from smartphones and laptops to data centers and supercomputers. However, the increasing usage of computers has led to a rise in energy consumption, which has significant environmental and economic consequences.

The hardware of computing systems has become more energy-efficient over the years. However, software remains a largely untapped area for energy optimization. The key to reducing energy consumption in computing systems lies in understanding the impact of software on the overall energy usage of the system. So, the need for tools and methods to measure software energy consumption is crucial. Those tools and methods should be flexible enough to be used in different computing environments.

This thesis reviews the current state-of-the-art tools for monitoring software energy consumption. After a list of their capacities, we identify the more promising tools and methods and compare their performance during experiments using different types of workloads. The thesis also presents a new tool called Geryon, which brings together the best techniques found in the tools reviewed. Geryon is a flexible and easy-to-use tool that provides multiple estimations at once. Those estimations are computed via simple power models and regression models trained on-the-fly. It also provides a way to plug in an external power model, allowing for more complex power models to be used. The tool is evaluated on the same workloads as the other tools to provide a fair comparison.

The transition to renewable energy sources requires advanced energy storage solutions to manage their intermittent nature. This thesis explores the feasibility of implementing Battery as a Service (BaaS) for a renewable energy community (RECs) setting, aiming to incorporate this model as part of an existing stacked revenue framework utilized by battery owners across various energy markets. By directly linking battery owners with energy communities, the study shows that renting out battery storage can eliminate intermediary overheads, thus providing financial benefits to both parties. The research addresses two main questions: developing a stacked revenue model for grid-connected batteries including energy communities, and comparing different battery sizing and control methods across various tariff schemes. The findings suggest that the proposed revenue model optimizes energy use and reduces costs for the community. This thesis contributes to the research field by presenting a viable economic model for integrating battery storage into decentralized energy communities.

Physics-Informed Neural Networks (PINNs) offer a promising approach to solving partial differential
equations (PDEs). In PINNs, physical laws are incorporated into the loss function, guiding the network to learn a model that adheres to these laws as defined by the PDEs. Training PINNs involves using three types of points: collocation points within the domain of the PDEs, boundary points on the edges of the domain, and initial points at the starting time (t = 0). A common challenge in training PINNs is the imbalance between the number of boundaries and initial points compared to collocation points, which can negatively impact the training process. Typically, the number of each type of point is manually set, and the number of collocation points is usually ten times that of boundary and initial points, leading to an uneven loss distribution over time. Our work introduces a method called Relative Residual Resampling (R3) to address this issue. This method dynamically adjusts the number of each type of training point to ensure a more balanced distribution. Consequently, the loss is more evenly spread across the time domain, enhancing the performance of the PINN. We tested our method on the 1D Heat Equation and 1D Diffusion Equation. The results demonstrate that our approach reduces the overall loss by at least 6%, and balances the loss distribution over time by reducing the loss range for at least 65% compared with the state-of-the-art residual-based resampling strategy. This improvement makes PINNs more accurate and efficient for solving time-dependent PDEs, providing a practical solution for applications where understanding temporal dynamics is crucial.

Depression, a leading cause of disability worldwide, is challenging to diagnose due to its reliance on subjective clinical evaluations. Metabolomics, which analyzes small molecules to reflect physiological and pathological states, holds promise for enhancing the diagnosis and identifying biomarkers for depression, potentially leading to better understanding and treatment options. Despite the complexity of metabolomics data, deep learning methods have not been extensively explored due to issues with interpretability, which are crucial for gaining insights into biological mechanisms. This study evaluates a biologically interpretable deep neural network, MetaboNet, trained on metabolomics data, for predicting depression and identifying key metabolites and biochemical pathways relevant to the condition. Our results demonstrate that MetaboNet outperforms logistic regression, though the overall classification performance remains modest. Notably, the classification results revealed sex-related differences, with better performance observed in females. Our findings do not support the capability of MetaboNet to identify biologically relevant individual metabolites. However, MetaboNet shows promise in identifying biochemical sub-pathways and super-pathways relevant to depression, which are validated by existing literature.

Agents improve by interacting with an environment and planning. By leveraging information about what they don't know, they can learn better and faster, at least in environments that benefit from exploring. They do this by estimating the uncertainty in their predictions. There are choices for how to estimate the uncertainty, and in this work, we look at what effect this choice has on the exploration and strength of agents playing board games. We compare the effect of a source of uncertainty which perfectly tracks what the agent has seen, and a source which generalizes. We also describe the challenges associated with tuning uncertainty estimators and show what considerations have to be made when exploration is not all you need.

Over the last decade, there have been significant advances in model-based deep reinforcement learning. One of the most successful such algorithms is AlphaZero which combines Monte Carlo Tree Search with deep learning. AlphaZero and its successors commonly describe a unified framework for tree construction and acting. For instance, build the tree with PUCT and act according to visitation counts. Policies based on visitation counts inherently make assumptions about the tree construction. This is problematic since it constrains the construction algorithm. For example, breadth-first tree construction yields a uniform visitation policy. To address this, we investigate the goals when extracting policies from decision trees and propose novel construction decoupled policies. Furthermore, we use these to modify how decision nodes are evaluated and utilize this during tree construction. We support the claim that our novel policies can benefit AlphaZero with theoretical analysis and empirical evidence. Our results on classical Gym environments show that the benefits are especially prominent for limited simulation budgets. The code is available through GitHub.

In recent years, the novel framing of the caching problem as an Online Convex Optimisation (OCO) problem has led to the introduction of several online caching policies. These policies are proven optimal with regard to regret for any arbitrary request pattern, including that of adversarial origin. Nevertheless, their performance is primarily affected by the tuning of their so-called hyperparameters (e.g. learning rate), which is often done under the presumption of adversarial conditions. Consequently, as not all request patterns encountered in practice are adversarial, this suggests potential for further improvements. Unfortunately, the tuning of these hyperparameters to achieve optimal performance across non-adversarial request sequences remains dubious and poses a new challenge. This paper proposes an online meta-learner that combines several instances of the OGA caching policy, each distinct in their learning rate, framing the problem as an expert advice decision problem. The proposed meta-learner dynamically shifts between caching experts and achieves a regret upper bound similar to that of the best-performing caching expert. The penalty introduced for learning the best expert is limited to a logarithmic dependence on the number of experts, which improves upon previous works. Numerical evaluations composed of synthetic request traces demonstrate consistent improvements when the caching experts' relative performance varies over time.

This paper investigates strategies to limit the cost of switching the cache in the context of an optimistic discrete caching problem. We have chosen as a starting point the current state-of-the-art in optimistic discrete caching, the Optimistic Follow-The-Perturbed-Leader (OFTPL) algorithm. We propose two strategies that attempt to limit this cost. The first approach sets a lower bound for the perturbation factor, thus including a mandatory amount of noise in the optimization of the cache state. The second approach investigates dynamically updating the perturbation factor to increase the switching cost, hence allowing the algorithm to adapt to the scenario at hand. Therefore, to the best of our knowledge, we design the first optimistic discrete caching algorithm that attempts to optimize the switching cost. Finally, we experiment and evaluate our solutions while highlighting their strengths and limitations.

This paper presents an adaptive per-file caching policy designed to dynamically adjust caching decisions based on the importance of the requested files. It relies on the Online Gradient Ascent (OGA) algorithm, which treats the caching problem as an online optimization problem. This methodology ensures minimal regret by continuously optimizing caching configurations in response to real-time request sequences. The caching configurations are optimized after every request using a constant learning rate. Because the trends of requested files can change, we will introduce two new algorithms that change the learning rate at every request to increase the adaptability. We will present two new algorithms, the Universally Adaptive Caching (UAC) algorithm and the Adaptive Per File Caching Algorithm (APFC), and will present scenarios to highlight their performances.

This paper explores the effect of forecasting methods on the Optimistic Follow The Regularized Leader (OFTRL) caching policy. It has been theoretically proven that the performance of OFTRL improves with accurate forecasters. However, the forecasters were portrayed as black boxes. In this paper, we do not treat forecasters as a black box but rather use recommender systems and temporal convolutional networks (TCN) implementations as forecasters for OFTRL in the caching context. The said forecasters predict the next file requests directly from the request trace rather than monitoring popularity. Using request traces extracted from the well-known MovieLens dataset, it was found that incorporating a forecaster into an optimistic learning algorithm is not straightforward. In fact, it was found that simpler approaches such as one that predicts the most requested file, can outperform more complicated deep learning models in terms of regret even if they possess a lower accuracy.

In the past few years, rapid strides have been made in the modelling of complex systems due to the advent of machine learning (ML) technologies. In particular, the transformer neural network (TNN) has gained a lot of attention due to its powerful “sequence-to-sequence” modelling for several tasks in science and engineering. Predictive ML models are trained to learn the relationship between a set of input and output data so that new input data can be mapped to their expected output values. This gives us the ability to understand the key factors impacting a system and to make predictions about its future behaviours. This research investigates how to use TNNs for decision making by optimising the output of a TNN. To this end, a non-convex mixed-integer non-liner programming (MINLP) formulation for a trained TNN is proposed. The proposed formulation facilitates solving problems with TNNs embedded
to global optimality. The effectiveness of the formulation is tested on three case studies consisting of an optimal trajectory problem, a verification problem, and a reactor optimization case study. Results show that optimisation over small TNNs can be achieved in under 3 minutes. However the tractability of the formulation quickly vanishes for larger models, highlighting the need for further research to refine the proposed formulation.

Solving routing problems efficiently is instrumental in minimizing operational costs in logistics. These routing problems are hard to solve and often take a lot of time to find a good solution. In this thesis, we present a methodology that tackles the challenge of efficiently solving recurring instances of the Vehicle Routing Problem with Time Windows by recycling solutions. By making more problem-specific assumptions, we introduce a solution recycling approach that can leverage shared solution structures across similar instances. This accelerates the solution-finding process. We implement our methodology in the framework of constraint programming and show that such a methodology is actually useful and is a concept that is yet unexplored in combinatorial optimization.

Automated imaging systems, critical in domains like medical imaging, autonomous driving, and security, experience noise from camera sensors and electronic circuits in bad or dark lighting conditions. This impacts downstream tasks, including object detection. However, an analysis of strategies combining denoising and object detection is lacking. This study addresses this gap by analyzing diverse strategies for optimizing both image quality and detection performance. Results reveal that isolating denoiser network optimization and training a detector on its outputs yields the best overall performance. Combining detection and denoising enhances detection outcomes. The results offer valuable insights to make educated decisions on how to combine denoising and detection in modern imaging systems.

This paper focuses on implementing and verifying the proofs presented in ``Finite Sets in Homotopy Type Theory" within the UniMath library. The UniMath library currently lacks support for higher inductive types, which are crucial for reasoning about finite sets in Homotopy Type Theory. This paper addresses that issue and introduces higher inductive types to UniMath. This is used to develop a computer-checked implementation of the proofs within "Finite Sets in Homotopy Type Theory." This implementation enables future research on finite sets in HoTT by providing accessible and reliable proofs.

This paper defines finite sets as Kuratowski-finite. This is in contrast with the most common notion of finiteness, e.g. Bishop-finite and enumerated types. I argue that Kuratowski-finiteness is the most general finite for which the usual operations of finite types and sub-objects can be operated upon.

To address the challenge of the time-consuming nature of proofreading proofs, computer proof assistants—such as the Coq proof assistant—have been developed. The Univalent Mathematics project aims to formalise mathematics using the Coq proof assistant from a univalent perspective, which is based on homotopy type theory.

The Symmetry book is a textbook about symmetries in mathematics written from a univalent viewpoint. This paper focuses on formalising the proofs in chapter 3 of the Symmetry book using the UniMath Coq library. Currently, the book is partly formalised in the Agda UniMath library. In this paper, we aim to formalise the chapter using the UniMath Coq library to verify its correctness. We have successfully formalised all the theorems in sections 3.1 to 3.3, along some other minor proofs.

This paper will give a formalisation of proofs, given in the paper "isomorphism is equality", in the proof assistant language Coq. The formalisations will be added to UniMath library. A library containing machine readable proofs in the mathematical field of Homotopy Type theory, a relatively new field which combines Homotopy Theory and Martin-Löf Type Theory. The proofs that have been formalised are the equality pair lemma and the proof that isomorphism is equivalent to equality. We have also constructed a concrete universe on which we defined a notion of isomorphism, as per the same paper.