149 citations · 825 across the 48 of their papers we have counts for
7 papers · 1 filter
First Experiments with Neural Translation of Informal to Formal Mathematics
Qingxiang Wang, Cezary Kaliszyk, Josef Urban
We report on our experiments to train deep neural networks that automatically translate informalized LaTeX-written Mizar texts into the formal Mizar language. To the best of our kn…
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…
Machine Learning Guidance and Proof Certification for Connection Tableaux
Michael Färber, Cezary Kaliszyk, Josef Urban
Connection calculi allow for very compact implementations of goal-directed proof search. We give an overview of our work related to connection tableaux calculi: First, we show opti…
Learning to Reason with HOL4 tactics
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
Techniques combining machine learning with translation to automated reasoning have recently become an important component of formal proof assistants. Such "hammer" tech- niques com…
TacticToe: Learning to Prove with Tactics
Thibault Gauthier, Cezary Kaliszyk, Josef Urban +2
We implement a automated tactical prover TacticToe on top of the HOL4 interactive theorem prover. TacticToe learns from human proofs which mathematical technique is suitable in eac…
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
Bartosz Piotrowski, Josef Urban
ATPboost is a system for solving sets of large-theory problems by interleaving ATP runs with state-of-the-art machine learning of premise selection from the proofs. Unlike many pre…
ProofWatch: Watchlist Guidance for Large Theories in E
Zarathustra Goertzel, Jan Jakubův, Stephan Schulz +1
Watchlist (also hint list) is a mechanism that allows related proofs to guide a proof search for a new conjecture. This mechanism has been used with the Otter and Prover9 theorem p…