Bridging Continuous Learning and Discrete Optimisation in Artificial Intelligence

Artificial intelligence has always had two distinct aspects. One searches, plans, schedules and proves: it is discrete, exact and verifiable, and its native language is combinatorics. The other perceives, predicts and generalises from data: today that means neural networks, which are continuous, statistical and trained by gradients, and whose native language is calculus. After decades of oscillating between the two, the field has settled on hybrid approaches. A navigation app feeds learnt journey times into a route planner; a language model calls upon a tool and reads back the result; and a demand forecast determines which power stations will operate tomorrow.

Every such system contains a link between a continuous learner and a discrete decision. What matters is not the quality of either part on its own, but the result produced by the system as a whole. The continuous part is therefore trained end-to-end, so that it learns to make proper use of the discrete one. The standard method for such training is gradient descent: nudge the parameters in the direction of a better final decision, and repeat. Through the discrete component, however, this breaks down: a decision either remains unchanged or jumps, and neither tells the learner which way to move.

We will examine the few principled methods for obtaining a useful update direction nonetheless, ranging from straightforward techniques and reinforcement learning to smoothed surrogates, implicit differentiation and differentiable simulation, and consider what each of them sacrifices in return. The navigation app, the tool-using model and the power grid all depend on the answer.

Reflections on Working on Visualisation with Industry Partners – and Looking Ahead

With the digitalisation of the manufacturing industry, energy supplies and other sectors, enormous amounts of IoT (Internet of Things) data are being collected. Expectations regarding quality, costs, delivery times, durability and environmental considerations are rising at a similar pace. Data-driven manufacturing and planning open up unprecedented opportunities to understand the impact of decisions on engineering performance and customer satisfaction. Visual analytics plays a vital role in transforming data into actionable decisions, which is increasingly becoming a key factor for companies seeking to remain competitive. Visual analytics has already demonstrated its effectiveness in analysing IoT data across various projects, as outlined in this talk. However, there are still some major challenges ahead of us. We continue to face Big Data challenges when it comes to providing a concise overview of large volumes of data. Furthermore, there are many challenges associated with the successful application of visualisation, both within the manufacturing and energy sectors, and from the perspective of visualisation research. In this talk, I will reflect on our past experiences in applying Visual Analytics in research projects in collaboration with industry partners and describe the main challenges we are currently facing.

CoFI break

Untangling Surfaces via Shape and Mesh Repulsion

Triangle meshes are one of the fundamental representations of 3D geometry in computer graphics, geometry processing and simulation. In practice, however, meshes often contain self-intersections and other geometric defects that make them difficult or impossible to use. In this talk, I will present a geometric approach we have developed for automatically untangling such surfaces whilst preserving their connectivity and overall shape. Our method combines repulsion between intersecting parts of the surface with energies that preserve shape and mesh quality. I will focus on the geometric ideas behind the method, the optimisation challenges that arise, and the broader question of how to robustly repair complex 3D geometry. The talk will be aimed at a broad computer science audience and will rely heavily on visual examples.

Safe Reinforcement Learning Using Shield Synthesis for LTL Modulo Theories

"In recent years, machine learning models – and in particular reinforcement learning (RL) – have achieved remarkable success in various domains, including sequential decision-making. However, these models tend to exhibit unsafe behaviour, preventing their deployment in safety-critical systems. To address this issue, considerable research is focused on developing methods that guarantee the safe behaviour of a given RL model, also referred to as ‘Safe Reinforcement Learning’.

A prominent approach to safe RL is shielding, which incorporates an external component generated using formal methods – known as a shield – that blocks or corrects unwanted behaviour. Despite significant progress, shielding suffers from a major drawback: classical shielding is based on properties in propositional temporal logics, typically LTL, and is unsuitable for richer logics. This, in turn, limits the widespread applicability of shielding in many real-world systems where the dynamics are complex.

In this work, we address this gap and extend shielding to LTL modulo theories by building upon recent advances in reactive synthesis modulo theories. LTL modulo theories allow the use of both temporal modalities and literals for arbitrary theories. This has enabled us to develop a novel approach for generating shields that conform to complex safety specifications in these more expressive logics.

This is a “neurosymbolic” solution, in the sense that we build a system that combines the complex objectives and behaviours of RL with the safety guarantees of formal synthesis.

The outline of the talk is as follows: (1) to explain the rationale for safe reinforcement learning; (2) to introduce temporal logic and reactive synthesis; (3) to present our work on synthesis modulo theories; and (4) to describe how to extend synthesis modulo theories for shielding."

AI in Teaching @ FI: Practices, Tools, and Inspiration

This faculty showcase features short, hands-on presentations from FI colleagues who are actively integrating AI into their teaching. Discover local best practices, explore tried-and-tested AI tools you can adopt straight away, and be inspired to experiment in your own courses. This session offers a clear overview of current AI practices at our faculty and provides a collaborative space to exchange ideas and tools with your peers.

