1 citations · 1 across the 3 of their papers we have counts for
6 papers
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…