Bridging Continuous Learning and Discrete Optimisation in Artificial Intelligence

Artificial intelligence has always had two halves. 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 invokes 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-maker. 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 part. 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 changes abruptly, 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 digitisation of the manufacturing industry, energy supplies and other sectors, enormous amounts of IoT (Internet of Things) data are being collected. Expectations regarding quality, costs, lead times, durability and environmental considerations are rising at a similar rate. 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 value 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 of 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 systems. However, these models tend to exhibit unsafe behaviour, precluding their deployment in safety-critical systems. To address this issue, considerable research has 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 construct a system that combines the complex objectives and behaviours of reinforcement learning 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; (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.

TBA

Automatic Heuristic Discovery for Combinatorial Optimisation using Large Language Models

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 examine the core technical challenges currently being tackled under the TWIST Programme of the Ministry of Industry and Trade of the Czech Republic.

TBA

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 staff, areas of interest, involvement in grants, and ongoing collaborations at the university, in the Czech Republic and internationally; future directions and current research and development outcomes.

TBA