22 citations · 55 across the 10 of their papers we have counts for
16 papers
Reintroducing the Second Player in EPR
Leroy Chew, Mikoláš Janota, Miroslav Olšák +1
We present a PSPACE-complete fragment of first order logic we call QEALM (QBF-like EPR by Alternating Level-ordered Miniscoping). Unlike other well-known fragments it is closer to…
Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
Yuri Chervonyi, Trieu H. Trinh, Miroslav Olšák +8
We present AlphaGeometry2 (AG2), a significantly improved version of AlphaGeometry introduced in (Trinh et al., 2024), which has now surpassed an average gold medalist in solving O…
Planning from Pixels in Environments with Combinatorially Hard Search Spaces
Marco Bagatella, Mirek Olšák, Michal Rolínek +1
The ability to form complex plans based on raw visual input is a litmus test for current capabilities of artificial intelligence, as it requires a seamless combination of visual pr…
Learning Theorem Proving Components
Karel Chvalovský, Jan Jakubův, Miroslav Olšák +1
Saturation-style automated theorem provers (ATPs) based on the given clause procedure are today the strongest general reasoners for classical first-order logic. The clause selectio…
Fast and Slow Enigmas and Parental Guidance
Zarathustra Goertzel, Karel Chvalovský, Jan Jakubův +2
We describe several additions to the ENIGMA system that guides clause selection in the E automated theorem prover. First, we significantly speed up its neural guidance by adding se…
Learning to solve geometric construction problems from images
J. Macke, J. Sedlar, M. Olsak +2
We describe a purely image-based method for finding geometric constructions with a ruler and compass in the Euclidea geometric game. The method is based on adapting the Mask R-CNN…
The Role of Entropy in Guiding a Connection Prover
Zsolt Zombori, Josef Urban, Miroslav Olšák
In this work we study how to learn good algorithms for selecting reasoning steps in theorem proving. We explore this in the connection tableau calculus implemented by leanCoP where…
ω-categorical structures avoiding height 1 identities
Manuel Bodirsky, Antoine Mottet, Miroslav Olšák +3
The algebraic dichotomy conjecture for Constraint Satisfaction Problems (CSPs) of reducts of (infinite) finitely bounded homogeneous structures states that such CSPs are polynomial…
GeoLogic -- Graphical interactive theorem prover for Euclidean geometry
Miroslav Olšák
Domain of mathematical logic in computers is dominated by automated theorem provers (ATP) and interactive theorem provers (ITP). Both of these are hard to access by AI from the hum…
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
Jan Jakubův, Karel Chvalovský, Miroslav Olšák +3
We describe an implementation of gradient boosting and neural guidance of saturation-style automated theorem provers that does not depend on consistent symbol names across problems…
Property Invariant Embedding for Automated Reasoning
Miroslav Olšák, Cezary Kaliszyk, Josef Urban
Automated reasoning and theorem proving have recently become major challenges for machine learning. In other domains, representations that are able to abstract over unimportant tra…
Dichotomy for symmetric Boolean PCSPs
Miron Ficak, Marcin Kozik, Miroslav Olsak +1
A PCSP is a combination of two CSPs defined by two similar templates; the computational question is to distinguish a YES instance of the first one from a NO instance of the second.…
Topology is relevant (in a dichotomy conjecture for infinite-domain constraint satisfaction problems)
Manuel Bodirsky, Antoine Mottet, Miroslav Olšák +3
The algebraic dichotomy conjecture for Constraint Satisfaction Problems (CSPs) of reducts of (infinite) finitely bounded homogeneous structures states that such CSPs are polynomial…
Maltsev conditions for general congruence meet-semidistributive algebras
Miroslav Olšák
Meet semidistributive varieties are in a sense the last of the most important classes in universal algebra for which it is unknown whether it can be characterized by a strong Malts…
Reinforcement Learning of Theorem Proving
Cezary Kaliszyk, Josef Urban, Henryk Michalewski +1
We introduce a theorem proving algorithm that uses practically no domain heuristics for guiding its connection-style proof search. Instead, it runs many Monte-Carlo simulations gui…
Equations in oligomorphic clones and the Constraint Satisfaction Problem for -categorical structures
Libor Barto, Michael Kompatscher, Miroslav Olšák +2
There exist two conjectures for constraint satisfaction problems (CSPs) of reducts of finitely bounded homogeneous structures: the first one states that tractability of the CSP of…