b'Josef Urban'

research

∙ 05/04/2022

The Isabelle ENIGMA

We significantly improve the performance of the E automated theorem prov...

Zarathustra A. Goertzel, et al. ∙

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...

Kimberley Parsons Trommler, et al. ∙

research

∙ 02/24/2022

Learning Program Synthesis for Integer Sequences from Scratch

We present a self-learning approach for synthesizing programs from integ...

Thibault Gauthier, et al. ∙

research

∙ 01/28/2022

Six Questions about 6G

Although 5G (Fifth Generation) mobile technology is still in the rollout...

Kimberley Parsons Trommler, et al. ∙

research

∙ 07/21/2021

Learning Theorem Proving Components

Saturation-style automated theorem provers (ATPs) based on the given cla...

Karel Chvalovský, et al. ∙

research

∙ 07/14/2021

Fast and Slow Enigmas and Parental Guidance

We describe several additions to the ENIGMA system that guides clause se...

Zarathustra Goertzel, et al. ∙

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...

Zsolt Zombori, et al. ∙

research

∙ 04/12/2021

Online Machine Learning Techniques for Coq: A Comparison

We present a comparison of several online machine learning techniques fo...

Liao Zhang, et al. ∙

research

∙ 02/10/2021

Learning Equational Theorem Proving

We develop Stratified Shortest Solution Imitation Learning (3SIL) to lea...

Jelle Piepenbrock, et al. ∙

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...

Lasse Blaauwbroek, et al. ∙

research

∙ 05/29/2020

First Neural Conjecturing Datasets and Experiments

We describe several datasets and first experiments with creating conject...

Josef Urban, et al. ∙

research

∙ 04/15/2020

Prolog Technology Reinforcement Learning Prover

We present a reinforcement learning toolkit for experiments with guiding...

Zsolt Zombori, et al. ∙

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...

Lasse Blaauwbroek, et al. ∙

research

∙ 03/11/2020

Stateful Premise Selection by Recurrent Neural Networks

In this work, we develop a new learning-based method for selecting facts...

Bartosz Piotrowski, et al. ∙

research

∙ 02/13/2020

ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)

We describe an implementation of gradient boosting and neural guidance o...

Jan Jakubův, et al. ∙

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...

Qingxiang Wang, et al. ∙

research

∙ 11/27/2019

Property Invariant Embedding for Automated Reasoning

Automated reasoning and theorem proving have recently become major chall...

Miroslav Olšák, et al. ∙

research

∙ 11/07/2019

Can Neural Networks Learn Symbolic Rewriting?

This work investigates if the current neural architectures are adequate ...

Bartosz Piotrowski, et al. ∙

research

∙ 05/30/2019

Towards Finding Longer Proofs

We present a reinforcement learning (RL) based guidance system for autom...

Zsolt Zombori, et al. ∙

research

∙ 05/23/2019

ENIGMAWatch: ProofWatch Meets ENIGMA

In this work we describe a new learning-based proof guidance -- ENIGMAWa...

Zarathustra Goertzel, et al. ∙

research

∙ 05/20/2019

Guiding Theorem Proving by Recurrent Neural Networks

We describe two theorem proving tasks -- premise selection and internal ...

Bartosz Piotrowski, et al. ∙

research

∙ 04/02/2019

Hammering Mizar by Learning Clause Guidance

We describe a very large improvement of existing hammer-style proof auto...

Jan Jakubův, et al. ∙

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...

Karel Chvalovský, et al. ∙

research

∙ 03/06/2019

GRUNGE: A Grand Unified ATP Challenge

This paper describes a large set of related theorem proving problems obt...

Chad E. Brown, et al. ∙

research

∙ 05/19/2018

Reinforcement Learning of Theorem Proving

We introduce a theorem proving algorithm that uses practically no domain...

Cezary Kaliszyk, et al. ∙

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...

Qingxiang Wang, et al. ∙

research

∙ 05/08/2018

Machine Learning Guidance and Proof Certification for Connection Tableaux

Connection calculi allow for very compact implementations of goal-direct...

Michael Färber, et al. ∙

research

∙ 05/08/2018

Machine Learning Guidance and Proof Certification for Connection Tableau

Connection calculi allow for very compact implementations of goal-direct...

Michael Färber, et al. ∙

research

∙ 04/02/2018

Learning to Prove with Tactics

We implement a automated tactical prover TacticToe on top of the HOL4 in...

Thibault Gauthier, et al. ∙

research

∙ 04/02/2018

Learning to Reason with HOL4 tactics

Techniques combining machine learning with translation to automated reas...

Thibault Gauthier, et al. ∙

research

∙ 02/12/2018

ProofWatch: Watchlist Guidance for Large Theories in E

Watchlist (also hint list) is a mechanism that allows related proofs to ...

Zarathustra Goertzel, et al. ∙

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...

Bartosz Piotrowski, et al. ∙

research

∙ 01/23/2017

ENIGMA: Efficient Learning-based Inference Guiding Machine

ENIGMA is a learning-based method for guiding given clause selection in ...

Jan Jakubův, et al. ∙

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...

Cezary Kaliszyk, et al. ∙

research

∙ 11/26/2016

BliStrTune: Hierarchical Invention of Theorem Proving Strategies

Inventing targeted proof search strategies for specific problem sets is ...

Jan Jakubův, et al. ∙

research

∙ 11/18/2016

Monte Carlo Connection Prover

Monte Carlo Tree Search (MCTS) is a technique to guide search in a large...

Michael Färber, et al. ∙

research

∙ 06/14/2016

DeepMath - Deep Sequence Models for Premise Selection

We study the effectiveness of neural sequence models for premise selecti...

Alex A. Alemi, et al. ∙

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...

Cezary Kaliszyk, et al. ∙

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...

Sebastiaan Joosten, et al. ∙

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 ...

Cezary Kaliszyk, et al. ∙

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...

Cezary Kaliszyk, et al. ∙

research

∙ 02/11/2014

Learning-assisted Theorem Proving with Millions of Lemmas

Large formal mathematical libraries consist of millions of atomic infere...

Cezary Kaliszyk, et al. ∙

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...

Cezary Kaliszyk, et al. ∙

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...

Daniel Kühlwein, et al. ∙

research

∙ 01/12/2013

BliStr: The Blind Strategymaker

BliStr is a system that automatically develops strategies for E prover o...

Josef Urban, et al. ∙

research

∙ 11/29/2012

Learning-Assisted Automated Reasoning with Flyspeck

The considerable mathematical knowledge encoded by the Flyspeck project ...

Cezary Kaliszyk, et al. ∙

research

∙ 09/18/2012

Theorem Proving in Large Formal Mathematics as an Emerging AI Field

In the recent years, we have linked a large corpus of formal mathematics...

Josef Urban, et al. ∙

research

∙ 09/03/2011

ATP and Presentation Service for Mizar Formalizations

This paper describes the Automated Reasoning for Mizar (MizAR) service, ...

Josef Urban, et al. ∙

research

∙ 08/17/2011

Premise Selection for Mathematics by Corpus Analysis and Kernel Methods

Smart premise selection is essential when using automated reasoning as a...

Jesse Alama, et al. ∙

research

∙ 05/25/2010

Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar

This paper presents a combination of several automated reasoning and pro...

Josef Urban, et al. ∙

Josef Urban

Featured Co-authors