44 citations · 111 across the 15 of their papers we have counts for
16 papers
Learning Conjecturing from Scratch
Thibault Gauthier, Josef Urban
We develop a self-learning approach for conjecturing of induction predicates on a dataset of 16197 problems derived from the OEIS. These problems are hard for today's SMT and ATP s…
A Formal Proof of R(4,5)=25
Thibault Gauthier, Chad E. Brown
In 1995, McKay and Radziszowski proved that the Ramsey number R(4,5) is equal to 25. Their proof relies on a combination of high-level arguments and computational steps. The author…
Learning Guided Automated Reasoning: A Brief Survey
Lasse Blaauwbroek, David Cerna, Thibault Gauthier +4
Automated theorem provers and formal proof assistants are general reasoning systems that are in theory capable of proving arbitrarily hard theorems, thus solving arbitrary problems…
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…
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…
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-…
Learned Provability Likelihood for Tactical Search
Thibault Gauthier
We present a method to estimate the provability of a mathematical formula. We adapt the tactical theorem prover TacticToe to factor in these estimations. Experiments over the HOL4…
Tree Neural Networks in HOL4
Thibault Gauthier
We present an implementation of tree neural networks within the proof assistant HOL4. Their architecture makes them naturally suited for approximating functions whose domain is a s…
Self-Learned Formula Synthesis in Set Theory
Chad E. Brown, Thibault Gauthier
A reinforcement learning algorithm accomplishes the task of synthesizing a set-theoretical formula that evaluates to given truth values for given assignments.
Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic
Thibault Gauthier
The paper describes a deep reinforcement learning framework based on self-supervised learning within the proof assistant HOL4. A close interaction between the machine learning modu…
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…
Learning to Reason with HOL4 tactics
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
Techniques combining machine learning with translation to automated reasoning have recently become an important component of formal proof assistants. Such "hammer" tech- niques com…
TacticToe: Learning to Prove with Tactics
Thibault Gauthier, Cezary Kaliszyk, Josef Urban +2
We implement a automated tactical prover TacticToe on top of the HOL4 interactive theorem prover. TacticToe learns from human proofs which mathematical technique is suitable in eac…
Premise Selection and External Provers for HOL4
Thibault Gauthier, Cezary Kaliszyk
Learning-assisted automated reasoning has recently gained popularity among the users of Isabelle/HOL, HOL Light, and Mizar. In this paper, we present an add-on to the HOL4 proof as…
Sharing HOL4 and HOL Light proof knowledge
Thibault Gauthier, Cezary Kaliszyk
New proof assistant developments often involve concepts similar to already formalized ones. When proving their properties, a human can often take inspiration from the existing form…
Matching concepts across HOL libraries
Thibault Gauthier, Cezary Kaliszyk
Many proof assistant libraries contain formalizations of the same mathematical concepts. The concepts are often introduced (defined) in different ways, but the properties that they…