research
∙
03/12/2023
MizAR 60 for Mizar 50
As a present to Mizar on its 50th anniversary, we develop an AI/TP syste...
share
research
∙
08/13/2022
Differentiable Inductive Logic Programming in High-Dimensional Space
Synthesizing large logic programs through Inductive Logic Programming (I...
research
∙
05/13/2022
Lash 1.0 (System Description)
Lash is a higher-order automated theorem prover created as a fork of the...
research
∙
05/04/2022
The Isabelle ENIGMA
We significantly improve the performance of the E automated theorem prov...
research
∙
04/26/2022
Formalizing a Diophantine Representation of the Set of Prime Numbers
The DPRM (Davis-Putnam-Robinson-Matiyasevich) theorem is the main step i...
research
∙
04/06/2022
Adversarial Learning to Reason in an Arbitrary Logic
Existing approaches to learning to prove theorems focus on particular lo...
research
∙
12/29/2021
Learning Higher-Order Programs without Meta-Interpretive Learning
Learning complex programs through inductive logic programming (ILP) rema...
research
∙
07/21/2021
JEFL: Joint Embedding of Formal Proof Libraries
The heterogeneous nature of the logical foundations used in different in...
research
∙
04/12/2021
Online Machine Learning Techniques for Coq: A Comparison
We present a comparison of several online machine learning techniques fo...
research
∙
01/25/2021
Disambiguating Symbolic Expressions in Informal Documents
We propose the task of disambiguating symbolic expressions in informal S...
research
∙
01/22/2021
A Study of Continuous Vector Representationsfor Theorem Proving
Applying machine learning to mathematical terms and formulas requires a ...
research
∙
05/26/2020
A Survey of Languages for Formalizing Mathematics
In order to work with mathematical content in computer systems, it is ne...
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
∙
03/06/2019
GRUNGE: A Grand Unified ATP Challenge
This paper describes a large set of related theorem proving problems obt...
research
∙
08/20/2018
Concrete Semantics with Coq and CoqHammer
The "Concrete Semantics" book gives an introduction to imperative progra...
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
∙
03/01/2017
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
Large computer-understandable proofs consist of millions of intermediate...
research
∙
01/24/2017
Deep Network Guided Proof Search
Deep learning techniques lie at the heart of several significant AI adva...
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/18/2016
Monte Carlo Connection Prover
Monte Carlo Tree Search (MCTS) is a technique to guide search in a large...
research
∙
06/17/2016
Proceedings First International Workshop on Hammers for Type Theories
This volume of EPTCS contains the proceedings of the First Workshop on H...
research
∙
09/11/2015
Premise Selection and External Provers for HOL4
Learning-assisted automated reasoning has recently gained popularity amo...
research
∙
09/11/2015
Sharing HOL4 and HOL Light proof knowledge
New proof assistant developments often involve concepts similar to alrea...
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
∙
11/29/2012