149 citations · 825 across the 48 of their papers we have counts for
9 papers · 1 filter
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Qingxiang Wang, Chad Brown, Cezary Kaliszyk +1
In this paper we share several experiments trying to automatically translate informal mathematics into formal mathematics. In our context informal mathematics refers to human-writt…
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…
Can Neural Networks Learn Symbolic Rewriting?
Bartosz Piotrowski, Josef Urban, Chad E. Brown +1
This work investigates if the current neural architectures are adequate for learning symbolic rewriting. Two kinds of data sets are proposed for this research -- one based on autom…
Towards Finding Longer Proofs
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski +2
We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). Unlike most learning based approaches, we…
ENIGMAWatch: ProofWatch Meets ENIGMA
Zarathustra Goertzel, Jan Jakubův, Josef Urban
In this work we describe a new learning-based proof guidance -- ENIGMAWatch -- for saturation-style first-order theorem provers. ENIGMAWatch combines two guiding approaches for the…
Guiding Inferences in Connection Tableau by Recurrent Neural Networks
Bartosz Piotrowski, Josef Urban
We present a dataset and experiments on applying recurrent neural networks (RNNs) for guiding clause selection in the connection tableau proof calculus. The RNN encodes a sequence…
Hammering Mizar by Learning Clause Guidance
Jan Jakubův, Josef Urban
We describe a very large improvement of existing hammer-style proof automation over large ITP libraries by combining learning and theorem proving. In particular, we have integrated…
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E
Karel Chvalovský, Jan Jakubův, Martin Suda +1
We describe an efficient implementation of clause guidance in saturation-based automated theorem provers extending the ENIGMA approach. Unlike in the first ENIGMA implementation wh…
GRUNGE: A Grand Unified ATP Challenge
Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk +2
This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalism…