Zobrazeno 1 - 10
of 40
pro vyhledávání: '"Gauthier, Thibault"'
Autor:
Gauthier, Thibault, Brown, Chad E.
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 authors have performed the computational parts of the proof with different i
Externí odkaz:
http://arxiv.org/abs/2404.01761
Autor:
Blaauwbroek, Lasse, Cerna, David, Gauthier, Thibault, Jakubův, Jan, Kaliszyk, Cezary, Suda, Martin, Urban, Josef
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 reducible to mathematics and logical reasoning. In practice, such sys
Externí odkaz:
http://arxiv.org/abs/2403.04017
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 programs generating the same OEIS sequence. Such programs were conjectur
Externí odkaz:
http://arxiv.org/abs/2304.02986
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 iterations of a self-learning loop that interleaves (i) training neural
Externí odkaz:
http://arxiv.org/abs/2301.11479
Autor:
Gauthier, Thibault, Urban, Josef
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-Line Encyclopedia of Integer Sequences. There, it discovers, on its ow
Externí odkaz:
http://arxiv.org/abs/2202.11908
Autor:
Gauthier, Thibault
Publikováno v:
EPTCS 342, 2021, pp. 78-85
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 library show an increase in the number of theorems re-proven by Tactic
Externí odkaz:
http://arxiv.org/abs/2109.03234
Autor:
Gauthier, Thibault
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 set of formulas. We measure the performance of our implementation and c
Externí odkaz:
http://arxiv.org/abs/2009.01827
Autor:
Brown, Chad E., Gauthier, Thibault
A reinforcement learning algorithm accomplishes the task of synthesizing a set-theoretical formula that evaluates to given truth values for given assignments.
Externí odkaz:
http://arxiv.org/abs/1912.01525
Autor:
Gauthier, Thibault
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 modules and the HOL4 library is achieved by the choice of tree neural netw
Externí odkaz:
http://arxiv.org/abs/1910.11797
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 formalisms are in higher-order logic (with and without type variables) and firs
Externí odkaz:
http://arxiv.org/abs/1903.02539