Name: Vampire with a Neural Flair
Start: 2025-11-20T16:00:00+01:00
End: 2025-11-20T17:00:00+01:00

Automated theorem proving is a classical branch of symbolic AI. Rooted in formal logic, it aims to endow computers with the reasoning skills of mathematicians. A theorem prover must explore a vast space of possible derivations in search of a proof for a given conjecture. Good heuristics—analogous to a mathematician’s intuitions—help it fight the looming combinatorial explosion. In this talk, I will introduce the award-winning theorem prover Vampire and show how a powerful guiding heuristic, supported by a deep neural network, can be automatically learned from the prover’s own experience through reinforcement learning.

\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-

⌚️ **Start**: 16:00 and end at 17:00, both online and offline in **Truhlárna Karlín** (Šaldova 388/5) - **Onsite attendance is limited to 70 people.**
🎙️ **Speaker:** RNDr. Martin Suda, Ph.D.
🍻 **Networking** after the seminar – great food and cold beer waiting for you!
**🎥 Recording:** After the event we will publish a recording and post a link to it in the comments.
🚪**Doors open** at 15:45, and the event officially starts at 16:00.
Your expertise is about to take off. Can't wait to have you on board!
\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-
**Who is hosting the event**
**GLAMI** is a leading European fashion discovery platform active in 14 countries. It brings 500,000 orders monthly to the 4,000+ shops listed. [GLAMI](https://glami.group/) has an in-house team of 10+ AI researchers and developers. Machine learning models handle the entire personalization and catalog ranking process, manage bidding in marketing tools, and take care of content management and categorization.
[Tonda Hoskovec](https://www.linkedin.com/in/antonin-hoskovec-52b611a0/), CAIO at GLAMI, is the main organizer of Miton AI Times.
**Miton** is a Czech VC with portfolio companies like Rossum, Equilibre, or Rohlik. Apart from supporting Miton AI Times, Miton also issues the bi-weekly [AI Newsletter](https://mitonainewsletter.substack.com/).
[Read more about Miton and AI](https://www.miton.cz/en/ai/)

GLAMI

Miton AI Times

Technology

Artificial Intelligence

Big Data

Natural Language Processing

Machine Learning

Data Science

Artificial Intelligence Programming

Artificial Intelligence Applications

is a senior reseacher at [CTU/CIIRC](https://www.ciirc.cvut.cz/cs/) and the head of the [Automated Reasoning Group](https://www.ciirc.cvut.cz/cs/teams-labs/ai/ar/) there. His main research interest is automated reasoning, machine learning and thier fruitful combinations

Miton AI Times

Vampire with a Neural Flair

Miton AI Times

Details

Members are also interested in