Guaranteed to Exist, Hard to Find: Nash Equilibria and Cryptography

Nash famously proved that every finite game has an equilibrium in mixed strategies. Yet, more than seventy years later, we still do not know how to find one efficiently in general. Nash equilibria illustrate a broader phenomenon: a mathematical theorem can guarantee that a solution exists without providing an efficient way to find it. Such total search problems pose a particular challenge for computational complexity theory, as they cannot be addressed via NP-hardness.

In this talk, I will explain how cryptography provides a different kind of evidence for their intractability. At the heart of the algorithmic task of finding a Nash equilibrium lies a simple combinatorial puzzle: given a starting point on one of the paths in a huge graph, find another endpoint. I will describe how to embed a long computation into such a graph, accompanied by a short proof of correctness that is updated as the computation proceeds. Through a chain of reductions, this links the difficulty of finding Nash equilibria to the security of modern cryptographic proof systems. The talk will focus on the ideas behind this connection and what they reveal about the gap between existence and efficient computation.

No prior knowledge of cryptography or game theory is required.

Automatic Heuristic Discovery with Large Language Models

Designing high-performance heuristics is a complex task that requires both intuition and deep domain knowledge. Large language models (LLMs) have led to new ways of creating heuristics that rival the performance of state-of-the-art human-designed approaches. In this talk, I will introduce these new mechanisms for heuristic design and describe their advantages and limitations, with a focus on vehicle routing problems. I will introduce the VRPAgent method, an evolutionary approach to creating routing heuristics that rivals state-of-the-art Operations Research approaches. Furthermore, I will demonstrate the current state of the art regarding the effectiveness of agentic loops in solving various routing problems.

VisioTherapy: AI-based Physical Therapy on Your Smartphone

According to the WHO, approximately one-third of the global population suffers from health conditions that could be alleviated through physical rehabilitation. A global shortage of physiotherapists has created an urgent demand for scalable technologies to support patients during recovery. VisioTherapy addresses this gap by transforming a standard smartphone into a sophisticated rehabilitation tool. By monitoring patients via the device’s camera, the application provides real-time, personalised feedback on exercise performance to ensure safety and efficacy in a home setting. VisioTherapy is currently being tested in real-world pilot schemes at healthcare facilities in the Czech Republic and the United States.

The talk will introduce the VisioTherapy project—a collaborative effort between VisionCraft, the Faculty of Informatics at Masaryk University (FI MU) and Brno University Hospital. We will outline the application’s high-level architecture and explain what makes our approach unique. We will then explore the key technical challenges currently being tackled under the TWIST Programme of the Czech Ministry of Industry and Trade.

Jiří Gavenda: Can Bitcoin Be Anonymous? Analysing the Privacy Benefits of CoinJoins

By design, Bitcoin transactions are publicly available for anyone to inspect. The identities of payers and payees are replaced by randomly generated addresses, and a single user typically controls many addresses. However, a motivated adversary can still link the addresses of a single user by applying simple heuristics to the transaction graph, for example by assuming that all inputs to a transaction belong to the same person. Linking just one of these addresses to a real identity can then reveal the user’s entire transaction history.

CoinJoins are collaborative transactions that mix the funds of multiple users so that the users become indistinguishable under standard blockchain analysis. In this talk, we will look at recent research in this area. How can we measure the privacy these collaborative transactions provide? Do people actually use them? And which questions remain open?

Jan Mačák: Multi-agent Stochastic Shortest Path Problem

In this talk, I will introduce the multi-agent stochastic shortest path (MSSP) problem, in which k agents strive to reach a target state, aiming to minimise the expected time taken by any agent to reach the target. We analysed the computational and strategy complexity of the problem in both autonomous and coordinated settings, and designed efficient strategy-synthesis algorithms. The algorithms were experimentally evaluated on instances of increasing size against natural baselines.

From Brno to the Boundaries of Infinity

Kurt Gödel, a native of Brno who is rightly regarded as a logician of a stature comparable to Aristotle, demonstrated through his work both the completeness of first-order predicate logic for logic itself and the fundamental impossibility of constructing a similar formalised system for mathematics. The arithmetisation of mathematical concepts that he developed for this purpose also allows us to appreciate the richness of mathematical statements and to draw a metaphorical comparison between them and the vastness of the universe. This lecture is inspired by this year’s 120th anniversary of the birth of this distinguished figure, whom the Faculty of Informatics at Masaryk University honours on its insignia.

Lab Fest, held as part of the Informatics Colloquium, aims to familiarise the academic community with the activities of research groups at the faculty, specifically their staffing, areas of interest, involvement in grants, and ongoing collaborations at the university, within the Czech Republic and internationally; future directions and current research or development results.

SYBILA (Sequence Bioinformatics and Genomics Group: TBA

Computational Systems Biology Group): TBA