Extending the reach of automated algorithm design, optimisation and customisation

点击翻译按钮获取中文摘要

Challenging computational problems arise prominently in areas such as software verification, energy systems optimisation and analysis of large amounts of data. Efficient software systems for solving these problems are of crucial importance, and improvements to these systems will have considerable economic and societal benefits, e.g., in terms of more sustainable and efficient use of energy and resources. Our research aims at automatically designing, optimising and customising such software for specific application situations. Specifically, our Programming by Optimisation (PbO) approach takes broadly applicable, general-purpose software, makes it flexible and adaptable by encouraging and exposing design choices for key components, and then exploits this flexibility by automatically adapting the software to specific application situations, using advanced machine learning and optimisation techniques. PbO has already attracted much interest in academia and industry; the research proposed here aims to take PbO to the next level, with the goal of establishing this paradigm as a standard way of designing software for computational problems across a wide range of application domains. Towards this end, we will address three major challenges arising in the context of software development using PbO (and beyond). Firstly, it can be very expensive to evaluate configurations or variants of a given piece of software - too expensive to permit direct design optimisation on sets of benchmarks representing the size and difficulty of those problem instances encountered in the intended application. Secondly, e.g., in applications dealing with sensitive data, it may be impossible to perform design optimisation as part of the development process; instead, it may have to be done post-deployment, in the actual application context, using substantially more limited computational resources. Thirdly, creating, managing and assessing design choices can be rather expensive in terms of human expert time. Our methodological work on overcoming these challenges will be guided and validated using three prominent and important applications: - software verification based on state-of-the-art SAT-modulo-theory (SMT) solvers (A1); - automated design and configuration of machine learning pipelines for analysing large amounts of data (A2); and - optimisation of software systems for generation and storage of clean energy (A3). We expect our work, which combines advances in machine learning and optimisation, to take automated algorithm design, optimisation and customisation to the next level, to have transformative impact on the design of software for these and other computationally challenging applications, thus creating very significant value within the information technology sector that produces such software and in the areas that rely on their application.