Miroslav Olsák

39 papers A* 5A 1B 3C 1Journal 26Unranked 3

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Reintroducing the Second Player in EPR. CoRR Leroy Chew, Mikolás Janota, Miroslav Olsák, Martin Suda
2025	J	`jnl`	Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2. CoRR Yuri Chervonyi, Trieu H. Trinh, Miroslav Olsák, Xiaomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, Vikas Verma, Quoc V. Le, Thang Luong
2025	J	`jnl`	Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2. J. Mach. Learn. Res. Yuri Chervonyi, Trieu H. Trinh, Miroslav Olsák, Xiaomeng Yang, Hoang H. Nguyen, Marcelo Menegali, Junehyuk Jung, Junsu Kim, Vikas Verma, Quoc V. Le, Thang Luong
2025	J	`jnl`	Invariant neural architecture for learning term synthesis in instantiation proving. J. Symb. Comput. Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolás Janota
2024	J	`jnl`	Graph2Tac: Learning Hierarchical Representations of Math Concepts in Theorem proving. CoRR Jason Rute, Miroslav Olsák, Lasse Blaauwbroek, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, Vasily Pestun
2024	J	`jnl`	Hashing Modulo Context-Sensitive α-Equivalence. CoRR Lasse Blaauwbroek, Miroslav Olsák, Herman Geuvers
2024	J	`jnl`	Hashing Modulo Context-Sensitive 𝛼-Equivalence. Proc. ACM Program. Lang. Lasse Blaauwbroek, Miroslav Olsák, Herman Geuvers
2023	J	`jnl`	Alien Coding. CoRR Thibault Gauthier, Miroslav Olsák, Josef Urban
2023	J	`jnl`	Alien coding. Int. J. Approx. Reason. Thibault Gauthier, Miroslav Olsák, Josef Urban
2022	J	`jnl`	Machine Learning Meets The Herbrand Universe. CoRR Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolas Janota
2022	B	`conf`	The Isabelle ENIGMA. ITP Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban
2022	J	`jnl`	The Isabelle ENIGMA. CoRR Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban
2021	J	`jnl`	Erratum: Equations in oligomorphic clones and the constraint satisfaction problem for ω-categorical structures. J. Math. Log. Libor Barto, Michael Kompatscher, Miroslav Olsák, Trung Van Pham, Michael Pinsker
2021	—	`conf`	Fast and Slow Enigmas and Parental Guidance. FroCoS Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
2021	J	`jnl`	Fast and Slow Enigmas and Parental Guidance. CoRR Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
2021	B	`conf`	Learning Theorem Proving Components. TABLEAUX Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
2021	J	`jnl`	Learning Theorem Proving Components. CoRR Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
2021	C	`conf`	Learning to Solve Geometric Construction Problems from Images. CICM Jaroslav Macke, Jirí Sedlár, Miroslav Olsák, Josef Urban, Josef Sivic
2021	J	`jnl`	Learning to solve geometric construction problems from images. CoRR Jaroslav Macke, Jirí Sedlár, Miroslav Olsák, Josef Urban, Josef Sivic
2021	J	`jnl`	Maltsev conditions for General Congruence Meet-semidistributive Algebras. J. Symb. Log. Miroslav Olsák
2021	A*	`conf`	Planning from Pixels in Environments with Combinatorially Hard Search Spaces. NeurIPS Marco Bagatella, Miroslav Olsák, Michal Rolínek, Georg Martius
2021	B	`conf`	The Role of Entropy in Guiding a Connection Prover. TABLEAUX Zsolt Zombori, Josef Urban, Miroslav Olsák
2021	J	`jnl`	The Role of Entropy in Guiding a Connection Prover. CoRR Zsolt Zombori, Josef Urban, Miroslav Olsák
2020	—	`conf`	ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description). IJCAR (2) Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
2020	J	`jnl`	ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description). CoRR Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
2020	—	`conf`	GeoLogic - Graphical Interactive Theorem Prover for Euclidean Geometry. ICMS Miroslav Olsák
2020	J	`jnl`	GeoLogic - Graphical interactive theorem prover for Euclidean geometry. CoRR Miroslav Olsák
2020	J	`jnl`	Loop conditions for strongly connected digraphs. Int. J. Algebra Comput. Miroslav Olsák
2020	A	`conf`	Property Invariant Embedding for Automated Reasoning. ECAI Miroslav Olsák, Cezary Kaliszyk, Josef Urban
2020	J	`jnl`	ω-categorical structures avoiding height 1 identities. CoRR Manuel Bodirsky, Antoine Mottet, Miroslav Olsák, Jakub Oprsal, Michael Pinsker, Ross Willard
2019	A*	`conf`	Dichotomy for Symmetric Boolean PCSPs. ICALP Miron Ficak, Marcin Kozik, Miroslav Olsák, Szymon Stankiewicz
2019	J	`jnl`	Dichotomy for symmetric Boolean PCSPs. CoRR Miron Ficak, Marcin Kozik, Miroslav Olsák, Szymon Stankiewicz
2019	J	`jnl`	Equations in oligomorphic clones and the constraint satisfaction problem for ω-categorical structures. J. Math. Log. Libor Barto, Michael Kompatscher, Miroslav Olsák, Van Trung Pham, Michael Pinsker
2019	J	`jnl`	Property Invariant Embedding for Automated Reasoning. CoRR Miroslav Olsák, Cezary Kaliszyk, Josef Urban
2019	A*	`conf`	Topology is relevant (in a dichotomy conjecture for infinite-domain constraint satisfaction problems). LICS Manuel Bodirsky, Antoine Mottet, Miroslav Olsák, Jakub Oprsal, Michael Pinsker, Ross Willard
2019	J	`jnl`	Topology is relevant (in the infinite-domain dichotomy conjecture for constraint satisfaction problems). CoRR Manuel Bodirsky, Antoine Mottet, Miroslav Olsák, Jakub Oprsal, Michael Pinsker, Ross Willard
2018	A*	`conf`	Reinforcement Learning of Theorem Proving. NeurIPS Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olsák
2017	A*	`conf`	The equivalence of two dichotomy conjectures for infinite domain constraint satisfaction problems. LICS Libor Barto, Michael Kompatscher, Miroslav Olsák, Trung Van Pham, Michael Pinsker
2016	J	`jnl`	Equations in oligomorphic clones and the Constraint Satisfaction Problem for $ω$-categorical structures. CoRR Libor Barto, Michael Kompatscher, Miroslav Olsák, Michael Pinsker, Van Trung Pham