Miroslav Olsák

According to our database, Miroslav Olsák authored at least 28 papers between 2017 and 2025.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2025

Invariant neural architecture for learning term synthesis in instantiation proving.

Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolás Janota

J. Symb. Comput., 2025

2024

Hashing Modulo Context-Sensitive 𝛼-Equivalence.

Lasse Blaauwbroek, Miroslav Olsák, Herman Geuvers

Proc. ACM Program. Lang., 2024

Graph2Tac: Learning Hierarchical Representations of Math Concepts in Theorem proving.

Jason Rute, Miroslav Olsák, Lasse Blaauwbroek, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, Vasily Pestun

CoRR, 2024

Symbolic Computation for All the Fun.

Chad E. Brown, Mikolas Janota, Mirek Olsák

Proceedings of the Joint Proceedings of the 9th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 9th Satisfiability Checking and Symbolic Computation Workshop (SC-Square), 2024

Graph2Tac: Online Representation Learning of Formal Math Concepts.

Lasse Blaauwbroek, Mirek Olsák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, Vasily Pestun

Proceedings of the Forty-first International Conference on Machine Learning, 2024

The IMO Small Challenge: Not-Too-Hard Olympiad Math Datasets for LLMs.

Simon Frieder, Mirek Olsák, Julius Berner, Thomas Lukasiewicz

Proceedings of the Second Tiny Papers Track at ICLR 2024, 2024

2023

Alien coding.

Thibault Gauthier, Miroslav Olsák, Josef Urban

Int. J. Approx. Reason., November, 2023

MizAR 60 for Mizar 50.

Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

2022

Machine Learning Meets The Herbrand Universe.

Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolas Janota

CoRR, 2022

The Isabelle ENIGMA.

Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

2021

Maltsev conditions for General Congruence Meet-semidistributive Algebras.

Miroslav Olsák

J. Symb. Log., 2021

Erratum: Equations in oligomorphic clones and the constraint satisfaction problem for ω-categorical structures.

Libor Barto, Michael Kompatscher, Miroslav Olsák, Trung Van Pham, Michael Pinsker

J. Math. Log., 2021

The Role of Entropy in Guiding a Connection Prover.

Zsolt Zombori, Josef Urban, Miroslav Olsák

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2021

Learning Theorem Proving Components.

Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2021

Planning from Pixels in Environments with Combinatorially Hard Search Spaces.

Marco Bagatella, Miroslav Olsák, Michal Rolínek, Georg Martius

Proceedings of the Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, 2021

Learning to Solve Geometric Construction Problems from Images.

Jaroslav Macke, Jirí Sedlár, Miroslav Olsák, Josef Urban, Josef Sivic

Proceedings of the Intelligent Computer Mathematics - 14th International Conference, 2021

Fast and Slow Enigmas and Parental Guidance.

Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban

Proceedings of the Frontiers of Combining Systems - 13th International Symposium, 2021

2020

Loop conditions for strongly connected digraphs.

Miroslav Olsák

Int. J. Algebra Comput., 2020

ω-categorical structures avoiding height 1 identities.

Manuel Bodirsky, Antoine Mottet, Miroslav Olsák, Jakub Oprsal, Michael Pinsker, Ross Willard

CoRR, 2020

GeoLogic - Graphical Interactive Theorem Prover for Euclidean Geometry.

Miroslav Olsák

Proceedings of the Mathematical Software - ICMS 2020, 2020

Property Invariant Embedding for Automated Reasoning.

Miroslav Olsák, Cezary Kaliszyk, Josef Urban

Proceedings of the ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020, 2020

ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description).

Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Equations in oligomorphic clones and the constraint satisfaction problem for ω-categorical structures.

Libor Barto, Michael Kompatscher, Miroslav Olsák, Van Trung Pham, Michael Pinsker

J. Math. Log., 2019

Topology is relevant (in the infinite-domain dichotomy conjecture for constraint satisfaction problems).

Manuel Bodirsky, Antoine Mottet, Miroslav Olsák, Jakub Oprsal, Michael Pinsker, Ross Willard

CoRR, 2019

Topology is relevant (in a dichotomy conjecture for infinite-domain constraint satisfaction problems).

Manuel Bodirsky, Antoine Mottet, Miroslav Olsák, Jakub Oprsal, Michael Pinsker, Ross Willard

Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019

Dichotomy for Symmetric Boolean PCSPs.

Miron Ficak, Marcin Kozik, Miroslav Olsák, Szymon Stankiewicz

Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, 2019

2018

Reinforcement Learning of Theorem Proving.

Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olsák

Proceedings of the Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, 2018

2017

The equivalence of two dichotomy conjectures for infinite domain constraint satisfaction problems.

Libor Barto, Michael Kompatscher, Miroslav Olsák, Trung Van Pham, Michael Pinsker

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017