The Austrian Academy of Sciences (ÖAW) has once again awarded a number of grants for doctoral research projects. Three of these have been awarded to PhD students at TU Wien. Surprisingly, two of the projects share a culinary theme: whilst Christoph Spiess is researching mathematical sandwiches, Maximilian Kovar is developing a cookbook for artificial intelligence. Johannes Weiser completes the trio with a PhD thesis on the theoretical limits of methods for the automatic verification of computer programmes – which sounds very theoretical, but has enormous practical implications.

Maximilian Kovar: „Data for Chemical Reaction Machine Learning"

PhD supervisor: Esther Heid
Institute of Materials Chemistry, Faculty of Technical Chemistry

Maximilian Kovar is a PhD student at the Institute of Materials Chemistry at Vienna University of Technology. His doctoral thesis focuses on machine learning in the field of chemical reactions. The aim is for AI to be able, in future, to predict – even before experiments are carried out – whether reactions will work, under what conditions they will proceed optimally, and whether the effort involved is justified. This will help to save resources and minimise the need for dangerous experiments.

However, for such models to make reliable predictions, they require high-quality training data. This is precisely where the research project comes in: it investigates which chemical reactions are particularly well suited to training artificial intelligence efficiently, and why. This also involves fundamental questions of predictability and chemical similarity. The aim is to create efficient datasets that can serve as a ‘textbook’ for future AI assistants in synthetic chemistry.

You can think of it as a cookbook for artificial intelligence: it shouldn’t contain as many recipes as possible, but rather exactly the right examples. The model is designed to learn the basic principles so that, using the right starting materials under the right conditions, it can successfully ‘cook’ the desired reaction, as we say in chemistry.

Christoph Spiess: „Omega-categorical sandwiches for Promise Constraint Satisfaction Problems"

PhD supervisor: Michael Pinsker
Institute of Discrete Mathematics and Geometry, Faculty of Mathematics and Geoinformation

In his doctoral thesis, Christoph Spiess examines how constraints on the fulfilment of conditions can be overcome. An algorithm must determine whether certain conditions can be satisfied simultaneously. A classic example: can a map be coloured using only three colours in such a way that neighbouring countries never share the same colour?

Such CSPs are described by mathematical structures. Combining two of these results in a Promise-CSP (PCSP). The question is then no longer simply ‘Is it possible with three colours?’, but ‘Is it possible with three colours – or does it fail even with five?’. And this is where the maths takes on a culinary flavour: if you find another structure that lies between these two, it is called a ‘cheese structure’. Together with the two finite ‘bread structures’, it forms a mathematical sandwich. The key point is this: if you have an algorithm for the CSP of the cheese structure, you automatically also have an algorithm for the PCSP of the entire sandwich – the ready-to-eat dish, so to speak: Christoph Spiess is conducting research into identifying infinite cheese structures for which known algorithms can be efficiently transferred to finite Promise-CSPs. This would enable researchers in future to draw on tried-and-tested CSP algorithms, rather than having to develop them from scratch for every new problem. This saves computation time, opens up new fields of application and strengthens the bridge between theoretical mathematics and practical algorithmics.

Johannes Weiser: „Limits of Methods for Solving Constrained Horn Clauses"

PhD supervisor: Stefan Hetzl
Institute of Discrete Mathematics and Geometry, Faculty of Mathematics and Geoinformation

In his doctoral thesis, Johannes Weiser is investigating the theoretical limits of methods for the automatic verification of computer programmes – his seemingly abstract topic is deeply rooted in the everyday lives of all users.

The focus is on Constrained Horn Clauses, a mathematical formalism that can be used to model and analyse software. This makes it possible to check whether a programme will run safely under all conceivable inputs – or whether, for example, it will crash because a division by zero occurs. You can think of it as a kind of ‘mathematical safety check’ that guarantees the software will not make any unexpected errors.

The catch is this: it is fundamentally impossible to carry out a fully automated verification of software. In practice, therefore, various methods are used, each of which can only resolve specific cases. If such a method fails, it often remains unclear whether this is due to limited resources or a fundamental limitation of the algorithm.

Johannes Weiser takes this as his starting point and explores the theoretical limits of these methods. In doing so, he helps to determine which algorithm is best suited to solving a particular problem. This not only improves our understanding of existing methods, but also supports the development of new, more efficient methods, for example in critical fields ranging from medical technology and flight control to banking systems. Where errors can be life-threatening or costly, this research helps to ensure that programmes do their ‘homework’ before they are even put into use.

Congratulations to the scholarship recipients!