Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2.
CoRR, February, 2025
Invariant neural architecture for learning term synthesis in instantiation proving.
J. Symb. Comput., 2025
Hashing Modulo Context-Sensitive 𝛼-Equivalence.
Proc. ACM Program. Lang., 2024
Graph2Tac: Learning Hierarchical Representations of Math Concepts in Theorem proving.
CoRR, 2024
Symbolic Computation for All the Fun.
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.
Proceedings of the Forty-first International Conference on Machine Learning, 2024
The IMO Small Challenge: Not-Too-Hard Olympiad Math Datasets for LLMs.
Proceedings of the Second Tiny Papers Track at ICLR 2024, 2024
Int. J. Approx. Reason., November, 2023
Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023
Machine Learning Meets The Herbrand Universe.
CoRR, 2022
Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022
Maltsev conditions for General Congruence Meet-semidistributive Algebras.
J. Symb. Log., 2021
Erratum: Equations in oligomorphic clones and the constraint satisfaction problem for ω-categorical structures.
J. Math. Log., 2021
The Role of Entropy in Guiding a Connection Prover.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2021
Learning Theorem Proving Components.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2021
Planning from Pixels in Environments with Combinatorially Hard Search Spaces.
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.
Proceedings of the Intelligent Computer Mathematics - 14th International Conference, 2021
Fast and Slow Enigmas and Parental Guidance.
Proceedings of the Frontiers of Combining Systems - 13th International Symposium, 2021
Loop conditions for strongly connected digraphs.
Int. J. Algebra Comput., 2020
ω-categorical structures avoiding height 1 identities.
CoRR, 2020
GeoLogic - Graphical Interactive Theorem Prover for Euclidean Geometry.
Proceedings of the Mathematical Software - ICMS 2020, 2020
Property Invariant Embedding for Automated Reasoning.
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).
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020
Equations in oligomorphic clones and the constraint satisfaction problem for ω-categorical structures.
J. Math. Log., 2019
Topology is relevant (in the infinite-domain dichotomy conjecture for constraint satisfaction problems).
CoRR, 2019
Topology is relevant (in a dichotomy conjecture for infinite-domain constraint satisfaction problems).
Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019
Dichotomy for Symmetric Boolean PCSPs.
Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, 2019
Reinforcement Learning of Theorem Proving.
Proceedings of the Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, 2018
The equivalence of two dichotomy conjectures for infinite domain constraint satisfaction problems.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017