research
∙
05/13/2023
Translating SUMO-K to Higher-Order Set Theory
We describe a translation from a fragment of SUMO (SUMO-K) into higher-o...
share
research
∙
04/06/2023
A Mathematical Benchmark for Inductive Theorem Provers
We present a benchmark of 29687 problems derived from the On-Line Encycl...
research
∙
03/12/2023
MizAR 60 for Mizar 50
As a present to Mizar on its 50th anniversary, we develop an AI/TP syste...
research
∙
01/27/2023
Alien Coding
We introduce a self-learning algorithm for synthesizing programs for OEI...
research
∙
10/07/2022
Machine Learning Meets The Herbrand Universe
The appearance of strong CDCL-based propositional (SAT) solvers has grea...
research
∙
05/04/2022
The Isabelle ENIGMA
We significantly improve the performance of the E automated theorem prov...
research
∙
03/24/2022
PREVIEW VERSION: Six Insights into 6G: Orientation and Input for Developing Your Strategic 6G Research Plan
This is the PREVIEW version of a paper about 6G. This paper is a summa...
research
∙
02/24/2022
Learning Program Synthesis for Integer Sequences from Scratch
We present a self-learning approach for synthesizing programs from integ...
research
∙
01/28/2022
Six Questions about 6G
Although 5G (Fifth Generation) mobile technology is still in the rollout...
research
∙
07/21/2021
Learning Theorem Proving Components
Saturation-style automated theorem provers (ATPs) based on the given cla...
research
∙
07/14/2021
Fast and Slow Enigmas and Parental Guidance
We describe several additions to the ENIGMA system that guides clause se...
research
∙
05/31/2021
The Role of Entropy in Guiding a Connection Prover
In this work we study how to learn good algorithms for selecting reasoni...
research
∙
04/12/2021
Online Machine Learning Techniques for Coq: A Comparison
We present a comparison of several online machine learning techniques fo...
research
∙
02/10/2021
Learning Equational Theorem Proving
We develop Stratified Shortest Solution Imitation Learning (3SIL) to lea...
research
∙
07/31/2020
The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq
We present Tactician, a tactic learner and prover for the Coq Proof Assi...
research
∙
05/29/2020
First Neural Conjecturing Datasets and Experiments
We describe several datasets and first experiments with creating conject...
research
∙
04/15/2020
Prolog Technology Reinforcement Learning Prover
We present a reinforcement learning toolkit for experiments with guiding...
research
∙
03/20/2020
Tactic Learning and Proving for the Coq Proof Assistant
We present a system that utilizes machine learning for tactic proof sear...
research
∙
03/11/2020
Stateful Premise Selection by Recurrent Neural Networks
In this work, we develop a new learning-based method for selecting facts...
research
∙
02/13/2020
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
We describe an implementation of gradient boosting and neural guidance o...
research
∙
12/05/2019
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
In this paper we share several experiments trying to automatically trans...
research
∙
11/27/2019
Property Invariant Embedding for Automated Reasoning
Automated reasoning and theorem proving have recently become major chall...
research
∙
11/07/2019
Can Neural Networks Learn Symbolic Rewriting?
This work investigates if the current neural architectures are adequate ...
research
∙
05/30/2019
Towards Finding Longer Proofs
We present a reinforcement learning (RL) based guidance system for autom...
research
∙
05/23/2019
ENIGMAWatch: ProofWatch Meets ENIGMA
In this work we describe a new learning-based proof guidance -- ENIGMAWa...
research
∙
05/20/2019
Guiding Theorem Proving by Recurrent Neural Networks
We describe two theorem proving tasks -- premise selection and internal ...
research
∙
04/02/2019
Hammering Mizar by Learning Clause Guidance
We describe a very large improvement of existing hammer-style proof auto...
research
∙
03/07/2019
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E
We describe an efficient implementation of clause guidance in saturation...
research
∙
03/06/2019
GRUNGE: A Grand Unified ATP Challenge
This paper describes a large set of related theorem proving problems obt...
research
∙
05/19/2018
Reinforcement Learning of Theorem Proving
We introduce a theorem proving algorithm that uses practically no domain...
research
∙
05/10/2018
First Experiments with Neural Translation of Informal to Formal Mathematics
We report on our first experiments to train deep neural networks that au...
research
∙
05/08/2018
Machine Learning Guidance and Proof Certification for Connection Tableaux
Connection calculi allow for very compact implementations of goal-direct...
research
∙
05/08/2018
Machine Learning Guidance and Proof Certification for Connection Tableau
Connection calculi allow for very compact implementations of goal-direct...
research
∙
04/02/2018
Learning to Prove with Tactics
We implement a automated tactical prover TacticToe on top of the HOL4 in...
research
∙
04/02/2018
Learning to Reason with HOL4 tactics
Techniques combining machine learning with translation to automated reas...
research
∙
02/12/2018
ProofWatch: Watchlist Guidance for Large Theories in E
Watchlist (also hint list) is a mechanism that allows related proofs to ...
research
∙
02/09/2018
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
ATPboost is a system for solving sets of large-theory problems by interl...
research
∙
01/23/2017
ENIGMA: Efficient Learning-based Inference Guiding Machine
ENIGMA is a learning-based method for guiding given clause selection in ...
research
∙
11/29/2016
Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving
We study methods for automated parsing of informal mathematical expressi...
research
∙
11/26/2016
BliStrTune: Hierarchical Invention of Theorem Proving Strategies
Inventing targeted proof search strategies for specific problem sets is ...
research
∙
11/18/2016
Monte Carlo Connection Prover
Monte Carlo Tree Search (MCTS) is a technique to guide search in a large...
research
∙
06/14/2016
DeepMath - Deep Sequence Models for Premise Selection
We study the effectiveness of neural sequence models for premise selecti...
research
∙
10/20/2014
Certified Connection Tableaux Proofs for HOL Light and TPTP
In the recent years, the Metis prover based on ordered paramodulation an...
research
∙
06/06/2014
Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems
This paper reports our initial experiments with using external ATP on so...
research
∙
05/14/2014
Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description
The goal of this project is to (i) accumulate annotated informal/formal ...
research
∙
02/11/2014
Machine Learner for Automated Reasoning 0.4 and 0.5
Machine Learner for Automated Reasoning (MaLARea) is a learning and reas...
research
∙
02/11/2014
Learning-assisted Theorem Proving with Millions of Lemmas
Large formal mathematical libraries consist of millions of atomic infere...
research
∙
09/19/2013
HOL(y)Hammer: Online ATP Service for HOL Light
HOL(y)Hammer is an online AI/ATP service for formal (computer-understand...
research
∙
08/09/2013
MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers
MaLeS is an automatic tuning framework for automated theorem provers. It...
research
∙
01/12/2013