149 citations · 825 across the 48 of their papers we have counts for
65 papers
Translating SUMO-K to Higher-Order Set Theory
Chad Brown, Adam Pease, Josef Urban
We describe a translation from a fragment of SUMO (SUMO-K) into higher-order set theory. The translation provides a formal semantics for portions of SUMO which are beyond first-ord…
A Mathematical Benchmark for Inductive Theorem Provers
Thibault Gauthier, Chad E. Brown, Mikolas Janota +1
We present a benchmark of 29687 problems derived from the On-Line Encyclopedia of Integer Sequences (OEIS). Each problem expresses the equivalence of two syntactically different pr…
MizAR 60 for Mizar 50
Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel +6
As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60\% of the Mizar theorems in the hammer setting. We also automatically pr…
Alien Coding
Thibault Gauthier, Miroslav Olšák, Josef Urban
We introduce a self-learning algorithm for synthesizing programs for OEIS sequences. The algorithm starts from scratch initially generating programs at random. Then it runs many it…
Machine Learning Meets The Herbrand Universe
Jelle Piepenbrock, Josef Urban, Konstantin Korovin +3
The appearance of strong CDCL-based propositional (SAT) solvers has greatly advanced several areas of automated reasoning (AR). One of the directions in AR is thus to apply SAT sol…
The Isabelle ENIGMA
Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk +3
We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In parti…
Learning Program Synthesis for Integer Sequences from Scratch
Thibault Gauthier, Josef Urban
We present a self-learning approach for synthesizing programs from integer sequences. Our method relies on a tree search guided by a learned policy. Our system is tested on the On-…
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…
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…
Online Machine Learning Techniques for Coq: A Comparison
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski +3
We present a comparison of several online machine learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on top of Tactician, a plugin f…
Learning Equational Theorem Proving
Jelle Piepenbrock, Tom Heskes, Mikoláš Janota +1
We develop Stratified Shortest Solution Imitation Learning (3SIL) to learn equational theorem proving in a deep reinforcement learning (RL) setting. The self-trained models achieve…
The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq
Lasse Blaauwbroek, Josef Urban, Herman Geuvers
We present Tactician, a tactic learner and prover for the Coq Proof Assistant. Tactician helps users make tactical proof decisions while they retain control over the general proof…
First Neural Conjecturing Datasets and Experiments
Josef Urban, Jan Jakubův
We describe several datasets and first experiments with creating conjectures by neural methods. The datasets are based on the Mizar Mathematical Library processed in several forms…
Prolog Technology Reinforcement Learning Prover
Zsolt Zombori, Josef Urban, Chad E. Brown
We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to exte…
Tactic Learning and Proving for the Coq Proof Assistant
Lasse Blaauwbroek, Josef Urban, Herman Geuvers
We present a system that utilizes machine learning for tactic proof search in the Coq Proof Assistant. In a similar vein as the TacticToe project for HOL4, our system predicts appr…
Stateful Premise Selection by Recurrent Neural Networks
Bartosz Piotrowski, Josef Urban
In this work, we develop a new learning-based method for selecting facts (premises) when proving new goals over large formal libraries. Unlike previous methods that choose sets of…
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…
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…