Martin Suda
RICAIP Tenure Track holder
Senior researcher at the Czech Institute of Informatics, Robotics and Cybernetics (CIIRC)
Machine Learning – Automated Reasoning
Previous Experience
Martin Suda currently holds a senior researcher position at CIIRC CTU, conducting research in areas of Automated Reasoning (AR) and Machine Learning (ML). He’s a PI of the Czech Science Foundation project MLTPA and a co-PI of the RenPhil project DEEPER. Previously, he was a postdoc at the University of Manchester, UK and at TU Wien, Vienna, Austria focusing on Automated Theorem Proving.
He has received his Ph.D. from the Max-Planck-Institut für Informatik and the Saarland University in Saarbrücken, Germany, and at the Faculty of Mathematics and Physics, Charles University in Prague, Czech Republic.
Martin Suda is known as a co-developer of and one of the researchers behind Vampire, a world leading automatic theorem prover for first-order logic with theories, as exemplified by its victories at the annual CADE ATP System Competition and by its strong participation at SMTCOMP.
Current Focus
Martin Suda is pursuing research where he can develop rigorous mathematical theories as foundations to building software with actual practical impact. In addition to Automated Reasoning his research interests include Theory of Boolean Satistiablity, QBF and DQBF solving, and Automated Planning.
Martin Suda’s work has been focused on the automatic theorem proving (ATP) and how it can be improved with the help of machine learning (ML). Since recently, Martin is also (in collaboration with Adam Pease, the author of the Suggested Upper Merged Ontology, aka SUMO) exploring the potential of automated theorem provers for large ontology reasoning. He is currently the Principal Investigator of the MLTPA GACR project (2024-2026) while also contributing to the CoreSense project (Horizon Europe, 2022-2026).
I wish for RICAIP to continue growing as a leading European hub for AI, robotics, and Industry 4.0, strengthening its role as a bridge between cutting-edge research and real industrial impact.
Recent successes and results – What recent research achievements or milestones are you most proud of?
I am most proud of my last year’s work and a corresponding CADE 2025 paper titled “Efficient Neural Clause-Selection Reinforcement” in which I managed to demonstrate an unprecedented performance improvement of the theorem prover Vampire on the standard theorem proving problem library called TPTP by 20%. Vampire under the neural guidance described in this work was also able to solve many problems not known to be previously solved by any automatic theorem prover.
Biggest challenges and future plans – What are the main challenges currently facing your research areas, and what directions do you plan to pursue in the coming years?
The next big challenge is to extend the results from the previous year to support higher-order logic. While first-order logic is the traditional lingua franca of systems like Vampire, in recent years higher-order logic extensions have been implemented. Higher-order logic is more powerful in terms of expressivity (which is better from the user’s perspective), but more challenging to handle efficiently by the prover. At the same time, however, improvements on this front would be immediately appreciated by our main users of the interactive theorem provers (a.k.a. proof assistants) whose native language is typically higher-order and they immediately benefit from better automation.
International collaborations with other teams/ projects etc. – Your work involves collaborations across institutions and projects. How do international partnerships influence your research, and what value do they bring?
International collaboration is essential in our case. Vampire is a project developed jointly by teams in Manchester and Southampton, UK, Vienna in Austria and us here in Prague at CIIRC. On the most recent Deeper project we also collaborate with the University in Melbourne, Australia. Many of the colleagues there are also friends. We meet in person at least once a year to discuss progress and exchange ideas. Typically, such meetings also lead to joint publications or exchange of students.
Tenure track position – How has progressing into a tenure-track research role influenced your career, both professionally and personally?
Progressing into a tenure-track role has given me greater independence to shape my research agenda and pursue ambitious ideas, while also increasing my responsibility in mentoring students and contributing to the academic community. On a personal level, it has brought a stronger sense of stability and long-term purpose, alongside the challenge of balancing research, teaching, and collaboration commitments.
Selected publications
| Martin Suda Efficient Neural Clause-Selection Reinforcement arxiv | |
| Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdu, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, Andrei Voronkov The Vampire Diary arxiv | |
| Bhayat, A., Suda, M. A Higher-Order Vampire (Short Paper) In: Benzmüller, C., Heule, M.J., Schmidt, R.A. (eds) Automated Reasoning. IJCAR 2024. Lecture Notes in Computer Science, vol 14739. Springer, Cham. | |
| Bártek, F., Chvalovský, K., Suda, M. Regularization in Spider-Style Strategy Discovery and Schedule Construction. In: Benzmüller, C., Heule, M.J., Schmidt, R.A. (eds) Automated Reasoning. IJCAR 2024. Lecture Notes in Computer Science(), vol 14739. Springer, Cham. | |
| Einarsdóttir, S.H., Hajdu, M., Johansson, M., Smallbone, N., Suda, M. Lemma Discovery and Strategies for Automated Induction. In: Benzmüller, C., Heule, M.J., Schmidt, R.A. (eds) Automated Reasoning. IJCAR 2024. Lecture Notes in Computer Science(), vol 14739. Springer, Cham. | |
| Filip Bártek, Karel Chvalovský, Martin Suda Cautious Specialization of Strategy Schedules PAAR’24: 9th Workshop on Practical Aspects of Automated Reasoning. CEUR Workshop proceedings | |
| Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban MizAR 60 for Mizar 50, Fourteenth Conference on Interactive Theorem Proving – ITP, 2023 | |
| Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban MizAR 60 for Mizar 50, Fourteenth Conference on Interactive Theorem Proving – ITP, 2023 | |
| Filip Bártek, Martin Suda How Much Should This Symbol Weigh? A GNN-Advised Clause Selection, 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning – LPAR , 2023 | |
| Michael Rawson, Martin Suda, Petra Hozzová, Giles Reger: Reuse of Introduced Symbols in Automatic Theorem Provers. PAAR’22: 8th Workshop on Practical Aspects of Automated Reasoning, August 11–12, 2022. | |
| M Suda: Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description). IJCAR 2022: 659-667 Lecture Notes in Computer Science(), vol 13385. Springer, Cham. DOI 10.1007/978-3-031-10769-6_38 | |
| M Suda: Improving ENIGMA-style Clause Selection while Learning From History. In: Automated Deduction – CADE 28. 28th International Conference on Automated Deduction, Pittsburgh, 2021-07-12/2021-07-15. Springer, Cham, 2021. p. 543-561. Lecture Notes in Artificial Intelligence. vol. 12699. ISSN 0302-9743. ISBN 978-3-030-79875-8. DOI 10.1007/978-3-030-79876-5_31 | |
| F Bártek, M Suda: Neural Precedence Recommender. In: Automated Deduction – CADE 28. 28th International Conference on Automated Deduction, Pittsburgh, 2021-07-12/2021-07-15. Springer, Cham, p. 525-542. Lecture Notes in Artificial Intelligence. vol. 12699. ISSN 1611-3349. ISBN 978-3-030-79876-5. DOI 10.1007/978-3-030-79876-5_30 | |
| N Froleyks, M Heule, M Iser, M Järvisalo, M Suda: SAT Competition 2020. Artificial Intelligence. 2021, 301 ISSN 0004-3702. DOI 10.1016/j.artint.2021.103572 | |
| M Suda: Vampire with a Brain Is a Good ITP Hammer. In: Frontiers of Combining Systems. 13th International Symposium, FroCoS 2021, Birmingham, 2021-09-08/2021-09-10. Cham: Springer, 2021. p. 192-209. 1. ISSN 0302-9743. ISBN 978-3-030-86204-6. DOI 10.1007/978-3-030-86205-3_11 |